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

State before:
α : Type u
c : Prop
t e : α
⊢ if c then (if c then t else e) = t else (if c then t else e) = e
Tactic:
match Classical.em c with
| Or.inl hc  => rw [if_pos hc, if_pos hc]
| Or.inr hnc => rw [if_neg hnc, if_neg hnc]
State after:
no goals

State before:
α : Type u
c : Prop
t e : α
hc : c
⊢ if c then (if c then t else e) = t else (if c then t else e) = e
Tactic:
rw [if_pos hc, if_pos hc]
State after:
no goals

State before:
α : Type u
c : Prop
t e : α
hnc : ¬c
⊢ if c then (if c then t else e) = t else (if c then t else e) = e
Tactic:
rw [if_neg hnc, if_neg hnc]
State after:
no goals