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 : ℕ
⊢ coeff (W.preΨ' n) ((HPow.hPow (β := ℕ) n 2 - if Even n then 4 else 1) / 2) = (↑(if Even n then n / 2 else n) : R)
have h : Eq.{u + 1} (α := R) (↑(if Even n then n / 2 else n) : R) (↑(expCoeff n) : R)
Tactic: convert! (W.natDegree_coeff_preΨ' n).right using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ Eq.{u + 1} (α := R) (↑(if Even n then n / 2 else n) : R) (↑(expCoeff n) : R)
have h : ∀ (n : ℕ), Eq.{u + 1} (α := R) (↑(if Even (2 * n) then 2 * n / 2 else 2 * n) : R) (↑(expCoeff (2 * n)) : R)
Tactic: rcases n.even_or_odd' with ⟨n, rfl | rfl⟩
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 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (↑(if Even (2 * n) then 2 * n / 2 else 2 * n) : R) (↑(expCoeff (2 * n)) : R)
⊢ Eq.{u + 1} (α := R) (↑(if Even n then n / 2 else n) : R) (↑(expCoeff n) : R)
have h₁ : ∀ (n : ℕ),
  Eq.{u + 1} (α := R) (↑(if Even (2 * n + 1) then (2 * n + 1) / 2 else 2 * n + 1) : R) (↑(expCoeff (2 * n + 1)) : R)
Tactic: rcases n.even_or_odd' with ⟨n, rfl | rfl⟩
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 2 - if Even n then 4 else 1) / 2) ≠ 0
have inl : ∀ (n : ℕ) (h : Ne.{u + 1} (α := R) (↑(2 * n) : R) 0),
  coeff (W.preΨ' (2 * n)) ((HPow.hPow (β := ℕ) (2 * n) 2 - if Even (2 * n) then 4 else 1) / 2) ≠ 0
Tactic: rcases n.even_or_odd' with ⟨n, rfl | rfl⟩
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
inl :
  ∀ (n : ℕ) (h : Ne.{u + 1} (α := R) (↑(2 * n) : R) 0),
    coeff (W.preΨ' (2 * n)) ((HPow.hPow (β := ℕ) (2 * n) 2 - if Even (2 * n) then 4 else 1) / 2) ≠ 0
⊢ coeff (W.preΨ' n) ((HPow.hPow (β := ℕ) n 2 - if Even n then 4 else 1) / 2) ≠ 0
have inr : ∀ (n : ℕ) (h : Ne.{u + 1} (α := R) (↑(2 * n + 1) : R) 0),
  coeff (W.preΨ' (2 * n + 1)) ((HPow.hPow (β := ℕ) (2 * n + 1) 2 - if Even (2 * n + 1) then 4 else 1) / 2) ≠ 0
Tactic: rcases n.even_or_odd' with ⟨n, rfl | rfl⟩
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) (↑(2 * n) : R) 0
⊢ coeff (W.preΨ' (2 * n)) ((HPow.hPow (β := ℕ) (2 * n) 2 - if Even (2 * n) then 4 else 1) / 2) ≠ 0
have inl : Ne.{u + 1} (α := R) (↑n : R) 0
Tactic: rw [coeff_preΨ', if_pos <| even_two_mul n, n.mul_div_cancel_left two_pos]
-- 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) (↑(2 * n + 1) : R) 0
⊢ coeff (W.preΨ' (2 * n + 1)) ((HPow.hPow (β := ℕ) (2 * n + 1) 2 - if Even (2 * n + 1) then 4 else 1) / 2) ≠ 0
have inr : Ne.{u + 1} (α := R) (↑(if Even (2 * n + 1) then (2 * n + 1) / 2 else 2 * n + 1) : R) 0
Tactic: rwa [coeff_preΨ', if_neg n.not_even_two_mul_add_one]
-- 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
h : Ne.{u + 1} (α := R) (↑n : R) 0
⊢ 0 < natDegree (W.preΨ' n)
have simp_rw : 2 ≤ HPow.hPow (β := ℕ) n 2 - if Even n then 4 else 1
Tactic: simp_rw [W.natDegree_preΨ' h, Nat.div_pos_iff, zero_lt_two, true_and]
-- 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
h : Ne.{u + 1} (α := R) (↑n : R) 0
⊢ 2 ≤ HPow.hPow (β := ℕ) n 2 - if Even n then 4 else 1
have pos : Even n → 2 ≤ HPow.hPow (β := ℕ) n 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
n : ℕ
hn : 2 < n
h : Ne.{u + 1} (α := R) (↑n : R) 0
pos : Even n → 2 ≤ HPow.hPow (β := ℕ) n 2 - 4
⊢ 2 ≤ HPow.hPow (β := ℕ) n 2 - if Even n then 4 else 1
have neg : ¬Even n → 2 ≤ HPow.hPow (β := ℕ) n 2 - 1
Tactic: split_ifs
-- 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 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 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 pos : ∀ (hn : 2 < n), Ne (α := R[X]) (W.preΨ' n) 0
Tactic: by_cases hn : 2 < n
-- 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
pos : ∀ (hn : 2 < n), Ne (α := R[X]) (W.preΨ' n) 0
⊢ Ne (α := R[X]) (W.preΨ' n) 0
have neg : ∀ (hn : ¬2 < n), Ne (α := R[X]) (W.preΨ' n) 0
Tactic: by_cases hn : 2 < n
-- 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
hn : ¬2 < n
⊢ Ne (α := R[X]) (W.preΨ' n) 0
have neg : ∀ (h : Ne.{u + 1} (α := R) (↑0 : R) 0) (hn : ¬LT.lt (α := ℕ) 2 0), Ne (α := R[X]) (W.preΨ' 0) 0
Tactic: rcases n with _ | _ | _
Cleared hypotheses: n, h, hn
-- 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
hn : ¬2 < n
neg : ∀ (h : Ne.{u + 1} (α := R) (↑0 : R) 0) (hn : ¬LT.lt (α := ℕ) 2 0), Ne (α := R[X]) (W.preΨ' 0) 0
⊢ Ne (α := R[X]) (W.preΨ' n) 0
have neg₁ : ∀ (h : Ne.{u + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 0 1) : R) 0) (hn : ¬2 < HAdd.hAdd (α := ℕ) 0 1),
  Ne (α := R[X]) (W.preΨ' (HAdd.hAdd (α := ℕ) 0 1)) 0
Tactic: rcases n with _ | _ | _
Cleared hypotheses: n, h, hn
-- 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
hn : ¬2 < n
neg : ∀ (h : Ne.{u + 1} (α := R) (↑0 : R) 0) (hn : ¬LT.lt (α := ℕ) 2 0), Ne (α := R[X]) (W.preΨ' 0) 0
neg₁ :
  ∀ (h : Ne.{u + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 0 1) : R) 0) (hn : ¬2 < HAdd.hAdd (α := ℕ) 0 1),
    Ne (α := R[X]) (W.preΨ' (HAdd.hAdd (α := ℕ) 0 1)) 0
⊢ Ne (α := R[X]) (W.preΨ' n) 0
have neg₂ : ∀ (n : ℕ) (h : Ne.{u + 1} (α := R) (↑(n + 1 + 1) : R) 0) (hn : ¬2 < n + 1 + 1), Ne (α := R[X]) (W.preΨ' (n + 1 + 1)) 0
Tactic: rcases n with _ | _ | _
Cleared hypotheses: n, h, hn
-- 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.preΨ (↑n : ℤ)) ≤
      (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - if Even (α := ℤ) (↑n : ℤ) then 4 else 1) / 2
n : ℕ
⊢ natDegree (W.preΨ (-(↑n : ℤ))) ≤
    (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - if Even (α := ℤ) (-(↑n : ℤ)) then 4 else 1) / 2
have neg : natDegree (-W.preΨ (↑n : ℤ)) ≤
  (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - if Even (α := ℤ) (-(↑n : ℤ)) then 4 else 1) / 2
Tactic: simp_rw [preΨ_neg, natDegree_neg, Int.natAbs_neg, even_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.preΨ (↑n : ℤ)) ≤
      (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - if Even (α := ℤ) (↑n : ℤ) then 4 else 1) / 2
n : ℕ
neg :
  natDegree (-W.preΨ (↑n : ℤ)) ≤
    (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - if Even (α := ℤ) (-(↑n : ℤ)) then 4 else 1) / 2
⊢ natDegree (W.preΨ (-(↑n : ℤ))) ≤
    (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - if Even (α := ℤ) (-(↑n : ℤ)) then 4 else 1) / 2
have neg₁ : natDegree (W.preΨ (↑n : ℤ)) ≤
  (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - if Even (α := ℤ) (-(↑n : ℤ)) then 4 else 1) / 2
Tactic: simp_rw [preΨ_neg, natDegree_neg, Int.natAbs_neg, even_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.preΨ (↑n : ℤ)) ≤
      (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - if Even (α := ℤ) (↑n : ℤ) then 4 else 1) / 2
n : ℕ
neg :
  natDegree (-W.preΨ (↑n : ℤ)) ≤
    (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - if Even (α := ℤ) (-(↑n : ℤ)) then 4 else 1) / 2
neg₁ :
  natDegree (W.preΨ (↑n : ℤ)) ≤
    (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - if Even (α := ℤ) (-(↑n : ℤ)) then 4 else 1) / 2
⊢ natDegree (W.preΨ (-(↑n : ℤ))) ≤
    (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - if Even (α := ℤ) (-(↑n : ℤ)) then 4 else 1) / 2
have neg₂ : natDegree (W.preΨ (↑n : ℤ)) ≤
  (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - if Even (α := ℤ) (-(↑n : ℤ)) then 4 else 1) / 2
Tactic: simp_rw [preΨ_neg, natDegree_neg, Int.natAbs_neg, even_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.preΨ (↑n : ℤ)) ≤
      (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - if Even (α := ℤ) (↑n : ℤ) then 4 else 1) / 2
n : ℕ
neg :
  natDegree (-W.preΨ (↑n : ℤ)) ≤
    (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - if Even (α := ℤ) (-(↑n : ℤ)) then 4 else 1) / 2
neg₁ :
  natDegree (W.preΨ (↑n : ℤ)) ≤
    (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - if Even (α := ℤ) (-(↑n : ℤ)) then 4 else 1) / 2
neg₂ :
  natDegree (W.preΨ (↑n : ℤ)) ≤
    (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - if Even (α := ℤ) (-(↑n : ℤ)) then 4 else 1) / 2
⊢ natDegree (W.preΨ (-(↑n : ℤ))) ≤
    (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - if Even (α := ℤ) (-(↑n : ℤ)) then 4 else 1) / 2
have neg₃ : natDegree (W.preΨ (↑n : ℤ)) ≤ (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - if Even (α := ℤ) (↑n : ℤ) then 4 else 1) / 2
Tactic: simp_rw [preΨ_neg, natDegree_neg, Int.natAbs_neg, even_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.preΨ n) ≤ (HPow.hPow (β := ℕ) n.natAbs 2 - if Even n then 4 else 1) / 2
have nat : ∀ (n : ℕ),
  natDegree (W.preΨ (↑n : ℤ)) ≤
    (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - if Even (α := ℤ) (↑n : ℤ) then 4 else 1) / 2
Tactic: induction n using Int.negInduction with
  | nat n => exact_mod_cast W.preΨ_ofNat n ▸ W.natDegree_preΨ'_le n
  | neg ih => simp_rw [preΨ_neg, natDegree_neg, Int.natAbs_neg, even_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.preΨ (↑n : ℤ)) ≤
      (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - if Even (α := ℤ) (↑n : ℤ) then 4 else 1) / 2
⊢ natDegree (W.preΨ n) ≤ (HPow.hPow (β := ℕ) n.natAbs 2 - if Even n then 4 else 1) / 2
have neg : ∀
  (ih :
    ∀ (n : ℕ),
      natDegree (W.preΨ (↑n : ℤ)) ≤
        (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - if Even (α := ℤ) (↑n : ℤ) then 4 else 1) / 2)
  (n : ℕ),
  natDegree (W.preΨ (-(↑n : ℤ))) ≤
    (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2 - if Even (α := ℤ) (-(↑n : ℤ)) then 4 else 1) / 2
Tactic: induction n using Int.negInduction with
  | nat n => exact_mod_cast W.preΨ_ofNat n ▸ W.natDegree_preΨ'_le n
  | neg ih => simp_rw [preΨ_neg, natDegree_neg, Int.natAbs_neg, even_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.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)
have neg : -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: simp_rw [preΨ_neg, coeff_neg, Int.natAbs_neg, even_neg]
-- 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.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)
have neg : ∀ (n : ℕ)
  (ih :
    coeff (W.preΨ (↑(2 * n) : ℤ))
        ((HPow.hPow (β := ℕ) (Int.natAbs (↑(2 * n) : ℤ)) 2 - if Even (α := ℤ) (↑(2 * n) : ℤ) then 4 else 1) / 2) =
      (↑(if Even (α := ℤ) (↑(2 * n) : ℤ) then HDiv.hDiv (α := ℤ) (↑(2 * n) : ℤ) 2 else (↑(2 * n) : ℤ)) : R)),
  -coeff (W.preΨ (↑(2 * n) : ℤ))
        ((HPow.hPow (β := ℕ) (Int.natAbs (↑(2 * n) : ℤ)) 2 - if Even (α := ℤ) (↑(2 * n) : ℤ) then 4 else 1) / 2) =
    (↑(if Even (α := ℤ) (↑(2 * n) : ℤ) then HDiv.hDiv (α := ℤ) (-(↑(2 * n) : ℤ)) 2 else -(↑(2 * n) : ℤ)) : R)
Tactic: rcases ih n, n.even_or_odd' with ⟨ih, ⟨n, rfl | rfl⟩⟩
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.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 : ℕ
neg :
  ∀ (n : ℕ)
    (ih :
      coeff (W.preΨ (↑(2 * n) : ℤ))
          ((HPow.hPow (β := ℕ) (Int.natAbs (↑(2 * n) : ℤ)) 2 - if Even (α := ℤ) (↑(2 * n) : ℤ) then 4 else 1) / 2) =
        (↑(if Even (α := ℤ) (↑(2 * n) : ℤ) then HDiv.hDiv (α := ℤ) (↑(2 * n) : ℤ) 2 else (↑(2 * n) : ℤ)) : R)),
    -coeff (W.preΨ (↑(2 * n) : ℤ))
          ((HPow.hPow (β := ℕ) (Int.natAbs (↑(2 * n) : ℤ)) 2 - if Even (α := ℤ) (↑(2 * n) : ℤ) then 4 else 1) / 2) =
      (↑(if Even (α := ℤ) (↑(2 * n) : ℤ) then HDiv.hDiv (α := ℤ) (-(↑(2 * n) : ℤ)) 2 else -(↑(2 * n) : ℤ)) : R)
⊢ -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)
have neg₁ : ∀ (n : ℕ)
  (ih :
    coeff (W.preΨ (↑(2 * n + 1) : ℤ))
        ((HPow.hPow (β := ℕ) (Int.natAbs (↑(2 * n + 1) : ℤ)) 2 - if Even (α := ℤ) (↑(2 * n + 1) : ℤ) then 4 else 1) /
          2) =
      (↑(if Even (α := ℤ) (↑(2 * n + 1) : ℤ) then HDiv.hDiv (α := ℤ) (↑(2 * n + 1) : ℤ) 2 else (↑(2 * n + 1) : ℤ)) :
        R)),
  -coeff (W.preΨ (↑(2 * n + 1) : ℤ))
        ((HPow.hPow (β := ℕ) (Int.natAbs (↑(2 * n + 1) : ℤ)) 2 - if Even (α := ℤ) (↑(2 * n + 1) : ℤ) then 4 else 1) /
          2) =
    (↑(if Even (α := ℤ) (↑(2 * n + 1) : ℤ) then HDiv.hDiv (α := ℤ) (-(↑(2 * n + 1) : ℤ)) 2 else -(↑(2 * n + 1) : ℤ)) :
      R)
Tactic: rcases ih n, n.even_or_odd' with ⟨ih, ⟨n, rfl | rfl⟩⟩
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_1 :
  ∀ (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 : ℕ
ih :
  coeff (W.preΨ (↑(2 * n) : ℤ))
      ((HPow.hPow (β := ℕ) (Int.natAbs (↑(2 * n) : ℤ)) 2 - if Even (α := ℤ) (↑(2 * n) : ℤ) then 4 else 1) / 2) =
    (↑(if Even (α := ℤ) (↑(2 * n) : ℤ) then HDiv.hDiv (α := ℤ) (↑(2 * n) : ℤ) 2 else (↑(2 * n) : ℤ)) : R)
⊢ -coeff (W.preΨ (↑(2 * n) : ℤ))
        ((HPow.hPow (β := ℕ) (Int.natAbs (↑(2 * n) : ℤ)) 2 - if Even (α := ℤ) (↑(2 * n) : ℤ) then 4 else 1) / 2) =
    (↑(if Even (α := ℤ) (↑(2 * n) : ℤ) then HDiv.hDiv (α := ℤ) (-(↑(2 * n) : ℤ)) 2 else -(↑(2 * 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) : R) else (↑n : R))
  (ih :
    coeff (W.preΨ (HMul.hMul (α := ℤ) 2 (↑n : ℤ)))
        ((HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑n : ℤ)).natAbs 2 - 4) / 2) =
      (↑(HMul.hMul (α := ℤ) 2 (↑n : ℤ) / 2) : R)),
  -coeff (W.preΨ (HMul.hMul (α := ℤ) 2 (↑n : ℤ)))
        ((HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑n : ℤ)).natAbs 2 - 4) / 2) =
    -(↑(HMul.hMul (α := ℤ) 2 (↑n : ℤ) / 2) : R)
Tactic: push_cast [even_two_mul, Int.not_even_two_mul_add_one, Int.neg_ediv_of_dvd ⟨n, rfl⟩] at *
Cleared hypotheses: ih_1, ih
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
ih_1 :
  ∀ (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 : ℕ
ih :
  coeff (W.preΨ (↑(2 * n + 1) : ℤ))
      ((HPow.hPow (β := ℕ) (Int.natAbs (↑(2 * n + 1) : ℤ)) 2 - if Even (α := ℤ) (↑(2 * n + 1) : ℤ) then 4 else 1) / 2) =
    (↑(if Even (α := ℤ) (↑(2 * n + 1) : ℤ) then HDiv.hDiv (α := ℤ) (↑(2 * n + 1) : ℤ) 2 else (↑(2 * n + 1) : ℤ)) : R)
⊢ -coeff (W.preΨ (↑(2 * n + 1) : ℤ))
        ((HPow.hPow (β := ℕ) (Int.natAbs (↑(2 * n + 1) : ℤ)) 2 - if Even (α := ℤ) (↑(2 * n + 1) : ℤ) then 4 else 1) /
          2) =
    (↑(if Even (α := ℤ) (↑(2 * n + 1) : ℤ) then HDiv.hDiv (α := ℤ) (-(↑(2 * n + 1) : ℤ)) 2 else -(↑(2 * n + 1) : ℤ)) :
      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) : R) else (↑n : R))
  (ih :
    coeff (W.preΨ (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1))
        ((HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1).natAbs 2 - 1) / 2) =
      HMul.hMul (α := R) 2 (↑n : R) + 1),
  -coeff (W.preΨ (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1))
        ((HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1).natAbs 2 - 1) / 2) =
    -(HMul.hMul (α := R) 2 (↑n : R) + 1)
Tactic: push_cast [even_two_mul, Int.not_even_two_mul_add_one, Int.neg_ediv_of_dvd ⟨n, rfl⟩] at *
Cleared hypotheses: ih_1, ih
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
ih_1 :
  ∀ (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) : R) else (↑n : R)
ih :
  coeff (W.preΨ (HMul.hMul (α := ℤ) 2 (↑n : ℤ)))
      ((HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑n : ℤ)).natAbs 2 - 4) / 2) =
    (↑(HMul.hMul (α := ℤ) 2 (↑n : ℤ) / 2) : R)
⊢ -coeff (W.preΨ (HMul.hMul (α := ℤ) 2 (↑n : ℤ)))
        ((HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑n : ℤ)).natAbs 2 - 4) / 2) =
    -(↑(HMul.hMul (α := ℤ) 2 (↑n : ℤ) / 2) : R)
have neg : Eq.{u + 1} (α := R) (-(↑(HMul.hMul (α := ℤ) 2 (↑n : ℤ) / 2) : R)) (-(↑(HMul.hMul (α := ℤ) 2 (↑n : ℤ) / 2) : R))
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
ih_1 :
  ∀ (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) : R) else (↑n : R)
ih :
  coeff (W.preΨ (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1))
      ((HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1).natAbs 2 - 1) / 2) =
    HMul.hMul (α := R) 2 (↑n : R) + 1
⊢ -coeff (W.preΨ (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1))
        ((HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1).natAbs 2 - 1) / 2) =
    -(HMul.hMul (α := R) 2 (↑n : R) + 1)
have neg : -(HMul.hMul (α := R) 2 (↑n : R) + 1) = -(HMul.hMul (α := R) 2 (↑n : R) + 1)
Tactic: rw [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.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 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)
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