Theorem: Smt.Reconstruct.Prop.ite_eq (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
α : Sort u_1
c : Prop
h : Decidable c
x y : α
⊢ if c then (if c then x else y) = x else (if c then x else y) = y
Tactic:
cases h
State after:
case isFalse
α : Sort u_1
c : Prop
x y : α
h✝ : ¬c
⊢ if c then (if c then x else y) = x else (if c then x else y) = y

case isTrue
α : Sort u_1
c : Prop
x y : α
h✝ : c
⊢ if c then (if c then x else y) = x else (if c then x else y) = y

State before:
case isFalse
α : Sort u_1
c : Prop
x y : α
h✝ : ¬c
⊢ if c then (if c then x else y) = x else (if c then x else y) = y

case isTrue
α : Sort u_1
c : Prop
x y : α
h✝ : c
⊢ if c then (if c then x else y) = x else (if c then x else y) = y
Tactic:
all_goals simp_all
State after:
no goals

State before:
case isTrue
α : Sort u_1
c : Prop
x y : α
h✝ : c
⊢ if c then (if c then x else y) = x else (if c then x else y) = y
Tactic:
simp_all
State after:
no goals