proving `h ▸ x = h' ▸ x`

Stream: lean4

[Tomas Skrivan]

How do I prove that h ▸ x = h' ▸ x i.e. rfl with two different casts?

mwe

example {I : Type _} {X : I → Type _}
  (i i' : I) (xi : X i) (h : i = i') (h' : X i = X i')
  : h ▸ x = h' ▸ x := by sorry

Anyway, I guess the advice is stop doing whatever I was doing that got me here :)

[Adam Topaz]

example {I : Type _} {X : I → Type _}
  (i i' : I) (xi : X i) (h : i = i') (h' : X i = X i') :
    h ▸ x = h' ▸ x := by
  subst h ; rfl

[Tomas Skrivan]

Is there a way to do it without referencing h or h'?

[Adam Topaz]

I don't think so.

[Tomas Skrivan]

Ahh with few congr and funext I can navigate inside of the if statement where this was and assign a name to h. Ok it works now, thanks!

[Adam Topaz]

Do you know about generalize_proofs? It's a tactic that lets you name proofs that might be useful in your actual use case.

[Tomas Skrivan]

No I do not know this, I will look it up. Interestingly searching mathlib4 doc for "generalize_proofs" does not yield a useful link. Searching "GeneralizeProofs" works though

[Adam Topaz]

The tactic is generalize_proofs as you can see here: https://github.com/leanprover-community/mathlib4/blob/383ec12856a51cae18f9790f4e66595289b574a6/Mathlib/Tactic/GeneralizeProofs.lean#L102

[Adam Topaz]

it's a shame that we don't (yet?!) have a good way to search for tactics using the actual syntax of the tactic :-/

[Kyle Miller]

It needs a little help with the motive in the second subst, but here's one solution:

import Mathlib.Tactic

set_option autoImplicit true

example {I : Type _} {X : I → Type _}
  (i i' : I) (xi : X i) (h : i = i') (h' : X i = X i')
  : h ▸ xi = h' ▸ xi := by
  apply eq_of_heq
  rw [rec_heq_iff_heq, heq_rec_iff_heq (C := id)]

This is an example of where HEq is useful, since it lets you shake off casts.

[Kyle Miller]

If you don't do (C := id) then it thinks that X is the motive, leading it down the wrong path, and it fails to rewrite.

[Kevin Buzzard]

This proof still "uses h" in the sense that h is mentioned in the statement of the theorem :-)

[Tomas Skrivan]

Kevin Buzzard said:

This proof still "uses h" in the sense that h is mentioned in the statement of the theorem :-)

Ok :) here is a more realistic example of what I was doing

example {I : Type _} {X : I⊕I → Type _} [DecidableEq I]
  (i i' : I) (xi : X (.inl i)) (yi : X (.inl i'))
  : (if h : i=i' then h ▸ xi else yi)
    =
    if h : (Sum.inl (β:=I) i)=(.inl i') then h ▸ xi else yi :=
by
  simp
  congr
  funext h
  subst h
  rfl

[Floris van Doorn]

Tomas Skrivan said:

Is there a way to do it without referencing h or h'?

I recommend making this general version a lemma and then use rw [my_lemma] in your application.