Theorem: heq_of_eq_left' (Qpf/Util/HEq.lean)

State before:
α β : Sort u_1
a : α
b : β
h : α = β
⊢ cast h a = b → HEq a b
Tactic:
intro eq
State after:
α β : Sort u_1
a : α
b : β
h : α = β
eq : cast h a = b
⊢ HEq a b

State before:
α β : Sort u_1
a : α
b : β
h : α = β
eq : cast h a = b
⊢ HEq a b
Tactic:
apply HEq.symm
State after:
case h
α β : Sort u_1
a : α
b : β
h : α = β
eq : cast h a = b
⊢ HEq b a

State before:
case h
α β : Sort u_1
a : α
b : β
h : α = β
eq : cast h a = b
⊢ HEq b a
Tactic:
apply heq_of_eq' h eq.symm
State after:
no goals