fix: respect type reducibility when generating injectivity lemmas

[eric-wieser]

The relevant test case is:

def WrappedNat (_n : Nat) := Nat

structure WithWrapped : Type :=
(n : Nat)
(m : WrappedNat n)

#check WithWrapped.mk.injEq
#print WithWrapped.noConfusionType

The diff due to this PR is intended to be

 WithWrapped.mk.injEq (n : Nat) (m : WrappedNat n) (n : Nat) (m : WrappedNat n) :
-  ({ n := n, m := m } = { n := n, m := m }) = (n = n ∧ m = m)
+  ({ n := n, m := m } = { n := n, m := m }) = (n = n ∧ HEq m m)
@[reducible] protected def WithWrapped.noConfusionType.{u} : Sort u → WithWrapped → WithWrapped → Sort u :=
-fun P v1 v2 => WithWrapped.casesOn v1 fun n m => WithWrapped.casesOn v2 fun n_1 m_1 => (n = n_1 → m = m_1 → P) → P
+fun P v1 v2 => WithWrapped.casesOn v1 fun n m => WithWrapped.casesOn v2 fun n_1 m_1 => (n = n_1 → HEq m m_1 → P) → P

This forward-ports leanprover-community/lean#812.

For now, I am just creating this to see if it passes CI, since CI appears not to run on my branch in a fork.

[Kha]

The CI failure seems to be a simple matter of reordered messages; do we agree on the general change?

[leodemoura]

The CI failure seems to be a simple matter of reordered messages.

I don't look at PRs until it is green. We should make it clear to all PR submitters that this is a requirement.

do we agree on the general change?

The change is not properly motivated. A link to another thread is not an acceptable. We should also make it clear on the contribution guidelines that a clear and short motivation for unsolicited PRs is a requirement.

[eric-wieser]

In lean 3, this was possible with type_context_old ctx(env, transparency_mode::Reducible);; but type_context_old no longer exists.

I think the issue here is that mk_no_confusion_type is using the kernel, when it should be using the elaborator; but fixing that is a large refactor.