awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
pos :
  Even n →
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
      1 + (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 - 4) + 3
⊢ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
    1 + (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 - if Even n then 4 else 1) + if Even n then 3 else 0
have neg : ¬Even n →
  HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
    1 + (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 - 1) + 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (hypothesis)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
⊢ natDegree (W.Φ (↑(n + 1 + 1) : ℤ)) ≤ HPow.hPow (β := ℕ) (n + 1 + 1) 2 ∧
    coeff (W.Φ (↑(n + 1 + 1) : ℤ)) (HPow.hPow (β := ℕ) (n + 1 + 1) 2) = 1
have hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
Tactic: have hd : (n + 1 + 1) ^ 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3 := by
    push_cast [← @Nat.cast_inj ℤ, expDegree_cast (n + 1).succ_ne_zero, Nat.even_add_one, ite_not]
    split_ifs <;> ring1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
⊢ HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
have push_cast : 2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
  (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) 2 - if Even n then 1 else 4) +
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 2 - if Even n then 1 else 4) +
    HMul.hMul (α := ℤ) 2 (if Even n then 0 else 3)
Tactic: push_cast [← @Nat.cast_inj ℤ, ← mul_left_cancel_iff_of_pos (b := (_ ^ 2 : ℤ)) two_pos, mul_add,
      expDegree_cast (n + 2).succ_ne_zero, expDegree_cast n.succ_ne_zero, Nat.even_add_one, ite_not]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
⊢ 2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) 2 - if Even n then 1 else 4) +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 2 - if Even n then 1 else 4) +
      HMul.hMul (α := ℤ) 2 (if Even n then 0 else 3)
have pos : Even n →
  2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) 2 - 1 +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 2 - 1) +
      HMul.hMul (α := ℤ) 2 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
pos :
  Even n →
    2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) 2 - 1 +
          (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 2 - 1) +
        HMul.hMul (α := ℤ) 2 0
⊢ 2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) 2 - if Even n then 1 else 4) +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 2 - if Even n then 1 else 4) +
      HMul.hMul (α := ℤ) 2 (if Even n then 0 else 3)
have neg : ¬Even n →
  2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) 2 - 4 +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 2 - 4) +
      HMul.hMul (α := ℤ) 2 3
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (hypothesis)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
⊢ natDegree (W.Φ (↑(n + 1 + 1) : ℤ)) ≤ HPow.hPow (β := ℕ) (n + 1 + 1) 2 ∧
    coeff (W.Φ (↑(n + 1 + 1) : ℤ)) (HPow.hPow (β := ℕ) (n + 1 + 1) 2) = 1
have hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
Tactic: have hd' : (n + 1 + 1) ^ 2 =
      expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0 := by
    push_cast [← @Nat.cast_inj ℤ, ← mul_left_cancel_iff_of_pos (b := (_ ^ 2 : ℤ)) two_pos, mul_add,
      expDegree_cast (n + 2).succ_ne_zero, expDegree_cast n.succ_ne_zero, Nat.even_add_one, ite_not]
    split_ifs <;> ring1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
⊢ 1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
have push_cast : 1 =
  (1 * HPow.hPow (β := ℕ) (if Even n then HAdd.hAdd (α := ℚ) (↑n : ℚ) 2 / 2 else HAdd.hAdd (α := ℚ) (↑n : ℚ) 2) 2 *
      if Even n then 4 else 1) -
    ((if Even n then HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / 2) *
        if Even n then HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 else HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 / 2) *
      if Even n then 1 else 4
Tactic: push_cast [← @Int.cast_inj ℚ, expCoeff_cast, Nat.even_add_one, ite_not]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
⊢ 1 =
    (1 * HPow.hPow (β := ℕ) (if Even n then HAdd.hAdd (α := ℚ) (↑n : ℚ) 2 / 2 else HAdd.hAdd (α := ℚ) (↑n : ℚ) 2) 2 *
        if Even n then 4 else 1) -
      ((if Even n then HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / 2) *
          if Even n then HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 else HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 / 2) *
        if Even n then 1 else 4
have pos : Even n →
  1 =
    1 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 2 / 2) 2 * 4 -
      HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
pos :
  Even n →
    1 =
      1 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 2 / 2) 2 * 4 -
        HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * 1
⊢ 1 =
    (1 * HPow.hPow (β := ℕ) (if Even n then HAdd.hAdd (α := ℚ) (↑n : ℚ) 2 / 2 else HAdd.hAdd (α := ℚ) (↑n : ℚ) 2) 2 *
        if Even n then 4 else 1) -
      ((if Even n then HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 else HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / 2) *
          if Even n then HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 else HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 / 2) *
        if Even n then 1 else 4
have neg : ¬Even n →
  1 =
    1 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 2) 2 * 1 -
      HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / 2 * (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 / 2) * 4
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (hypothesis)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
⊢ natDegree (W.Φ (↑(n + 1 + 1) : ℤ)) ≤ HPow.hPow (β := ℕ) (n + 1 + 1) 2 ∧
    coeff (W.Φ (↑(n + 1 + 1) : ℤ)) (HPow.hPow (β := ℕ) (n + 1 + 1) 2) = 1
have hc : 1 =
  (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
    expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
Tactic: have hc : (1 : ℤ) = 1 * expCoeff (n + 2) ^ 2 * (if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * (if Even (n + 1) then 4 else 1) := by
    push_cast [← @Int.cast_inj ℚ, expCoeff_cast, Nat.even_add_one, ite_not]
    split_ifs <;> ring1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ natDegree (W.Φ (↑(n + 1 + 1) : ℤ)) ≤ HPow.hPow (β := ℕ) (n + 1 + 1) 2 ∧
    coeff (W.Φ (↑(n + 1 + 1) : ℤ)) (HPow.hPow (β := ℕ) (n + 1 + 1) 2) = 1
have succ : ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1 + 1)) 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
        HMul.hMul (α := R[X]) (W.preΨ' (n + 1 + 2)) (W.preΨ' (n + 1)) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    HPow.hPow (β := ℕ) (n + 1 + 1) 2 ∧
  ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1 + 1)) 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
          HMul.hMul (α := R[X]) (W.preΨ' (n + 1 + 2)) (W.preΨ' (n + 1)) * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
      (HPow.hPow (β := ℕ) (n + 1 + 1) 2) =
    1
Tactic: rw [Nat.cast_add, Nat.cast_one, Φ_ofNat]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1 + 1)) 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
          HMul.hMul (α := R[X]) (W.preΨ' (n + 1 + 2)) (W.preΨ' (n + 1)) *
            if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
      HPow.hPow (β := ℕ) (n + 1 + 1) 2 ∧
    ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1 + 1)) 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
            HMul.hMul (α := R[X]) (W.preΨ' (n + 1 + 2)) (W.preΨ' (n + 1)) * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
        (HPow.hPow (β := ℕ) (n + 1 + 1) 2) =
      1
have succ : ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1 + 1)) 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (n + 1 + 2)) (W.preΨ' (n + 1)) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
  HPow.hPow (β := ℕ) (n + 1 + 1) 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
succ :
  ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1 + 1)) 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
        HMul.hMul (α := R[X]) (W.preΨ' (n + 1 + 2)) (W.preΨ' (n + 1)) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    HPow.hPow (β := ℕ) (n + 1 + 1) 2
⊢ ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1 + 1)) 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
          HMul.hMul (α := R[X]) (W.preΨ' (n + 1 + 2)) (W.preΨ' (n + 1)) *
            if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
      HPow.hPow (β := ℕ) (n + 1 + 1) 2 ∧
    ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1 + 1)) 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
            HMul.hMul (α := R[X]) (W.preΨ' (n + 1 + 2)) (W.preΨ' (n + 1)) * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
        (HPow.hPow (β := ℕ) (n + 1 + 1) 2) =
      1
have succ₁ : ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1 + 1)) 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
        HMul.hMul (α := R[X]) (W.preΨ' (n + 1 + 2)) (W.preΨ' (n + 1)) * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
    (HPow.hPow (β := ℕ) (n + 1 + 1) 2) =
  1
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1 + 1)) 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
        HMul.hMul (α := R[X]) (W.preΨ' (n + 1 + 2)) (W.preΨ' (n + 1)) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    HPow.hPow (β := ℕ) (n + 1 + 1) 2
have succ : ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1 + 1)) 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (n + 1 + 2)) (W.preΨ' (n + 1)) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
  max (1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3)
    (expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0)
Tactic: nth_rw 1 [← max_self <| (_ + _) ^ 2, hd, hd']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1 + 1)) 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
        HMul.hMul (α := R[X]) (W.preΨ' (n + 1 + 2)) (W.preΨ' (n + 1)) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    max (1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3)
      (expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0)
have succ : natDegree (if Even (n + 1) then 1 else W.Ψ₂Sq) ≤ if Even (n + 1) then 0 else 3
Tactic: refine natDegree_sub_le_of_le (dm (dm natDegree_X_le (dp h.1)) ?_) (dm (dm h.1 h.1) ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
succ : natDegree (if Even (n + 1) then 1 else W.Ψ₂Sq) ≤ if Even (n + 1) then 0 else 3
⊢ ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1 + 1)) 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
        HMul.hMul (α := R[X]) (W.preΨ' (n + 1 + 2)) (W.preΨ' (n + 1)) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    max (1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3)
      (expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0)
have succ₁ : natDegree (if Even (n + 1) then W.Ψ₂Sq else 1) ≤ if Even (n + 1) then 3 else 0
Tactic: refine natDegree_sub_le_of_le (dm (dm natDegree_X_le (dp h.1)) ?_) (dm (dm h.1 h.1) ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ natDegree (if Even (n + 1) then 1 else W.Ψ₂Sq) ≤ if Even (n + 1) then 0 else 3
have pos : Even (n + 1) → natDegree.{u} (R := R) 1 ≤ 0
Tactic: split_ifs