Theorem: LO.FirstOrder.Arith.Hierarchy.iff_iff (Logic/FirstOrder/Arith/Hierarchy.lean)

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
b : Polarity
s : ℕ
p q : Semiformula L μ n
⊢ Hierarchy b s (p ⟷ q) ↔ Hierarchy b s p ∧ Hierarchy b.alt s p ∧ Hierarchy b s q ∧ Hierarchy b.alt s q
Tactic:
simp[Semiformula.iff_eq]
State after:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
b : Polarity
s : ℕ
p q : Semiformula L μ n
⊢ (Hierarchy b.alt s p ∧ Hierarchy b s q) ∧ Hierarchy b.alt s q ∧ Hierarchy b s p ↔
    Hierarchy b s p ∧ Hierarchy b.alt s p ∧ Hierarchy b s q ∧ Hierarchy b.alt s q

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
b : Polarity
s : ℕ
p q : Semiformula L μ n
⊢ (Hierarchy b.alt s p ∧ Hierarchy b s q) ∧ Hierarchy b.alt s q ∧ Hierarchy b s p ↔
    Hierarchy b s p ∧ Hierarchy b.alt s p ∧ Hierarchy b s q ∧ Hierarchy b.alt s q
Tactic:
tauto
State after:
no goals