mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
n : Fin 2
a✝ : Nontrivial R
⊢ (if hp : Subsingleton R then default else (AdjoinRoot.powerBasis' ⋯).basis.reindex (finCongr ⋯)) n =
    (AdjoinRoot.powerBasis' ⋯).gen ^ ↑n

Tactic:
dif_neg <| not_subsingleton R,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
n : Fin 2
a✝ : Nontrivial R
⊢ ((AdjoinRoot.powerBasis' ⋯).basis.reindex (finCongr ⋯)) n = (AdjoinRoot.powerBasis' ⋯).gen ^ ↑n
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
y p q : R[X]
⊢ ((mk W') (C p) * 1 + (mk W') (C q) * (mk W') Y) * (mk W') (C y) =
    (mk W') (C p) * (mk W') (C y) * 1 + (mk W') (C q) * (mk W') (C y) * (mk W') Y

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ (fun x ↦ x ^ 2) Y - (C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) - C (C W'.a₁ * X + C W'.a₃) * Y) =
    (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) * 1

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
Y_sq : (mk W') Y ^ 2 = (mk W') (C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) - C (C W'.a₁ * X + C W'.a₃) * Y)
⊢ (mk W') (C p) * (1 * (mk W') Y) +
      (mk W') (C q) *
        ((mk W') (C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) -
          (mk W') (C (C W'.a₁ * X + C W'.a₃)) * (mk W') Y) =
    (mk W') (C q) * ((mk W') (C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) * 1) +
      ((mk W') (C p) - (mk W') (C q) * (mk W') (C (C W'.a₁ * X + C W'.a₃))) * (mk W') Y

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case e_a.e_6
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ Y -
        (-(C (C ℓ) * (C (C (W'.addX x₁ x₂ ℓ)) - C (C x₁)) + C (C y₁)) - C (C W'.a₁) * C (C (W'.addX x₁ x₂ ℓ)) -
          C (C W'.a₃)) +
      (C X - C (C (W'.addX x₁ x₂ ℓ))) * (C (C W'.a₁) + C (C ℓ)) =
    C (C W'.a₁) * C X + C (C W'.a₃) + (C (C ℓ) * (C X - C (C x₁)) + C (C y₁)) + Y

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case e_a.e_6
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ Y - C (C y) + (C X - C (C x)) * -C (C ℓ) = Y - (C (C ℓ) * (C X - C (C x)) + C (C y))

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ = x₂
⊢ y₂ * (x₁ - x₂) = (y₁ - y₂) * (x₂ - x₁) + (x₁ - x₂) * y₁

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case e_a.e_6
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ Y - (C (C (W.slope x₁ x₂ y₁ y₂)) * (C (C x₂) - C (C x₁)) + C (C y₁)) +
      (C X - C (C x₂)) * -C (C (W.slope x₁ x₂ y₁ y₂)) =
    Y - (C (C (W.slope x₁ x₂ y₁ y₂)) * (C X - C (C x₁)) + C (C y₁))

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ (Y - C (C y)) * (Y - (-C (C y) - C (C W.a₁) * C (C x) - C (C W.a₃))) -
          (C X - C (C x)) *
            (C X ^ 2 + (C (C x) + C (C W.a₂)) * C X + (C (C x) ^ 2 + C (C W.a₂) * C (C x) + C (C W.a₄)) -
              C (C W.a₁) * Y) +
        (C (C y) ^ 2 + C (C W.a₁) * C (C x) * C (C y) + C (C W.a₃) * C (C y)) -
      ((Y ^ 2 + (C (C W.a₁) * C X + C (C W.a₃)) * Y -
            (C X ^ 3 + C (C W.a₂) * C X ^ 2 + C (C W.a₄) * C X + C (C W.a₆))) *
          1 +
        (C (C x) ^ 3 + C (C W.a₂) * C (C x) ^ 2 + C (C W.a₄) * C (C x) + C (C W.a₆))) =
    0

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case inl
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hx : W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0
W_X : F := W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)
⊢ 1 * -1 *
      (C X ^ 2 + (C (C x) + C (C W.a₂)) * C X + (C (C x) ^ 2 + C (C W.a₂) * C (C x) + C (C W.a₄)) - C (C W.a₁) * Y) =
    (C (C W.a₁) * C (C y) - (3 * C (C x) ^ 2 + 2 * C (C W.a₂) * C (C x) + C (C W.a₄))) * 1 +
          1 * -(C X + (2 * C (C x) + C (C W.a₂))) * (C X - C (C x)) +
        1 * C (C W.a₁) * (Y - C (C y)) +
      (C (C W.a₁) * C (C y) - (3 * C (C x) ^ 2 + 2 * C (C W.a₂) * C (C x) + C (C W.a₄))) * 0 * (Y - C (C (W.negY x y)))

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ -(((1 - 0) * (X - C x₂) + (X - C x₁) * (1 - 0)) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) +
        (X - C x₁) * (X - C x₂) * (1 - 0)) =
    -((X - C x₁) * (X - C x₂) + (X - C x₁) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) +
        (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case inr
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hy : 2 * y + W.a₁ * x + W.a₃ ≠ 0
W_Y : F := 2 * y + W.a₁ * x + W.a₃
⊢ (2 * C (C y) + C (C W.a₁) * C (C x) + C (C W.a₃)) * 0 *
      (C X ^ 2 + (C (C x) + C (C W.a₂)) * C X + (C (C x) ^ 2 + C (C W.a₂) * C (C x) + C (C W.a₄)) - C (C W.a₁) * Y) =
    (2 * C (C y) + C (C W.a₁) * C (C x) + C (C W.a₃)) * 1 +
          (2 * C (C y) + C (C W.a₁) * C (C x) + C (C W.a₃)) * 0 * (C X - C (C x)) +
        1 * (Y - C (C y)) +
      1 * -1 * (Y - (-C (C y) - C (C W.a₁) * C (C x) - C (C W.a₃)))

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx :
  W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - (3 * W'.addX x₁ x₂ ℓ ^ 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) = 0 ∧
    2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) = 0
⊢ 2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) * ℓ +
            (W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) * ℓ) -
          (3 * W'.addX x₁ x₂ ℓ ^ 2 + W'.a₂ * (2 * W'.addX x₁ x₂ ℓ) + W'.a₄) +
        (0 + ℓ * 0) -
      (0 +
        (W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - (3 * W'.addX x₁ x₂ ℓ ^ 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) +
          ℓ * (2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃)))) =
    0

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ (y₁ - y₂) * (y₁ - y₂ + (x₁ - x₂) * W.a₁) - (x₁ - x₂) ^ 2 * W.a₂ - x₁ * (x₁ - x₂) ^ 2 - x₂ * (x₁ - x₂) ^ 2 =
    (y₁ - (-y₂ - x₂ * W.a₁ - W.a₃)) * (y₁ - (-y₂ - x₂ * W.a₁ - W.a₃) + (x₁ - x₂) * W.a₁) - (x₁ - x₂) ^ 2 * W.a₂ -
          x₁ * (x₁ - x₂) ^ 2 -
        x₂ * (x₁ - x₂) ^ 2 -
      (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) * (y₂ - (-y₂ - x₂ * W.a₁ - W.a₃))

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ y₁ *
          (x₂ * (x₁ - x₂) ^ 2 -
            ((y₁ - y₂) * (y₁ - y₂ + (x₁ - x₂) * W.a₁) - (x₁ - x₂) ^ 2 * W.a₂ - x₁ * (x₁ - x₂) ^ 2 -
              x₂ * (x₁ - x₂) ^ 2)) +
        y₂ *
          ((y₁ - y₂) * (y₁ - y₂ + (x₁ - x₂) * W.a₁) - (x₁ - x₂) ^ 2 * W.a₂ - x₁ * (x₁ - x₂) ^ 2 - x₂ * (x₁ - x₂) ^ 2 -
            x₁ * (x₁ - x₂) ^ 2) +
      ((y₁ - y₂) *
          ((y₁ - y₂) * (y₁ - y₂ + (x₁ - x₂) * W.a₁) - (x₁ - x₂) ^ 2 * W.a₂ - x₁ * (x₁ - x₂) ^ 2 - x₂ * (x₁ - x₂) ^ 2 -
            x₁ * (x₁ - x₂) ^ 2) +
        y₁ * (x₁ - x₂) ^ 3) =
    0

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: case a
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ (-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃ -
            (-(-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃) -
                W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) -
              W.a₃)) *
          (x₂ - x₁) +
        2 * 0 -
      ((y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) -
          (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) +
        2 *
          (y₁ * (x₂ - addX ?m.71 x₁ x₂ (slope ?m.71 x₁ x₂ y₁ y₂)) +
              y₂ * (addX ?m.71 x₁ x₂ (slope ?m.71 x₁ x₂ y₁ y₂) - x₁) +
            negAddY ?m.71 x₁ x₂ y₁ (slope ?m.71 x₁ x₂ y₁ y₂) * (x₁ - x₂))) =
    0

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c : ℤ
⊢ atom W a b * atom W a c - W a * W 0 * atom W b c + atom W a c * atom W b a +
        (W a * W 0 * atom W b c + atom W a c * -atom W a b) -
      (W a * W 0 * atom W c b + (W a * W 0 * -atom W c b + atom W a c * atom W b a)) =
    0

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c : ℤ
⊢ atom W a b * atom W c b - atom W a c * (W b * W 0) + atom W a b * atom W b c +
        (W b * W 0 * atom W c a + atom W a b * -atom W b c) -
      (W b * W 0 * atom W c a + (W b * W 0 * -atom W a c + atom W a b * atom W c b)) =
    0

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: x✝³ x✝² x✝¹ x✝ : ℤ
⊢ (x✝³ + x✝² + x✝) * (x✝³ - x✝²) * (x✝¹ + x✝) * x✝¹ - (x✝³ + x✝¹ + x✝) * (x✝³ - x✝¹) * (x✝² + x✝) * x✝² +
      (x✝² + x✝¹ + x✝) * (x✝² - x✝¹) * (x✝³ + x✝) * x✝³ =
    0

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
h : IsEllipticNet W
x : R
p q r s : ℤ
⊢ x * W (p + q + s) * (x * W (p - q)) * (x * W (r + s)) * (x * W r) -
            x * W (p + r + s) * (x * W (p - r)) * (x * W (q + s)) * (x * W q) +
          x * W (q + r + s) * (x * W (q - r)) * (x * W (p + s)) * (x * W p) +
        x ^ 4 * 0 -
      (0 +
        x ^ 4 *
          (W (p + q + s) * W (p - q) * W (r + s) * W r - W (p + r + s) * W (p - r) * W (q + s) * W q +
            W (q + r + s) * W (q - r) * W (p + s) * W p)) =
    0

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case a
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := (y₁ - W.negY x₁ y₁) ^ 2
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ 1 * (Y - (-Y - (C (C W.a₁) * C X + C (C W.a₃)))) * (Y - (-Y - (C (C W.a₁) * C X + C (C W.a₃)))) +
        -4 * (C (C x₁) ^ 3 + C (C W.a₂) * C (C x₁) ^ 2 + C (C W.a₄) * C (C x₁) + C (C W.a₆)) -
      ((C (C y₁) - (-C (C y₁) - C (C W.a₁) * C (C x₁) - C (C W.a₃))) ^ 2 * 1 +
              1 * 4 *
                (Y ^ 2 + (C (C W.a₁) * C X + C (C W.a₃)) * Y -
                  (C X ^ 3 + C (C W.a₂) * C X ^ 2 + C (C W.a₄) * C X + C (C W.a₆))) +
            (1 * 4 * C X ^ 2 + (1 * 4 * C (C x₁) + 1 * (C (C W.a₁) ^ 2 + 4 * C (C W.a₂))) * C X +
                (1 * 4 * C (C x₁) ^ 2 + 1 * (C (C W.a₁) ^ 2 + 4 * C (C W.a₂)) * C (C x₁) +
                  1 * 2 * (2 * C (C W.a₄) + C (C W.a₁) * C (C W.a₃)))) *
              (C X - C (C x₁)) +
          (C (C y₁) - (-C (C y₁) - C (C W.a₁) * C (C x₁) - C (C W.a₃))) ^ 2 * 0 * (C X - C (C x₁)) +
        -4 * (C (C y₁) ^ 2 + C (C W.a₁) * C (C x₁) * C (C y₁) + C (C W.a₃) * C (C y₁))) =
    0

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
h : IsEllipticSequence W
x : R
p q r : ℤ
⊢ x * W (p + q) * (x * W (p - q)) * (x * W r) * (x * W r) - x * W (p + r) * (x * W (p - r)) * (x * W q) * (x * W q) +
        x * W (q + r) * (x * W (q - r)) * (x * W p) * (x * W p) -
      x ^ 4 *
        (W (p + q) * W (p - q) * W r * W r - W (p + r) * W (p - r) * W q * W q + W (q + r) * W (q - r) * W p * W p) =
    0

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n) =
      preNormEDS b c d (↑n - 1) ^ 2 * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 2) -
        preNormEDS b c d (↑n - 2) * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 1) ^ 2
m : ℕ
⊢ -(preNormEDS b c d (↑m - 1) ^ 2 * preNormEDS b c d ↑m * preNormEDS b c d (↑m + 2) -
        preNormEDS b c d (↑m - 2) * preNormEDS b c d ↑m * preNormEDS b c d (↑m + 1) ^ 2) =
    (-preNormEDS b c d (↑m + 1)) ^ 2 * -preNormEDS b c d ↑m * -preNormEDS b c d (↑m - 2) -
      -preNormEDS b c d (↑m + 2) * -preNormEDS b c d ↑m * (-preNormEDS b c d (↑m - 1)) ^ 2

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
hx : x₁ - x₂ ≠ 0
⊢ (C (C x₁) - C (C x₂)) * 0 * (Y - W.negPolynomial) =
    (C (C x₁) - C (C x₂)) * 1 + 1 * (C X - C (C x₁)) + 1 * -1 * (C X - C (C x₂))

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ -(↑m + 1) + 2 = -(↑m - 1)

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ -(↑m + 1) + 1 = -↑m

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ -((preNormEDS b c d (↑m + 2) * preNormEDS b c d ↑m ^ 3 * if Even ↑m then b else 1) -
        preNormEDS b c d (↑m - 1) * preNormEDS b c d (↑m + 1) ^ 3 * if Even ↑m then 1 else b) =
    (-preNormEDS b c d (↑m - 1) * (-preNormEDS b c d (↑m + 1)) ^ 3 * if Even ↑m then 1 else b) -
      -preNormEDS b c d (↑m + 2) * (-preNormEDS b c d ↑m) ^ 3 * if Even ↑m then b else 1

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ (((-preNormEDS (b ^ 4) c d (k - -1)) ^ 2 * -preNormEDS (b ^ 4) c d (k - 2) -
        -preNormEDS (b ^ 4) c d (k - -2) * (-preNormEDS (b ^ 4) c d (k - 1)) ^ 2) *
      if Even k then 1 else b) =
    (preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k - -2) -
        preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k - -1) ^ 2) *
      if Even k then 1 else b

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ preNormEDS (b ^ 4) c d k *
      ((preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k + 2) -
          preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k + 1) ^ 2) *
        if Even k then 1 else b) =
    (preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d k * preNormEDS (b ^ 4) c d (k + 2) -
        preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d k * preNormEDS (b ^ 4) c d (k + 1) ^ 2) *
      if Even k then 1 else b

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
h✝ : Even k
⊢ (preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k + 2) -
          preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k + 1) ^ 2) *
        1 *
      b =
    (preNormEDS (b ^ 4) c d (k - 1) * 1) ^ 2 * (preNormEDS (b ^ 4) c d (k + 2) * b) -
      preNormEDS (b ^ 4) c d (k - 2) * b * (preNormEDS (b ^ 4) c d (k + 1) * 1) ^ 2

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
h✝ : ¬Even k
⊢ (preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k + 2) -
          preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k + 1) ^ 2) *
        b *
      b =
    (preNormEDS (b ^ 4) c d (k - 1) * b) ^ 2 * (preNormEDS (b ^ 4) c d (k + 2) * 1) -
      preNormEDS (b ^ 4) c d (k - 2) * 1 * (preNormEDS (b ^ 4) c d (k + 1) * b) ^ 2

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℤ
⊢ normEDS b c d m *
      (normEDS b c d (m - 1) ^ 2 * normEDS b c d (m + 2) - normEDS b c d (m - 2) * normEDS b c d (m + 1) ^ 2) =
    normEDS b c d (m - 1) ^ 2 * normEDS b c d m * normEDS b c d (m + 2) -
      normEDS b c d (m - 2) * normEDS b c d m * normEDS b c d (m + 1) ^ 2

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℤ
h✝ : Even m
⊢ (preNormEDS (b ^ 4) c d (m + 2) * preNormEDS (b ^ 4) c d m ^ 3 * b ^ 4 -
        preNormEDS (b ^ 4) c d (m - 1) * preNormEDS (b ^ 4) c d (m + 1) ^ 3 * 1) *
      1 =
    preNormEDS (b ^ 4) c d (m + 2) * b * (preNormEDS (b ^ 4) c d m * b) ^ 3 -
      preNormEDS (b ^ 4) c d (m - 1) * 1 * (preNormEDS (b ^ 4) c d (m + 1) * 1) ^ 3

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℤ
h✝ : ¬Even m
⊢ (preNormEDS (b ^ 4) c d (m + 2) * preNormEDS (b ^ 4) c d m ^ 3 * 1 -
        preNormEDS (b ^ 4) c d (m - 1) * preNormEDS (b ^ 4) c d (m + 1) ^ 3 * b ^ 4) *
      1 =
    preNormEDS (b ^ 4) c d (m + 2) * 1 * (preNormEDS (b ^ 4) c d m * 1) ^ 3 -
      preNormEDS (b ^ 4) c d (m - 1) * b * (preNormEDS (b ^ 4) c d (m + 1) * b) ^ 3

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ (p * 1 + q * 0) *
        ((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) * if 0 = 1 then 1 else 0) +
          (p - q * (C W'.a₁ * X + C W'.a₃)) * 1) -
      (q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) * 1 + (p - q * (C W'.a₁ * X + C W'.a₃)) * 0) *
        ((p * if 0 = 1 then 1 else 0) + q * 1) =
    p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ C p ^ 2 - C p * C q * (C (C W'.a₁) * C X + C (C W'.a₃)) -
        C q ^ 2 * (C X ^ 3 + C (C W'.a₂) * C X ^ 2 + C (C W'.a₄) * C X + C (C W'.a₆)) -
      (C p + C q * Y) * (C p + C q * (-Y - (C (C W'.a₁) * C X + C (C W'.a₃)))) =
    (Y ^ 2 + (C (C W'.a₁) * C X + C (C W'.a₃)) * Y -
        (C X ^ 3 + C (C W'.a₂) * C X ^ 2 + C (C W'.a₄) * C X + C (C W'.a₆))) *
      C q ^ 2

Tactic:
ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (2 * ↑n + 1) =
      complEDS b c d k ↑n ^ 2 * normEDS b c d ((↑n + 1) * k + 1) * normEDS b c d ((↑n + 1) * k - 1) -
        complEDS b c d k (↑n + 1) ^ 2 * normEDS b c d (↑n * k + 1) * normEDS b c d (↑n * k - 1)
m : ℕ
⊢ -(↑m + 1) + 1 = -↑m

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case pos
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
hp : ¬p = 0
hq : q = 0
⊢ (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree =
    max (2 • p.degree) (2 • q.degree + 3)

pp: case neg
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
hp : ¬p = 0
hq : ¬q = 0
⊢ (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree =
    max (2 • p.degree) (2 • q.degree + 3)

Tactic:
· simp only [hq, hdp, sub_zero, zero_mul, mul_zero, zero_pow two_ne_zero]
      exact (max_bot_right _).symm

Goal state after:
case neg
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
hp : ¬p = 0
hq : ¬q = 0
⊢ (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree =
    max (2 • p.degree) (2 • q.degree + 3)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (2 * ↑n + 1) =
      complEDS b c d k ↑n ^ 2 * normEDS b c d ((↑n + 1) * k + 1) * normEDS b c d ((↑n + 1) * k - 1) -
        complEDS b c d k (↑n + 1) ^ 2 * normEDS b c d (↑n * k + 1) * normEDS b c d (↑n * k - 1)
m : ℕ
⊢ -(complEDS b c d k ↑m ^ 2 * normEDS b c d ((↑m + 1) * k + 1) * normEDS b c d ((↑m + 1) * k - 1) -
        complEDS b c d k (↑m + 1) ^ 2 * normEDS b c d (↑m * k + 1) * normEDS b c d (↑m * k - 1)) =
    (-complEDS b c d k (↑m + 1)) ^ 2 * -normEDS b c d (↑m * k - 1) * -normEDS b c d (↑m * k + 1) -
      (-complEDS b c d k ↑m) ^ 2 * -normEDS b c d ((↑m + 1) * k - 1) * -normEDS b c d ((↑m + 1) * k + 1)

Tactic:
ring1

Goal state after: