Theorem: LO.FirstOrder.Structure.numeral_eq_numeral (Logic/FirstOrder/Arith/Basic.lean)

State before:
L : Language
inst✝¹¹ : Operator.Zero L
inst✝¹⁰ : Operator.One L
inst✝⁹ : Operator.Add L
M : Type u
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : Structure L M
inst✝² : Structure.Zero L M
inst✝¹ : Structure.One L M
inst✝ : Structure.Add L M
⊢ Semiterm.Operator.val 0 ![] = ORingSymbol.numeral 0
Tactic:
simp[ORingSymbol.numeral, Semiterm.Operator.numeral_zero]
State after:
no goals

State before:
L : Language
inst✝¹¹ : Operator.Zero L
inst✝¹⁰ : Operator.One L
inst✝⁹ : Operator.Add L
M : Type u
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : Structure L M
inst✝² : Structure.Zero L M
inst✝¹ : Structure.One L M
inst✝ : Structure.Add L M
⊢ Semiterm.Operator.val 1 ![] = ORingSymbol.numeral 1
Tactic:
simp[ORingSymbol.numeral, Semiterm.Operator.numeral_one]
State after:
no goals

State before:
L : Language
inst✝¹¹ : Operator.Zero L
inst✝¹⁰ : Operator.One L
inst✝⁹ : Operator.Add L
M : Type u
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : Structure L M
inst✝² : Structure.Zero L M
inst✝¹ : Structure.One L M
inst✝ : Structure.Add L M
z : ℕ
⊢ Semiterm.Operator.val (Operator.numeral L (z + 2)) ![] = ORingSymbol.numeral (z + 2)
Tactic:
simp[ORingSymbol.numeral, Semiterm.Operator.numeral_add_two,
  Semiterm.Operator.val_comp, Matrix.fun_eq_vec₂, numeral_eq_numeral (z + 1)]
State after:
no goals