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

State before:
L✝ : Language
inst✝² : L✝.LT
μ : Type v
L : Language
inst✝¹ : L.Eq
inst✝ : L.LT
n : ℕ
Γ : Polarity
s : ℕ
t u : Semiterm L μ n
⊢ Hierarchy Γ s (“!!t ≤ !!u”)
Tactic:
simp[Semiformula.Operator.operator, Matrix.fun_eq_vec₂,
  Semiformula.Operator.Eq.sentence_eq, Semiformula.Operator.LT.sentence_eq,
  Semiformula.Operator.LE.sentence_eq]
State after:
no goals