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
n : ℤ
nat :
  ∀ (n : ℕ),
    coeff (W.preΨ (↑n : ℤ))
        ((HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - if Even (α := ℤ) (↑n : ℤ) then 4 else 1) / 2) =
      (↑(if Even (α := ℤ) (↑n : ℤ) then HDiv.hDiv (α := ℤ) (↑n : ℤ) 2 else (↑n : ℤ)) : R)
⊢ coeff (W.preΨ n) ((HPow.hPow (β := ℕ) n.natAbs 2 - if Even n then 4 else 1) / 2) =
    (↑(if Even n then n / 2 else n) : R)
have neg : ∀
  (ih :
    ∀ (n : ℕ),
      coeff (W.preΨ (↑n : ℤ))
          ((HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - if Even (α := ℤ) (↑n : ℤ) then 4 else 1) / 2) =
        (↑(if Even (α := ℤ) (↑n : ℤ) then HDiv.hDiv (α := ℤ) (↑n : ℤ) 2 else (↑n : ℤ)) : R))
  (n : ℕ),
  coeff (W.preΨ (-(↑n : ℤ)))
      ((HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - if Even (α := ℤ) (-(↑n : ℤ)) then 4 else 1) / 2) =
    (↑(if Even (α := ℤ) (-(↑n : ℤ)) then HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) 2 else -(↑n : ℤ)) : R)
Tactic: induction n using Int.negInduction with
  | nat n => exact_mod_cast W.preΨ_ofNat n ▸ W.coeff_preΨ' n
  | neg ih n =>
    simp_rw [preΨ_neg, coeff_neg, Int.natAbs_neg, even_neg]
    rcases ih n, n.even_or_odd' with ⟨ih, ⟨n, rfl | rfl⟩⟩ <;>
      push_cast [even_two_mul, Int.not_even_two_mul_add_one, Int.neg_ediv_of_dvd ⟨n, rfl⟩] at * <;>
      rw [ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
⊢ coeff (W.preΨ n) ((HPow.hPow (β := ℕ) n.natAbs 2 - if Even n then 4 else 1) / 2) ≠ 0
have nat : ∀ (n : ℕ) (h : Ne.{u + 1} (α := R) (↑(↑n : ℤ) : R) 0),
  coeff (W.preΨ (↑n : ℤ)) ((HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - if Even (α := ℤ) (↑n : ℤ) then 4 else 1) / 2) ≠
    0
Tactic: induction n using Int.negInduction with
  | nat n => simpa only [preΨ_ofNat, Int.even_coe_nat]
      using W.coeff_preΨ'_ne_zero <| by exact_mod_cast h
  | neg ih n => simpa only [preΨ_neg, coeff_neg, neg_ne_zero, Int.natAbs_neg, even_neg]
        using ih n <| neg_ne_zero.mp <| by exact_mod_cast h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
nat :
  ∀ (n : ℕ) (h : Ne.{u + 1} (α := R) (↑(↑n : ℤ) : R) 0),
    coeff (W.preΨ (↑n : ℤ))
        ((HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - if Even (α := ℤ) (↑n : ℤ) then 4 else 1) / 2) ≠
      0
⊢ coeff (W.preΨ n) ((HPow.hPow (β := ℕ) n.natAbs 2 - if Even n then 4 else 1) / 2) ≠ 0
have neg : ∀
  (ih :
    ∀ (n : ℕ) (h : Ne.{u + 1} (α := R) (↑(↑n : ℤ) : R) 0),
      coeff (W.preΨ (↑n : ℤ))
          ((HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - if Even (α := ℤ) (↑n : ℤ) then 4 else 1) / 2) ≠
        0)
  (n : ℕ) (h : Ne.{u + 1} (α := R) (↑(-(↑n : ℤ)) : R) 0),
  coeff (W.preΨ (-(↑n : ℤ)))
      ((HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - if Even (α := ℤ) (-(↑n : ℤ)) then 4 else 1) / 2) ≠
    0
Tactic: induction n using Int.negInduction with
  | nat n => simpa only [preΨ_ofNat, Int.even_coe_nat]
      using W.coeff_preΨ'_ne_zero <| by exact_mod_cast h
  | neg ih n => simpa only [preΨ_neg, coeff_neg, neg_ne_zero, Int.natAbs_neg, even_neg]
        using ih n <| neg_ne_zero.mp <| by exact_mod_cast h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
hn : 2 < n.natAbs
h : Ne.{u + 1} (α := R) (↑n : R) 0
⊢ 0 < natDegree (W.preΨ n)
have nat : ∀ (n : ℕ) (hn : 2 < Int.natAbs (↑n : ℤ)) (h : Ne.{u + 1} (α := R) (↑(↑n : ℤ) : R) 0), 0 < natDegree (W.preΨ (↑n : ℤ))
Tactic: induction n using Int.negInduction with
  | nat n => simpa only [preΨ_ofNat] using W.natDegree_preΨ'_pos hn <| by exact_mod_cast h
  | neg ih n => simpa only [preΨ_neg, natDegree_neg]
        using ih n (by rwa [← Int.natAbs_neg]) <| neg_ne_zero.mp <| by exact_mod_cast h
Cleared hypotheses: n, hn, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
hn : 2 < n.natAbs
h : Ne.{u + 1} (α := R) (↑n : R) 0
nat :
  ∀ (n : ℕ) (hn : 2 < Int.natAbs (↑n : ℤ)) (h : Ne.{u + 1} (α := R) (↑(↑n : ℤ) : R) 0), 0 < natDegree (W.preΨ (↑n : ℤ))
⊢ 0 < natDegree (W.preΨ n)
have neg : ∀
  (ih :
    ∀ (n : ℕ) (hn : 2 < Int.natAbs (↑n : ℤ)) (h : Ne.{u + 1} (α := R) (↑(↑n : ℤ) : R) 0),
      0 < natDegree (W.preΨ (↑n : ℤ)))
  (n : ℕ) (hn : 2 < Int.natAbs (-(↑n : ℤ))) (h : Ne.{u + 1} (α := R) (↑(-(↑n : ℤ)) : R) 0),
  0 < natDegree (W.preΨ (-(↑n : ℤ)))
Tactic: induction n using Int.negInduction with
  | nat n => simpa only [preΨ_ofNat] using W.natDegree_preΨ'_pos hn <| by exact_mod_cast h
  | neg ih n => simpa only [preΨ_neg, natDegree_neg]
        using ih n (by rwa [← Int.natAbs_neg]) <| neg_ne_zero.mp <| by exact_mod_cast h
Cleared hypotheses: n, hn, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
⊢ leadingCoeff (W.preΨ n) = (↑(if Even n then n / 2 else n) : R)
have rw : coeff (W.preΨ n) (natDegree (W.preΨ n)) = (↑(if Even n then n / 2 else n) : R)
Tactic: rw [leadingCoeff, W.natDegree_preΨ h, coeff_preΨ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
rw : coeff (W.preΨ n) (natDegree (W.preΨ n)) = (↑(if Even n then n / 2 else n) : R)
⊢ leadingCoeff (W.preΨ n) = (↑(if Even n then n / 2 else n) : R)
have rw₁ : coeff (W.preΨ n) ((HPow.hPow (β := ℕ) n.natAbs 2 - if Even n then 4 else 1) / 2) = (↑(if Even n then n / 2 else n) : R)
Tactic: rw [leadingCoeff, W.natDegree_preΨ h, coeff_preΨ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
rw : coeff (W.preΨ n) (natDegree (W.preΨ n)) = (↑(if Even n then n / 2 else n) : R)
rw₁ :
  coeff (W.preΨ n) ((HPow.hPow (β := ℕ) n.natAbs 2 - if Even n then 4 else 1) / 2) =
    (↑(if Even n then n / 2 else n) : R)
⊢ leadingCoeff (W.preΨ n) = (↑(if Even n then n / 2 else n) : R)
have rw₂ : Eq.{u + 1} (α := R) (↑(if Even n then n / 2 else n) : R) (↑(if Even n then n / 2 else n) : R)
Tactic: rw [leadingCoeff, W.natDegree_preΨ h, coeff_preΨ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
⊢ Ne (α := R[X]) (W.preΨ n) 0
have nat : ∀ (n : ℕ) (h : Ne.{u + 1} (α := R) (↑(↑n : ℤ) : R) 0), Ne (α := R[X]) (W.preΨ (↑n : ℤ)) 0
Tactic: induction n using Int.negInduction with
  | nat n => simpa only [preΨ_ofNat] using W.preΨ'_ne_zero <| by exact_mod_cast h
  | neg ih n => simpa only [preΨ_neg, neg_ne_zero]
        using ih n <| neg_ne_zero.mp <| by exact_mod_cast h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
nat : ∀ (n : ℕ) (h : Ne.{u + 1} (α := R) (↑(↑n : ℤ) : R) 0), Ne (α := R[X]) (W.preΨ (↑n : ℤ)) 0
⊢ Ne (α := R[X]) (W.preΨ n) 0
have neg : ∀ (ih : ∀ (n : ℕ) (h : Ne.{u + 1} (α := R) (↑(↑n : ℤ) : R) 0), Ne (α := R[X]) (W.preΨ (↑n : ℤ)) 0) (n : ℕ)
  (h : Ne.{u + 1} (α := R) (↑(-(↑n : ℤ)) : R) 0), Ne (α := R[X]) (W.preΨ (-(↑n : ℤ))) 0
Tactic: induction n using Int.negInduction with
  | nat n => simpa only [preΨ_ofNat] using W.preΨ'_ne_zero <| by exact_mod_cast h
  | neg ih n => simpa only [preΨ_neg, neg_ne_zero]
        using ih n <| neg_ne_zero.mp <| by exact_mod_cast h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
⊢ natDegree (W.ΨSq (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) n 2 - 1 ∧
    coeff (W.ΨSq (↑n : ℤ)) (HPow.hPow (β := ℕ) n 2 - 1) = (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2) : R)
have zero : natDegree (W.ΨSq (↑0 : ℤ)) ≤ HPow.hPow (α := ℕ) (β := ℕ) 0 2 - 1 ∧
  coeff (W.ΨSq (↑0 : ℤ)) (HPow.hPow (α := ℕ) (β := ℕ) 0 2 - 1) = (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑0 : ℤ) 2) : R)
Tactic: rcases n with _ | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
zero :
  natDegree (W.ΨSq (↑0 : ℤ)) ≤ HPow.hPow (α := ℕ) (β := ℕ) 0 2 - 1 ∧
    coeff (W.ΨSq (↑0 : ℤ)) (HPow.hPow (α := ℕ) (β := ℕ) 0 2 - 1) = (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑0 : ℤ) 2) : R)
⊢ natDegree (W.ΨSq (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) n 2 - 1 ∧
    coeff (W.ΨSq (↑n : ℤ)) (HPow.hPow (β := ℕ) n 2 - 1) = (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2) : R)
have succ : ∀ (n : ℕ),
  natDegree (W.ΨSq (↑(n + 1) : ℤ)) ≤ HPow.hPow (β := ℕ) (n + 1) 2 - 1 ∧
    coeff (W.ΨSq (↑(n + 1) : ℤ)) (HPow.hPow (β := ℕ) (n + 1) 2 - 1) =
      (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2) : R)
Tactic: rcases n with _ | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
⊢ HPow.hPow (β := ℕ) (n + 1) 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
have push_cast : HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 + HMul.hMul (α := ℤ) 2 (↑n : ℤ) * 1 =
  (HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 + HMul.hMul (α := ℤ) 2 (↑n : ℤ) * 1 + 1 - if Even n.succ then 4 else 1) +
    if Even (n + 1) then 3 else 0
Tactic: push_cast [← @Nat.cast_inj ℤ, add_sq, expDegree_cast n.succ_ne_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 + HMul.hMul (α := ℤ) 2 (↑n : ℤ) * 1 =
    (HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 + HMul.hMul (α := ℤ) 2 (↑n : ℤ) * 1 + 1 - if Even n.succ then 4 else 1) +
      if Even (n + 1) then 3 else 0
have pos : Even n.succ →
  HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 + HMul.hMul (α := ℤ) 2 (↑n : ℤ) * 1 =
    HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 + HMul.hMul (α := ℤ) 2 (↑n : ℤ) * 1 + 1 - 4 + 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
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
pos :
  Even n.succ →
    HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 + HMul.hMul (α := ℤ) 2 (↑n : ℤ) * 1 =
      HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 + HMul.hMul (α := ℤ) 2 (↑n : ℤ) * 1 + 1 - 4 + 3
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 + HMul.hMul (α := ℤ) 2 (↑n : ℤ) * 1 =
    (HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 + HMul.hMul (α := ℤ) 2 (↑n : ℤ) * 1 + 1 - if Even n.succ then 4 else 1) +
      if Even (n + 1) then 3 else 0
have neg : ¬Even n.succ →
  HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 + HMul.hMul (α := ℤ) 2 (↑n : ℤ) * 1 =
    HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 + HMul.hMul (α := ℤ) 2 (↑n : ℤ) * 1 + 1 - 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
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
⊢ natDegree (W.ΨSq (↑(n + 1) : ℤ)) ≤ HPow.hPow (β := ℕ) (n + 1) 2 - 1 ∧
    coeff (W.ΨSq (↑(n + 1) : ℤ)) (HPow.hPow (β := ℕ) (n + 1) 2 - 1) =
      (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2) : R)
have hd : HPow.hPow (β := ℕ) (n + 1) 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
Tactic: have hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0 := by
    push_cast [← @Nat.cast_inj ℤ, add_sq, expDegree_cast n.succ_ne_zero]
    split_ifs <;> ring1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1) 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2 = HPow.hPow (β := ℕ) (expCoeff (n + 1)) 2 * if Even (n + 1) then 4 else 1
have push_cast : HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) 2 =
  HPow.hPow (β := ℕ) (if Even (n + 1) then HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 / 2 else HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) 2 *
    if Even (n + 1) then 4 else 1
Tactic: push_cast [← @Int.cast_inj ℚ, expCoeff_cast]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1) 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
⊢ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) 2 =
    HPow.hPow (β := ℕ) (if Even (n + 1) then HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 / 2 else HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) 2 *
      if Even (n + 1) then 4 else 1
have pos : Even (n + 1) →
  HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) 2 = HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 / 2) 2 * 4
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1) 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
pos :
  Even (n + 1) →
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) 2 = HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 / 2) 2 * 4
⊢ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) 2 =
    HPow.hPow (β := ℕ) (if Even (n + 1) then HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 / 2 else HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) 2 *
      if Even (n + 1) then 4 else 1
have neg : ¬Even (n + 1) →
  HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) 2 = HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) 2 * 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (hypothesis)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1) 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
⊢ natDegree (W.ΨSq (↑(n + 1) : ℤ)) ≤ HPow.hPow (β := ℕ) (n + 1) 2 - 1 ∧
    coeff (W.ΨSq (↑(n + 1) : ℤ)) (HPow.hPow (β := ℕ) (n + 1) 2 - 1) =
      (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2) : R)
have hc : HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2 = HPow.hPow (β := ℕ) (expCoeff (n + 1)) 2 * if Even (n + 1) then 4 else 1
Tactic: have hc : (n + 1 : ℕ) ^ 2 = expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1 := by
    push_cast [← @Int.cast_inj ℚ, expCoeff_cast]
    split_ifs <;> ring1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1) 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2 = HPow.hPow (β := ℕ) (expCoeff (n + 1)) 2 * if Even (n + 1) then 4 else 1
⊢ natDegree (W.ΨSq (↑(n + 1) : ℤ)) ≤ HPow.hPow (β := ℕ) (n + 1) 2 - 1 ∧
    coeff (W.ΨSq (↑(n + 1) : ℤ)) (HPow.hPow (β := ℕ) (n + 1) 2 - 1) =
      (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2) : R)
have succ : ((HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0) ∧
  (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
      (2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0) =
    (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2) : R)
Tactic: rw [ΨSq_ofNat, hd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1) 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2 = HPow.hPow (β := ℕ) (expCoeff (n + 1)) 2 * if Even (n + 1) then 4 else 1
⊢ ((HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
      2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0) ∧
    (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
        (2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0) =
      (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2) : R)
have succ : (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
  2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1) 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2 = HPow.hPow (β := ℕ) (expCoeff (n + 1)) 2 * if Even (n + 1) then 4 else 1
succ :
  (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
⊢ ((HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
      2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0) ∧
    (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
        (2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0) =
      (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2) : R)
have succ₁ : (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
    (2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0) =
  (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2) : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1) 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2 = HPow.hPow (β := ℕ) (expCoeff (n + 1)) 2 * if Even (n + 1) then 4 else 1
⊢ (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    2 * 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_mul_le_of_le (dp h.1) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1) 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2 = HPow.hPow (β := ℕ) (expCoeff (n + 1)) 2 * if Even (n + 1) then 4 else 1
⊢ natDegree (if Even (n + 1) then W.Ψ₂Sq else 1) ≤ if Even (n + 1) then 3 else 0
have pos : Even (n + 1) → natDegree W.Ψ₂Sq ≤ 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
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1) 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2 = HPow.hPow (β := ℕ) (expCoeff (n + 1)) 2 * if Even (n + 1) then 4 else 1
pos : Even (n + 1) → natDegree W.Ψ₂Sq ≤ 3
⊢ natDegree (if Even (n + 1) then W.Ψ₂Sq else 1) ≤ if Even (n + 1) then 3 else 0
have neg : ¬Even (n + 1) → 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
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1) 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2 = HPow.hPow (β := ℕ) (expCoeff (n + 1)) 2 * if Even (n + 1) then 4 else 1
⊢ (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
      (2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0) =
    (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2) : R)
have succ : (HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (n + 1)) : R) 2 * if Even (n + 1) then 4 else 1) =
  (↑(HPow.hPow (β := ℕ) (expCoeff (n + 1)) 2 * if Even (n + 1) then 4 else 1) : R)
Tactic: rw [coeff_mul_add_eq_of_natDegree_le (dp h.1), coeff_pow_of_natDegree_le h.1, h.2,
      apply_ite₂ coeff, coeff_Ψ₂Sq, coeff_one_zero, hc]