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 := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
h₅ :
  natDegree (W.preΨ' (m + 5)) ≤ expDegree (m + 5) ∧
    coeff (W.preΨ' (m + 5)) (expDegree (m + 5)) = (↑(expCoeff (m + 5)) : R)
⊢ coeff (W.preΨ' (2 * (m + 3))) (expDegree (2 * (m + 3))) = (↑(expCoeff (2 * (m + 3))) : R)
have even : HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (m + 2)) : R) 2 * (↑(expCoeff (m + 3)) : R) * (↑(expCoeff (m + 5)) : R) -
    HMul.hMul (α := R) (↑(expCoeff (m + 1)) : R) (↑(expCoeff (m + 3)) : R) *
      HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (m + 4)) : R) 2 =
  (↑(HPow.hPow (β := ℕ) (expCoeff (m + 2)) 2 * expCoeff (m + 3) * expCoeff (m + 5) -
        expCoeff (m + 1) * expCoeff (m + 3) * HPow.hPow (β := ℕ) (expCoeff (m + 4)) 2) :
    R)
Tactic: nth_rw 1 [preΨ'_even, coeff_sub, (expDegree_rec m).1.1, cm (dm (dp h₂.1) h₃.1) h₅.1,
        cm (dp h₂.1) h₃.1, cp h₂.1, h₂.2, h₃.2, h₅.2, (expDegree_rec m).1.2,
        cm (dm h₁.1 h₃.1) (dp h₄.1), cm h₁.1 h₃.1, h₁.2, cp h₄.1, h₃.2, h₄.2, (expCoeff_rec m).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 := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
h₅ :
  natDegree (W.preΨ' (m + 5)) ≤ expDegree (m + 5) ∧
    coeff (W.preΨ' (m + 5)) (expDegree (m + 5)) = (↑(expCoeff (m + 5)) : R)
⊢ HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (m + 2)) : R) 2 * (↑(expCoeff (m + 3)) : R) * (↑(expCoeff (m + 5)) : R) -
      HMul.hMul (α := R) (↑(expCoeff (m + 1)) : R) (↑(expCoeff (m + 3)) : R) *
        HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (m + 4)) : R) 2 =
    (↑(HPow.hPow (β := ℕ) (expCoeff (m + 2)) 2 * expCoeff (m + 3) * expCoeff (m + 5) -
          expCoeff (m + 1) * expCoeff (m + 3) * HPow.hPow (β := ℕ) (expCoeff (m + 4)) 2) :
      R)
have even : Eq.{u + 1} (α := R)
  (↑(HPow.hPow (β := ℕ) (expCoeff (m + 2)) 2 * expCoeff (m + 3) * expCoeff (m + 5) -
        expCoeff (m + 1) * expCoeff (m + 3) * HPow.hPow (β := ℕ) (expCoeff (m + 4)) 2) :
    R)
  (↑(HPow.hPow (β := ℕ) (expCoeff (m + 2)) 2 * expCoeff (m + 3) * expCoeff (m + 5) -
        expCoeff (m + 1) * expCoeff (m + 3) * HPow.hPow (β := ℕ) (expCoeff (m + 4)) 2) :
    R)
Tactic: norm_cast
-- 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 := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
⊢ natDegree (W.preΨ' (2 * (m + 2) + 1)) ≤ expDegree (2 * (m + 2) + 1) ∧
    coeff (W.preΨ' (2 * (m + 2) + 1)) (expDegree (2 * (m + 2) + 1)) = (↑(expCoeff (2 * (m + 2) + 1)) : R)
have odd : ((W.preΨ' (m + 4) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 2)) 3 *
          if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1) -
        W.preΨ' (m + 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 3)) 3 *
          if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤
    expDegree (2 * (m + 2) + 1) ∧
  ((W.preΨ' (m + 4) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 2)) 3 *
            if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1) -
          W.preΨ' (m + 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 3)) 3 *
            if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).coeff
      (expDegree (2 * (m + 2) + 1)) =
    (↑(expCoeff (2 * (m + 2) + 1)) : R)
Tactic: rw [preΨ'_odd]
-- 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 := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
⊢ ((W.preΨ' (m + 4) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 2)) 3 *
            if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1) -
          W.preΨ' (m + 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 3)) 3 *
            if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤
      expDegree (2 * (m + 2) + 1) ∧
    ((W.preΨ' (m + 4) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 2)) 3 *
              if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1) -
            W.preΨ' (m + 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 3)) 3 *
              if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).coeff
        (expDegree (2 * (m + 2) + 1)) =
      (↑(expCoeff (2 * (m + 2) + 1)) : R)
have odd : ((W.preΨ' (m + 4) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 2)) 3 *
        if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1) -
      W.preΨ' (m + 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 3)) 3 *
        if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤
  expDegree (2 * (m + 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 := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
odd :
  ((W.preΨ' (m + 4) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 2)) 3 *
          if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1) -
        W.preΨ' (m + 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 3)) 3 *
          if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤
    expDegree (2 * (m + 2) + 1)
⊢ ((W.preΨ' (m + 4) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 2)) 3 *
            if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1) -
          W.preΨ' (m + 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 3)) 3 *
            if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤
      expDegree (2 * (m + 2) + 1) ∧
    ((W.preΨ' (m + 4) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 2)) 3 *
              if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1) -
            W.preΨ' (m + 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 3)) 3 *
              if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).coeff
        (expDegree (2 * (m + 2) + 1)) =
      (↑(expCoeff (2 * (m + 2) + 1)) : R)
have odd₁ : ((W.preΨ' (m + 4) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 2)) 3 *
          if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1) -
        W.preΨ' (m + 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 3)) 3 *
          if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).coeff
    (expDegree (2 * (m + 2) + 1)) =
  (↑(expCoeff (2 * (m + 2) + 1)) : R)
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 := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
⊢ ((W.preΨ' (m + 4) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 2)) 3 *
          if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1) -
        W.preΨ' (m + 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 3)) 3 *
          if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤
    expDegree (2 * (m + 2) + 1)
have odd : ((W.preΨ' (m + 4) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 2)) 3 *
        if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1) -
      W.preΨ' (m + 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 3)) 3 *
        if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤
  max (expDegree (m + 4) + 3 * expDegree (m + 2) + if Even m then HMul.hMul (α := ℕ) 2 3 else 0)
    (expDegree (m + 1) + 3 * expDegree (m + 3) + if Even m then 0 else HMul.hMul (α := ℕ) 2 3)
Tactic: nth_rw 1 [← max_self <| expDegree _, (expDegree_rec m).2.1, (expDegree_rec m).2.2]
-- 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 := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
⊢ ((W.preΨ' (m + 4) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 2)) 3 *
          if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1) -
        W.preΨ' (m + 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 3)) 3 *
          if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤
    max (expDegree (m + 4) + 3 * expDegree (m + 2) + if Even m then HMul.hMul (α := ℕ) 2 3 else 0)
      (expDegree (m + 1) + 3 * expDegree (m + 3) + if Even m then 0 else HMul.hMul (α := ℕ) 2 3)
have odd : (if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1).natDegree ≤ if Even m then HMul.hMul (α := ℕ) 2 3 else 0
Tactic: refine natDegree_sub_le_of_le (dm (dm h₄.1 (dp h₂.1)) ?_) (dm (dm h₁.1 (dp 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 := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
odd :
  (if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1).natDegree ≤
    if Even m then HMul.hMul (α := ℕ) 2 3 else 0
⊢ ((W.preΨ' (m + 4) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 2)) 3 *
          if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1) -
        W.preΨ' (m + 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 3)) 3 *
          if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤
    max (expDegree (m + 4) + 3 * expDegree (m + 2) + if Even m then HMul.hMul (α := ℕ) 2 3 else 0)
      (expDegree (m + 1) + 3 * expDegree (m + 3) + if Even m then 0 else HMul.hMul (α := ℕ) 2 3)
have odd₁ : (if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤ if Even m then 0 else HMul.hMul (α := ℕ) 2 3
Tactic: refine natDegree_sub_le_of_le (dm (dm h₄.1 (dp h₂.1)) ?_) (dm (dm h₁.1 (dp 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 := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
⊢ (if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1).natDegree ≤
    if Even m then HMul.hMul (α := ℕ) 2 3 else 0
have pos : Even m → (HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤ HMul.hMul (α := ℕ) 2 3
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 := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
pos : Even m → (HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤ HMul.hMul (α := ℕ) 2 3
⊢ (if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1).natDegree ≤
    if Even m then HMul.hMul (α := ℕ) 2 3 else 0
have neg : ¬Even m → natDegree.{u} (R := R) 1 ≤ 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 := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
⊢ (if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤
    if Even m then 0 else HMul.hMul (α := ℕ) 2 3
have pos : Even m → natDegree.{u} (R := R) 1 ≤ 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 := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
pos : Even m → natDegree.{u} (R := R) 1 ≤ 0
⊢ (if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤
    if Even m then 0 else HMul.hMul (α := ℕ) 2 3
have neg : ¬Even m → (HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤ HMul.hMul (α := ℕ) 2 3
Tactic: split_ifs