awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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
⊢ coeff (W.ΨSq n) (HPow.hPow (β := ℕ) n.natAbs 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]

Premises used: Int.cast_pow, neg_sq, WeierstrassCurve.ΨSq_neg, Int.natAbs_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : NoZeroDivisors R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
⊢ coeff (W.ΨSq n) (HPow.hPow (β := ℕ) n.natAbs 2 - 1) ≠ 0

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : NoZeroDivisors R
n : ℤ
h : Ne.{u + 1} (α := R) (↑n : R) 0
⊢ natDegree (W.ΨSq n) = HPow.hPow (β := ℕ) n.natAbs 2 - 1

Tactic:
natDegree_eq_of_le_of_coeff_ne_zero (W.natDegree_ΨSq_le n) <| W.coeff_ΨSq_ne_zero h

Premises used: WeierstrassCurve.coeff_ΨSq_ne_zero, WeierstrassCurve.natDegree_ΨSq_le, 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
inst_1 : NoZeroDivisors R
n : ℤ
hn : 1 < n.natAbs
h : Ne.{u + 1} (α := R) (↑n : R) 0
⊢ 0 < natDegree (W.ΨSq n)

Tactic:
simpa [W.natDegree_ΨSq h]

Premises used: WeierstrassCurve.natDegree_ΨSq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
rw₂ rw₃ : HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
⊢ leadingCoeff (W.ΨSq n) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2

Tactic:
rw [leadingCoeff, W.natDegree_ΨSq h, coeff_ΨSq]

Premises used: WeierstrassCurve.natDegree_ΨSq, Polynomial.leadingCoeff, WeierstrassCurve.coeff_ΨSq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
neg : ∀ (hn : ¬1 < n.natAbs), Ne (α := R[X]) (W.ΨSq n) 0
⊢ Ne (α := R[X]) (W.ΨSq n) 0

Tactic:
by_cases hn : 1 < n.natAbs

Premises used: Int.natAbs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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

Tactic:
ne_zero_of_natDegree_gt <| W.natDegree_ΨSq_pos hn h

Premises used: Polynomial.ne_zero_of_natDegree_gt, WeierstrassCurve.natDegree_ΨSq_pos
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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

Tactic:
exact ne_zero_of_natDegree_gt <| W.natDegree_ΨSq_pos hn h

Premises used: Polynomial.ne_zero_of_natDegree_gt, WeierstrassCurve.natDegree_ΨSq_pos
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
neg₁ : ∀ (m : ℕ) (hm : n.natAbs = m + 1), Ne (α := R[X]) (W.ΨSq n) 0
⊢ Ne (α := R[X]) (W.ΨSq n) 0

Tactic:
rcases hm : n.natAbs with _ | m

Premises used: Int.natAbs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
hm : n.natAbs = 0
⊢ Ne (α := R[X]) (W.ΨSq n) 0

Tactic:
push_cast [Int.natAbs_eq_zero.mp hm, ne_self_iff_false] at h

Premises used: ne_self_iff_false, Int.natAbs_eq_zero, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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

Tactic:
rcases Int.natAbs_eq_iff.mp hm with rfl | rfl

Premises used: Int.natAbs_eq_iff, Iff.mp, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
⊢ m = 0

Tactic:
rw [hm, Nat.lt_add_left_iff_pos, Nat.not_lt_eq, Nat.le_zero] at hn

Premises used: Nat.le_zero, Nat.lt_add_left_iff_pos, Nat.not_lt_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
hn₁ : m = 0
⊢ Int.natAbs (↑(m + 1) : ℤ) = m + 1

Tactic:
rw [hm, Nat.lt_add_left_iff_pos, Nat.not_lt_eq, Nat.le_zero] at hn

Premises used: Nat.le_zero, Nat.lt_add_left_iff_pos, Nat.not_lt_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
⊢ m = 0

Tactic:
rw [hm, Nat.lt_add_left_iff_pos, Nat.not_lt_eq, Nat.le_zero] at hn

Premises used: Nat.le_zero, Nat.lt_add_left_iff_pos, Nat.not_lt_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
hn₁ : m = 0
⊢ Int.natAbs (-(↑(m + 1) : ℤ)) = m + 1

Tactic:
rw [hm, Nat.lt_add_left_iff_pos, Nat.not_lt_eq, Nat.le_zero] at hn

Premises used: Nat.le_zero, Nat.lt_add_left_iff_pos, Nat.not_lt_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
neg : Ne.{u + 1} (α := R[X]) 1 0
⊢ Ne (α := R[X]) (W.ΨSq (↑(m + 1) : ℤ)) 0

Tactic:
push_cast [hn, ΨSq_neg, ΨSq_one]

Premises used: WeierstrassCurve.ΨSq_one, WeierstrassCurve.ΨSq_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
neg : Ne.{u + 1} (α := R[X]) 1 0
⊢ Ne (α := R[X]) (W.ΨSq (-(↑(m + 1) : ℤ))) 0

Tactic:
push_cast [hn, ΨSq_neg, ΨSq_one]

Premises used: WeierstrassCurve.ΨSq_one, WeierstrassCurve.ΨSq_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
push_cast : Eq.{u + 1} (α := R[X]) 0 0
⊢ Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑(↑(m + 1) : ℤ) : R)) ((C : (a : R) → R[X]) 0)

Tactic:
push_cast [hn, C_neg, C_1, h', neg_zero, C_0]

Premises used: Polynomial.C_1, Polynomial.C_0, Polynomial.C_neg, neg_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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]) 0 0

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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.{u + 1} (α := R[X]) 1 0

Tactic:
exact fun h' => h <| C_injective <| by push_cast [hn, C_neg, C_1, h', neg_zero, C_0]; rfl

Premises used: Polynomial.C_injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
push_cast : Eq.{u + 1} (α := R[X]) 0 0
⊢ Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑(-(↑(m + 1) : ℤ)) : R)) ((C : (a : R) → R[X]) 0)

Tactic:
push_cast [hn, C_neg, C_1, h', neg_zero, C_0]

Premises used: Polynomial.C_1, Polynomial.C_0, Polynomial.C_neg, neg_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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]) 0 0

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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.{u + 1} (α := R[X]) 1 0

Tactic:
exact fun h' => h <| C_injective <| by push_cast [hn, C_neg, C_1, h', neg_zero, C_0]; rfl

Premises used: Polynomial.C_injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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
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
⊢ natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) n 2 ∧ coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) n 2) = 1

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

Tactic:
simp [natDegree_X_le]

Premises used: Polynomial.natDegree_X_le
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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) := ⋯
⊢ 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:
simp [natDegree_X_le]

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

Tactic:
push_cast [← @Nat.cast_inj ℤ, expDegree_cast (n + 1).succ_ne_zero, Nat.even_add_one, ite_not]

Premises used: Nat.even_add_one, Nat.cast_inj, Nat.succ_ne_zero, HAdd.hAdd, ite_not, _private.0.WeierstrassCurve.expDegree_cast, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 : ℕ
pos :
  Even n →
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
      1 + (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 - 4) + 3
neg :
  ¬Even n →
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
      1 + (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 - 1) + 0
⊢ 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:
split_ifs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 : ℕ
h_1 : Even n
⊢ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
    1 + (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 - 4) + 3

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

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

Tactic:
have hd : (n + 1 + 1) ^ 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3 := by
    push_cast [← @Nat.cast_inj ℤ, expDegree_cast (n + 1).succ_ne_zero, Nat.even_add_one, ite_not]
    split_ifs <;> ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
push_cast :
  2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) 2 - if Even n then 1 else 4) +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 2 - if Even n then 1 else 4) +
      HMul.hMul (α := ℤ) 2 (if Even n then 0 else 3)
⊢ HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0

Tactic:
push_cast [← @Nat.cast_inj ℤ, ← mul_left_cancel_iff_of_pos (b := (_ ^ 2 : ℤ)) two_pos, mul_add,
      expDegree_cast (n + 2).succ_ne_zero, expDegree_cast n.succ_ne_zero, Nat.even_add_one, ite_not]

Premises used: Nat.even_add_one, two_pos, Nat.cast_inj, Nat.succ_ne_zero, HAdd.hAdd, ite_not, _private.0.WeierstrassCurve.expDegree_cast, mul_add, OfNat.ofNat, mul_left_cancel_iff_of_pos
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
pos :
  Even n →
    2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) 2 - 1 +
          (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 2 - 1) +
        HMul.hMul (α := ℤ) 2 0
neg :
  ¬Even n →
    2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) 2 - 4 +
          (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 2 - 4) +
        HMul.hMul (α := ℤ) 2 3
⊢ 2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) 2 - if Even n then 1 else 4) +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 2 - if Even n then 1 else 4) +
      HMul.hMul (α := ℤ) 2 (if Even n then 0 else 3)

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
h_1 : Even n
⊢ 2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) 2 - 1 +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 2 - 1) +
      HMul.hMul (α := ℤ) 2 0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
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 : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
h_1 : ¬Even n
⊢ 2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) 2 =
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) 2 - 4 +
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 2 - 4) +
      HMul.hMul (α := ℤ) 2 3

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

Tactic:
have hd' : (n + 1 + 1) ^ 2 =
      expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0 := by
    push_cast [← @Nat.cast_inj ℤ, ← mul_left_cancel_iff_of_pos (b := (_ ^ 2 : ℤ)) two_pos, mul_add,
      expDegree_cast (n + 2).succ_ne_zero, expDegree_cast n.succ_ne_zero, Nat.even_add_one, ite_not]
    split_ifs <;> ring1