mathlib-initiative/mathlib-tactics huggingface dataset:
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₂
⊢ W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) =
    W.addX x₁ x₂ (W.slope x₁ x₂ y₁ (W.negY x₂ y₂)) - (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / (x₂ - x₁) ^ 2

Tactic:
[

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) =
    W.addX x₁ x₂ (W.slope x₁ x₂ y₁ (W.negY x₂ y₂)) - (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / (x₂ - x₁) ^ 2
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₂
⊢ W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)) =
    W.addX x₁ x₂ ((y₁ - W.negY x₂ y₂) / (x₁ - x₂)) - (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / (x₂ - x₁) ^ 2

Tactic:
addX,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ ((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ =
    ((y₁ - W.negY x₂ y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - W.negY x₂ y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ -
      (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / (x₂ - x₁) ^ 2
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₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) +
      W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂) =
    0

Tactic:
[

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ y₁ * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) +
      W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

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₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span
        {XClass W x₁ * XClass W x₂, XClass W x₁ * YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)),
          YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XClass W x₂,
          YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
            YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))} *
      span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})

Tactic:
[

Goal state after:
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
⊢ span
        {XClass W x₁ * XClass W x₂, XClass W x₁ * YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)),
          YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XClass W x₂,
          YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
            YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))} *
      span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
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₂
⊢ W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) -
      W.negY (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) =
    ((y₂ - W.negY x₂ y₂) * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) -
        (y₁ - W.negY x₁ y₁) * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) /
      (x₂ - x₁)

Tactic:
[

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) -
      W.negY (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) =
    ((y₂ - W.negY x₂ y₂) * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) -
        (y₁ - W.negY x₁ y₁) * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) /
      (x₂ - x₁)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

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₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span
            {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                (mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
          span
            {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                  (mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
        span
          {XClass W x₁ * (mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
              XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
      span
        {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) * XClass W x₂ *
            XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})

Tactic:
[

Goal state after:
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
⊢ span
            {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                (mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
          span
            {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                  (mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
        span
          {XClass W x₁ * (mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
              XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
      span
        {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) * XClass W x₂ *
            XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case e'_2.e'_5
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
⊢ span {XClass W x₁} ⊔ (span {XClass W x₂} ⊔ span {(mk W) (Y - W.negPolynomial)}) = ⊤

Tactic:
[

Goal state after:
case e'_2.e'_5
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
⊢ span {XClass W x₁} ⊔ (span {XClass W x₂} ⊔ span {(mk W) (Y - W.negPolynomial)}) = ⊤
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
⊢ atom W a (-b) = atom W a b

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
⊢ atom W a (-b) = atom W a b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
⊢ atom W (2 * a) (2 * b) = W (a + b) * W (a - b)

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
⊢ atom W (2 * a) (2 * b) = W (a + b) * W (a - b)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
⊢ atom W (2 * a + 1) (2 * b + 1) = W (a + b + 1) * W (a - b)

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
⊢ atom W (2 * a + 1) (2 * b + 1) = W (a + b + 1) * W (a - b)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: 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
a b : ℤ
⊢ f (atom W a b) = atom (⇑f ∘ W) a b

Tactic:
[

Goal state after:
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
a b : ℤ
⊢ f (atom W a b) = atom (⇑f ∘ W) a b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c : ℤ
⊢ atomRel W a a b c = W a * W 0 * atom W b c

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c : ℤ
⊢ atomRel W a a b c = W a * W 0 * atom W b c
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 : ℤ
⊢ atomRel W a b a c + (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 : ℤ
⊢ atomRel W a b a c + (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: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c : ℤ
⊢ atomRel W a b c a = W a * W 0 * atom W b c

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c : ℤ
⊢ atomRel W a b c a = W a * W 0 * atom W b c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c : ℤ
⊢ atomRel W a b b c = W b * W 0 * atom W a c

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c : ℤ
⊢ atomRel W a b b c = W b * W 0 * atom W a c
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 : ℤ
⊢ atomRel W a b c b + (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 : ℤ
⊢ atomRel W a b c b + (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: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c : ℤ
⊢ atomRel W a b c c = W c * W 0 * atom W a b

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c : ℤ
⊢ atomRel W a b c c = W c * W 0 * atom W a b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W (-a) b c d = atomRel W a b c d

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W (-a) b c d = atomRel W a b c d
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W a (-b) c d = atomRel W a b c d

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W a (-b) c d = atomRel W a b c d
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W a b (-c) d = atomRel W a b c d

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W a b (-c) d = atomRel W a b c d
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
⊢ atomRel W a b c (-d) = atomRel W a b c d

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
⊢ atomRel W a b c (-d) = atomRel W a b c d
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W |a| b c d = atomRel W a b c d

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W |a| b c d = atomRel W a b c d
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W a |b| c d = atomRel W a b c d

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W a |b| c d = atomRel W a b c d
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W a b |c| d = atomRel W a b c d

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W a b |c| d = atomRel W a b c d
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
⊢ atomRel W a b c |d| = atomRel W a b c d

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
⊢ atomRel W a b c |d| = atomRel W a b c d
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
parity : d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2
⊢ atomRel W ((a + b + c + d) / 2 - d) ((a + b + c + d) / 2 - c) ((a + b + c + d) / 2 - b) ((a + b + c + d) / 2 - a) =
    atomRel W a b c d

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
parity : d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2
⊢ atomRel W ((a + b + c + d) / 2 - d) ((a + b + c + d) / 2 - c) ((a + b + c + d) / 2 - b) ((a + b + c + d) / 2 - a) =
    atomRel W a b c d
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: 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
a b c d : ℤ
⊢ f (atomRel W a b c d) = atomRel (⇑f ∘ W) a b c d

Tactic:
[

Goal state after:
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
a b c d : ℤ
⊢ f (atomRel W a b c d) = atomRel (⇑f ∘ W) a b c d
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
p q r s : ℤ
⊢ rel W p q r s = atomRel W (2 * p + s) (2 * q + s) (2 * r + s) s

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
p q r s : ℤ
⊢ rel W p q r s = atomRel W (2 * p + s) (2 * q + s) (2 * r + s) s
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
⊢ atomRel W (2 * a) (2 * b) (2 * c) (2 * d) = rel W (a - d) (b - d) (c - d) (2 * d)

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
⊢ atomRel W (2 * a) (2 * b) (2 * c) (2 * d) = rel W (a - d) (b - d) (c - d) (2 * d)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
p q r s : ℤ
⊢ rel W (-p) (-q) (-r) (-s) = rel W p q r s

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
p q r s : ℤ
⊢ rel W (-p) (-q) (-r) (-s) = rel W p q r s
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: 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
p q r s : ℤ
⊢ f (rel W p q r s) = rel (⇑f ∘ W) p q r s

Tactic:
[

Goal state after:
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
p q r s : ℤ
⊢ f (rel W p q r s) = rel (⇑f ∘ W) p q r s
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: x✝³ x✝² x✝¹ x✝ : ℤ
⊢ rel id x✝³ x✝² x✝¹ x✝ = 0

Tactic:
[

Goal state after:
x✝³ x✝² x✝¹ x✝ : ℤ
⊢ rel id x✝³ x✝² x✝¹ x✝ = 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 : ℤ
⊢ rel (x • W) p q r s + x ^ 4 * 0 - (0 + x ^ 4 * rel W p q r s) = 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 : ℤ
⊢ rel (x • W) p q r s + x ^ 4 * 0 - (0 + x ^ 4 * rel W p q r s) = 0
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat.succ.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * ↑(m + 1 + 1 + 1)) =
    preNormEDS b c d (↑(m + 1 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 2) -
      preNormEDS b c d (↑(m + 1 + 1 + 1) - 2) * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 1) ^ 2

Tactic:
[

Goal state after:
case nat.succ.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * ↑(m + 1 + 1 + 1)) =
    preNormEDS b c d (↑(m + 1 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 2) -
      preNormEDS b c d (↑(m + 1 + 1 + 1) - 2) * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 1) ^ 2
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 (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

Tactic:
[

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

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

Tactic:
[

Goal state after:
case nat.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
n✝ : ℕ
⊢ preNormEDS b c d (2 * ↑(n✝ + 1 + 1) + 1) =
    (preNormEDS b c d (↑(n✝ + 1 + 1) + 2) * preNormEDS b c d ↑(n✝ + 1 + 1) ^ 3 * if Even ↑(n✝ + 1 + 1) then b else 1) -
      preNormEDS b c d (↑(n✝ + 1 + 1) - 1) * preNormEDS b c d (↑(n✝ + 1 + 1) + 1) ^ 3 *
        if Even ↑(n✝ + 1 + 1) then 1 else b
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 (2 * -↑(m + 1) + 1) =
    (preNormEDS b c d (-↑(m + 1) + 2) * preNormEDS b c d (-↑(m + 1)) ^ 3 * if Even (-↑(m + 1)) then b else 1) -
      preNormEDS b c d (-↑(m + 1) - 1) * preNormEDS b c d (-↑(m + 1) + 1) ^ 3 * if Even (-↑(m + 1)) then 1 else b

Tactic:
[

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ complEDS₂ b c d (-k) = complEDS₂ b c d k

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ complEDS₂ b c d (-k) = complEDS₂ b c d k
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
n : ℤ
⊢ normEDS b c d (-n) = -normEDS b c d n

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
n : ℤ
⊢ normEDS b c d (-n) = -normEDS b c d n
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ normEDS b c d k * complEDS₂ b c d k = normEDS b c d (2 * k)

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ normEDS b c d k * complEDS₂ b c d k = normEDS b c d (2 * k)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ complEDS₂ b c d k * b =
    normEDS b c d (k - 1) ^ 2 * normEDS b c d (k + 2) - normEDS b c d (k - 2) * normEDS b c d (k + 1) ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ (Algebra.norm R[X]) (p • 1 + q • (mk W') Y) =
    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:
[

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ (Algebra.norm R[X]) (p • 1 + q • (mk W') Y) =
    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₆)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
[

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