Theorem: ℤθ.my_zsmul_succ' (Mordell4/CubicRing.lean)

State before:
a b c : ℤθ
⊢ ∀ (n : ℕ) (a : ℤθ), zsmul (Int.ofNat (Nat.succ n)) a = add a (zsmul (Int.ofNat n) a)
Tactic:
intro n a
State after:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ zsmul (Int.ofNat (Nat.succ n)) a = add a (zsmul (Int.ofNat n) a)

State before:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ zsmul (Int.ofNat (Nat.succ n)) a = add a (zsmul (Int.ofNat n) a)
Tactic:
change
  (⟨Int.ofNat n.succ * a.f, Int.ofNat n.succ * a.g, Int.ofNat n.succ * a.h⟩ : ℤθ) =
    (⟨a.f + Int.ofNat n * a.f, a.g + Int.ofNat n * a.g, a.h + Int.ofNat n * a.h⟩ : ℤθ)
State after:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ { f := Int.ofNat (Nat.succ n) * a.f, g := Int.ofNat (Nat.succ n) * a.g, h := Int.ofNat (Nat.succ n) * a.h } =
    { f := a.f + Int.ofNat n * a.f, g := a.g + Int.ofNat n * a.g, h := a.h + Int.ofNat n * a.h }

State before:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ { f := Int.ofNat (Nat.succ n) * a.f, g := Int.ofNat (Nat.succ n) * a.g, h := Int.ofNat (Nat.succ n) * a.h } =
    { f := a.f + Int.ofNat n * a.f, g := a.g + Int.ofNat n * a.g, h := a.h + Int.ofNat n * a.h }
Tactic:
norm_num
State after:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.f = a.f + ↑n * a.f ∧ (↑n + 1) * a.g = a.g + ↑n * a.g ∧ (↑n + 1) * a.h = a.h + ↑n * a.h

State before:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.f = a.f + ↑n * a.f ∧ (↑n + 1) * a.g = a.g + ↑n * a.g ∧ (↑n + 1) * a.h = a.h + ↑n * a.h
Tactic:
constructor
State after:
case left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.f = a.f + ↑n * a.f

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.g = a.g + ↑n * a.g ∧ (↑n + 1) * a.h = a.h + ↑n * a.h

State before:
case left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.f = a.f + ↑n * a.f

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.g = a.g + ↑n * a.g ∧ (↑n + 1) * a.h = a.h + ↑n * a.h
Tactic:
linarith
State after:
case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.g = a.g + ↑n * a.g ∧ (↑n + 1) * a.h = a.h + ↑n * a.h

State before:
case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.g = a.g + ↑n * a.g ∧ (↑n + 1) * a.h = a.h + ↑n * a.h
Tactic:
constructor
State after:
case right.left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.g = a.g + ↑n * a.g

case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.h = a.h + ↑n * a.h

State before:
case right.left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.g = a.g + ↑n * a.g

case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.h = a.h + ↑n * a.h
Tactic:
linarith
State after:
case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.h = a.h + ↑n * a.h

State before:
case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.h = a.h + ↑n * a.h
Tactic:
linarith
State after:
no goals