chore(data/equiv/basic): add lemmas about equiv.cast (#6246)

src/data/equiv/basic.lean

@@ -237,6 +237,17 @@ end
 
 @[simp] theorem cast_apply {α β} (h : α = β) (x : α) : equiv.cast h x = cast h x := rfl
 
+@[simp] theorem cast_symm {α β} (h : α = β) : (equiv.cast h).symm = equiv.cast h.symm := rfl
+
+@[simp] theorem cast_refl {α} : equiv.cast (rfl : α = α) = equiv.refl α := rfl
+
+@[simp] theorem cast_trans {α β γ} (h : α = β) (h2 : β = γ) :
+  (equiv.cast h).trans (equiv.cast h2) = equiv.cast (h.trans h2) :=
+ext $ λ x, by { substs h h2, refl }
+
+lemma cast_eq_iff_heq {α β} (h : α = β) {a : α} {b : β} : equiv.cast h a = b ↔ a == b :=
+by { subst h, simp }
+
 lemma symm_apply_eq {α β} (e : α ≃ β) {x y} : e.symm x = y ↔ x = e y :=
 ⟨λ H, by simp [H.symm], λ H, by simp [H]⟩