feat(logic/basic): Generalize congr_fun_heq (#13867)

The lemma holds for arbitrary heterogeneous equalities, not only that given by casts.

src/logic/basic.lean

@@ -152,6 +152,10 @@ assume ⟨h⟩, h.elim
 @[simp] theorem exists_pempty {P : pempty → Prop} : (∃ x : pempty, P x) ↔ false :=
 ⟨λ h, by { cases h with w, cases w }, false.elim⟩
 
+lemma congr_heq {α β γ : Sort*} {f : α → γ} {g : β → γ} {x : α} {y : β} (h₁ : f == g)
+  (h₂ : x == y) : f x = g y :=
+by { cases h₂, cases h₁, refl }
+
 lemma congr_arg_heq {α} {β : α → Sort*} (f : ∀ a, β a) : ∀ {a₁ a₂ : α}, a₁ = a₂ → f a₁ == f a₂
 | a _ rfl := heq.rfl
 
@@ -885,10 +889,6 @@ lemma heq_of_cast_eq :
   ∀ {α β : Sort*} {a : α} {a' : β} (e : α = β) (h₂ : cast e a = a'), a == a'
 | α ._ a a' rfl h := eq.rec_on h (heq.refl _)
 
-lemma congr_fun_heq {α β γ : Sort*} {f : α → γ} {g : β → γ} (h₁ : β = α) (h₂ : f == g) (x : β) :
-  f (cast h₁ x) = g x :=
-by { subst h₁, rw [eq_of_heq h₂, cast_eq] }
-
 lemma cast_eq_iff_heq {α β : Sort*} {a : α} {a' : β} {e : α = β} : cast e a = a' ↔ a == a' :=
 ⟨heq_of_cast_eq _, λ h, by cases h; refl⟩
 

src/set_theory/game/ordinal.lean

@@ -63,7 +63,7 @@ by { rw to_pgame, refl }
 
 @[simp] theorem to_pgame_move_left {o : ordinal} (i : o.out.α) :
   o.to_pgame.move_left (to_left_moves_to_pgame i) = (typein (<) i).to_pgame :=
-by { rw to_left_moves_to_pgame, exact congr_fun_heq _ to_pgame_move_left_heq i }
+by { rw to_left_moves_to_pgame, exact congr_heq to_pgame_move_left_heq (cast_heq _ i) }
 
 theorem to_pgame_lt {a b : ordinal} (h : a < b) : a.to_pgame < b.to_pgame :=
 begin