awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
rw :
  Eq (α := ClassGroup W.CoordinateRing)
    ((ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (XYIdeal' h₁ * XYIdeal' h₂) :
      ClassGroup W.CoordinateRing)
    ((ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (XYIdeal' (x := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) ⋯) :
      ClassGroup W.CoordinateRing)
⊢ HMul.hMul (α := ClassGroup W.CoordinateRing) (β := ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (XYIdeal' h₁) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (XYIdeal' h₂) :
        ClassGroup W.CoordinateRing) =
    (ClassGroup.mk W.FunctionField :
        (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
      (XYIdeal' (x := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) ⋯)

Tactic:
rw [← map_mul]

Premises used: map_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ Eq (α := ClassGroup W.CoordinateRing)
    ((ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (XYIdeal' h₁ * XYIdeal' h₂) :
      ClassGroup W.CoordinateRing)
    ((ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (XYIdeal' (x := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) ⋯) :
      ClassGroup W.CoordinateRing)

Tactic:
(ClassGroup.mk_eq_mk_of_coe_ideal (coeIdeal_mul ..).symm <| XYIdeal'_eq _).mpr
    ⟨_, _, XClass_ne_zero _, YClass_ne_zero _, XYIdeal_mul_XYIdeal h₁.left h₂.left hxy⟩

Premises used: Iff.mpr, ClassGroup.mk_eq_mk_of_coe_ideal, WeierstrassCurve.Affine.CoordinateRing.YClass_ne_zero, And.left, WeierstrassCurve.Affine.CoordinateRing.XClass_ne_zero, And.intro, Exists.intro, WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ Eq (α := ClassGroup W.CoordinateRing)
    ((ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (XYIdeal' h₁ * XYIdeal' h₂) :
      ClassGroup W.CoordinateRing)
    ((ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (XYIdeal' (x := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) ⋯) :
      ClassGroup W.CoordinateRing)

Tactic:
exact (ClassGroup.mk_eq_mk_of_coe_ideal (coeIdeal_mul ..).symm <| XYIdeal'_eq _).mpr
    ⟨_, _, XClass_ne_zero _, YClass_ne_zero _, XYIdeal_mul_XYIdeal h₁.left h₂.left hxy⟩

Premises used: Iff.mpr, ClassGroup.mk_eq_mk_of_coe_ideal, WeierstrassCurve.Affine.CoordinateRing.YClass_ne_zero, And.left, WeierstrassCurve.Affine.CoordinateRing.XClass_ne_zero, And.intro, Exists.intro, WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p q : R[X]
⊢ (p * 1 + q * 0) *
        ((q *
              HAdd.hAdd (β := R[X])
                (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
                ((C : (a : R) → R[X]) W'.a₆ : R[X]) *
            if Eq (α := Fin 2) 0 1 then 1 else 0) +
          (p -
              q *
                HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
                  ((C : (a : R) → R[X]) W'.a₃ : R[X])) *
            1) -
      (q *
              HAdd.hAdd (β := R[X])
                (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
                ((C : (a : R) → R[X]) W'.a₆ : R[X]) *
            1 +
          (p -
              q *
                HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
                  ((C : (a : R) → R[X]) W'.a₃ : R[X])) *
            0) *
        ((p * if Eq (α := Fin 2) 0 1 then 1 else 0) + q * 1) =
    HPow.hPow (β := ℕ) p 2 -
        p * q *
          HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
            ((C : (a : R) → R[X]) W'.a₃ : R[X]) -
      HPow.hPow (β := ℕ) q 2 *
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p q : R[X]
⊢ HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) p : R[X][Y]) 2 -
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) p : R[X][Y])
              ((C : (a : R[X]) → R[X][Y]) q : R[X][Y]) *
            HAdd.hAdd (β := R[X][Y])
              (HMul.hMul (α := R[X][Y]) (β := R[X][Y])
                ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₁) : R[X][Y])
                ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
              ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₃) : R[X][Y]) -
        HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) q : R[X][Y]) 2 *
          HAdd.hAdd (β := R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 3 +
                HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₂) : R[X][Y])
                  (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 2) +
              HMul.hMul (α := R[X][Y]) (β := R[X][Y])
                ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₄) : R[X][Y])
                ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
            ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₆) : R[X][Y]) -
      HAdd.hAdd (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) p : R[X][Y])
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) q : R[X][Y]) Y) *
        HAdd.hAdd (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) p : R[X][Y])
          (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) q : R[X][Y])
            (-Y -
              HAdd.hAdd (β := R[X][Y])
                (HMul.hMul (α := R[X][Y]) (β := R[X][Y])
                  ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₁) : R[X][Y])
                  ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
                ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₃) : R[X][Y]))) =
    (HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
          HAdd.hAdd (β := R[X][Y])
              (HMul.hMul (α := R[X][Y]) (β := R[X][Y])
                ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₁) : R[X][Y])
                ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
              ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₃) : R[X][Y]) *
            Y -
        HAdd.hAdd (β := R[X][Y])
          (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 3 +
              HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₂) : R[X][Y])
                (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) 2) +
            HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₄) : R[X][Y])
              ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
          ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₆) : R[X][Y])) *
      HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) q : R[X][Y]) 2

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
⊢ (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 p.degree

Tactic:
have hdp : (p ^ 2).degree = 2 • p.degree := degree_pow p 2
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 p.degree
grw :
  (p * q).degree +
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₃ : R[X])).degree ≤
    p.degree + q.degree + 1
grw₁ :
  p.degree + q.degree +
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₃ : R[X])).degree ≤
    p.degree + q.degree + 1
grw₂ grw₃ : p.degree + q.degree + 1 ≤ p.degree + q.degree + 1
⊢ (p * q *
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₃ : R[X])).degree ≤
    p.degree + q.degree + 1

Tactic:
grw [degree_mul, degree_mul, degree_linear_le]

Premises used: Polynomial.degree_linear_le, Polynomial.degree_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 p.degree
⊢ (p * q *
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₃ : R[X])).degree ≤
    p.degree + q.degree + 1

Tactic:
have hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1 := by
    grw [degree_mul, degree_mul, degree_linear_le]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 p.degree
hdpq :
  (p * q *
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₃ : R[X])).degree ≤
    p.degree + q.degree + 1
rw :
  (HPow.hPow (β := ℕ) q 2).degree +
      (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
    HSMul.hSMul (α := ℕ) 2 q.degree + 3
rw₁ :
  HSMul.hSMul (α := ℕ) 2 q.degree +
      (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
    HSMul.hSMul (α := ℕ) 2 q.degree + 3
rw₂ :
  HSMul.hSMul (α := ℕ) 2 q.degree +
      (HAdd.hAdd (β := R[X])
          (1 * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
    HSMul.hSMul (α := ℕ) 2 q.degree + 3
rw₃ :
  HSMul.hSMul (α := ℕ) 2 q.degree +
      (HAdd.hAdd (β := R[X])
          ((C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
    HSMul.hSMul (α := ℕ) 2 q.degree + 3
rw₄ rw₅ : HSMul.hSMul (α := ℕ) 2 q.degree + 3 = HSMul.hSMul (α := ℕ) 2 q.degree + 3
⊢ (HPow.hPow (β := ℕ) q 2 *
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
    HSMul.hSMul (α := ℕ) 2 q.degree + 3

Tactic:
rw [degree_mul, degree_pow, ← one_mul <| X ^ 3, ← C_1, degree_cubic <| one_ne_zero' R]

Premises used: Polynomial.C_1, Polynomial.degree_pow, one_ne_zero', Polynomial.degree_cubic, Polynomial.X, one_mul, Polynomial.degree_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 p.degree
hdpq :
  (p * q *
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₃ : R[X])).degree ≤
    p.degree + q.degree + 1
⊢ (HPow.hPow (β := ℕ) q 2 *
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
    HSMul.hSMul (α := ℕ) 2 q.degree + 3

Tactic:
have hdq :
      (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3 := by
    rw [degree_mul, degree_pow, ← one_mul <| X ^ 3, ← C_1, degree_cubic <| one_ne_zero' R]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 p.degree
hdpq :
  (p * q *
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₃ : R[X])).degree ≤
    p.degree + q.degree + 1
hdq :
  (HPow.hPow (β := ℕ) q 2 *
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
    HSMul.hSMul (α := ℕ) 2 q.degree + 3
rw :
  (HPow.hPow (β := ℕ) p 2 -
          p * q *
            HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
              ((C : (a : R) → R[X]) W'.a₃ : R[X]) -
        HPow.hPow (β := ℕ) q 2 *
          HAdd.hAdd (β := R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
            ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
    max (HSMul.hSMul (α := ℕ) 2 p.degree) (HSMul.hSMul (α := ℕ) 2 q.degree + 3)
⊢ degree.{r} (R := R)
      ((Algebra.norm R[X] : (a : W'.CoordinateRing) → R[X])
        (HSMul.hSMul (β := W'.CoordinateRing) p 1 +
          HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y))) =
    max (HSMul.hSMul (α := ℕ) 2 p.degree) (HSMul.hSMul (α := ℕ) 2 q.degree + 3)

Tactic:
rw [norm_smul_basis]

Premises used: WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 p.degree
hdpq :
  (p * q *
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₃ : R[X])).degree ≤
    p.degree + q.degree + 1
hdq :
  (HPow.hPow (β := ℕ) q 2 *
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
    HSMul.hSMul (α := ℕ) 2 q.degree + 3
pos :
  ∀ (hp : p = 0),
    (HPow.hPow (β := ℕ) p 2 -
            p * q *
              HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
                ((C : (a : R) → R[X]) W'.a₃ : R[X]) -
          HPow.hPow (β := ℕ) q 2 *
            HAdd.hAdd (β := R[X])
              (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
              ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
      max (HSMul.hSMul (α := ℕ) 2 p.degree) (HSMul.hSMul (α := ℕ) 2 q.degree + 3)
neg :
  ∀ (hp : ¬p = 0),
    (HPow.hPow (β := ℕ) p 2 -
            p * q *
              HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
                ((C : (a : R) → R[X]) W'.a₃ : R[X]) -
          HPow.hPow (β := ℕ) q 2 *
            HAdd.hAdd (β := R[X])
              (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
              ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
      max (HSMul.hSMul (α := ℕ) 2 p.degree) (HSMul.hSMul (α := ℕ) 2 q.degree + 3)
⊢ (HPow.hPow (β := ℕ) p 2 -
          p * q *
            HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
              ((C : (a : R) → R[X]) W'.a₃ : R[X]) -
        HPow.hPow (β := ℕ) q 2 *
          HAdd.hAdd (β := R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
            ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
    max (HSMul.hSMul (α := ℕ) 2 p.degree) (HSMul.hSMul (α := ℕ) 2 q.degree + 3)

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 p.degree
hdpq :
  (p * q *
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₃ : R[X])).degree ≤
    p.degree + q.degree + 1
hdq :
  (HPow.hPow (β := ℕ) q 2 *
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
    HSMul.hSMul (α := ℕ) 2 q.degree + 3
hp : p = 0
pos :
  HSMul.hSMul (α := ℕ) 2 q.degree + 3 =
    max (HSMul.hSMul (α := ℕ) 2 (degree.{r} (R := R) 0)) (HSMul.hSMul (α := ℕ) 2 q.degree + 3)
⊢ (HPow.hPow (β := ℕ) p 2 -
          p * q *
            HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
              ((C : (a : R) → R[X]) W'.a₃ : R[X]) -
        HPow.hPow (β := ℕ) q 2 *
          HAdd.hAdd (β := R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
            ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
    max (HSMul.hSMul (α := ℕ) 2 p.degree) (HSMul.hSMul (α := ℕ) 2 q.degree + 3)

Tactic:
simp only [hp, hdq, neg_zero, zero_sub, zero_mul, zero_pow two_ne_zero, degree_neg]

Premises used: MulZeroClass.zero_mul, two_ne_zero, Polynomial.degree_neg, neg_zero, zero_pow, zero_sub
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 p.degree
hdpq :
  (p * q *
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₃ : R[X])).degree ≤
    p.degree + q.degree + 1
hdq :
  (HPow.hPow (β := ℕ) q 2 *
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
    HSMul.hSMul (α := ℕ) 2 q.degree + 3
hp : p = 0
⊢ HSMul.hSMul (α := ℕ) 2 q.degree + 3 =
    max (HSMul.hSMul (α := ℕ) 2 (degree.{r} (R := R) 0)) (HSMul.hSMul (α := ℕ) 2 q.degree + 3)

Tactic:
(max_bot_left _).symm

Premises used: max_bot_left, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 p.degree
hdpq :
  (p * q *
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₃ : R[X])).degree ≤
    p.degree + q.degree + 1
hdq :
  (HPow.hPow (β := ℕ) q 2 *
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])).degree =
    HSMul.hSMul (α := ℕ) 2 q.degree + 3
hp : p = 0
⊢ HSMul.hSMul (α := ℕ) 2 q.degree + 3 =
    max (HSMul.hSMul (α := ℕ) 2 (degree.{r} (R := R) 0)) (HSMul.hSMul (α := ℕ) 2 q.degree + 3)

Tactic:
exact (max_bot_left _).symm

Premises used: max_bot_left, Eq.symm