Theorem: heq_fun_congr (Qpf/Util/HEq.lean)

State before:
α α' : Sort u_1
γ : Sort u_2
a : γ → α
h : α = α'
⊢ HEq (fun x => cast h (a x)) a
Tactic:
cases h
State after:
case refl
α : Sort u_1
γ : Sort u_2
a : γ → α
⊢ HEq (fun x => cast ⋯ (a x)) a

State before:
case refl
α : Sort u_1
γ : Sort u_2
a : γ → α
⊢ HEq (fun x => cast ⋯ (a x)) a
Tactic:
simp only [cast_eq, heq_eq_eq]
State after:
no goals