Theorem: ℤα.my_zsmul_succ' (Mordell4/Rt7Ring.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.z, Int.ofNat n.succ * a.w⟩ : ℤα) =
    (⟨a.z + Int.ofNat n * a.z, a.w + Int.ofNat n * a.w⟩ : ℤα)
State after:
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ { z := Int.ofNat (Nat.succ n) * a.z, w := Int.ofNat (Nat.succ n) * a.w } =
    { z := a.z + Int.ofNat n * a.z, w := a.w + Int.ofNat n * a.w }

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

State before:
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ (↑n + 1) * a.z = a.z + ↑n * a.z ∧ (↑n + 1) * a.w = a.w + ↑n * a.w
Tactic:
constructor
State after:
case left
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ (↑n + 1) * a.z = a.z + ↑n * a.z

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

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

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

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