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

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

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