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
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)
⊢ (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₁ : natDegree (if Even (n + 1) then W.Ψ₂Sq else 1) ≤ if Even (n + 1) then 3 else 0
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]
-- 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) (β := ℕ) (↑(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)
have 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)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
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
have neg : natDegree (W.ΨSq (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - 1
Tactic: simp_rw [ΨSq_neg, Int.natAbs_neg, ih]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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
⊢ natDegree (W.ΨSq (-(↑n : ℤ))) ≤ HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - 1
have neg₁ : natDegree (W.ΨSq (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1
Tactic: simp_rw [ΨSq_neg, Int.natAbs_neg, ih]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ natDegree (W.ΨSq n) ≤ HPow.hPow (β := ℕ) n.natAbs 2 - 1
have nat : ∀ (n : ℕ), natDegree (W.ΨSq (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 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]
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 : ℤ
nat : ∀ (n : ℕ), natDegree (W.ΨSq (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1
⊢ natDegree (W.ΨSq n) ≤ HPow.hPow (β := ℕ) n.natAbs 2 - 1
have 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
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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 : ℕ
⊢ coeff (W.ΨSq (-(↑n : ℤ))) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - 1) =
    HPow.hPow (α := R) (β := ℕ) (↑(-(↑n : ℤ)) : R) 2
have neg : 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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
⊢ coeff (W.ΨSq (-(↑n : ℤ))) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - 1) =
    HPow.hPow (α := R) (β := ℕ) (↑(-(↑n : ℤ)) : R) 2
have neg₁ : 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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
⊢ coeff (W.ΨSq (-(↑n : ℤ))) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - 1) =
    HPow.hPow (α := R) (β := ℕ) (↑(-(↑n : ℤ)) : R) 2
have neg₂ : coeff (W.ΨSq (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1) =
  (↑(HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 2) : R)
Tactic: rw [ΨSq_neg, Int.natAbs_neg, ← Int.cast_pow, neg_sq, Int.cast_pow, ih]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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)
⊢ coeff (W.ΨSq (-(↑n : ℤ))) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - 1) =
    HPow.hPow (α := R) (β := ℕ) (↑(-(↑n : ℤ)) : R) 2
have neg₃ : coeff (W.ΨSq (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1) =
  (↑(HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2) : R)
Tactic: rw [ΨSq_neg, Int.natAbs_neg, ← Int.cast_pow, neg_sq, Int.cast_pow, ih]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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)
⊢ coeff (W.ΨSq (-(↑n : ℤ))) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - 1) =
    HPow.hPow (α := R) (β := ℕ) (↑(-(↑n : ℤ)) : R) 2
have neg₄ : 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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
⊢ coeff (W.ΨSq (-(↑n : ℤ))) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - 1) =
    HPow.hPow (α := R) (β := ℕ) (↑(-(↑n : ℤ)) : R) 2
have neg₅ : HPow.hPow (α := R) (β := ℕ) (↑(↑n : ℤ) : R) 2 = HPow.hPow (α := R) (β := ℕ) (↑(↑n : ℤ) : R) 2
Tactic: rw [ΨSq_neg, Int.natAbs_neg, ← Int.cast_pow, neg_sq, Int.cast_pow, ih]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ coeff (W.ΨSq n) (HPow.hPow (β := ℕ) n.natAbs 2 - 1) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
have nat : ∀ (n : ℕ),
  coeff (W.ΨSq (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1) =
    HPow.hPow (α := R) (β := ℕ) (↑(↑n : ℤ) : R) 2
Tactic: induction n using Int.negInduction with
  | nat n => exact_mod_cast (W.natDegree_coeff_ΨSq_ofNat n).right
  | neg ih => rw [ΨSq_neg, Int.natAbs_neg, ← Int.cast_pow, neg_sq, Int.cast_pow, 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 : ℤ
nat :
  ∀ (n : ℕ),
    coeff (W.ΨSq (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1) =
      HPow.hPow (α := R) (β := ℕ) (↑(↑n : ℤ) : R) 2
⊢ coeff (W.ΨSq n) (HPow.hPow (β := ℕ) n.natAbs 2 - 1) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
have neg : ∀
  (ih :
    ∀ (n : ℕ),
      coeff (W.ΨSq (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - 1) =
        HPow.hPow (α := R) (β := ℕ) (↑(↑n : ℤ) : R) 2)
  (n : ℕ),
  coeff (W.ΨSq (-(↑n : ℤ))) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - 1) =
    HPow.hPow (α := R) (β := ℕ) (↑(-(↑n : ℤ)) : R) 2
Tactic: induction n using Int.negInduction with
  | nat n => exact_mod_cast (W.natDegree_coeff_ΨSq_ofNat n).right
  | neg ih => rw [ΨSq_neg, Int.natAbs_neg, ← Int.cast_pow, neg_sq, Int.cast_pow, 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
inst_1 : NoZeroDivisors R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
⊢ leadingCoeff (W.ΨSq n) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
have rw : coeff (W.ΨSq n) (natDegree (W.ΨSq n)) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
Tactic: rw [leadingCoeff, W.natDegree_ΨSq h, coeff_ΨSq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : NoZeroDivisors R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
rw : coeff (W.ΨSq n) (natDegree (W.ΨSq n)) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
⊢ leadingCoeff (W.ΨSq n) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
have rw₁ : coeff (W.ΨSq n) (HPow.hPow (β := ℕ) n.natAbs 2 - 1) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
Tactic: rw [leadingCoeff, W.natDegree_ΨSq h, coeff_ΨSq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : NoZeroDivisors R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
rw : coeff (W.ΨSq n) (natDegree (W.ΨSq n)) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
rw₁ : coeff (W.ΨSq n) (HPow.hPow (β := ℕ) n.natAbs 2 - 1) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
⊢ leadingCoeff (W.ΨSq n) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
have rw₂ : HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
Tactic: rw [leadingCoeff, W.natDegree_ΨSq h, coeff_ΨSq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : NoZeroDivisors R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
⊢ Ne (α := R[X]) (W.ΨSq n) 0
have pos : ∀ (hn : 1 < n.natAbs), Ne (α := R[X]) (W.ΨSq n) 0
Tactic: by_cases hn : 1 < n.natAbs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : NoZeroDivisors R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
pos : ∀ (hn : 1 < n.natAbs), Ne (α := R[X]) (W.ΨSq n) 0
⊢ Ne (α := R[X]) (W.ΨSq n) 0
have neg : ∀ (hn : ¬1 < n.natAbs), Ne (α := R[X]) (W.ΨSq n) 0
Tactic: by_cases hn : 1 < n.natAbs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : NoZeroDivisors R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
hn : ¬1 < n.natAbs
⊢ Ne (α := R[X]) (W.ΨSq n) 0
have neg : ∀ (hm : n.natAbs = 0), Ne (α := R[X]) (W.ΨSq n) 0
Tactic: rcases hm : n.natAbs with _ | m
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : NoZeroDivisors R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
hn : ¬1 < n.natAbs
neg : ∀ (hm : n.natAbs = 0), Ne (α := R[X]) (W.ΨSq n) 0
⊢ Ne (α := R[X]) (W.ΨSq n) 0
have neg₁ : ∀ (m : ℕ) (hm : n.natAbs = m + 1), Ne (α := R[X]) (W.ΨSq n) 0
Tactic: rcases hm : n.natAbs with _ | m
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : NoZeroDivisors R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
hn : ¬1 < n.natAbs
m : ℕ
hm : n.natAbs = m + 1
⊢ Ne (α := R[X]) (W.ΨSq n) 0
have neg : ∀ (h : Ne.{u + 1} (α := R) (↑(↑(m + 1) : ℤ) : R) 0) (hn : ¬1 < Int.natAbs (↑(m + 1) : ℤ))
  (hm : Int.natAbs (↑(m + 1) : ℤ) = m + 1), Ne (α := R[X]) (W.ΨSq (↑(m + 1) : ℤ)) 0
Tactic: rcases Int.natAbs_eq_iff.mp hm with rfl | rfl
Cleared hypotheses: n, h, hn, hm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : NoZeroDivisors R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
hn : ¬1 < n.natAbs
m : ℕ
hm : n.natAbs = m + 1
neg :
  ∀ (h : Ne.{u + 1} (α := R) (↑(↑(m + 1) : ℤ) : R) 0) (hn : ¬1 < Int.natAbs (↑(m + 1) : ℤ))
    (hm : Int.natAbs (↑(m + 1) : ℤ) = m + 1), Ne (α := R[X]) (W.ΨSq (↑(m + 1) : ℤ)) 0
⊢ Ne (α := R[X]) (W.ΨSq n) 0
have neg₁ : ∀ (h : Ne.{u + 1} (α := R) (↑(-(↑(m + 1) : ℤ)) : R) 0) (hn : ¬1 < Int.natAbs (-(↑(m + 1) : ℤ)))
  (hm : Int.natAbs (-(↑(m + 1) : ℤ)) = m + 1), Ne (α := R[X]) (W.ΨSq (-(↑(m + 1) : ℤ))) 0
Tactic: rcases Int.natAbs_eq_iff.mp hm with rfl | rfl
Cleared hypotheses: n, h, hn, hm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (hypothesis)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : NoZeroDivisors R
m : ℕ
h : Ne.{u + 1} (α := R) (↑(↑(m + 1) : ℤ) : R) 0
hn : ¬1 < Int.natAbs (↑(m + 1) : ℤ)
hm : Int.natAbs (↑(m + 1) : ℤ) = m + 1
⊢ Ne (α := R[X]) (W.ΨSq (↑(m + 1) : ℤ)) 0
have hn₁ : m = 0
Tactic: rw [hm, Nat.lt_add_left_iff_pos, Nat.not_lt_eq, Nat.le_zero] at hn
Cleared hypotheses: hn, hm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (hypothesis)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : NoZeroDivisors R
m : ℕ
h : Ne.{u + 1} (α := R) (↑(-(↑(m + 1) : ℤ)) : R) 0
hn : ¬1 < Int.natAbs (-(↑(m + 1) : ℤ))
hm : Int.natAbs (-(↑(m + 1) : ℤ)) = m + 1
⊢ Ne (α := R[X]) (W.ΨSq (-(↑(m + 1) : ℤ))) 0
have hn₁ : m = 0
Tactic: rw [hm, Nat.lt_add_left_iff_pos, Nat.not_lt_eq, Nat.le_zero] at hn
Cleared hypotheses: hn, hm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : NoZeroDivisors R
m : ℕ
h : Ne.{u + 1} (α := R) (↑(↑(m + 1) : ℤ) : R) 0
hn : m = 0
hm : Int.natAbs (↑(m + 1) : ℤ) = m + 1
⊢ Ne (α := R[X]) (W.ΨSq (↑(m + 1) : ℤ)) 0
have neg : Ne.{u + 1} (α := R[X]) 1 0
Tactic: push_cast [hn, ΨSq_neg, ΨSq_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : NoZeroDivisors R
m : ℕ
h : Ne.{u + 1} (α := R) (↑(-(↑(m + 1) : ℤ)) : R) 0
hn : m = 0
hm : Int.natAbs (-(↑(m + 1) : ℤ)) = m + 1
⊢ Ne (α := R[X]) (W.ΨSq (-(↑(m + 1) : ℤ))) 0
have neg : Ne.{u + 1} (α := R[X]) 1 0
Tactic: push_cast [hn, ΨSq_neg, ΨSq_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : NoZeroDivisors R
m : ℕ
h : Ne.{u + 1} (α := R) (↑(↑(m + 1) : ℤ) : R) 0
hn : m = 0
hm : Int.natAbs (↑(m + 1) : ℤ) = m + 1
h' : Eq.{u + 1} (α := R[X]) 1 0
⊢ Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑(↑(m + 1) : ℤ) : R)) ((C : (a : R) → R[X]) 0)
have push_cast : Eq.{u + 1} (α := R[X]) 0 0
Tactic: push_cast [hn, C_neg, C_1, h', neg_zero, C_0]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : NoZeroDivisors R
m : ℕ
h : Ne.{u + 1} (α := R) (↑(-(↑(m + 1) : ℤ)) : R) 0
hn : m = 0
hm : Int.natAbs (-(↑(m + 1) : ℤ)) = m + 1
h' : Eq.{u + 1} (α := R[X]) 1 0
⊢ Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑(-(↑(m + 1) : ℤ)) : R)) ((C : (a : R) → R[X]) 0)
have push_cast : Eq.{u + 1} (α := R[X]) 0 0
Tactic: push_cast [hn, C_neg, C_1, h', neg_zero, C_0]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
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) := ⋯
⊢ natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) n 2 ∧ coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) n 2) = 1
have zero : natDegree (W.Φ (↑0 : ℤ)) ≤ HPow.hPow (α := ℕ) (β := ℕ) 0 2 ∧ coeff (W.Φ (↑0 : ℤ)) (HPow.hPow (α := ℕ) (β := ℕ) 0 2) = 1
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 : ℕ
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) := ⋯
zero :
  natDegree (W.Φ (↑0 : ℤ)) ≤ HPow.hPow (α := ℕ) (β := ℕ) 0 2 ∧
    coeff (W.Φ (↑0 : ℤ)) (HPow.hPow (α := ℕ) (β := ℕ) 0 2) = 1
⊢ natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) n 2 ∧ coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) n 2) = 1
have succ : natDegree (W.Φ (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) ≤ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℕ) 0 1) 2 ∧
  coeff (W.Φ (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℕ) 0 1) 2) = 1
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 : ℕ
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) := ⋯
zero :
  natDegree (W.Φ (↑0 : ℤ)) ≤ HPow.hPow (α := ℕ) (β := ℕ) 0 2 ∧
    coeff (W.Φ (↑0 : ℤ)) (HPow.hPow (α := ℕ) (β := ℕ) 0 2) = 1
succ :
  natDegree (W.Φ (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) ≤ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℕ) 0 1) 2 ∧
    coeff (W.Φ (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℕ) 0 1) 2) = 1
⊢ natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) n 2 ∧ coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) n 2) = 1
have succ₁ : ∀ (n : ℕ),
  natDegree (W.Φ (↑(n + 1 + 1) : ℤ)) ≤ HPow.hPow (β := ℕ) (n + 1 + 1) 2 ∧
    coeff (W.Φ (↑(n + 1 + 1) : ℤ)) (HPow.hPow (β := ℕ) (n + 1 + 1) 2) = 1
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
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 : ℕ
⊢ HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
have push_cast : HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
  1 + (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 - if Even n then 4 else 1) + if Even n then 3 else 0
Tactic: push_cast [← @Nat.cast_inj ℤ, expDegree_cast (n + 1).succ_ne_zero, Nat.even_add_one, ite_not]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
⊢ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
    1 + (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 - if Even n then 4 else 1) + if Even n then 3 else 0
have pos : Even n →
  HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
    1 + (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 - 4) + 3
Tactic: split_ifs