awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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)

Tactic:
natDegree_sub_le_of_le (dm (dm h₄.1 (dp h₂.1)) ?_) (dm (dm h₁.1 (dp h₃.1)) ?_)

Premises used: Polynomial.natDegree_sub_le_of_le, And.left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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
⊢ ((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:
refine natDegree_sub_le_of_le (dm (dm h₄.1 (dp h₂.1)) ?_) (dm (dm h₁.1 (dp h₃.1)) ?_)

Premises used: Polynomial.natDegree_sub_le_of_le, And.left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
neg : ¬Even m → natDegree.{u} (R := R) 1 ≤ 0
⊢ (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:
split_ifs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
neg : ¬Even m → (HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤ HMul.hMul (α := ℕ) 2 3
⊢ (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:
split_ifs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 : Even m
⊢ (HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤ HMul.hMul (α := ℕ) 2 3

Tactic:
simp only [natDegree_one.le, dp W.natDegree_Ψ₂Sq_le]

Premises used: Eq.le, Polynomial.natDegree_one, WeierstrassCurve.natDegree_Ψ₂Sq_le
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 : ¬Even m
⊢ natDegree.{u} (R := R) 1 ≤ 0

Tactic:
simp only [natDegree_one.le, dp W.natDegree_Ψ₂Sq_le]

Premises used: Eq.le, Polynomial.natDegree_one, WeierstrassCurve.natDegree_Ψ₂Sq_le
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 : Even m
⊢ natDegree.{u} (R := R) 1 ≤ 0

Tactic:
simp only [natDegree_one.le, dp W.natDegree_Ψ₂Sq_le]

Premises used: Eq.le, Polynomial.natDegree_one, WeierstrassCurve.natDegree_Ψ₂Sq_le
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 : ¬Even m
⊢ (HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2).natDegree ≤ HMul.hMul (α := ℕ) 2 3

Tactic:
simp only [natDegree_one.le, dp W.natDegree_Ψ₂Sq_le]

Premises used: Eq.le, Polynomial.natDegree_one, WeierstrassCurve.natDegree_Ψ₂Sq_le
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 :
  (((↑(expCoeff (m + 4)) : R) * HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (m + 2)) : R) 3 *
        if Even m then HPow.hPow (α := R) (β := ℕ) 4 2 else 1) -
      (↑(expCoeff (m + 1)) : R) * HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (m + 3)) : R) 3 *
        if Even m then 1 else HPow.hPow (α := R) (β := ℕ) 4 2) =
    (↑((expCoeff (m + 4) * HPow.hPow (β := ℕ) (expCoeff (m + 2)) 3 *
            if Even m then HPow.hPow (α := ℤ) (β := ℕ) 4 2 else 1) -
          expCoeff (m + 1) * HPow.hPow (β := ℕ) (expCoeff (m + 3)) 3 *
            if Even m then 1 else HPow.hPow (α := ℤ) (β := ℕ) 4 2) :
      R)
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
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).coeff
      (expDegree (2 * (m + 2) + 1)) =
    (↑(expCoeff (2 * (m + 2) + 1)) : R)

Tactic:
nth_rw 1 [coeff_sub, (expDegree_rec m).2.1, cm (dm h₄.1 (dp h₂.1)), cm h₄.1 (dp h₂.1),
        h₄.2, cp h₂.1, h₂.2, apply_ite₂ coeff, cp W.natDegree_Ψ₂Sq_le, coeff_Ψ₂Sq, coeff_one_zero,
        (expDegree_rec m).2.2, cm (dm h₁.1 (dp h₃.1)), cm h₁.1 (dp h₃.1), h₁.2, cp h₃.1, h₃.2,
        apply_ite₂ coeff, cp W.natDegree_Ψ₂Sq_le, coeff_one_zero, coeff_Ψ₂Sq, (expCoeff_rec m).2]

Premises used: WeierstrassCurve.coeff_Ψ₂Sq, apply_ite₂, _private.0.WeierstrassCurve.expDegree_rec, Polynomial.coeff, And.right, And.left, Polynomial.coeff_sub, _private.0.WeierstrassCurve.expCoeff_rec, WeierstrassCurve.natDegree_Ψ₂Sq_le, Polynomial.coeff_one_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 odd₁ odd₂ odd₃ :
  Eq.{u + 1} (α := R)
    (↑(expCoeff (m + 4) * HPow.hPow (β := ℕ) (expCoeff (m + 2)) 3 *
            (↑(if Even m then HPow.hPow (α := ℕ) (β := ℕ) 4 2 else 1) : ℤ) -
          expCoeff (m + 1) * HPow.hPow (β := ℕ) (expCoeff (m + 3)) 3 *
            (↑(if Even m then 1 else HPow.hPow (α := ℕ) (β := ℕ) 4 2) : ℤ)) :
      R)
    (↑(expCoeff (m + 4) * HPow.hPow (β := ℕ) (expCoeff (m + 2)) 3 *
            (↑(if Even m then HPow.hPow (α := ℕ) (β := ℕ) 4 2 else 1) : ℤ) -
          expCoeff (m + 1) * HPow.hPow (β := ℕ) (expCoeff (m + 3)) 3 *
            (↑(if Even m then 1 else HPow.hPow (α := ℕ) (β := ℕ) 4 2) : ℤ)) :
      R)
⊢ (((↑(expCoeff (m + 4)) : R) * HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (m + 2)) : R) 3 *
        if Even m then HPow.hPow (α := R) (β := ℕ) 4 2 else 1) -
      (↑(expCoeff (m + 1)) : R) * HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (m + 3)) : R) 3 *
        if Even m then 1 else HPow.hPow (α := R) (β := ℕ) 4 2) =
    (↑((expCoeff (m + 4) * HPow.hPow (β := ℕ) (expCoeff (m + 2)) 3 *
            if Even m then HPow.hPow (α := ℤ) (β := ℕ) 4 2 else 1) -
          expCoeff (m + 1) * HPow.hPow (β := ℕ) (expCoeff (m + 3)) 3 *
            if Even m then 1 else HPow.hPow (α := ℤ) (β := ℕ) 4 2) :
      R)

Tactic:
norm_cast
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ natDegree (W.preΨ' n) ≤ (HPow.hPow (β := ℕ) n 2 - if Even n then 4 else 1) / 2

Tactic:
(W.natDegree_coeff_preΨ' n).left

Premises used: _private.0.WeierstrassCurve.expDegree, _private.0.WeierstrassCurve.natDegree_coeff_preΨ', And.left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R)

Tactic:
(W.natDegree_coeff_preΨ' n).right

Premises used: _private.0.WeierstrassCurve.natDegree_coeff_preΨ', And.right
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
h : Eq.{u + 1} (α := R) (↑(if Even n then n / 2 else n) : R) (↑(expCoeff n) : R)
⊢ coeff (W.preΨ' n) ((HPow.hPow (β := ℕ) n 2 - if Even n then 4 else 1) / 2) = (↑(if Even n then n / 2 else n) : R)

Tactic:
convert! (W.natDegree_coeff_preΨ' n).right using 1

Premises used: _private.0.WeierstrassCurve.natDegree_coeff_preΨ', And.right
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ∀ (n : ℕ), Eq.{u + 1} (α := R) (↑(if Even (2 * n) then 2 * n / 2 else 2 * n) : R) (↑(expCoeff (2 * n)) : R)
h₁ :
  ∀ (n : ℕ),
    Eq.{u + 1} (α := R) (↑(if Even (2 * n + 1) then (2 * n + 1) / 2 else 2 * n + 1) : R) (↑(expCoeff (2 * n + 1)) : R)
⊢ Eq.{u + 1} (α := R) (↑(if Even n then n / 2 else n) : R) (↑(expCoeff n) : R)

Tactic:
rcases n.even_or_odd' with ⟨n, rfl | rfl⟩

Premises used: Nat.even_or_odd', rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ Eq.{u + 1} (α := R) (↑(if Even (2 * n) then 2 * n / 2 else 2 * n) : R) (↑(expCoeff (2 * n)) : R)

Tactic:
simp [expCoeff, n.not_even_two_mul_add_one]

Premises used: Nat.not_even_two_mul_add_one, _private.0.WeierstrassCurve.expCoeff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ Eq.{u + 1} (α := R) (↑(if Even (2 * n + 1) then (2 * n + 1) / 2 else 2 * n + 1) : R) (↑(expCoeff (2 * n + 1)) : R)

Tactic:
simp [expCoeff, n.not_even_two_mul_add_one]

Premises used: Nat.not_even_two_mul_add_one, _private.0.WeierstrassCurve.expCoeff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
h : Ne.{u + 1} (α := R) (↑n : R) 0
inl :
  ∀ (n : ℕ) (h : Ne.{u + 1} (α := R) (↑(2 * n) : R) 0),
    coeff (W.preΨ' (2 * n)) ((HPow.hPow (β := ℕ) (2 * n) 2 - if Even (2 * n) then 4 else 1) / 2) ≠ 0
inr :
  ∀ (n : ℕ) (h : Ne.{u + 1} (α := R) (↑(2 * n + 1) : R) 0),
    coeff (W.preΨ' (2 * n + 1)) ((HPow.hPow (β := ℕ) (2 * n + 1) 2 - if Even (2 * n + 1) then 4 else 1) / 2) ≠ 0
⊢ coeff (W.preΨ' n) ((HPow.hPow (β := ℕ) n 2 - if Even n then 4 else 1) / 2) ≠ 0

Tactic:
rcases n.even_or_odd' with ⟨n, rfl | rfl⟩

Premises used: Nat.even_or_odd', rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
h : Ne.{u + 1} (α := R) (↑(2 * n) : R) 0
inl : Ne.{u + 1} (α := R) (↑n : R) 0
⊢ coeff (W.preΨ' (2 * n)) ((HPow.hPow (β := ℕ) (2 * n) 2 - if Even (2 * n) then 4 else 1) / 2) ≠ 0

Tactic:
rw [coeff_preΨ', if_pos <| even_two_mul n, n.mul_div_cancel_left two_pos]

Premises used: WeierstrassCurve.coeff_preΨ', Nat.mul_div_cancel_left, two_pos, if_pos, even_two_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
h : Ne.{u + 1} (α := R) (↑(2 * n) : R) 0
rwa : Ne.{u + 1} (α := R) (↑(2 * n) : R) 0
m : ℕ
rwa₁ : Ne.{u + 1} (α := R) (↑(2 * n) : R) 0
m₁ : ℕ
rwa₂ : Ne.{u + 1} (α := R) (↑(2 * n) : R) 0
m₂ : ℕ
rwa₃ : Ne.{u + 1} (α := R) (↑(2 * n) : R) 0
m₃ : ℕ
⊢ HMul.hMul (α := R) (↑2 : R) (↑n : R) ≠ 0

Tactic:
rwa [← Nat.cast_mul]

Premises used: Nat.cast_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
h : Ne.{u + 1} (α := R) (↑(2 * n) : R) 0
⊢ Ne.{u + 1} (α := R) (↑n : R) 0

Tactic:
exact right_ne_zero_of_mul <| by rwa [← Nat.cast_mul]

Premises used: right_ne_zero_of_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
h : Ne.{u + 1} (α := R) (↑(2 * n + 1) : R) 0
inr : Ne.{u + 1} (α := R) (↑(if Even (2 * n + 1) then (2 * n + 1) / 2 else 2 * n + 1) : R) 0
inr₁ inr₂ inr₃ inr₄ : Ne.{u + 1} (α := R) (↑(2 * n + 1) : R) 0
⊢ coeff (W.preΨ' (2 * n + 1)) ((HPow.hPow (β := ℕ) (2 * n + 1) 2 - if Even (2 * n + 1) then 4 else 1) / 2) ≠ 0

Tactic:
rwa [coeff_preΨ', if_neg n.not_even_two_mul_add_one]

Premises used: WeierstrassCurve.coeff_preΨ', Nat.not_even_two_mul_add_one, if_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
h : Ne.{u + 1} (α := R) (↑n : R) 0
⊢ natDegree (W.preΨ' n) = (HPow.hPow (β := ℕ) n 2 - if Even n then 4 else 1) / 2

Tactic:
natDegree_eq_of_le_of_coeff_ne_zero (W.natDegree_preΨ'_le n) <| W.coeff_preΨ'_ne_zero h

Premises used: WeierstrassCurve.natDegree_preΨ'_le, Polynomial.natDegree_eq_of_le_of_coeff_ne_zero, WeierstrassCurve.coeff_preΨ'_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : Ne.{u + 1} (α := R) (↑n : R) 0
simp_rw : 2 ≤ HPow.hPow (β := ℕ) n 2 - if Even n then 4 else 1
⊢ 0 < natDegree (W.preΨ' n)

Tactic:
simp_rw [W.natDegree_preΨ' h, Nat.div_pos_iff, zero_lt_two, true_and]

Premises used: Nat.div_pos_iff, WeierstrassCurve.natDegree_preΨ', zero_lt_two, true_and
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : Ne.{u + 1} (α := R) (↑n : R) 0
pos : Even n → 2 ≤ HPow.hPow (β := ℕ) n 2 - 4
neg : ¬Even n → 2 ≤ HPow.hPow (β := ℕ) n 2 - 1
⊢ 2 ≤ HPow.hPow (β := ℕ) n 2 - if Even n then 4 else 1

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : Ne.{u + 1} (α := R) (↑n : R) 0
h_1 : Even n
⊢ 2 ≤ HPow.hPow (β := ℕ) n 2 - 4

Tactic:
Nat.AtLeastTwo.prop.trans <| Nat.sub_le_sub_right (Nat.pow_le_pow_left hn 2) _

Premises used: Nat.AtLeastTwo.prop, Nat.sub_le_sub_right, LE.le.trans, OfNat.ofNat, Nat.pow_le_pow_left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : Ne.{u + 1} (α := R) (↑n : R) 0
h_1 : Even n
⊢ 2 ≤ HPow.hPow (β := ℕ) n 2 - 4

Tactic:
exact Nat.AtLeastTwo.prop.trans <| Nat.sub_le_sub_right (Nat.pow_le_pow_left hn 2) _

Premises used: Nat.AtLeastTwo.prop, Nat.sub_le_sub_right, LE.le.trans, OfNat.ofNat, Nat.pow_le_pow_left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : Ne.{u + 1} (α := R) (↑n : R) 0
h_1 : ¬Even n
⊢ 2 ≤ HPow.hPow (β := ℕ) n 2 - 1

Tactic:
Nat.AtLeastTwo.prop.trans <| Nat.sub_le_sub_right (Nat.pow_le_pow_left hn 2) _

Premises used: Nat.AtLeastTwo.prop, Nat.sub_le_sub_right, LE.le.trans, OfNat.ofNat, Nat.pow_le_pow_left