Theorem: LO.FirstOrder.Semiterm.complexity_one (Logic/FirstOrder/Basic/Operator.lean)

State before:
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
⊢ (Operator.const op(1)).complexity = 1
Tactic:
simp [Operator.const, Operator.operator, Operator.numeral, Operator.One.term_eq, complexity_func]
State after:
no goals