awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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 (HPow.hPow (β := ℕ) p 2).degree (HSMul.hSMul (α := ℕ) 2 (some dq) + 3)

Tactic:
(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

Premises used: Iff.mpr, max_lt_iff, And.intro, Polynomial.degree_sub_eq_left_of_degree_lt, Eq.trans_lt, Polynomial.degree_add_le, max_eq_left_of_lt, Eq.symm, LE.le.trans_lt, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
neg₁ : HSMul.hSMul (α := ℕ) 2 (some dq) + 3 < (HPow.hPow (β := ℕ) p 2).degree
neg₂ : HSMul.hSMul (α := ℕ) 2 (some dq) + 3 < (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)

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

Premises used: Iff.mpr, max_lt_iff, And.intro, Polynomial.degree_sub_eq_left_of_degree_lt, Eq.trans_lt, Polynomial.degree_add_le, max_eq_left_of_lt, Eq.symm, LE.le.trans_lt, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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 h₁ : HSMul.hSMul (α := ℕ) 2 (some dp) = HSMul.hSMul (α := ℕ) 2 (some dp)
⊢ HSMul.hSMul (α := ℕ) 2 (some dp) = (HPow.hPow (β := ℕ) p 2).degree

Tactic:
rw [hdp]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
neg : some dp + some dq + 1 < HSMul.hSMul (α := ℕ) 2 (some dp)
⊢ some dp + some dq + 1 < (HPow.hPow (β := ℕ) p 2).degree

Tactic:
rw [hdp]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
neg : HSMul.hSMul (α := ℕ) 2 (some dq) + 3 < HSMul.hSMul (α := ℕ) 2 (some dp)
⊢ HSMul.hSMul (α := ℕ) 2 (some dq) + 3 < (HPow.hPow (β := ℕ) p 2).degree

Tactic:
rw [hdp]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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 ≤ dp + dq + 1 →
    -1 + (HMul.hMul (α := ℤ) 2 (↑dp : ℤ) - (HAdd.hAdd (α := ℤ) (↑dp : ℤ) (↑dq : ℤ) + 1)) +
        (HAdd.hAdd (α := ℤ) (↑dq : ℤ) 1 + 1 - (↑dp : ℤ)) =
      0
⊢ dp + dq + 1 < 2 * dp

Tactic:
linarith only [hpq]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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 < HSMul.hSMul (α := ℕ) 2 (some dp)

Tactic:
exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]

Premises used: Iff.mpr, WithBot.coe_lt_coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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
linarith₁ : 2 * dp ≤ 2 * dq + 3 → GT.gt (α := ℤ) 2 0
⊢ 2 * dq + 3 < 2 * dp

Tactic:
linarith only [hpq]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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 < HSMul.hSMul (α := ℕ) 2 (some dp)

Tactic:
exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]

Premises used: Iff.mpr, WithBot.coe_lt_coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
x : W'.CoordinateRing
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
⊢ degree.{r} (R := R) ((Algebra.norm R[X] : (a : W'.CoordinateRing) → R[X]) x) ≠ 1

Tactic:
rcases exists_smul_basis_eq x with ⟨p, q, rfl⟩

Premises used: WeierstrassCurve.Affine.CoordinateRing.exists_smul_basis_eq, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
rw : max (HSMul.hSMul (α := ℕ) 2 p.degree) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 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))) ≠
    1

Tactic:
rw [degree_norm_smul_basis]

Premises used: WeierstrassCurve.Affine.CoordinateRing.degree_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]
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
some₂ : ∀ (n : ℕ), max (HSMul.hSMul (α := ℕ) 2 (Option.some (n + 1 + 1))) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1
⊢ max (HSMul.hSMul (α := ℕ) 2 p.degree) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1

Tactic:
rcases p.degree with (_ | _ | _ | _)

Premises used: Polynomial.degree
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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 (α := ℕ) (β := WithBot ℕ) 2 ⊥ + 3) ≠ 1
none₁ :
  ∀ (a : ℕ), max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 Option.none) (HSMul.hSMul (α := ℕ) 2 (↑a : WithBot ℕ) + 3) ≠ 1
⊢ max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 Option.none) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1

Tactic:
cases q.degree

Premises used: Polynomial.degree
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
some : max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 (Option.some 0)) (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 ⊥ + 3) ≠ 1
some₁ :
  ∀ (a : ℕ),
    max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 (Option.some 0)) (HSMul.hSMul (α := ℕ) 2 (↑a : WithBot ℕ) + 3) ≠ 1
⊢ max (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 (Option.some 0)) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1

Tactic:
cases q.degree

Premises used: Polynomial.degree
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
some :
  max (HSMul.hSMul (α := ℕ) 2 (Option.some (HAdd.hAdd (α := ℕ) 0 1))) (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 ⊥ + 3) ≠
    1
some₁ :
  ∀ (a : ℕ),
    max (HSMul.hSMul (α := ℕ) 2 (Option.some (HAdd.hAdd (α := ℕ) 0 1))) (HSMul.hSMul (α := ℕ) 2 (↑a : WithBot ℕ) + 3) ≠
      1
⊢ max (HSMul.hSMul (α := ℕ) 2 (Option.some (HAdd.hAdd (α := ℕ) 0 1))) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1

Tactic:
cases q.degree

Premises used: Polynomial.degree
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
n : ℕ
some : max (HSMul.hSMul (α := ℕ) 2 (Option.some (n + 1 + 1))) (HSMul.hSMul (α := ℕ) (β := WithBot ℕ) 2 ⊥ + 3) ≠ 1
some₁ :
  ∀ (a : ℕ), max (HSMul.hSMul (α := ℕ) 2 (Option.some (n + 1 + 1))) (HSMul.hSMul (α := ℕ) 2 (↑a : WithBot ℕ) + 3) ≠ 1
⊢ max (HSMul.hSMul (α := ℕ) 2 (Option.some (n + 1 + 1))) (HSMul.hSMul (α := ℕ) 2 q.degree + 3) ≠ 1

Tactic:
cases q.degree

Premises used: Polynomial.degree
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
n a : ℕ
⊢ max (HSMul.hSMul (α := ℕ) 2 (some (n + 1 + 1))) (HSMul.hSMul (α := ℕ) 2 (↑a : WithBot ℕ) + 3) ≠ 1

Tactic:
(lt_max_of_lt_right <| (cmp_eq_lt_iff ..).mp rfl).ne'

Premises used: lt_max_of_lt_right, LT.lt.ne', Iff.mp, cmp_eq_lt_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
n a : ℕ
⊢ max (HSMul.hSMul (α := ℕ) 2 (some (n + 1 + 1))) (HSMul.hSMul (α := ℕ) 2 (↑a : WithBot ℕ) + 3) ≠ 1

Tactic:
exact (lt_max_of_lt_right <| (cmp_eq_lt_iff ..).mp rfl).ne'

Premises used: lt_max_of_lt_right, LT.lt.ne', Iff.mp, cmp_eq_lt_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
x : W'.CoordinateRing
⊢ natDegree.{r} (R := R) ((Algebra.norm R[X] : (a : W'.CoordinateRing) → R[X]) x) ≠ 1

Tactic:
degree_norm_ne_one x ∘ (degree_eq_iff_natDegree_eq_of_pos zero_lt_one).mpr

Premises used: Iff.mpr, Function.comp, Polynomial.degree_eq_iff_natDegree_eq_of_pos, zero_lt_one, WeierstrassCurve.Affine.CoordinateRing.degree_norm_ne_one, Not
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 property : p Point.zero
⊢ (fun (P : WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }) ↦
        (Option.casesOn (motive :=
            fun (x : WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }) ↦
            { P : W'.Point // p P }) P (Subtype.mk (p := fun (P : W'.Point) ↦ p P) Point.zero p0)
            fun (xy : { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }) ↦
            Subtype.mk (p := fun (P : W'.Point) ↦ p P) (Point.some (↑xy : R × R).1 (↑xy : R × R).2 ⋯) ⋯ :
          { P : W'.Point // p P }))
      ((fun (x : { P : W'.Point // p P }) ↦
          (match (motive :=
              { P : W'.Point // p P } →
                WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) })
              x with
            | ⟨Point.zero, property⟩ => none
            | ⟨Point.some x y h, ph⟩ =>
              some
                (Subtype.mk (p := fun (xy : R × R) ↦ ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h))
                  (x, y) ⋯) :
            WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }))
        (Subtype.mk (p := fun (P : W'.Point) ↦ p P) Point.zero property)) =
    Subtype.mk (p := fun (P : W'.Point) ↦ p P) Point.zero property

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 : p Point.zero
x y : R
h : W'.Nonsingular x y
property : p (Point.some x y h)
⊢ (fun (P : WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }) ↦
        (Option.casesOn (motive :=
            fun (x : WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }) ↦
            { P : W'.Point // p P }) P (Subtype.mk (p := fun (P : W'.Point) ↦ p P) Point.zero p0)
            fun (xy : { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }) ↦
            Subtype.mk (p := fun (P : W'.Point) ↦ p P) (Point.some (↑xy : R × R).1 (↑xy : R × R).2 ⋯) ⋯ :
          { P : W'.Point // p P }))
      ((fun (x : { P : W'.Point // p P }) ↦
          (match (motive :=
              { P : W'.Point // p P } →
                WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) })
              x with
            | ⟨Point.zero, property⟩ => none
            | ⟨Point.some x y h, ph⟩ =>
              some
                (Subtype.mk (p := fun (xy : R × R) ↦ ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h))
                  (x, y) ⋯) :
            WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }))
        (Subtype.mk (p := fun (P : W'.Point) ↦ p P) (Point.some x y h) property)) =
    Subtype.mk (p := fun (P : W'.Point) ↦ p P) (Point.some x y h) property

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 : p Point.zero
⊢ Eq.{r + 1} (α := WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) })
    ((fun (x : { P : W'.Point // p P }) ↦
        (match (motive :=
            { P : W'.Point // p P } →
              WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) })
            x with
          | ⟨Point.zero, property⟩ => none
          | ⟨Point.some x y h, ph⟩ =>
            some
              (Subtype.mk (p := fun (xy : R × R) ↦ ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h)) (x, y)
                ⋯) :
          WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }))
      ((fun (P : WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }) ↦
          (Option.casesOn (motive :=
              fun (x : WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }) ↦
              { P : W'.Point // p P }) P (Subtype.mk (p := fun (P : W'.Point) ↦ p P) Point.zero p0)
              fun (xy : { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }) ↦
              Subtype.mk (p := fun (P : W'.Point) ↦ p P) (Point.some (↑xy : R × R).1 (↑xy : R × R).2 ⋯) ⋯ :
            { P : W'.Point // p P }))
        none))
    none

Tactic:
rfl