Gabriel Ebner

I've just learned about this issue in the comments of https://github.com/leanprover/lean-client-js/pull/12. To repeat my comment there: the unspoken assumption with JSON-based protocols is that it is always safe to add...

Oof, I think this is an ugly error... When we elaborate the Lean 4 notation command, we get this: ```lean /- sources/mathlib/src/data/real/basic.lean:1:270000: error: application type mismatch Lean.withRef f✝ argument f✝...

Apparently, this instance is dangerous now: ```lean @DirectSum.GradeZero.nonUnitalNonAssocSemiring : {ι : Type ?u.302} → [_inst_1 : DecidableEq ι] → (A : ι → Type ?u.303) → [_inst_2 : AddZeroClass ι]...

Changing `Zero.zero` to `0` didn't help. 😢

Maybe after the discrimination tree refactor where we no longer do iota-reduction. (Right now `0` is binported as `@ofNat ι 0 { ofNat := Zero.zero }`.)

Function coercion is missing as well. That is, if you have `x : Equiv A B`, then `(x : A → B)` won't work.

What's happening here is that the smart unfolding lemma from Lean 3 is indeed successfully applied, but *without* reducing to any of the cases. For reference, this is the binported...

This seems to be a bug in the AST export.

We could also remove `reducible` from `set.inj_on`.

`category_theory.sites.pretopology` finished after more than an hour of runtime.