awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : Ne.{u + 1} (α := R) (↑n : R) 0
h_1 : ¬Even n
⊢ 2 ≤ HPow.hPow (β := ℕ) n 2 - 1

Tactic:
exact Nat.AtLeastTwo.prop.trans <| Nat.sub_le_sub_right (Nat.pow_le_pow_left hn 2) _

Premises used: Nat.AtLeastTwo.prop, Nat.sub_le_sub_right, LE.le.trans, OfNat.ofNat, Nat.pow_le_pow_left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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)
rw₂ rw₃ : Eq.{u + 1} (α := R) (↑(if Even n then n / 2 else n) : R) (↑(if Even n then n / 2 else n) : R)
⊢ leadingCoeff (W.preΨ' n) = (↑(if Even n then n / 2 else n) : R)

Tactic:
rw [leadingCoeff, W.natDegree_preΨ' h, coeff_preΨ']

Premises used: WeierstrassCurve.coeff_preΨ', Polynomial.leadingCoeff, WeierstrassCurve.natDegree_preΨ'
-- 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
pos : ∀ (hn : 2 < n), Ne (α := R[X]) (W.preΨ' n) 0
neg : ∀ (hn : ¬2 < n), Ne (α := R[X]) (W.preΨ' n) 0
⊢ Ne (α := R[X]) (W.preΨ' n) 0

Tactic:
by_cases hn : 2 < n
-- 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
hn : 2 < n
⊢ Ne (α := R[X]) (W.preΨ' n) 0

Tactic:
ne_zero_of_natDegree_gt <| W.natDegree_preΨ'_pos hn h

Premises used: WeierstrassCurve.natDegree_preΨ'_pos, Polynomial.ne_zero_of_natDegree_gt
-- 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
hn : 2 < n
⊢ Ne (α := R[X]) (W.preΨ' n) 0

Tactic:
exact ne_zero_of_natDegree_gt <| W.natDegree_preΨ'_pos hn h

Premises used: WeierstrassCurve.natDegree_preΨ'_pos, Polynomial.ne_zero_of_natDegree_gt
-- 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
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
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
⊢ Ne (α := R[X]) (W.preΨ' n) 0

Tactic:
rcases n with _ | _ | _
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
h : Ne.{u + 1} (α := R) (↑0 : R) 0
hn : ¬LT.lt (α := ℕ) 2 0
⊢ Ne (α := R[X]) (W.preΨ' 0) 0

Tactic:
aesop
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
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:
aesop
-- 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 + 1 + 1) : R) 0
hn : ¬2 < n + 1 + 1
⊢ Ne (α := R[X]) (W.preΨ' (n + 1 + 1)) 0

Tactic:
aesop
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ natDegree (W.preΨ (↑n : ℤ)) ≤
    (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2 - if Even (α := ℤ) (↑n : ℤ) then 4 else 1) / 2

Tactic:
exact_mod_cast W.preΨ_ofNat n ▸ W.natDegree_preΨ'_le n
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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

Tactic:
simp_rw [preΨ_neg, natDegree_neg, Int.natAbs_neg, even_neg, ih]

Premises used: WeierstrassCurve.preΨ_neg, Polynomial.natDegree_neg, Int.natAbs_neg, even_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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
⊢ natDegree (W.preΨ n) ≤ (HPow.hPow (β := ℕ) n.natAbs 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]

Premises used: WeierstrassCurve.preΨ_neg, Polynomial.natDegree_neg, Int.natAbs_neg, even_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve 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:
exact_mod_cast W.preΨ_ofNat n ▸ W.coeff_preΨ' n
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 :
  -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 (β := ℕ) (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]

Premises used: WeierstrassCurve.preΨ_neg, Polynomial.coeff_neg, Int.natAbs_neg, even_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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)
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)
⊢ -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:
rcases ih n, n.even_or_odd' with ⟨ih, ⟨n, rfl | rfl⟩⟩

Premises used: Nat.even_or_odd', rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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)
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)
⊢ -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:
push_cast [even_two_mul, Int.not_even_two_mul_add_one, Int.neg_ediv_of_dvd ⟨n, rfl⟩] at *

Premises used: Int.not_even_two_mul_add_one, Nat.cast, even_two_mul, Exists.intro, Int.neg_ediv_of_dvd, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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)
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)
⊢ -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:
push_cast [even_two_mul, Int.not_even_two_mul_add_one, Int.neg_ediv_of_dvd ⟨n, rfl⟩] at *

Premises used: Int.not_even_two_mul_add_one, Nat.cast, even_two_mul, Exists.intro, Int.neg_ediv_of_dvd, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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)
neg neg₁ :
  Eq.{u + 1} (α := R) (-(↑(HMul.hMul (α := ℤ) 2 (↑n : ℤ) / 2) : R)) (-(↑(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:
rw [ih]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
neg neg₁ : -(HMul.hMul (α := R) 2 (↑n : R) + 1) = -(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:
rw [ih]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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)
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)
⊢ 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:
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]

Premises used: Int.not_even_two_mul_add_one, even_two_mul, Int.even_or_odd', WeierstrassCurve.preΨ_neg, Exists.intro, Polynomial.coeff_neg, Int.natAbs_neg, Int.neg_ediv_of_dvd, even_neg, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve 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
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:
simpa only [preΨ_ofNat, Int.even_coe_nat]
      using W.coeff_preΨ'_ne_zero <| by exact_mod_cast h

Premises used: WeierstrassCurve.preΨ_ofNat, WeierstrassCurve.coeff_preΨ'_ne_zero, Int.even_coe_nat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
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
⊢ 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
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:
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

Premises used: WeierstrassCurve.preΨ_neg, Iff.mp, Polynomial.coeff_neg, neg_ne_zero, Int.natAbs_neg, even_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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
⊢ coeff (W.preΨ n) ((HPow.hPow (β := ℕ) n.natAbs 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

Premises used: WeierstrassCurve.preΨ_ofNat, WeierstrassCurve.preΨ_neg, Iff.mp, Polynomial.coeff_neg, neg_ne_zero, Int.natAbs_neg, even_neg, WeierstrassCurve.coeff_preΨ'_ne_zero, Int.even_coe_nat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
⊢ natDegree (W.preΨ n) = (HPow.hPow (β := ℕ) n.natAbs 2 - if Even n then 4 else 1) / 2

Tactic:
natDegree_eq_of_le_of_coeff_ne_zero (W.natDegree_preΨ_le n) <| W.coeff_preΨ_ne_zero h

Premises used: WeierstrassCurve.natDegree_preΨ_le, WeierstrassCurve.coeff_preΨ_ne_zero, Polynomial.natDegree_eq_of_le_of_coeff_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < Int.natAbs (↑n : ℤ)
h : Ne.{u + 1} (α := R) (↑(↑n : ℤ) : R) 0
⊢ Ne.{u + 1} (α := R) (↑(Int.natAbs (↑n : ℤ)) : R) 0

Tactic:
exact_mod_cast h
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < Int.natAbs (↑n : ℤ)
h : Ne.{u + 1} (α := R) (↑(↑n : ℤ) : R) 0
⊢ 0 < natDegree (W.preΨ (↑n : ℤ))

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

Premises used: WeierstrassCurve.natDegree_preΨ'_pos, WeierstrassCurve.preΨ_ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
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
rwa rwa₁ rwa₂ rwa₃ : 2 < Int.natAbs (-(↑n : ℤ))
⊢ 2 < Int.natAbs (↑n : ℤ)

Tactic:
rwa [← Int.natAbs_neg]

Premises used: Int.natAbs_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
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
⊢ 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
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:
simpa only [preΨ_neg, natDegree_neg]
        using ih n (by rwa [← Int.natAbs_neg]) <| neg_ne_zero.mp <| by exact_mod_cast h

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

Premises used: WeierstrassCurve.natDegree_preΨ'_pos, WeierstrassCurve.preΨ_ofNat, WeierstrassCurve.preΨ_neg, Iff.mp, neg_ne_zero, Polynomial.natDegree_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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)
rw₂ rw₃ : Eq.{u + 1} (α := R) (↑(if Even n then n / 2 else n) : R) (↑(if Even n then n / 2 else n) : R)
⊢ leadingCoeff (W.preΨ n) = (↑(if Even n then n / 2 else n) : R)

Tactic:
rw [leadingCoeff, W.natDegree_preΨ h, coeff_preΨ]

Premises used: WeierstrassCurve.coeff_preΨ, Polynomial.leadingCoeff, WeierstrassCurve.natDegree_preΨ