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
p q : Semiformula L μ n
⊢ Hierarchy b 0 (p ⟷ q) ↔ Hierarchy b 0 p ∧ Hierarchy b 0 q
Tactic:
simp[Semiformula.iff_eq]
State after:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
b : Polarity
p q : Semiformula L μ n
⊢ Hierarchy b 0 p → Hierarchy b 0 q → Hierarchy b 0 q ∧ Hierarchy b 0 p

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