Theorem: cast_symm (GMLInit/Logic/Cast.lean)

State before:
α β : Sort u_1
h : α = β
a : α
b : β
⊢ cast h a = b ↔ a = cast ⋯ b
Tactic:
cases h
State after:
case refl
α : Sort u_1
a b : α
⊢ cast ⋯ a = b ↔ a = cast ⋯ b

State before:
case refl
α : Sort u_1
a b : α
⊢ cast ⋯ a = b ↔ a = cast ⋯ b
Tactic:
exact Iff.rfl
State after:
no goals