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 := ⋯
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
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
⊢ 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:
push_cast [← @Int.cast_inj ℚ, expCoeff_cast, Nat.even_add_one, ite_not]

Premises used: Nat.even_add_one, Int.cast_inj, _private.0.WeierstrassCurve.expCoeff_cast, ite_not
-- 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 := ⋯
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
neg :
  ¬Even n →
    1 =
      1 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 2) 2 * 1 -
        HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / 2 * (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 / 2) * 4
⊢ 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:
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 := ⋯
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
h_1 : Even n
⊢ 1 =
    1 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 2 / 2) 2 * 4 -
      HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * 1

Tactic:
ring1
-- 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 := ⋯
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
h_1 : ¬Even n
⊢ 1 =
    1 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 2) 2 * 1 -
      HAdd.hAdd (α := ℚ) (↑n : ℚ) 3 / 2 * (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 / 2) * 4

Tactic:
ring1
-- 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 := ⋯
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

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
-- 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 := ⋯
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).coeff
        (HPow.hPow (β := ℕ) (n + 1 + 1) 2) =
      1
⊢ natDegree (W.Φ (↑(n + 1 + 1) : ℤ)) ≤ HPow.hPow (β := ℕ) (n + 1 + 1) 2 ∧
    coeff (W.Φ (↑(n + 1 + 1) : ℤ)) (HPow.hPow (β := ℕ) (n + 1 + 1) 2) = 1

Tactic:
rw [Nat.cast_add, Nat.cast_one, Φ_ofNat]

Premises used: WeierstrassCurve.Φ_ofNat, Nat.cast_add, Nat.cast_one
-- 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 := ⋯
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
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
⊢ ((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:
constructor
-- 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 := ⋯
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 ≤
    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)
⊢ ((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:
nth_rw 1 [← max_self <| (_ + _) ^ 2, hd, hd']

Premises used: max_self, HAdd.hAdd
-- 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 := ⋯
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)

Tactic:
natDegree_sub_le_of_le (dm (dm natDegree_X_le (dp h.1)) ?_) (dm (dm h.1 h.1) ?_)

Premises used: Polynomial.natDegree_sub_le_of_le, And.left, Polynomial.natDegree_X_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 := ⋯
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
succ₁ : natDegree (if Even (n + 1) then W.Ψ₂Sq else 1) ≤ if Even (n + 1) then 3 else 0
⊢ ((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:
refine natDegree_sub_le_of_le (dm (dm natDegree_X_le (dp h.1)) ?_) (dm (dm h.1 h.1) ?_)

Premises used: Polynomial.natDegree_sub_le_of_le, And.left, Polynomial.natDegree_X_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 := ⋯
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
pos : Even (n + 1) → natDegree.{u} (R := R) 1 ≤ 0
neg : ¬Even (n + 1) → natDegree W.Ψ₂Sq ≤ 3
⊢ natDegree (if Even (n + 1) then 1 else W.Ψ₂Sq) ≤ if Even (n + 1) then 0 else 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 := ⋯
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
pos : Even (n + 1) → natDegree W.Ψ₂Sq ≤ 3
neg : ¬Even (n + 1) → natDegree.{u} (R := R) 1 ≤ 0
⊢ natDegree (if Even (n + 1) then W.Ψ₂Sq else 1) ≤ if Even (n + 1) then 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 := ⋯
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
h_1 : Even (n + 1)
⊢ natDegree.{u} (R := R) 1 ≤ 0

Tactic:
simp only [natDegree_one.le, 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 := ⋯
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
h_1 : ¬Even (n + 1)
⊢ natDegree W.Ψ₂Sq ≤ 3

Tactic:
simp only [natDegree_one.le, 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 := ⋯
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
h_1 : Even (n + 1)
⊢ natDegree W.Ψ₂Sq ≤ 3

Tactic:
simp only [natDegree_one.le, 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 := ⋯
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
h_1 : ¬Even (n + 1)
⊢ natDegree.{u} (R := R) 1 ≤ 0

Tactic:
simp only [natDegree_one.le, 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 := ⋯
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 :
  ((1 * HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (n + 1 + 1)) : R) 2 * if Even (n + 1) then 1 else 4) -
      HMul.hMul (α := R) (↑(expCoeff (n + 1 + 2)) : R) (↑(expCoeff (n + 1)) : R) * if Even (n + 1) then 4 else 1) =
    1
succ₁ : natDegree (if Even (n + 1) then W.Ψ₂Sq else 1) ≤ if Even (n + 1) then 3 else 0
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).coeff
      (HPow.hPow (β := ℕ) (n + 1 + 1) 2) =
    1

Tactic:
nth_rw 1 [coeff_sub, hd, hd', cm (dm natDegree_X_le (dp h.1)), cm natDegree_X_le (dp h.1),
      coeff_X_one, coeff_pow_of_natDegree_le h.1, h.2, apply_ite₂ coeff, coeff_one_zero, coeff_Ψ₂Sq,
      cm (dm h.1 h.1), cm h.1 h.1, h.2, h.2, apply_ite₂ coeff, coeff_one_zero, coeff_Ψ₂Sq]

Premises used: WeierstrassCurve.coeff_Ψ₂Sq, apply_ite₂, Polynomial.coeff_X_one, Polynomial.coeff_pow_of_natDegree_le, Polynomial.coeff, And.right, And.left, Polynomial.coeff_sub, Polynomial.natDegree_X_le, Polynomial.coeff_one_zero