awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
rw : Eq (α := B[X][Y]) (W⁄B).ψ₂ ((W⁄A).map (↑f : A →+* B)).ψ₂
rw₁ rw₂ : Eq (α := B[X][Y]) (W⁄B).ψ₂ (W⁄B).ψ₂
⊢ Eq (α := B[X][Y]) (W⁄B).ψ₂ (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) (W⁄A).ψ₂)

Tactic:
rw [← map_ψ₂, map_baseChange]

Premises used: WeierstrassCurve.map_ψ₂, WeierstrassCurve.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
rw : Eq (α := B[X]) (W⁄B).Ψ₂Sq ((W⁄A).map (↑f : A →+* B)).Ψ₂Sq
rw₁ rw₂ : Eq (α := B[X]) (W⁄B).Ψ₂Sq (W⁄B).Ψ₂Sq
⊢ Eq (α := B[X]) (W⁄B).Ψ₂Sq (Polynomial.map (↑f : A →+* B) (W⁄A).Ψ₂Sq)

Tactic:
rw [← map_Ψ₂Sq, map_baseChange]

Premises used: WeierstrassCurve.map_Ψ₂Sq, WeierstrassCurve.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
rw : Eq (α := B[X]) (W⁄B).Ψ₃ ((W⁄A).map (↑f : A →+* B)).Ψ₃
rw₁ rw₂ : Eq (α := B[X]) (W⁄B).Ψ₃ (W⁄B).Ψ₃
⊢ Eq (α := B[X]) (W⁄B).Ψ₃ (Polynomial.map (↑f : A →+* B) (W⁄A).Ψ₃)

Tactic:
rw [← map_Ψ₃, map_baseChange]

Premises used: WeierstrassCurve.map_baseChange, WeierstrassCurve.map_Ψ₃
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
rw : Eq (α := B[X]) (W⁄B).preΨ₄ ((W⁄A).map (↑f : A →+* B)).preΨ₄
rw₁ rw₂ : Eq (α := B[X]) (W⁄B).preΨ₄ (W⁄B).preΨ₄
⊢ Eq (α := B[X]) (W⁄B).preΨ₄ (Polynomial.map (↑f : A →+* B) (W⁄A).preΨ₄)

Tactic:
rw [← map_preΨ₄, map_baseChange]

Premises used: WeierstrassCurve.map_baseChange, WeierstrassCurve.map_preΨ₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℕ
rw : Eq (α := B[X]) ((W⁄B).preΨ' n) (((W⁄A).map (↑f : A →+* B)).preΨ' n)
rw₁ rw₂ : Eq (α := B[X]) ((W⁄B).preΨ' n) ((W⁄B).preΨ' n)
⊢ Eq (α := B[X]) ((W⁄B).preΨ' n) (Polynomial.map (↑f : A →+* B) ((W⁄A).preΨ' n))

Tactic:
rw [← map_preΨ', map_baseChange]

Premises used: WeierstrassCurve.map_preΨ', WeierstrassCurve.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
rw : Eq (α := B[X]) ((W⁄B).preΨ n) (((W⁄A).map (↑f : A →+* B)).preΨ n)
rw₁ rw₂ : Eq (α := B[X]) ((W⁄B).preΨ n) ((W⁄B).preΨ n)
⊢ Eq (α := B[X]) ((W⁄B).preΨ n) (Polynomial.map (↑f : A →+* B) ((W⁄A).preΨ n))

Tactic:
rw [← map_preΨ, map_baseChange]

Premises used: WeierstrassCurve.map_baseChange, WeierstrassCurve.map_preΨ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
rw : Eq (α := B[X]) ((W⁄B).ΨSq n) (((W⁄A).map (↑f : A →+* B)).ΨSq n)
rw₁ rw₂ : Eq (α := B[X]) ((W⁄B).ΨSq n) ((W⁄B).ΨSq n)
⊢ Eq (α := B[X]) ((W⁄B).ΨSq n) (Polynomial.map (↑f : A →+* B) ((W⁄A).ΨSq n))

Tactic:
rw [← map_ΨSq, map_baseChange]

Premises used: WeierstrassCurve.map_ΨSq, WeierstrassCurve.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
rw : Eq (α := B[X][Y]) ((W⁄B).Ψ n) (((W⁄A).map (↑f : A →+* B)).Ψ n)
rw₁ rw₂ : Eq (α := B[X][Y]) ((W⁄B).Ψ n) ((W⁄B).Ψ n)
⊢ Eq (α := B[X][Y]) ((W⁄B).Ψ n) (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) ((W⁄A).Ψ n))

Tactic:
rw [← map_Ψ, map_baseChange]

Premises used: WeierstrassCurve.map_Ψ, WeierstrassCurve.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
rw : Eq (α := B[X]) ((W⁄B).Φ n) (((W⁄A).map (↑f : A →+* B)).Φ n)
rw₁ rw₂ : Eq (α := B[X]) ((W⁄B).Φ n) ((W⁄B).Φ n)
⊢ Eq (α := B[X]) ((W⁄B).Φ n) (Polynomial.map (↑f : A →+* B) ((W⁄A).Φ n))

Tactic:
rw [← map_Φ, map_baseChange]

Premises used: WeierstrassCurve.map_Φ, WeierstrassCurve.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
rw : Eq (α := B[X][Y]) ((W⁄B).ψ n) (((W⁄A).map (↑f : A →+* B)).ψ n)
rw₁ rw₂ : Eq (α := B[X][Y]) ((W⁄B).ψ n) ((W⁄B).ψ n)
⊢ Eq (α := B[X][Y]) ((W⁄B).ψ n) (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) ((W⁄A).ψ n))

Tactic:
rw [← map_ψ, map_baseChange]

Premises used: WeierstrassCurve.map_baseChange, WeierstrassCurve.map_ψ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
rw : Eq (α := B[X][Y]) ((W⁄B).φ n) (((W⁄A).map (↑f : A →+* B)).φ n)
rw₁ rw₂ : Eq (α := B[X][Y]) ((W⁄B).φ n) ((W⁄B).φ n)
⊢ Eq (α := B[X][Y]) ((W⁄B).φ n) (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) ((W⁄A).φ n))

Tactic:
rw [← map_φ, map_baseChange]

Premises used: WeierstrassCurve.map_φ, WeierstrassCurve.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
a : max (max (max (0 + HMul.hMul (α := ℕ) 3 1) (0 + HMul.hMul (α := ℕ) 2 1)) (HAdd.hAdd (α := ℕ) 0 1)) 0 ≤ 3
⊢ (HAdd.hAdd (β := R[X])
        ((C : (a : R) → R[X]) 4 * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W.b₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (2 * W.b₄) : R[X]) X)
        ((C : (a : R) → R[X]) W.b₆ : R[X])).natDegree ≤
    3

Tactic:
compute_degree
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
rs :
  ((((if 3 = 0 + HMul.hMul (α := ℕ) 3 1 then
            (if Eq (α := ℕ) 0 0 then 4 else 0) *
              if HMul.hMul (α := ℕ) 3 1 = HMul.hMul (α := ℕ) 3 1 then
                HPow.hPow (α := R) (β := ℕ) (if Eq (α := ℕ) 1 1 then 1 else 0) 3
              else 0
          else 0) +
          if 3 = 0 + HMul.hMul (α := ℕ) 2 1 then
            (if Eq (α := ℕ) 0 0 then W.b₂ else 0) *
              if HMul.hMul (α := ℕ) 2 1 = HMul.hMul (α := ℕ) 2 1 then
                HPow.hPow (α := R) (β := ℕ) (if Eq (α := ℕ) 1 1 then 1 else 0) 2
              else 0
          else 0) +
        if 3 = HAdd.hAdd (α := ℕ) 0 1 then (if Eq (α := ℕ) 0 0 then 2 * W.b₄ else 0) * if Eq (α := ℕ) 1 1 then 1 else 0
        else 0) +
      if Eq (α := ℕ) 3 0 then W.b₆ else 0) =
    4
h : HAdd.hAdd (α := ℕ) 0 1 ≤ 3
h₁ : 0 + HMul.hMul (α := ℕ) 3 1 ≤ 3
h₂ : 0 + HMul.hMul (α := ℕ) 2 1 ≤ 3
h₃ : HMul.hMul (α := ℕ) 3 1 ≤ HMul.hMul (α := ℕ) 3 1
h₄ : HMul.hMul (α := ℕ) 2 1 ≤ HMul.hMul (α := ℕ) 2 1
h₅ : LE.le (α := ℕ) 1 3
h₆ : LE.le (α := ℕ) 2 3
⊢ (HAdd.hAdd (β := R[X])
          ((C : (a : R) → R[X]) 4 * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W.b₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (2 * W.b₄) : R[X]) X)
          ((C : (a : R) → R[X]) W.b₆ : R[X])).coeff
      3 =
    4

Tactic:
compute_degree!
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h rwa rwa₁ rwa₂ rwa₃ : Ne.{u + 1} (α := R) 4 0
⊢ coeff W.Ψ₂Sq 3 ≠ 0

Tactic:
rwa [coeff_Ψ₂Sq]

Premises used: WeierstrassCurve.coeff_Ψ₂Sq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 4 0
⊢ natDegree W.Ψ₂Sq = 3

Tactic:
natDegree_eq_of_le_of_coeff_ne_zero W.natDegree_Ψ₂Sq_le <| W.coeff_Ψ₂Sq_ne_zero h

Premises used: Polynomial.natDegree_eq_of_le_of_coeff_ne_zero, WeierstrassCurve.natDegree_Ψ₂Sq_le, WeierstrassCurve.coeff_Ψ₂Sq_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 4 0
⊢ 0 < natDegree W.Ψ₂Sq

Tactic:
W.natDegree_Ψ₂Sq h ▸ three_pos

Premises used: three_pos, Eq.rec, WeierstrassCurve.natDegree_Ψ₂Sq, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 4 0
rw : coeff W.Ψ₂Sq (natDegree W.Ψ₂Sq) = 4
rw₁ : coeff W.Ψ₂Sq 3 = 4
rw₂ rw₃ : Eq.{u + 1} (α := R) 4 4
⊢ leadingCoeff W.Ψ₂Sq = 4

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

Premises used: WeierstrassCurve.coeff_Ψ₂Sq, Polynomial.leadingCoeff, WeierstrassCurve.natDegree_Ψ₂Sq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 4 0
⊢ Ne (α := R[X]) W.Ψ₂Sq 0

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

Premises used: WeierstrassCurve.natDegree_Ψ₂Sq_pos, Polynomial.ne_zero_of_natDegree_gt
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
a :
  max
      (max
        (max (max (0 + HMul.hMul (α := ℕ) 4 1) (0 + HMul.hMul (α := ℕ) 3 1))
          (HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 2 1))
        (HAdd.hAdd (α := ℕ) 0 0 + 1))
      0 ≤
    4
⊢ (HAdd.hAdd (β := R[X])
        (3 * HPow.hPow (α := R[X]) (β := ℕ) X 4 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W.b₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
            HMul.hMul (α := R[X]) (β := R[X]) (3 : R[X]) ((C : (a : R) → R[X]) W.b₄ : R[X]) *
              HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          HMul.hMul (α := R[X]) (β := R[X]) (3 : R[X]) ((C : (a : R) → R[X]) W.b₆ : R[X]) * X)
        ((C : (a : R) → R[X]) W.b₈ : R[X])).natDegree ≤
    4

Tactic:
compute_degree
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
rs :
  (((((if 4 = 0 + HMul.hMul (α := ℕ) 4 1 then
              (↑(if Eq (α := ℕ) 0 0 then 3 else 0) : R) *
                if HMul.hMul (α := ℕ) 4 1 = HMul.hMul (α := ℕ) 4 1 then
                  HPow.hPow (α := R) (β := ℕ) (if Eq (α := ℕ) 1 1 then 1 else 0) 4
                else 0
            else 0) +
            if 4 = 0 + HMul.hMul (α := ℕ) 3 1 then
              (if Eq (α := ℕ) 0 0 then W.b₂ else 0) *
                if HMul.hMul (α := ℕ) 3 1 = HMul.hMul (α := ℕ) 3 1 then
                  HPow.hPow (α := R) (β := ℕ) (if Eq (α := ℕ) 1 1 then 1 else 0) 3
                else 0
            else 0) +
          if 4 = HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 2 1 then
            (if HAdd.hAdd (α := ℕ) 0 0 = HAdd.hAdd (α := ℕ) 0 0 then
                (↑(if Eq (α := ℕ) 0 0 then 3 else 0) : R) * if Eq (α := ℕ) 0 0 then W.b₄ else 0
              else 0) *
              if HMul.hMul (α := ℕ) 2 1 = HMul.hMul (α := ℕ) 2 1 then
                HPow.hPow (α := R) (β := ℕ) (if Eq (α := ℕ) 1 1 then 1 else 0) 2
              else 0
          else 0) +
        if 4 = HAdd.hAdd (α := ℕ) 0 0 + 1 then
          (if HAdd.hAdd (α := ℕ) 0 0 = HAdd.hAdd (α := ℕ) 0 0 then
              (↑(if Eq (α := ℕ) 0 0 then 3 else 0) : R) * if Eq (α := ℕ) 0 0 then W.b₆ else 0
            else 0) *
            if Eq (α := ℕ) 1 1 then 1 else 0
        else 0) +
      if Eq (α := ℕ) 4 0 then W.b₈ else 0) =
    3
h : HAdd.hAdd (α := ℕ) 0 0 + 1 ≤ 4
h₁ : HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 2 1 ≤ 4
h₂ : 0 + HMul.hMul (α := ℕ) 4 1 ≤ 4
h₃ : 0 + HMul.hMul (α := ℕ) 3 1 ≤ 4
h₄ h₅ : HAdd.hAdd (α := ℕ) 0 0 ≤ HAdd.hAdd (α := ℕ) 0 0
h₆ : HMul.hMul (α := ℕ) 2 1 ≤ HMul.hMul (α := ℕ) 2 1
h₇ : HMul.hMul (α := ℕ) 4 1 ≤ HMul.hMul (α := ℕ) 4 1
h₈ : HMul.hMul (α := ℕ) 3 1 ≤ HMul.hMul (α := ℕ) 3 1
h₉ : LE.le (α := ℕ) 1 4
h₁₀ : LE.le (α := ℕ) 2 4
h₁₁ : LE.le (α := ℕ) 3 4
⊢ (HAdd.hAdd (β := R[X])
          (3 * HPow.hPow (α := R[X]) (β := ℕ) X 4 +
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W.b₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
              HMul.hMul (α := R[X]) (β := R[X]) (3 : R[X]) ((C : (a : R) → R[X]) W.b₄ : R[X]) *
                HPow.hPow (α := R[X]) (β := ℕ) X 2 +
            HMul.hMul (α := R[X]) (β := R[X]) (3 : R[X]) ((C : (a : R) → R[X]) W.b₆ : R[X]) * X)
          ((C : (a : R) → R[X]) W.b₈ : R[X])).coeff
      4 =
    3

Tactic:
compute_degree!
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h rwa rwa₁ rwa₂ rwa₃ : Ne.{u + 1} (α := R) 3 0
⊢ coeff W.Ψ₃ 4 ≠ 0

Tactic:
rwa [coeff_Ψ₃]

Premises used: WeierstrassCurve.coeff_Ψ₃
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 3 0
⊢ natDegree W.Ψ₃ = 4

Tactic:
natDegree_eq_of_le_of_coeff_ne_zero W.natDegree_Ψ₃_le <| W.coeff_Ψ₃_ne_zero h

Premises used: WeierstrassCurve.coeff_Ψ₃_ne_zero, WeierstrassCurve.natDegree_Ψ₃_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
h : Ne.{u + 1} (α := R) 3 0
⊢ 0 < natDegree W.Ψ₃

Tactic:
W.natDegree_Ψ₃ h ▸ four_pos

Premises used: four_pos, Eq.rec, WeierstrassCurve.natDegree_Ψ₃, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 3 0
rw : coeff W.Ψ₃ (natDegree W.Ψ₃) = 3
rw₁ : coeff W.Ψ₃ 4 = 3
rw₂ rw₃ : Eq.{u + 1} (α := R) 3 3
⊢ leadingCoeff W.Ψ₃ = 3

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

Premises used: Polynomial.leadingCoeff, WeierstrassCurve.natDegree_Ψ₃, WeierstrassCurve.coeff_Ψ₃
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 3 0
⊢ Ne (α := R[X]) W.Ψ₃ 0

Tactic:
ne_zero_of_natDegree_gt <| W.natDegree_Ψ₃_pos h

Premises used: Polynomial.ne_zero_of_natDegree_gt, WeierstrassCurve.natDegree_Ψ₃_pos
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
a :
  max
      (max
        (max
          (max
            (max (max (0 + HMul.hMul (α := ℕ) 6 1) (0 + HMul.hMul (α := ℕ) 5 1))
              (HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 4 1))
            (HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 3 1))
          (HAdd.hAdd (α := ℕ) 0 0 + HMul.hMul (α := ℕ) 2 1))
        (HAdd.hAdd (α := ℕ) 0 1))
      0 ≤
    6
⊢ (HAdd.hAdd (β := R[X])
        (2 * HPow.hPow (α := R[X]) (β := ℕ) X 6 +
                  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W.b₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 5) +
                HMul.hMul (α := R[X]) (β := R[X]) (5 : R[X]) ((C : (a : R) → R[X]) W.b₄ : R[X]) *
                  HPow.hPow (α := R[X]) (β := ℕ) X 4 +
              HMul.hMul (α := R[X]) (β := R[X]) (10 : R[X]) ((C : (a : R) → R[X]) W.b₆ : R[X]) *
                HPow.hPow (α := R[X]) (β := ℕ) X 3 +
            HMul.hMul (α := R[X]) (β := R[X]) (10 : R[X]) ((C : (a : R) → R[X]) W.b₈ : R[X]) *
              HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (W.b₂ * W.b₈ - W.b₄ * W.b₆) : R[X]) X)
        ((C : (a : R) → R[X]) (W.b₄ * W.b₈ - HPow.hPow (β := ℕ) W.b₆ 2) : R[X])).natDegree ≤
    6

Tactic:
compute_degree
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h rwa rwa₁ rwa₂ rwa₃ : Ne.{u + 1} (α := R) 2 0
⊢ coeff W.preΨ₄ 6 ≠ 0

Tactic:
rwa [coeff_preΨ₄]

Premises used: WeierstrassCurve.coeff_preΨ₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 2 0
⊢ natDegree W.preΨ₄ = 6

Tactic:
natDegree_eq_of_le_of_coeff_ne_zero W.natDegree_preΨ₄_le <| W.coeff_preΨ₄_ne_zero h

Premises used: WeierstrassCurve.coeff_preΨ₄_ne_zero, WeierstrassCurve.natDegree_preΨ₄_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
h : Ne.{u + 1} (α := R) 2 0
linarith :
  natDegree W.preΨ₄ ≤ 0 →
    HMul.hMul (α := ℤ) 6 (-1) + HSub.hSub (α := ℤ) (↑(natDegree W.preΨ₄) : ℤ) 0 +
        -HSub.hSub (α := ℤ) (↑(natDegree W.preΨ₄) : ℤ) 6 =
      0
linarith₁ : natDegree W.preΨ₄ ≤ 0 → GT.gt (α := ℤ) 6 0
⊢ 0 < natDegree W.preΨ₄

Tactic:
linarith only [W.natDegree_preΨ₄ h]

Premises used: WeierstrassCurve.natDegree_preΨ₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 2 0
rw : coeff W.preΨ₄ (natDegree W.preΨ₄) = 2
rw₁ : coeff W.preΨ₄ 6 = 2
rw₂ rw₃ : Eq.{u + 1} (α := R) 2 2
⊢ leadingCoeff W.preΨ₄ = 2

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

Premises used: Polynomial.leadingCoeff, WeierstrassCurve.natDegree_preΨ₄, WeierstrassCurve.coeff_preΨ₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
h : Ne.{u + 1} (α := R) 2 0
⊢ Ne (α := R[X]) W.preΨ₄ 0

Tactic:
ne_zero_of_natDegree_gt <| W.natDegree_preΨ₄_pos h

Premises used: WeierstrassCurve.natDegree_preΨ₄_pos, Polynomial.ne_zero_of_natDegree_gt
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
n : ℕ
hn : n ≠ 0
inl :
  ∀ (n : ℕ) (hn : 2 * n ≠ 0),
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * n)) : ℤ) =
      HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * n) : ℤ) 2 - if Even (2 * n) then 4 else 1
inr :
  ∀ (n : ℕ) (hn : 2 * n + 1 ≠ 0),
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * n + 1)) : ℤ) =
      HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * n + 1) : ℤ) 2 - if Even (2 * n + 1) then 4 else 1
⊢ HMul.hMul (α := ℤ) 2 (↑(expDegree n) : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - if Even n then 4 else 1

Tactic:
rcases n.even_or_odd' with ⟨n, rfl | rfl⟩

Premises used: Nat.even_or_odd', rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
n : ℕ
hn : 2 * n ≠ 0
inl :
  ∀ (hn : HMul.hMul (α := ℕ) 2 0 ≠ 0),
    HMul.hMul (α := ℤ) 2 (↑(expDegree (HMul.hMul (α := ℕ) 2 0)) : ℤ) =
      HPow.hPow (α := ℤ) (β := ℕ) (↑(HMul.hMul (α := ℕ) 2 0) : ℤ) 2 - if Even (HMul.hMul (α := ℕ) 2 0) then 4 else 1
inl₁ :
  ∀ (n : ℕ) (hn : 2 * (n + 1) ≠ 0),
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * (n + 1))) : ℤ) =
      HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * (n + 1)) : ℤ) 2 - if Even (2 * (n + 1)) then 4 else 1
⊢ HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * n)) : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * n) : ℤ) 2 - if Even (2 * n) then 4 else 1

Tactic:
rcases n with _ | n
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
hn : HMul.hMul (α := ℕ) 2 0 ≠ 0
⊢ HMul.hMul (α := ℤ) 2 (↑(expDegree (HMul.hMul (α := ℕ) 2 0)) : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑(HMul.hMul (α := ℕ) 2 0) : ℤ) 2 - if Even (HMul.hMul (α := ℕ) 2 0) then 4 else 1

Tactic:
contradiction
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
n : ℕ
hn : 2 * (n + 1) ≠ 0
⊢ HPow.hPow (β := ℕ) (2 * (n + 1)) 2 = 2 * (2 * n * (n + 2)) + 4

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
n : ℕ
hn : 2 * (n + 1) ≠ 0
inl :
  2 * (HMul.hMul (α := ℤ) 2 (↑n : ℤ) * HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) =
    HPow.hPow (β := ℕ) (2 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 2 - 4
⊢ HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * (n + 1))) : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * (n + 1)) : ℤ) 2 - if Even (2 * (n + 1)) then 4 else 1

Tactic:
push_cast [expDegree, show (2 * (n + 1)) ^ 2 = 2 * (2 * n * (n + 2)) + 4 by ring1, even_two_mul,
      Nat.add_sub_cancel, Nat.mul_div_cancel_left _ two_pos]

Premises used: _private.0.WeierstrassCurve.expDegree, Nat.mul_div_cancel_left, two_pos, even_two_mul, Nat.add_sub_cancel
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
n : ℕ
hn : 2 * (n + 1) ≠ 0
⊢ 2 * (HMul.hMul (α := ℤ) 2 (↑n : ℤ) * HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) =
    HPow.hPow (β := ℕ) (2 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 2 - 4

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
n : ℕ
hn : 2 * n + 1 ≠ 0
⊢ HPow.hPow (β := ℕ) (2 * n + 1) 2 = 2 * (2 * n * (n + 1)) + 1

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
n : ℕ
hn : 2 * n + 1 ≠ 0
inr :
  2 * (HMul.hMul (α := ℤ) 2 (↑n : ℤ) * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) 2 - 1
⊢ HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * n + 1)) : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * n + 1) : ℤ) 2 - if Even (2 * n + 1) then 4 else 1

Tactic:
push_cast [expDegree, show (2 * n + 1) ^ 2 = 2 * (2 * n * (n + 1)) + 1 by ring1,
      n.not_even_two_mul_add_one, Nat.add_sub_cancel, Nat.mul_div_cancel_left _ two_pos]

Premises used: _private.0.WeierstrassCurve.expDegree, Nat.mul_div_cancel_left, two_pos, Nat.not_even_two_mul_add_one, Nat.add_sub_cancel
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
n : ℕ
hn : 2 * n + 1 ≠ 0
⊢ 2 * (HMul.hMul (α := ℤ) 2 (↑n : ℤ) * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    HPow.hPow (β := ℕ) (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) 2 - 1

Tactic:
ring1