Theorem: ℤθ.my_zsmul_neg' (Mordell4/CubicRing.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.f, Int.negSucc n * a.g, Int.negSucc n * a.h⟩ : ℤθ) =
    (⟨-(Int.ofNat n.succ * a.f), -(Int.ofNat n.succ * a.g), -(Int.ofNat n.succ * a.h)⟩ : ℤθ)
State after:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ { f := Int.negSucc n * a.f, g := Int.negSucc n * a.g, h := Int.negSucc n * a.h } =
    { f := -(Int.ofNat (Nat.succ n) * a.f), g := -(Int.ofNat (Nat.succ n) * a.g), h := -(Int.ofNat (Nat.succ n) * a.h) }

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

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

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

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

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Tactic:
rw [Int.negSucc_coe]
State after:
case left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -↑(n + 1) * a.f = -((↑n + 1) * a.f)

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

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

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Tactic:
rw [Int.neg_mul_eq_neg_mul_symm]
State after:
case left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -(↑(n + 1) * a.f) = -((↑n + 1) * a.f)

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

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

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Tactic:
rw [Int.ofNat_add]
State after:
case left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -((↑n + ↑1) * a.f) = -((↑n + 1) * a.f)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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