Proposition dependent equality under cast

Stream: new members

[Igor Khavkine]

Hello. I've run into the following kind of goal while working on a proof and I'm at a complete loss how to prove it. Here's a #mwe:

import Mathlib

theorem puzzle (ι : Type) (E : ι → Type) (z : (i : ι) → E i) (i m : ι) (hi : i = m) :
    (hi.symm ▸ z m) = z i := by
  sorry -- rfl doesn't work

I've thrown all the tactics that I know at it, as well as some things that I could find in libraries with various combinations of "Eq" and "cast", but nothing works. Unless I'm missing something, the conclusion seems true and I hope that it is provable.

Any advice?

[Aaron Liu]

import Mathlib

theorem puzzle (ι : Type) (E : ι → Type) (z : (i : ι) → E i) (i m : ι) (hi : i = m) :
    (hi.symm ▸ z m) = z i := by
  cases hi; rfl

[Igor Khavkine]

Wow, thanks for the quick solution @Aaron Liu ! It works, but I'm still puzzled. What logic would lead one to finding this approach?

[Aaron Liu]

For me, it's because I have had to prove this exact lemma before.

[Igor Khavkine]

Well, that's great, of course. :) But to me it just looks like some Lean magic. What is cases hi doing anyway? The doc string for the cases doesn't seem very helpful for this case.

Also, I think I tried by_cases myself, but didn't get anywhere with that.

[Aaron Liu]

Here, cases hi is doing the basically the same thing as subst hi, maybe the docstring for subst will be more helpful.

[Aaron Liu]

It applies the induction rule for equality

[Edward van de Meent]

there are basically two things which make this work:

• the rewriting operation ▸ is able to reduce to the identity when the equality used is Eq.refl a : a = a
• when you do cases on an equality h : a = b (or subst, for that matter), you ask lean to change your goal in such a way that all occurrences of b become a, as well as change occurrences of h itself into a constructor for equality, which is Eq.refl a.

the two above things mean that after the cases, lean is able to reduce .symm and ▸ to just be left with z i = z i, which is solved with rfl

[Chase Norman]

Canonical can solve tricky dependent type theory problems like these:

import Canonical

theorem puzzle (ι : Type) (E : ι → Type) (z : (i : ι) → E i) (i m : ι) (hi : i = m) :
    (hi.symm ▸ z m) = z i := by
    -- canonical
    exact
      Eq.rec (motive := fun a t ↦ Eq.rec (motive := fun a t ↦ E a) (z m) t = z a) (Eq.refl (z m))
        (Eq.symm hi)

[Asei Inoue]

I think lean 4 web should have canonical.