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

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
m : ℕ
ξ : Type u_1
b : Polarity
s n : ℕ
p : Fin m → Semiformula L ξ n
⊢ Hierarchy b s (Matrix.conj fun j => p j) ↔ ∀ (j : Fin m), Hierarchy b s (p j)
Tactic:
cases m <;> simp
State after:
no goals