induction h vs rw h for `h : i = i'`

Stream: general

[Eric Wieser]

I was surprised to see tidy? generate induction h when h is an equality. I'm a little puzzled by the meaning of this, especially since rw h fails. The goal state was

h: i = i'
⊢ ↑(eq.rec ⟨↑si, _⟩ _) = ↑(eq.rec si h)

and after induction h becomes

⊢ ↑(eq.rec ⟨↑si, _⟩ _) = ↑(eq.rec si _)

Can someone explain to me the intuition here?

[Chris Hughes]

I don't know exactly what's going on here, but the reason rw doesn't work is probably because there is a term in the goal whose type contains i, which means that it is harder to generate the motive (the argument called C in the type of eq.rec) when making the proof term. induction on equality is basically just substitution, but the induction tactic has better support for computing the motive than rw, and makes the substitution everywhere. I think somehow it's easier to compute the motive when you rewrite at all your hypotheses, and also easier when one side of the equality is just a local constant.

[Eric Wieser]

Thanks, your wording made me realize that induction h is doing the same thing as subst h (which unlike rw h, also works)

[Eric Wieser]

For more context of what's going on, I'm trying to prove the trivial-but-somehow-not-refl statement in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Difficulty.20with.20dependent.20rewrites/near/214686669