Zulip Chat Archive

Stream: lean4

Topic: dependent products and equality


David Renshaw (Jul 05 2022 at 20:28):

Is there an easy way to prove bar below?

structure Foo (t1 : Type) (p : t1  Prop) where
  (a : t1)
  (b : p a)

lemma bar
  (t1 : Type)
  (p : t1  Prop)
  (x y : t1)
  (hab : x = y)
  (px : p x)
  (py : p y) : Foo.mk x px = Foo.mk y py := sorry

In Lean 3, the congr' tactic works, but I have been unable to find anything like that in Lean 4.

Kyle Miller (Jul 05 2022 at 20:31):

by cases hab; rfl works here. (You can do subst x instead of cases hab if you want.)

Kyle Miller (Jul 05 2022 at 20:32):

or by simp [hab]

David Renshaw (Jul 05 2022 at 20:34):

thanks!


Last updated: Dec 20 2023 at 11:08 UTC