Theorem: ℤα.my_zsmul_neg' (Mordell4/Rt7Ring.lean)

State before:
a b c : ℤα
⊢ ∀ (n : ℕ) (a : ℤα), zsmul (Int.negSucc n) a = neg (zsmul (↑(Nat.succ n)) a)
Tactic:
intro n a
State after:
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ zsmul (Int.negSucc n) a = neg (zsmul (↑(Nat.succ n)) a)

State before:
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ zsmul (Int.negSucc n) a = neg (zsmul (↑(Nat.succ n)) a)
Tactic:
simp
State after:
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ zsmul (Int.negSucc n) a = neg (zsmul (↑n + 1) a)

State before:
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ zsmul (Int.negSucc n) a = neg (zsmul (↑n + 1) a)
Tactic:
change
  (⟨Int.negSucc n * a.z, Int.negSucc n * a.w⟩ : ℤα) =
    (⟨-(Int.ofNat n.succ * a.z), -(Int.ofNat n.succ * a.w)⟩ : ℤα)
State after:
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ { z := Int.negSucc n * a.z, w := Int.negSucc n * a.w } =
    { z := -(Int.ofNat (Nat.succ n) * a.z), w := -(Int.ofNat (Nat.succ n) * a.w) }

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

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

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

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

case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ Int.negSucc n * a.w = -((↑n + 1) * a.w)
Tactic:
rw [Int.negSucc_coe]
State after:
case left
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ -↑(n + 1) * a.z = -((↑n + 1) * a.z)

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

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

case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ Int.negSucc n * a.w = -((↑n + 1) * a.w)
Tactic:
rw [Int.neg_mul_eq_neg_mul_symm]
State after:
case left
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ -(↑(n + 1) * a.z) = -((↑n + 1) * a.z)

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

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

case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ Int.negSucc n * a.w = -((↑n + 1) * a.w)
Tactic:
rw [Int.ofNat_add]
State after:
case left
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ -((↑n + ↑1) * a.z) = -((↑n + 1) * a.z)

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

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

case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ Int.negSucc n * a.w = -((↑n + 1) * a.w)
Tactic:
rw [Int.ofNat_one]
State after:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ Int.negSucc n * a.w = -((↑n + 1) * a.w)

State before:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ Int.negSucc n * a.w = -((↑n + 1) * a.w)
Tactic:
rw [Int.negSucc_coe]
State after:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ -↑(n + 1) * a.w = -((↑n + 1) * a.w)

State before:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ -↑(n + 1) * a.w = -((↑n + 1) * a.w)
Tactic:
rw [Int.neg_mul_eq_neg_mul_symm]
State after:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ -(↑(n + 1) * a.w) = -((↑n + 1) * a.w)

State before:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ -(↑(n + 1) * a.w) = -((↑n + 1) * a.w)
Tactic:
rw [Int.ofNat_add]
State after:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ -((↑n + ↑1) * a.w) = -((↑n + 1) * a.w)

State before:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ -((↑n + ↑1) * a.w) = -((↑n + 1) * a.w)
Tactic:
rw [Int.ofNat_one]
State after:
no goals