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

State before:
α : Sort u_1
a : α
motive : α → Sort u_2
h : a = a
t : motive a
⊢ dcast h t = t
Tactic:
cases h
State after:
case refl
α : Sort u_1
a : α
motive : α → Sort u_2
t : motive a
⊢ dcast ⋯ t = t

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