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

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

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