Missing HEq lemmas

Stream: Is there code for X?

[Violeta Hernández]

Are these in Mathlib? They seem like pretty useful simp lemmas

@[simp]
theorem cast_heq_iff_heq {α β γ : Sort u} (h : α = β) (a : α) (c : γ) :
    HEq (cast h a) c ↔ HEq a c := by
  subst h
  rfl

@[simp]
theorem heq_cast_iff_heq {α β γ : Sort u} (h : β = γ) (a : α) (b : β) :
    HEq a (cast h b) ↔ HEq a b := by
  subst h
  rfl

[Violeta Hernández]

(just golfed a particularly hellish 10-line proof in my own project to 4 lines using these!)

[Kyle Miller]

Seems like the could go near docs#rec_heq_iff_heq

[Kyle Miller]

One downside as simp lemmas is that they cause this h proof to be forgotten, in case somehow that proof is useful. It's not a big deal though, since it can always be recovered later or otherwise saved ahead of time (say with generalize_proofs)

[Violeta Hernández]

I would imagine that in most cases, there won't be other uses of type γ within a or b, in which case this is always an improvement

[Violeta Hernández]

#20847