awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
n : ℕ
h : Ne.{u + 1} (α := R) (↑(↑n : ℤ) : R) 0
⊢ Ne.{u + 1} (α := R) (↑n : R) 0

Tactic:
exact_mod_cast h
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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

Tactic:
simpa only [preΨ_ofNat] using W.preΨ'_ne_zero <| by exact_mod_cast h

Premises used: WeierstrassCurve.preΨ'_ne_zero, WeierstrassCurve.preΨ_ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
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.{u + 1} (α := R) (-(↑(↑n : ℤ) : R)) 0

Tactic:
exact_mod_cast h
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
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:
simpa only [preΨ_neg, neg_ne_zero]
        using ih n <| neg_ne_zero.mp <| by exact_mod_cast h

Premises used: WeierstrassCurve.preΨ_neg, Iff.mp, neg_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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
⊢ 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

Premises used: WeierstrassCurve.preΨ'_ne_zero, WeierstrassCurve.preΨ_ofNat, WeierstrassCurve.preΨ_neg, Iff.mp, neg_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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)
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)
⊢ natDegree (W.ΨSq (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) n 2 - 1 ∧
    coeff (W.ΨSq (↑n : ℤ)) (HPow.hPow (β := ℕ) n 2 - 1) = (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2) : R)

Tactic:
rcases n with _ | n
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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) := ⋯
⊢ natDegree (W.ΨSq (↑0 : ℤ)) ≤ HPow.hPow (α := ℕ) (β := ℕ) 0 2 - 1 ∧
    coeff (W.ΨSq (↑0 : ℤ)) (HPow.hPow (α := ℕ) (β := ℕ) 0 2 - 1) = (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑0 : ℤ) 2) : R)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 : ℕ
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
⊢ HPow.hPow (β := ℕ) (n + 1) 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0

Tactic:
push_cast [← @Nat.cast_inj ℤ, add_sq, expDegree_cast n.succ_ne_zero]

Premises used: add_sq, Nat.cast_inj, Nat.succ_ne_zero, _private.0.WeierstrassCurve.expDegree_cast
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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
⊢ 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:
split_ifs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 : ℕ
h_1 : 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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 : ℕ
h_1 : ¬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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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

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
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2 = HPow.hPow (β := ℕ) (expCoeff (n + 1)) 2 * if Even (n + 1) then 4 else 1

Tactic:
push_cast [← @Int.cast_inj ℚ, expCoeff_cast]

Premises used: Int.cast_inj, _private.0.WeierstrassCurve.expCoeff_cast
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
neg :
  ¬Even (n + 1) →
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) 2 = HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) 2 * 1
⊢ 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:
split_ifs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
h_1 : Even (n + 1)
⊢ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) 2 = HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 / 2) 2 * 4

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
h_1 : ¬Even (n + 1)
⊢ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) 2 = HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) 2 * 1

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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

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
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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).coeff
        (2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0) =
      (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1) : ℤ) 2) : R)
⊢ 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:
rw [ΨSq_ofNat, hd]

Premises used: WeierstrassCurve.ΨSq_ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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)
⊢ ((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:
constructor
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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

Tactic:
natDegree_mul_le_of_le (dp h.1) ?_

Premises used: And.left, Polynomial.natDegree_mul_le_of_le
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 : natDegree (if Even (n + 1) then W.Ψ₂Sq else 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

Tactic:
refine natDegree_mul_le_of_le (dp h.1) ?_

Premises used: And.left, Polynomial.natDegree_mul_le_of_le
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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
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
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
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
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
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) (β := ℕ) (↑(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)
succ₁ : natDegree (if Even (n + 1) then W.Ψ₂Sq else 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 [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]

Premises used: WeierstrassCurve.coeff_Ψ₂Sq, apply_ite₂, Polynomial.coeff_pow_of_natDegree_le, Polynomial.coeff, Polynomial.coeff_mul_add_eq_of_natDegree_le, And.right, And.left, Polynomial.coeff_one_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 succ₁ succ₂ succ₃ :
  Eq.{u + 1} (α := R) (↑(HPow.hPow (β := ℕ) (expCoeff (n + 1)) 2 * (↑(if Even (n + 1) then 4 else 1) : ℤ)) : R)
    (↑(HPow.hPow (β := ℕ) (expCoeff (n + 1)) 2 * (↑(if Even (n + 1) then 4 else 1) : ℤ)) : R)
⊢ (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:
norm_cast
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ natDegree (W.ΨSq (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1

Tactic:
(W.natDegree_coeff_ΨSq_ofNat n).left

Premises used: _private.0.WeierstrassCurve.natDegree_coeff_ΨSq_ofNat, And.left, Int.natAbs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ natDegree (W.ΨSq (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1

Tactic:
exact (W.natDegree_coeff_ΨSq_ofNat n).left

Premises used: _private.0.WeierstrassCurve.natDegree_coeff_ΨSq_ofNat, And.left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), natDegree (W.ΨSq (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1
n : ℕ
neg : natDegree (W.ΨSq (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - 1
neg₁ : natDegree (W.ΨSq (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1
⊢ natDegree (W.ΨSq (-(↑n : ℤ))) ≤ HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - 1

Tactic:
simp_rw [ΨSq_neg, Int.natAbs_neg, ih]

Premises used: WeierstrassCurve.ΨSq_neg, Int.natAbs_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
nat : ∀ (n : ℕ), natDegree (W.ΨSq (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1
neg :
  ∀ (ih : ∀ (n : ℕ), natDegree (W.ΨSq (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1) (n : ℕ),
    natDegree (W.ΨSq (-(↑n : ℤ))) ≤ HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - 1
⊢ natDegree (W.ΨSq n) ≤ HPow.hPow (β := ℕ) n.natAbs 2 - 1

Tactic:
induction n using Int.negInduction with
  | nat n => exact (W.natDegree_coeff_ΨSq_ofNat n).left
  | neg ih => simp_rw [ΨSq_neg, Int.natAbs_neg, ih]

Premises used: WeierstrassCurve.ΨSq_neg, Int.natAbs_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ coeff (W.ΨSq (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1) =
    HPow.hPow (α := R) (β := ℕ) (↑(↑n : ℤ) : R) 2

Tactic:
exact_mod_cast (W.natDegree_coeff_ΨSq_ofNat n).right

Premises used: _private.0.WeierstrassCurve.natDegree_coeff_ΨSq_ofNat, And.right
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
ih :
  ∀ (n : ℕ),
    coeff (W.ΨSq (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1) =
      HPow.hPow (α := R) (β := ℕ) (↑(↑n : ℤ) : R) 2
n : ℕ
neg :
  coeff (W.ΨSq (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - 1) =
    HPow.hPow (α := R) (β := ℕ) (↑(-(↑n : ℤ)) : R) 2
neg₁ :
  coeff (W.ΨSq (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1) =
    HPow.hPow (α := R) (β := ℕ) (↑(-(↑n : ℤ)) : R) 2
neg₂ :
  coeff (W.ΨSq (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1) =
    (↑(HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 2) : R)
neg₃ :
  coeff (W.ΨSq (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1) =
    (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2) : R)
neg₄ :
  coeff (W.ΨSq (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1) =
    HPow.hPow (α := R) (β := ℕ) (↑(↑n : ℤ) : R) 2
neg₅ neg₆ : HPow.hPow (α := R) (β := ℕ) (↑(↑n : ℤ) : R) 2 = HPow.hPow (α := R) (β := ℕ) (↑(↑n : ℤ) : R) 2
⊢ coeff (W.ΨSq (-(↑n : ℤ))) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - 1) =
    HPow.hPow (α := R) (β := ℕ) (↑(-(↑n : ℤ)) : R) 2

Tactic:
rw [ΨSq_neg, Int.natAbs_neg, ← Int.cast_pow, neg_sq, Int.cast_pow, ih]

Premises used: Int.cast_pow, neg_sq, WeierstrassCurve.ΨSq_neg, Int.natAbs_neg