fix: use reducible transparency when producing no_confusion_type and injectivity lemmas

[eric-wieser]

The relevant test case is

def wrapped_nat (n : nat) := nat

structure with_wrapped : Type :=
(n : nat)
(m : wrapped_nat n)

#check with_wrapped.mk.inj_eq

The diff due to this PR is

 ∀ {n : ℕ} {m : wrapped_nat n} {n' : ℕ} {m' : wrapped_nat n'},
-   with_wrapped.mk n m = with_wrapped.mk n' m' = (n = n' ∧ m = m'))
+   with_wrapped.mk n m = with_wrapped.mk n' m' = (n = n' ∧ m == m'))

which is an improvement since m and m' are not intended to be equal types.

It's not immediately clear to me whether this will stop the particular defeq check that is causing trouble in this motivating Zulip thread.

[kim-em]

I've build mathlib3 against this locally, no problems to report.

[ericrbg]

Scott, does it prevent the crash?

[eric-wieser]

I tried to test this in leanprover-community/mathlib3#19192 but I can't work out how to make a release to build against.

[kim-em]

But Eric, I don't think that helps: as I said I've already compiled mathlib3 master against this branch.

What I want is a mathlib3 commit that would fail against current lean3 master, that I can run against this.

[eric-wieser]

@semorrison, the point is that would give us a cache that we can try all the mwes from the thread in.

[eric-wieser]

Either way, I think the fact that mathlib succeeds with this change (combined with agreeing with the intended effect, whether or not it helps performance) is sufficient justification to merge it

[collares]

Doesn't an analogue of this have to land in Lean 4 first? What happens if this PR is merged and Leo doesn't like it for Lean 4?

[eric-wieser]

We can use the option to disable the generation of these lemmas in Lean 4.

[digama0]

fix: use semireducible transparency when producing no_confusion_type and injectivity lemmas #812

You mean reducible transparency, right?

[eric-wieser]

Yes, I can never remember if "X transparency" includes X or not...