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

State before:
α β γ : Sort u_1
h₁ : α = β
h₂ : β = γ
a : α
⊢ cast h₂ (cast h₁ a) = cast ⋯ a
Tactic:
cases h₁
State after:
case refl
α γ : Sort u_1
a : α
h₂ : α = γ
⊢ cast h₂ (cast ⋯ a) = cast ⋯ a

State before:
case refl
α γ : Sort u_1
a : α
h₂ : α = γ
⊢ cast h₂ (cast ⋯ a) = cast ⋯ a
Tactic:
cases h₂
State after:
case refl.refl
α : Sort u_1
a : α
⊢ cast ⋯ (cast ⋯ a) = cast ⋯ a

State before:
case refl.refl
α : Sort u_1
a : α
⊢ cast ⋯ (cast ⋯ a) = cast ⋯ a
Tactic:
rfl
State after:
no goals