mathlib-initiative/mathlib-tactics huggingface dataset:
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₁ y₁ : F
h₁ h₂ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
⊢ x₁ * (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
            (-(x₁ * (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁)) +
              (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) * (2 * y₁ + W.a₃)) -
          (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 * (y₁ * (y₁ + W.a₃) - W.a₆) +
        y₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 * (y₁ + x₁ * W.a₁ + W.a₃) -
      (-(x₁ ^ 2 *
            ((x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
                    (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁ + W.a₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃))) -
                  W.a₂ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 -
                x₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 -
              x₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2)) +
        (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 * (x₁ * (x₁ * (x₁ + W.a₂) + W.a₄) + W.a₆)) =
    0

Tactic:
;

Goal state after:
case a
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ h₂ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
⊢ x₁ * (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
            (-(x₁ * (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁)) +
              (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) * (2 * y₁ + W.a₃)) -
          (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 * (y₁ * (y₁ + W.a₃) - W.a₆) +
        y₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 * (y₁ + x₁ * W.a₁ + W.a₃) -
      (-(x₁ ^ 2 *
            ((x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
                    (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁ + W.a₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃))) -
                  W.a₂ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 -
                x₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 -
              x₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2)) +
        (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) ^ 2 * (x₁ * (x₁ * (x₁ + W.a₂) + W.a₄) + W.a₆)) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
a✝ : Nontrivial R
⊢ FaithfulSMul R[X] W'.CoordinateRing

Tactic:
;

Goal state after:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
a✝ : Nontrivial R
⊢ FaithfulSMul R[X] W'.CoordinateRing
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:
;

Goal state after:
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
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x : R
⊢ 0 < 2

Tactic:
;

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x : R
⊢ 0 < 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
y : R[X]
⊢ 1 < 2

Tactic:
;

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
y : R[X]
⊢ 1 < 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
x : R
y : R[X]
h : eval x (eval y W'.polynomial) = 0
⊢ Ideal.map (mk W') (span {C (X - C x), Y - C y}) =
    Ideal.map (Quotient.mkₐ R (span {W'.polynomial})) (span {C (X - C x), Y - C y})

Tactic:
;

Goal state after:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
x : R
y : R[X]
h : eval x (eval y W'.polynomial) = 0
⊢ Ideal.map (mk W') (span {C (X - C x), Y - C y}) =
    Ideal.map (Quotient.mkₐ R (span {W'.polynomial})) (span {C (X - C x), Y - C y})
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 - W.a₁ * x - W.a₃))) -
          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) +
        C (C (y ^ 2 + W.a₁ * x * y + 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 +
        C (C (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆))) =
    0

Tactic:
;

Goal state after:
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 - W.a₁ * x - W.a₃))) -
          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) +
        C (C (y ^ 2 + W.a₁ * x * y + 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 +
        C (C (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆))) =
    0
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:
;

Goal state after:
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
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ XYIdeal W x (C (W.negY x y)) * XYIdeal W x (C y) = XIdeal W x

Tactic:
have 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 := by
    linear_combination (norm := (rw [negY, polynomial]; C_simp; ring1))
      congr_arg C (congr_arg C ((equation_iff ..).mp h.left).symm)
  simp_rw [XYIdeal, XClass, YClass, span_pair_mul_span_pair, mul_comm, ← map_mul,
    AdjoinRoot.mk_eq_mk.mpr ⟨1, Y_rw⟩, map_mul, span_insert, ← span_singleton_mul_span_singleton,
    ← Ideal.mul_sup, ← span_insert]
  convert! mul_top (_ : Ideal W.CoordinateRing) using 2
  on_goal 2 => infer_instance
  simp_rw [← Set.image_singleton (f := mk W), ← Set.image_insert_eq, ← map_span]
  convert! map_top (R := F[X][Y]) (mk W) using 1
  apply congr_arg
  simp_rw [eq_top_iff_one, mem_span_insert', mem_span_singleton']
  rcases ((nonsingular_iff' ..).mp h).right with hx | hy
  · let W_X := W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)
    refine
      ⟨C <| C W_X⁻¹ * -(X + C (2 * x + W.a₂)), C <| C <| W_X⁻¹ * W.a₁, 0, C <| C <| W_X⁻¹ * -1, ?_⟩
    rw [← mul_right_inj' <| C_ne_zero.mpr <| C_ne_zero.mpr hx]
    simp only [W_X, mul_add, ← mul_assoc, ← C_mul, mul_inv_cancel₀ hx]
    C_simp
    ring1
  · let W_Y := 2 * y + W.a₁ * x + W.a₃
    refine ⟨0, C <| C W_Y⁻¹, C <| C <| W_Y⁻¹ * -1, 0, ?_⟩
    rw [negY, ← mul_right_inj' <| C_ne_zero.mpr <| C_ne_zero.mpr hy]
    simp only [W_Y, mul_add, ← mul_assoc, ← C_mul, mul_inv_cancel₀ hy]
    C_simp
    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:
;

Goal state after:
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
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:
;

Goal state after:
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
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:
;

Goal state after:
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
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:
;

Goal state after:
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
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_1
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofiltered I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : ReflectsFilteredColimits (forget CommRingCat)
⊢ ∀ (x : ((forget CommRingCat).mapCocone (Scheme.Γ.mapCocone c.op)).pt),
    ∃ i xi, x = (ConcreteCategory.hom (((forget CommRingCat).mapCocone (Scheme.Γ.mapCocone c.op)).ι.app i)) xi

Tactic:
exact fun s ↦ ⟨.op _, (exists_appTop_π_eq_of_isLimit D c hc s).choose_spec⟩

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
⊢ C (C 1) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) +
        -4 * C (C (x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆)) -
      (C (C ((y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2)) * 1 +
              C (C (1 * 4)) * (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₆)) +
            C
              ((C (1 * 4) * X ^ 2 + C (1 * 4 * x₁ + 1 * (W.a₁ ^ 2 + 4 * W.a₂)) * X +
                  C (1 * 4 * x₁ ^ 2 + 1 * (W.a₁ ^ 2 + 4 * W.a₂) * x₁ + 1 * 2 * (2 * W.a₄ + W.a₁ * W.a₃))) *
                (X - C x₁)) +
          C (C ((y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2)) * 0 * C (X - C x₁) +
        -4 * C (C (y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁))) =
    0

Tactic:
;

Goal state after:
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
⊢ C (C 1) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) +
        -4 * C (C (x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆)) -
      (C (C ((y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2)) * 1 +
              C (C (1 * 4)) * (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₆)) +
            C
              ((C (1 * 4) * X ^ 2 + C (1 * 4 * x₁ + 1 * (W.a₁ ^ 2 + 4 * W.a₂)) * X +
                  C (1 * 4 * x₁ ^ 2 + 1 * (W.a₁ ^ 2 + 4 * W.a₂) * x₁ + 1 * 2 * (2 * W.a₄ + W.a₁ * W.a₃))) *
                (X - C x₁)) +
          C (C ((y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2)) * 0 * C (X - C x₁) +
        -4 * C (C (y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁))) =
    0
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:
;

Goal state after:
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
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:
;

Goal state after:
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
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:
;

Goal state after:
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
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case bc
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
n : ℕ
m : ℕ := ⋯
hn : ¬Even n
⊢ m < n

Tactic:
;

Goal state after:
case bc
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
n : ℕ
m : ℕ := ⋯
hn : ¬Even n
⊢ m < n
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) *
      b =
    (preNormEDS (b ^ 4) c d (k - 1) * if Even (k - 1) then b else 1) ^ 2 *
        (preNormEDS (b ^ 4) c d (k + 2) * if Even k ↔ Even 2 then b else 1) -
      (preNormEDS (b ^ 4) c d (k - 2) * if Even (k - 2) then b else 1) *
        (preNormEDS (b ^ 4) c d (k + 1) * if Even k ↔ Even 1 then b else 1) ^ 2

Tactic:
Int.even_sub,

Goal state after:
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) *
      b =
    (preNormEDS (b ^ 4) c d (k - 1) * if Even k ↔ Even 1 then b else 1) ^ 2 *
        (preNormEDS (b ^ 4) c d (k + 2) * if Even k ↔ Even 2 then b else 1) -
      (preNormEDS (b ^ 4) c d (k - 2) * if Even k ↔ Even 2 then b else 1) *
        (preNormEDS (b ^ 4) c d (k + 1) * if Even k ↔ Even 1 then b else 1) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
Int.even_sub,

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