Theorem: dcast_comp (Extra/Cast/DCast.lean)

State before:
α : Sort u_1
a b c : α
motive : α → Sort u_2
hab : a = b
hbc : b = c
t : motive a
⊢ dcast hbc (dcast hab t) = dcast ⋯ t
Tactic:
cases hab
State after:
case refl
α : Sort u_1
a c : α
motive : α → Sort u_2
t : motive a
hbc : a = c
⊢ dcast hbc (dcast ⋯ t) = dcast ⋯ t

State before:
case refl
α : Sort u_1
a c : α
motive : α → Sort u_2
t : motive a
hbc : a = c
⊢ dcast hbc (dcast ⋯ t) = dcast ⋯ t
Tactic:
rfl
State after:
no goals