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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 (some dp)
hp' : p.degree = some dp
dq : ℕ
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 (some dq) + 3
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 ≤
    some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ some dp + some dq + 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
have neg : some dp + some dq + 1 < HSMul.hSMul (α := ℕ) 2 (some dq) + 3
Tactic: rw [hdq]
-- 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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 (some dp)
hp' : p.degree = some dp
dq : ℕ
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 (some dq) + 3
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 ≤
    some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ 2 * dp < 2 * dq + 3
have linarith : 2 * dq + 3 ≤ 2 * dp →
  -1 + (HMul.hMul (α := ℤ) 2 (↑dq : ℤ) + 3 - HMul.hMul (α := ℤ) 2 (↑dp : ℤ)) +
      2 * ((↑dp : ℤ) - HAdd.hAdd (α := ℤ) (↑dq : ℤ) 1) =
    0
Tactic: linarith only [hpq]
-- 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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 (some dp)
hp' : p.degree = some dp
dq : ℕ
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 (some dq) + 3
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 ≤
    some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
linarith :
  2 * dq + 3 ≤ 2 * dp →
    -1 + (HMul.hMul (α := ℤ) 2 (↑dq : ℤ) + 3 - HMul.hMul (α := ℤ) 2 (↑dp : ℤ)) +
        2 * ((↑dp : ℤ) - HAdd.hAdd (α := ℤ) (↑dq : ℤ) 1) =
      0
⊢ 2 * dp < 2 * dq + 3
have linarith₁ : 2 * dq + 3 ≤ 2 * dp → GT.gt (α := ℤ) 2 0
Tactic: linarith only [hpq]
-- 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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 (some dp)
hp' : p.degree = some dp
dq : ℕ
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 (some dq) + 3
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 ≤
    some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ dp + dq + 1 < 2 * dq + 3
have linarith : 2 * dq + 3 ≤ dp + dq + 1 →
  -1 + (HMul.hMul (α := ℤ) 2 (↑dq : ℤ) + 3 - (HAdd.hAdd (α := ℤ) (↑dp : ℤ) (↑dq : ℤ) + 1)) +
      ((↑dp : ℤ) - HAdd.hAdd (α := ℤ) (↑dq : ℤ) 1) =
    0
Tactic: linarith only [hpq]
-- 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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 (some dp)
hp' : p.degree = some dp
dq : ℕ
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 (some dq) + 3
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 ≤
    some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ (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 (some dp)) (HSMul.hSMul (α := ℕ) 2 (some dq) + 3)
have neg : (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 (some dp)) (HSMul.hSMul (α := ℕ) 2 (some dq) + 3)
Tactic: rw [sub_sub]
-- 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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 (some dp)
hp' : p.degree = some dp
dq : ℕ
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 (some dq) + 3
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 ≤
    some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ (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 (some dp)) (HSMul.hSMul (α := ℕ) 2 (some dq) + 3)
have h : HSMul.hSMul (α := ℕ) 2 (some dp) = (HPow.hPow (β := ℕ) p 2).degree
Tactic: convert!
              (degree_sub_eq_left_of_degree_lt <|
                    (degree_add_le _ _).trans_lt <|
                      max_lt_iff.mpr ⟨hdpq.trans_lt _, hdq.trans_lt _⟩).trans
                (max_eq_left_of_lt _).symm
-- 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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 (some dp)
hp' : p.degree = some dp
dq : ℕ
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 (some dq) + 3
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 ≤
    some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
h : HSMul.hSMul (α := ℕ) 2 (some dp) = (HPow.hPow (β := ℕ) p 2).degree
⊢ (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 (some dp)) (HSMul.hSMul (α := ℕ) 2 (some dq) + 3)
have neg : some dp + some dq + 1 < (HPow.hPow (β := ℕ) p 2).degree
Tactic: convert!
              (degree_sub_eq_left_of_degree_lt <|
                    (degree_add_le _ _).trans_lt <|
                      max_lt_iff.mpr ⟨hdpq.trans_lt _, hdq.trans_lt _⟩).trans
                (max_eq_left_of_lt _).symm
-- 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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 (some dp)
hp' : p.degree = some dp
dq : ℕ
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 (some dq) + 3
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 ≤
    some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
h : HSMul.hSMul (α := ℕ) 2 (some dp) = (HPow.hPow (β := ℕ) p 2).degree
neg : some dp + some dq + 1 < (HPow.hPow (β := ℕ) p 2).degree
⊢ (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 (some dp)) (HSMul.hSMul (α := ℕ) 2 (some dq) + 3)
have neg₁ : HSMul.hSMul (α := ℕ) 2 (some dq) + 3 < (HPow.hPow (β := ℕ) p 2).degree
Tactic: convert!
              (degree_sub_eq_left_of_degree_lt <|
                    (degree_add_le _ _).trans_lt <|
                      max_lt_iff.mpr ⟨hdpq.trans_lt _, hdq.trans_lt _⟩).trans
                (max_eq_left_of_lt _).symm
-- 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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 (some dp)
hp' : p.degree = some dp
dq : ℕ
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 (some dq) + 3
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 ≤
    some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ HSMul.hSMul (α := ℕ) 2 (some dp) = (HPow.hPow (β := ℕ) p 2).degree
have h : HSMul.hSMul (α := ℕ) 2 (some dp) = HSMul.hSMul (α := ℕ) 2 (some dp)
Tactic: rw [hdp]
-- 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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 (some dp)
hp' : p.degree = some dp
dq : ℕ
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 (some dq) + 3
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 ≤
    some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ some dp + some dq + 1 < (HPow.hPow (β := ℕ) p 2).degree
have neg : some dp + some dq + 1 < HSMul.hSMul (α := ℕ) 2 (some dp)
Tactic: rw [hdp]
-- 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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 (some dp)
hp' : p.degree = some dp
dq : ℕ
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 (some dq) + 3
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 ≤
    some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ HSMul.hSMul (α := ℕ) 2 (some dq) + 3 < (HPow.hPow (β := ℕ) p 2).degree
have neg : HSMul.hSMul (α := ℕ) 2 (some dq) + 3 < HSMul.hSMul (α := ℕ) 2 (some dp)
Tactic: rw [hdp]
-- 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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 (some dp)
hp' : p.degree = some dp
dq : ℕ
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 (some dq) + 3
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 ≤
    some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ dp + dq + 1 < 2 * dp
have linarith : 2 * dp ≤ dp + dq + 1 →
  -1 + (HMul.hMul (α := ℤ) 2 (↑dp : ℤ) - (HAdd.hAdd (α := ℤ) (↑dp : ℤ) (↑dq : ℤ) + 1)) +
      (HAdd.hAdd (α := ℤ) (↑dq : ℤ) 1 + 1 - (↑dp : ℤ)) =
    0
Tactic: linarith only [hpq]
-- 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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 (some dp)
hp' : p.degree = some dp
dq : ℕ
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 (some dq) + 3
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 ≤
    some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ 2 * dq + 3 < 2 * dp
have linarith : 2 * dp ≤ 2 * dq + 3 →
  -1 + (HMul.hMul (α := ℤ) 2 (↑dp : ℤ) - (HMul.hMul (α := ℤ) 2 (↑dq : ℤ) + 3)) +
      2 * (HAdd.hAdd (α := ℤ) (↑dq : ℤ) 1 + 1 - (↑dp : ℤ)) =
    0
Tactic: linarith only [hpq]
-- 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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 (some dp)
hp' : p.degree = some dp
dq : ℕ
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 (some dq) + 3
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 ≤
    some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
linarith :
  2 * dp ≤ 2 * dq + 3 →
    -1 + (HMul.hMul (α := ℤ) 2 (↑dp : ℤ) - (HMul.hMul (α := ℤ) 2 (↑dq : ℤ) + 3)) +
        2 * (HAdd.hAdd (α := ℤ) (↑dq : ℤ) 1 + 1 - (↑dp : ℤ)) =
      0
⊢ 2 * dq + 3 < 2 * dp
have linarith₁ : 2 * dp ≤ 2 * dq + 3 → GT.gt (α := ℤ) 2 0
Tactic: linarith only [hpq]
-- 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
x : W'.CoordinateRing
⊢ degree.{r} (R := R) ((Algebra.norm R[X] : (a : W'.CoordinateRing) → R[X]) x) ≠ 1
have rcases : ∀ (p q : R[X]),
  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))) ≠
    1
Tactic: rcases exists_smul_basis_eq x with ⟨p, q, rfl⟩
Cleared hypotheses: x
-- 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]
⊢ 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))) ≠
    1
have rw : max (HSMul.hSMul (α := ℕ) 2 p.degree) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
Tactic: rw [degree_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]
⊢ max (HSMul.hSMul (α := ℕ) 2 p.degree) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
have none : max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 none) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
Tactic: rcases p.degree with (_ | _ | _ | _)
-- 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]
none : max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 Option.none) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
⊢ max (HSMul.hSMul (α := ℕ) 2 p.degree) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
have some : max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 (some 0)) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
Tactic: rcases p.degree with (_ | _ | _ | _)
-- 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]
none : max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 Option.none) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
some : max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 (Option.some 0)) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
⊢ max (HSMul.hSMul (α := ℕ) 2 p.degree) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
have some₁ : max (HSMul.hSMul (α := ℕ) 2 (Option.some (HAdd.hAdd (α := ℕ) 0 1))) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
Tactic: rcases p.degree with (_ | _ | _ | _)
-- 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]
none : max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 Option.none) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
some : max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 (Option.some 0)) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
some₁ : max (HSMul.hSMul (α := ℕ) 2 (Option.some (HAdd.hAdd (α := ℕ) 0 1))) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
⊢ max (HSMul.hSMul (α := ℕ) 2 p.degree) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
have some₂ : ∀ (n : ℕ), max (HSMul.hSMul (α := ℕ) 2 (Option.some (n + 1 + 1))) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
Tactic: rcases p.degree with (_ | _ | _ | _)
-- 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]
⊢ max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 none) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
have none : max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 none) (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 ⊥ + 3) ≠ 1
Tactic: cases q.degree