awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
⊢ (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
have 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
Tactic: grw [degree_mul, degree_mul, degree_linear_le]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
⊢ (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
have grw₂ : p.degree + q.degree + 1 ≤ p.degree + q.degree + 1
Tactic: grw [degree_mul, degree_mul, degree_linear_le]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
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
⊢ 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)
have 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
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
have 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
Tactic: rw [degree_mul, degree_pow, ← one_mul <| X ^ 3, ← C_1, degree_cubic <| one_ne_zero' R]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
⊢ (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
have 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
Tactic: rw [degree_mul, degree_pow, ← one_mul <| X ^ 3, ← C_1, degree_cubic <| one_ne_zero' R]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
⊢ (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
have 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
Tactic: rw [degree_mul, degree_pow, ← one_mul <| X ^ 3, ← C_1, degree_cubic <| one_ne_zero' R]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
⊢ (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
have 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
Tactic: rw [degree_mul, degree_pow, ← one_mul <| X ^ 3, ← C_1, degree_cubic <| one_ne_zero' R]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
⊢ (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
have rw₄ : HSMul.hSMul (α := ℕ) 2 q.degree + 3 = HSMul.hSMul (α := ℕ) 2 q.degree + 3
Tactic: rw [degree_mul, degree_pow, ← one_mul <| X ^ 3, ← C_1, degree_cubic <| one_ne_zero' R]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
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
⊢ 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)
have 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
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
⊢ 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)
have 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)
Tactic: rw [norm_smul_basis]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
⊢ (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)
have 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)
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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)
⊢ (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)
have 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)
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
⊢ (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)
have pos : HSMul.hSMul (α := ℕ) 2 q.degree + 3 =
  max (HSMul.hSMul (α := ℕ) 2 (degree.{r} (R := R) 0)) (HSMul.hSMul (α := ℕ) 2 q.degree + 3)
Tactic: simp only [hp, hdq, neg_zero, zero_sub, zero_mul, zero_pow two_ne_zero, degree_neg]