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

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

State before:
case h
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₂ (cast h₁ a)) (cast ⋯ a)
Tactic:
apply HEq.trans (b:=cast h₁ a)
State after:
case h.h₁
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₂ (cast h₁ a)) (cast h₁ a)

case h.h₂
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₁ a) (cast ⋯ a)

State before:
case h.h₁
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₂ (cast h₁ a)) (cast h₁ a)

case h.h₂
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₁ a) (cast ⋯ a)
Tactic:
apply cast_heq
State after:
case h.h₂
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₁ a) (cast ⋯ a)

State before:
case h.h₂
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₁ a) (cast ⋯ a)
Tactic:
apply HEq.trans
State after:
case h.h₂.h₁
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₁ a) ?h.h₂.b

case h.h₂.h₂
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq ?h.h₂.b (cast ⋯ a)

case h.h₂.β
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ Sort u_1

case h.h₂.b
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ ?h.h₂.β

State before:
case h.h₂.h₁
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast h₁ a) ?h.h₂.b

case h.h₂.h₂
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq ?h.h₂.b (cast ⋯ a)

case h.h₂.β
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ Sort u_1

case h.h₂.b
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ ?h.h₂.β
Tactic:
apply cast_heq
State after:
case h.h₂.h₂
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq a (cast ⋯ a)

State before:
case h.h₂.h₂
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq a (cast ⋯ a)
Tactic:
apply HEq.symm
State after:
case h.h₂.h₂.h
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast ⋯ a) a

State before:
case h.h₂.h₂.h
γ α β : Sort u_1
a : α
h₁ : α = β
h₂ : β = γ
⊢ HEq (cast ⋯ a) a
Tactic:
apply cast_heq
State after:
no goals