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

State before:
L : Language
hz✝ : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
z : ℕ
hz : z ≠ 0
⊢ numeral L (z + 1) = op(+).comp ![numeral L z, op(1)]
Tactic:
simp [numeral]
State after:
L : Language
hz✝ : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
z : ℕ
hz : z ≠ 0
⊢ op(+).foldr op(1) (List.replicate z op(1)) =
    op(+).comp
      ![match z with
        | 0 => op(0)
        | n.succ => op(+).foldr op(1) (List.replicate n op(1)),
        op(1)]

State before:
L : Language
hz✝ : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
z : ℕ
hz : z ≠ 0
⊢ op(+).foldr op(1) (List.replicate z op(1)) =
    op(+).comp
      ![match z with
        | 0 => op(0)
        | n.succ => op(+).foldr op(1) (List.replicate n op(1)),
        op(1)]
Tactic:
cases' z with z
State after:
case zero
L : Language
hz✝ : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
hz : 0 ≠ 0
⊢ op(+).foldr op(1) (List.replicate 0 op(1)) =
    op(+).comp
      ![match 0 with
        | 0 => op(0)
        | n.succ => op(+).foldr op(1) (List.replicate n op(1)),
        op(1)]

case succ
L : Language
hz✝ : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
z : ℕ
hz : z + 1 ≠ 0
⊢ op(+).foldr op(1) (List.replicate (z + 1) op(1)) =
    op(+).comp
      ![match z + 1 with
        | 0 => op(0)
        | n.succ => op(+).foldr op(1) (List.replicate n op(1)),
        op(1)]

State before:
case zero
L : Language
hz✝ : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
hz : 0 ≠ 0
⊢ op(+).foldr op(1) (List.replicate 0 op(1)) =
    op(+).comp
      ![match 0 with
        | 0 => op(0)
        | n.succ => op(+).foldr op(1) (List.replicate n op(1)),
        op(1)]
Tactic:
simp at hz
State after:
no goals

State before:
case succ
L : Language
hz✝ : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
z : ℕ
hz : z + 1 ≠ 0
⊢ op(+).foldr op(1) (List.replicate (z + 1) op(1)) =
    op(+).comp
      ![match z + 1 with
        | 0 => op(0)
        | n.succ => op(+).foldr op(1) (List.replicate n op(1)),
        op(1)]
Tactic:
simp [Operator.foldr]
State after:
no goals