awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
simp_rw :
  HMul.hMul (α := R[X][Y]) (β := R[X][Y])
      ((C : (a : R[X]) → R[X][Y])
          ((W.preΨ (m + 2) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ m) 3 *
              if Even m then HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 else 1) -
            W.preΨ (m - 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m + 1)) 3 *
              if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2) :
        R[X][Y])
      (1 : R[X][Y]) =
    HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y])
            (if Even m then W.ψ₂ else 1) *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y])
              (if Even m then W.ψ₂ else 1))
            3 -
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y])
            (if ¬Even m then W.ψ₂ else 1) *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y])
              (if ¬Even m then W.ψ₂ else 1))
            3 +
      HMul.hMul (β := R[X][Y])
        (W.toAffine.polynomial *
          (HMul.hMul (α := R[X][Y]) 16 W.toAffine.polynomial - 8 * HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2))
        ((C : (a : R[X]) → R[X][Y])
            (if Even m then W.preΨ (m + 2) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ m) 3
            else -W.preΨ (m - 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m + 1)) 3) :
          R[X][Y])
⊢ W.Ψ (2 * m + 1) =
    W.Ψ (m + 2) * HPow.hPow (α := R[X][Y]) (β := ℕ) (W.Ψ m) 3 -
        W.Ψ (m - 1) * HPow.hPow (α := R[X][Y]) (β := ℕ) (W.Ψ (m + 1)) 3 +
      HMul.hMul (β := R[X][Y])
        (W.toAffine.polynomial *
          (HMul.hMul (α := R[X][Y]) 16 W.toAffine.polynomial - 8 * HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2))
        ((C : (a : R[X]) → R[X][Y])
            (if Even m then W.preΨ (m + 2) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ m) 3
            else -W.preΨ (m - 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m + 1)) 3) :
          R[X][Y])

Tactic:
simp_rw [Ψ, preΨ_odd, if_neg m.not_even_two_mul_add_one, Int.even_add, Int.even_sub, even_two,
    iff_true, Int.not_even_one, iff_false]

Premises used: iff_false, even_two, WeierstrassCurve.preΨ_odd, Int.not_even_one, iff_true, WeierstrassCurve.Ψ, Int.not_even_two_mul_add_one, Int.even_add, if_neg, Int.even_sub
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
h : Even m
pos :
  (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) 3) *
          HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.Ψ₂Sq : R[X][Y]) 2 -
        HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) 3) *
          1) *
      1 =
    HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) W.ψ₂ *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) W.ψ₂) 3 -
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) (1 : R[X][Y]) *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y])
              (1 : R[X][Y]))
            3 +
      W.toAffine.polynomial *
          (HMul.hMul (α := R[X][Y]) 16 W.toAffine.polynomial - 8 * HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2) *
        HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y])
          (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) 3)
⊢ HMul.hMul (α := R[X][Y]) (β := R[X][Y])
      ((C : (a : R[X]) → R[X][Y])
          (W.preΨ (m + 2) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ m) 3 * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 -
            W.preΨ (m - 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m + 1)) 3 * 1) :
        R[X][Y])
      (1 : R[X][Y]) =
    HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) W.ψ₂ *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) W.ψ₂) 3 -
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) (1 : R[X][Y]) *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y])
              (1 : R[X][Y]))
            3 +
      HMul.hMul (β := R[X][Y])
        (W.toAffine.polynomial *
          (HMul.hMul (α := R[X][Y]) 16 W.toAffine.polynomial - 8 * HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2))
        ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ m) 3) : R[X][Y])

Tactic:
C_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
h : ¬Even m
neg :
  (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) 3) *
          1 -
        HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) 3) *
          HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.Ψ₂Sq : R[X][Y]) 2) *
      1 =
    HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) (1 : R[X][Y]) *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) (1 : R[X][Y]))
            3 -
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) W.ψ₂ *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) W.ψ₂) 3 +
      W.toAffine.polynomial *
          (HMul.hMul (α := R[X][Y]) 16 W.toAffine.polynomial - 8 * HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2) *
        HMul.hMul (α := R[X][Y]) (-(C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y])
          (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) 3)
⊢ HMul.hMul (α := R[X][Y]) (β := R[X][Y])
      ((C : (a : R[X]) → R[X][Y])
          (W.preΨ (m + 2) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ m) 3 * 1 -
            W.preΨ (m - 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m + 1)) 3 *
              HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2) :
        R[X][Y])
      (1 : R[X][Y]) =
    HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) (1 : R[X][Y]) *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) (1 : R[X][Y]))
            3 -
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) W.ψ₂ *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) W.ψ₂) 3 +
      HMul.hMul (β := R[X][Y])
        (W.toAffine.polynomial *
          (HMul.hMul (α := R[X][Y]) 16 W.toAffine.polynomial - 8 * HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2))
        ((C : (a : R[X]) → R[X][Y]) (-W.preΨ (m - 1) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m + 1)) 3) : R[X][Y])

Tactic:
C_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
h : Even m
pos :
  (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) 3) *
          HPow.hPow (β := ℕ)
            (HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2 - HMul.hMul (α := R[X][Y]) 4 W.toAffine.polynomial) 2 -
        HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) 3) *
          1) *
      1 =
    HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) W.ψ₂ *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) W.ψ₂) 3 -
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) (1 : R[X][Y]) *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y])
              (1 : R[X][Y]))
            3 +
      W.toAffine.polynomial *
          (HMul.hMul (α := R[X][Y]) 16 W.toAffine.polynomial - 8 * HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2) *
        HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y])
          (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) 3)
⊢ (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) 3) *
          HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.Ψ₂Sq : R[X][Y]) 2 -
        HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) 3) *
          1) *
      1 =
    HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) W.ψ₂ *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) W.ψ₂) 3 -
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) (1 : R[X][Y]) *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y])
              (1 : R[X][Y]))
            3 +
      W.toAffine.polynomial *
          (HMul.hMul (α := R[X][Y]) 16 W.toAffine.polynomial - 8 * HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2) *
        HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y])
          (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) 3)

Tactic:
rw [C_Ψ₂Sq]

Premises used: WeierstrassCurve.C_Ψ₂Sq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
h : ¬Even m
neg :
  (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) 3) *
          1 -
        HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) 3) *
          HPow.hPow (β := ℕ)
            (HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2 - HMul.hMul (α := R[X][Y]) 4 W.toAffine.polynomial) 2) *
      1 =
    HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) (1 : R[X][Y]) *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) (1 : R[X][Y]))
            3 -
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) W.ψ₂ *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) W.ψ₂) 3 +
      W.toAffine.polynomial *
          (HMul.hMul (α := R[X][Y]) 16 W.toAffine.polynomial - 8 * HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2) *
        HMul.hMul (α := R[X][Y]) (-(C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y])
          (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) 3)
⊢ (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) 3) *
          1 -
        HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) 3) *
          HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.Ψ₂Sq : R[X][Y]) 2) *
      1 =
    HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) (1 : R[X][Y]) *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) (1 : R[X][Y]))
            3 -
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) W.ψ₂ *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) W.ψ₂) 3 +
      W.toAffine.polynomial *
          (HMul.hMul (α := R[X][Y]) 16 W.toAffine.polynomial - 8 * HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2) *
        HMul.hMul (α := R[X][Y]) (-(C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y])
          (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) 3)

Tactic:
rw [C_Ψ₂Sq]

Premises used: WeierstrassCurve.C_Ψ₂Sq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
h : Even m
⊢ (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) 3) *
          HPow.hPow (β := ℕ)
            (HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2 - HMul.hMul (α := R[X][Y]) 4 W.toAffine.polynomial) 2 -
        HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) 3) *
          1) *
      1 =
    HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) W.ψ₂ *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) W.ψ₂) 3 -
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) (1 : R[X][Y]) *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y])
              (1 : R[X][Y]))
            3 +
      W.toAffine.polynomial *
          (HMul.hMul (α := R[X][Y]) 16 W.toAffine.polynomial - 8 * HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2) *
        HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y])
          (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) 3)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
h : ¬Even m
⊢ (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) 3) *
          1 -
        HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) 3) *
          HPow.hPow (β := ℕ)
            (HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2 - HMul.hMul (α := R[X][Y]) 4 W.toAffine.polynomial) 2) *
      1 =
    HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) (1 : R[X][Y]) *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) (1 : R[X][Y]))
            3 -
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) W.ψ₂ *
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) W.ψ₂) 3 +
      W.toAffine.polynomial *
          (HMul.hMul (α := R[X][Y]) 16 W.toAffine.polynomial - 8 * HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2) *
        HMul.hMul (α := R[X][Y]) (-(C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y])
          (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) 3)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
rw :
  (HMul.hMul (α := R[X]) X (W.ΨSq (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) -
      HMul.hMul (α := R[X]) (W.preΨ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) (W.preΨ (↑n : ℤ)) *
        if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) then 1 else W.Ψ₂Sq) =
    (X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even n then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (n + 2)) (W.preΨ' n) * if Even n then W.Ψ₂Sq else 1
⊢ W.Φ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    (X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even n then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (n + 2)) (W.preΨ' n) * if Even n then W.Ψ₂Sq else 1

Tactic:
rw [Φ, add_sub_cancel_right]

Premises used: add_sub_cancel_right, WeierstrassCurve.Φ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
norm_cast :
  (HMul.hMul (α := R[X]) X (W.ΨSq (↑(n + 1) : ℤ)) -
      HMul.hMul (α := R[X]) (W.preΨ (↑(n + 1 + 1) : ℤ)) (W.preΨ (↑n : ℤ)) * if Even (n + 1) then 1 else W.Ψ₂Sq) =
    (X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even n then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (n + 2)) (W.preΨ' n) * if Even n then W.Ψ₂Sq else 1
⊢ (HMul.hMul (α := R[X]) X (W.ΨSq (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) -
      HMul.hMul (α := R[X]) (W.preΨ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) (W.preΨ (↑n : ℤ)) *
        if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) then 1 else W.Ψ₂Sq) =
    (X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even n then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (n + 2)) (W.preΨ' n) * if Even n then W.Ψ₂Sq else 1

Tactic:
norm_cast
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
simp_rw :
  (X * (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even (n + 1) then W.Ψ₂Sq else 1) -
      HMul.hMul (α := R[X]) (W.preΨ (↑(n + 1 + 1) : ℤ)) (W.preΨ (↑n : ℤ)) * if Even (n + 1) then 1 else W.Ψ₂Sq) =
    (X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even n then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (n + 2)) (W.preΨ' n) * if Even n then W.Ψ₂Sq else 1
simp_rw₁ :
  (X * (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if ¬Even n then W.Ψ₂Sq else 1) -
      HMul.hMul (α := R[X]) (W.preΨ (↑(n + 1 + 1) : ℤ)) (W.preΨ (↑n : ℤ)) * if ¬Even n then 1 else W.Ψ₂Sq) =
    (X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even n then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (n + 2)) (W.preΨ' n) * if Even n then W.Ψ₂Sq else 1
simp_rw₂ :
  (X * (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even n then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ (↑(n + 1 + 1) : ℤ)) (W.preΨ (↑n : ℤ)) * if Even n then W.Ψ₂Sq else 1) =
    (X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even n then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (n + 2)) (W.preΨ' n) * if Even n then W.Ψ₂Sq else 1
simp_rw₃ :
  ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even n then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ (↑(n + 1 + 1) : ℤ)) (W.preΨ (↑n : ℤ)) * if Even n then W.Ψ₂Sq else 1) =
    (X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even n then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (n + 2)) (W.preΨ' n) * if Even n then W.Ψ₂Sq else 1
⊢ (HMul.hMul (α := R[X]) X (W.ΨSq (↑(n + 1) : ℤ)) -
      HMul.hMul (α := R[X]) (W.preΨ (↑(n + 1 + 1) : ℤ)) (W.preΨ (↑n : ℤ)) * if Even (n + 1) then 1 else W.Ψ₂Sq) =
    (X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1)) 2 * if Even n then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (n + 2)) (W.preΨ' n) * if Even n then W.Ψ₂Sq else 1

Tactic:
simp_rw [ΨSq_ofNat, Nat.even_add_one, ite_not, ← mul_assoc, preΨ_ofNat]

Premises used: Nat.even_add_one, WeierstrassCurve.ΨSq_ofNat, mul_assoc, WeierstrassCurve.preΨ_ofNat, ite_not
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ Eq (α := R[X]) (W.Φ 0) 1

Tactic:
simp [Φ]

Premises used: WeierstrassCurve.Φ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ Eq (α := R[X]) (W.Φ 1) X

Tactic:
simp [Φ]

Premises used: WeierstrassCurve.Φ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ 2 = HAdd.hAdd (α := ℤ) (↑1 : ℤ) 1

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
rw :
  X * HPow.hPow (α := R[X]) (β := ℕ) 1 2 *
        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]) -
      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]) *
          1 *
        1 =
    HSub.hSub (β := R[X])
      (HPow.hPow (α := R[X]) (β := ℕ) X 4 -
          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])
⊢ W.Φ 2 =
    HSub.hSub (β := R[X])
      (HPow.hPow (α := R[X]) (β := ℕ) X 4 -
          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])

Tactic:
rw [show 2 = ((1 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_two, if_neg Nat.not_even_one, Ψ₂Sq,
    preΨ'_three, preΨ'_one, if_neg Nat.not_even_one, Ψ₃]

Premises used: WeierstrassCurve.preΨ'_one, WeierstrassCurve.Ψ₂Sq, WeierstrassCurve.preΨ'_three, Nat.not_even_one, WeierstrassCurve.Ψ₃, WeierstrassCurve.Φ_ofNat, if_neg, WeierstrassCurve.preΨ'_two