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

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * s ^ 2 +
              C (2 * W.b₂ * W.b₄ * W.b₈ - 2 * W.b₄ ^ 2 * W.b₆ - 10 * W.b₆ * W.b₈) * s * t +
            C (-(W.b₂ * W.b₆ * W.b₈) + W.b₄ * W.b₆ ^ 2) * s * u +
          C (3 * W.b₄ ^ 2 * W.b₈ - 3 * W.b₄ * W.b₆ ^ 2) * t ^ 2 +
        C (3 * W.b₄ * W.b₆ * W.b₈ - 3 * W.b₆ ^ 3) * t * u).IsHomogeneous
    2

pp: case «1»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(W.b₂ * W.b₄ * W.b₈) + W.b₄ ^ 2 * W.b₆ + 5 * W.b₆ * W.b₈) * s ^ 2 +
              C (2 * W.b₂ * W.b₆ * W.b₈ - 2 * W.b₄ * W.b₆ ^ 2 - 10 * W.b₈ ^ 2) * s * t +
            C (-(W.b₂ * W.b₈ ^ 2) + W.b₄ * W.b₆ * W.b₈) * s * u +
          C (3 * W.b₄ * W.b₆ * W.b₈ - 3 * W.b₆ ^ 3) * t ^ 2 +
        C (3 * W.b₄ * W.b₈ ^ 2 - 3 * W.b₆ ^ 2 * W.b₈) * t * u).IsHomogeneous
    2

pp: case «2»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (W.b₂ * W.b₆ * W.b₈ - 8 * W.b₄ ^ 2 * W.b₈ + 7 * W.b₄ * W.b₆ ^ 2) * s ^ 2 +
          C (-(6 * W.b₄ * W.b₆ * W.b₈) + 6 * W.b₆ ^ 3) * s * t +
        C (-(8 * W.b₄ * W.b₈ ^ 2) + 8 * W.b₆ ^ 2 * W.b₈) * s * u).IsHomogeneous
    2

pp: case «3»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (96 * W.b₆) * s * t + C (12 * W.b₂ * W.b₆ - 64 * W.b₈) * t ^ 2 + C (16 * W.b₄ * W.b₆) * t * u).IsHomogeneous 2

pp: case «4»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(48 * W.b₆)) * s ^ 2 + C (32 * W.b₈) * s * t + C (-(4 * W.b₂ * W.b₈) + 16 * W.b₄ * W.b₆) * t ^ 2 +
        C (16 * W.b₄ * W.b₈) * t * u).IsHomogeneous
    2

pp: case «5»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(12 * W.b₂ * W.b₆)) * s ^ 2 + C (8 * W.b₂ * W.b₈ - 32 * W.b₄ * W.b₆) * s * t + C (-(12 * W.b₆ ^ 2)) * s * u +
          C (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * t ^ 2 +
        C (4 * W.b₂ * W.b₄ * W.b₈ - 4 * W.b₂ * W.b₆ ^ 2) * t * u).IsHomogeneous
    2

pp: case «6»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-12) * t ^ 2 + C (-(4 * W.b₂)) * t * u + C (W.b₂ ^ 2 - 32 * W.b₄) * u ^ 2).IsHomogeneous 2

pp: case «7»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 6 * s * t + C (-W.b₂) * s * u + C (-(5 * W.b₄)) * t * u + C (W.b₂ * W.b₄ - 27 * W.b₆) * u ^ 2).IsHomogeneous 2

pp: case «8»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(8 * W.b₄)) * s * u + C (-(12 * W.b₆)) * t * u + C (W.b₄ ^ 2 - 28 * W.b₈) * u ^ 2).IsHomogeneous 2

Tactic:
·

Goal state after:
case «0»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * s ^ 2 +
              C (2 * W.b₂ * W.b₄ * W.b₈ - 2 * W.b₄ ^ 2 * W.b₆ - 10 * W.b₆ * W.b₈) * s * t +
            C (-(W.b₂ * W.b₆ * W.b₈) + W.b₄ * W.b₆ ^ 2) * s * u +
          C (3 * W.b₄ ^ 2 * W.b₈ - 3 * W.b₄ * W.b₆ ^ 2) * t ^ 2 +
        C (3 * W.b₄ * W.b₆ * W.b₈ - 3 * W.b₆ ^ 3) * t * u).IsHomogeneous
    2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(W.b₂ * W.b₄ * W.b₈) + W.b₄ ^ 2 * W.b₆ + 5 * W.b₆ * W.b₈) * s ^ 2 +
              C (2 * W.b₂ * W.b₆ * W.b₈ - 2 * W.b₄ * W.b₆ ^ 2 - 10 * W.b₈ ^ 2) * s * t +
            C (-(W.b₂ * W.b₈ ^ 2) + W.b₄ * W.b₆ * W.b₈) * s * u +
          C (3 * W.b₄ * W.b₆ * W.b₈ - 3 * W.b₆ ^ 3) * t ^ 2 +
        C (3 * W.b₄ * W.b₈ ^ 2 - 3 * W.b₆ ^ 2 * W.b₈) * t * u).IsHomogeneous
    2

pp: case «2»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (W.b₂ * W.b₆ * W.b₈ - 8 * W.b₄ ^ 2 * W.b₈ + 7 * W.b₄ * W.b₆ ^ 2) * s ^ 2 +
          C (-(6 * W.b₄ * W.b₆ * W.b₈) + 6 * W.b₆ ^ 3) * s * t +
        C (-(8 * W.b₄ * W.b₈ ^ 2) + 8 * W.b₆ ^ 2 * W.b₈) * s * u).IsHomogeneous
    2

pp: case «3»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (96 * W.b₆) * s * t + C (12 * W.b₂ * W.b₆ - 64 * W.b₈) * t ^ 2 + C (16 * W.b₄ * W.b₆) * t * u).IsHomogeneous 2

pp: case «4»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(48 * W.b₆)) * s ^ 2 + C (32 * W.b₈) * s * t + C (-(4 * W.b₂ * W.b₈) + 16 * W.b₄ * W.b₆) * t ^ 2 +
        C (16 * W.b₄ * W.b₈) * t * u).IsHomogeneous
    2

pp: case «5»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(12 * W.b₂ * W.b₆)) * s ^ 2 + C (8 * W.b₂ * W.b₈ - 32 * W.b₄ * W.b₆) * s * t + C (-(12 * W.b₆ ^ 2)) * s * u +
          C (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * t ^ 2 +
        C (4 * W.b₂ * W.b₄ * W.b₈ - 4 * W.b₂ * W.b₆ ^ 2) * t * u).IsHomogeneous
    2

pp: case «6»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-12) * t ^ 2 + C (-(4 * W.b₂)) * t * u + C (W.b₂ ^ 2 - 32 * W.b₄) * u ^ 2).IsHomogeneous 2

pp: case «7»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 6 * s * t + C (-W.b₂) * s * u + C (-(5 * W.b₄)) * t * u + C (W.b₂ * W.b₄ - 27 * W.b₆) * u ^ 2).IsHomogeneous 2

pp: case «8»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(8 * W.b₄)) * s * u + C (-(12 * W.b₆)) * t * u + C (W.b₄ ^ 2 - 28 * W.b₈) * u ^ 2).IsHomogeneous 2

Tactic:
·

Goal state after:
case «1»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(W.b₂ * W.b₄ * W.b₈) + W.b₄ ^ 2 * W.b₆ + 5 * W.b₆ * W.b₈) * s ^ 2 +
              C (2 * W.b₂ * W.b₆ * W.b₈ - 2 * W.b₄ * W.b₆ ^ 2 - 10 * W.b₈ ^ 2) * s * t +
            C (-(W.b₂ * W.b₈ ^ 2) + W.b₄ * W.b₆ * W.b₈) * s * u +
          C (3 * W.b₄ * W.b₆ * W.b₈ - 3 * W.b₆ ^ 3) * t ^ 2 +
        C (3 * W.b₄ * W.b₈ ^ 2 - 3 * W.b₆ ^ 2 * W.b₈) * t * u).IsHomogeneous
    2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case «2»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (W.b₂ * W.b₆ * W.b₈ - 8 * W.b₄ ^ 2 * W.b₈ + 7 * W.b₄ * W.b₆ ^ 2) * s ^ 2 +
          C (-(6 * W.b₄ * W.b₆ * W.b₈) + 6 * W.b₆ ^ 3) * s * t +
        C (-(8 * W.b₄ * W.b₈ ^ 2) + 8 * W.b₆ ^ 2 * W.b₈) * s * u).IsHomogeneous
    2

pp: case «3»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (96 * W.b₆) * s * t + C (12 * W.b₂ * W.b₆ - 64 * W.b₈) * t ^ 2 + C (16 * W.b₄ * W.b₆) * t * u).IsHomogeneous 2

pp: case «4»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(48 * W.b₆)) * s ^ 2 + C (32 * W.b₈) * s * t + C (-(4 * W.b₂ * W.b₈) + 16 * W.b₄ * W.b₆) * t ^ 2 +
        C (16 * W.b₄ * W.b₈) * t * u).IsHomogeneous
    2

pp: case «5»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(12 * W.b₂ * W.b₆)) * s ^ 2 + C (8 * W.b₂ * W.b₈ - 32 * W.b₄ * W.b₆) * s * t + C (-(12 * W.b₆ ^ 2)) * s * u +
          C (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * t ^ 2 +
        C (4 * W.b₂ * W.b₄ * W.b₈ - 4 * W.b₂ * W.b₆ ^ 2) * t * u).IsHomogeneous
    2

pp: case «6»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-12) * t ^ 2 + C (-(4 * W.b₂)) * t * u + C (W.b₂ ^ 2 - 32 * W.b₄) * u ^ 2).IsHomogeneous 2

pp: case «7»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 6 * s * t + C (-W.b₂) * s * u + C (-(5 * W.b₄)) * t * u + C (W.b₂ * W.b₄ - 27 * W.b₆) * u ^ 2).IsHomogeneous 2

pp: case «8»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(8 * W.b₄)) * s * u + C (-(12 * W.b₆)) * t * u + C (W.b₄ ^ 2 - 28 * W.b₈) * u ^ 2).IsHomogeneous 2

Tactic:
·

Goal state after:
case «2»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (W.b₂ * W.b₆ * W.b₈ - 8 * W.b₄ ^ 2 * W.b₈ + 7 * W.b₄ * W.b₆ ^ 2) * s ^ 2 +
          C (-(6 * W.b₄ * W.b₆ * W.b₈) + 6 * W.b₆ ^ 3) * s * t +
        C (-(8 * W.b₄ * W.b₈ ^ 2) + 8 * W.b₆ ^ 2 * W.b₈) * s * u).IsHomogeneous
    2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case «3»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (96 * W.b₆) * s * t + C (12 * W.b₂ * W.b₆ - 64 * W.b₈) * t ^ 2 + C (16 * W.b₄ * W.b₆) * t * u).IsHomogeneous 2

pp: case «4»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(48 * W.b₆)) * s ^ 2 + C (32 * W.b₈) * s * t + C (-(4 * W.b₂ * W.b₈) + 16 * W.b₄ * W.b₆) * t ^ 2 +
        C (16 * W.b₄ * W.b₈) * t * u).IsHomogeneous
    2

pp: case «5»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(12 * W.b₂ * W.b₆)) * s ^ 2 + C (8 * W.b₂ * W.b₈ - 32 * W.b₄ * W.b₆) * s * t + C (-(12 * W.b₆ ^ 2)) * s * u +
          C (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * t ^ 2 +
        C (4 * W.b₂ * W.b₄ * W.b₈ - 4 * W.b₂ * W.b₆ ^ 2) * t * u).IsHomogeneous
    2

pp: case «6»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-12) * t ^ 2 + C (-(4 * W.b₂)) * t * u + C (W.b₂ ^ 2 - 32 * W.b₄) * u ^ 2).IsHomogeneous 2

pp: case «7»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 6 * s * t + C (-W.b₂) * s * u + C (-(5 * W.b₄)) * t * u + C (W.b₂ * W.b₄ - 27 * W.b₆) * u ^ 2).IsHomogeneous 2

pp: case «8»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(8 * W.b₄)) * s * u + C (-(12 * W.b₆)) * t * u + C (W.b₄ ^ 2 - 28 * W.b₈) * u ^ 2).IsHomogeneous 2

Tactic:
·

Goal state after:
case «3»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (96 * W.b₆) * s * t + C (12 * W.b₂ * W.b₆ - 64 * W.b₈) * t ^ 2 + C (16 * W.b₄ * W.b₆) * t * u).IsHomogeneous 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case «4»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(48 * W.b₆)) * s ^ 2 + C (32 * W.b₈) * s * t + C (-(4 * W.b₂ * W.b₈) + 16 * W.b₄ * W.b₆) * t ^ 2 +
        C (16 * W.b₄ * W.b₈) * t * u).IsHomogeneous
    2

pp: case «5»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(12 * W.b₂ * W.b₆)) * s ^ 2 + C (8 * W.b₂ * W.b₈ - 32 * W.b₄ * W.b₆) * s * t + C (-(12 * W.b₆ ^ 2)) * s * u +
          C (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * t ^ 2 +
        C (4 * W.b₂ * W.b₄ * W.b₈ - 4 * W.b₂ * W.b₆ ^ 2) * t * u).IsHomogeneous
    2

pp: case «6»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-12) * t ^ 2 + C (-(4 * W.b₂)) * t * u + C (W.b₂ ^ 2 - 32 * W.b₄) * u ^ 2).IsHomogeneous 2

pp: case «7»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 6 * s * t + C (-W.b₂) * s * u + C (-(5 * W.b₄)) * t * u + C (W.b₂ * W.b₄ - 27 * W.b₆) * u ^ 2).IsHomogeneous 2

pp: case «8»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(8 * W.b₄)) * s * u + C (-(12 * W.b₆)) * t * u + C (W.b₄ ^ 2 - 28 * W.b₈) * u ^ 2).IsHomogeneous 2

Tactic:
·

Goal state after:
case «4»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(48 * W.b₆)) * s ^ 2 + C (32 * W.b₈) * s * t + C (-(4 * W.b₂ * W.b₈) + 16 * W.b₄ * W.b₆) * t ^ 2 +
        C (16 * W.b₄ * W.b₈) * t * u).IsHomogeneous
    2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n : ℕ
hn : n = 0
⊢ complEDS b c d k ↑n = complEDS' b c d k n

pp: case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n : ℕ
hn : ¬n = 0
⊢ complEDS b c d k ↑n = complEDS' b c d k n

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n : ℕ
hn : n = 0
⊢ complEDS b c d k ↑n = complEDS' b c d k n
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n : ℕ
hn : ¬n = 0
⊢ complEDS b c d k ↑n = complEDS' b c d k n

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n : ℕ
hn : ¬n = 0
⊢ complEDS b c d k ↑n = complEDS' b c d k n
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case «5»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(12 * W.b₂ * W.b₆)) * s ^ 2 + C (8 * W.b₂ * W.b₈ - 32 * W.b₄ * W.b₆) * s * t + C (-(12 * W.b₆ ^ 2)) * s * u +
          C (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * t ^ 2 +
        C (4 * W.b₂ * W.b₄ * W.b₈ - 4 * W.b₂ * W.b₆ ^ 2) * t * u).IsHomogeneous
    2

pp: case «6»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-12) * t ^ 2 + C (-(4 * W.b₂)) * t * u + C (W.b₂ ^ 2 - 32 * W.b₄) * u ^ 2).IsHomogeneous 2

pp: case «7»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 6 * s * t + C (-W.b₂) * s * u + C (-(5 * W.b₄)) * t * u + C (W.b₂ * W.b₄ - 27 * W.b₆) * u ^ 2).IsHomogeneous 2

pp: case «8»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(8 * W.b₄)) * s * u + C (-(12 * W.b₆)) * t * u + C (W.b₄ ^ 2 - 28 * W.b₈) * u ^ 2).IsHomogeneous 2

Tactic:
·

Goal state after:
case «5»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(12 * W.b₂ * W.b₆)) * s ^ 2 + C (8 * W.b₂ * W.b₈ - 32 * W.b₄ * W.b₆) * s * t + C (-(12 * W.b₆ ^ 2)) * s * u +
          C (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * t ^ 2 +
        C (4 * W.b₂ * W.b₄ * W.b₈ - 4 * W.b₂ * W.b₆ ^ 2) * t * u).IsHomogeneous
    2
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
⊢ (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
⊢ (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:
·

Goal state after:
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
⊢ (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 nat.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ complEDS b c d k (2 * ↑0) = complEDS b c d k ↑0 * complEDS₂ b c d (↑0 * k)

pp: case nat.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n✝ : ℕ
⊢ complEDS b c d k (2 * ↑(n✝ + 1)) = complEDS b c d k ↑(n✝ + 1) * complEDS₂ b c d (↑(n✝ + 1) * k)

Tactic:
·

Goal state after:
case nat.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ complEDS b c d k (2 * ↑0) = complEDS b c d k ↑0 * complEDS₂ b c d (↑0 * k)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case «6»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-12) * t ^ 2 + C (-(4 * W.b₂)) * t * u + C (W.b₂ ^ 2 - 32 * W.b₄) * u ^ 2).IsHomogeneous 2

pp: case «7»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 6 * s * t + C (-W.b₂) * s * u + C (-(5 * W.b₄)) * t * u + C (W.b₂ * W.b₄ - 27 * W.b₆) * u ^ 2).IsHomogeneous 2

pp: case «8»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(8 * W.b₄)) * s * u + C (-(12 * W.b₆)) * t * u + C (W.b₄ ^ 2 - 28 * W.b₈) * u ^ 2).IsHomogeneous 2

Tactic:
·

Goal state after:
case «6»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-12) * t ^ 2 + C (-(4 * W.b₂)) * t * u + C (W.b₂ ^ 2 - 32 * W.b₄) * u ^ 2).IsHomogeneous 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

pp: case nat.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n✝ : ℕ
⊢ complEDS b c d k (2 * ↑(n✝ + 1) + 1) =
    complEDS b c d k ↑(n✝ + 1) ^ 2 * normEDS b c d ((↑(n✝ + 1) + 1) * k + 1) * normEDS b c d ((↑(n✝ + 1) + 1) * k - 1) -
      complEDS b c d k (↑(n✝ + 1) + 1) ^ 2 * normEDS b c d (↑(n✝ + 1) * k + 1) * normEDS b c d (↑(n✝ + 1) * k - 1)

Tactic:
·

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

Goal state before:
pp: case «7»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 6 * s * t + C (-W.b₂) * s * u + C (-(5 * W.b₄)) * t * u + C (W.b₂ * W.b₄ - 27 * W.b₆) * u ^ 2).IsHomogeneous 2

pp: case «8»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(8 * W.b₄)) * s * u + C (-(12 * W.b₆)) * t * u + C (W.b₄ ^ 2 - 28 * W.b₈) * u ^ 2).IsHomogeneous 2

Tactic:
·

Goal state after:
case «7»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 6 * s * t + C (-W.b₂) * s * u + C (-(5 * W.b₄)) * t * u + C (W.b₂ * W.b₄ - 27 * W.b₆) * u ^ 2).IsHomogeneous 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
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
⊢ (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:
·

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
⊢ (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.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case «8»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(8 * W.b₄)) * s * u + C (-(12 * W.b₆)) * t * u + C (W.b₄ ^ 2 - 28 * W.b₈) * u ^ 2).IsHomogeneous 2

Tactic:
·

Goal state after:
case «8»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(8 * W.b₄)) * s * u + C (-(12 * W.b₆)) * t * u + C (W.b₄ ^ 2 - 28 * W.b₈) * u ^ 2).IsHomogeneous 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg.zero
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)
⊢ complEDS b c d k (2 * -↑0 + 1) =
    complEDS b c d k (-↑0) ^ 2 * normEDS b c d ((-↑0 + 1) * k + 1) * normEDS b c d ((-↑0 + 1) * k - 1) -
      complEDS b c d k (-↑0 + 1) ^ 2 * normEDS b c d (-↑0 * k + 1) * normEDS b c d (-↑0 * k - 1)

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 (2 * -↑(m + 1) + 1) =
    complEDS b c d k (-↑(m + 1)) ^ 2 * normEDS b c d ((-↑(m + 1) + 1) * k + 1) *
        normEDS b c d ((-↑(m + 1) + 1) * k - 1) -
      complEDS b c d k (-↑(m + 1) + 1) ^ 2 * normEDS b c d (-↑(m + 1) * k + 1) * normEDS b c d (-↑(m + 1) * k - 1)

Tactic:
·

Goal state after:
case neg.zero
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)
⊢ complEDS b c d k (2 * -↑0 + 1) =
    complEDS b c d k (-↑0) ^ 2 * normEDS b c d ((-↑0 + 1) * k + 1) * normEDS b c d ((-↑0 + 1) * k - 1) -
      complEDS b c d k (-↑0 + 1) ^ 2 * normEDS b c d (-↑0 * k + 1) * normEDS b c d (-↑0 * k - 1)
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:
·

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

Goal state before:
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:
·

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)