awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
h : ¬Even m
⊢ HMul.hMul (α := R[X][Y]) (β := R[X][Y])
        ((C : (a : R[X]) → R[X][Y])
            (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m - 1)) 2 * W.preΨ m * W.preΨ (m + 2) -
              HMul.hMul (α := R[X]) (W.preΨ (m - 2)) (W.preΨ m) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m + 1)) 2) :
          R[X][Y])
        W.ψ₂ *
      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.ψ₂) 2 *
          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]) *
        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]) -
      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]) *
          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]) *
        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.ψ₂) 2
have neg : (HMul.hMul (β := R[X][Y])
          (HMul.hMul (β := R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) 2)
            ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]))
          ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : 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])
            ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) *
          HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) 2) *
      W.ψ₂ *
    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.ψ₂) 2 *
        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]) *
      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]) -
    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]) *
        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]) *
      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.ψ₂) 2
Tactic: C_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ 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])
have 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])
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ 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])
have pos : Even m →
  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: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
h : Even m
⊢ 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])
have 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)
Tactic: C_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
h : ¬Even m
⊢ 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])
have 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)
Tactic: C_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
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 (α := 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)
have 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)
Tactic: rw [C_Ψ₂Sq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
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 (α := 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)
have 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)
Tactic: rw [C_Ψ₂Sq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ HPow.hPow (α := CoordinateRing W) (β := ℕ) ((mk W : (a : R[X][Y]) → CoordinateRing W) (W.Ψ n)) 2 =
    (mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) (W.ΨSq n))
have simp_rw : HPow.hPow (α := CoordinateRing W) (β := ℕ)
    ((mk W : (a : R[X][Y]) → CoordinateRing W)
        (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ n) : R[X][Y])
          (if Even n then W.ψ₂ else 1)) :
      CoordinateRing W)
    2 =
  (mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) (W.ΨSq n))
Tactic: simp_rw [Ψ, ΨSq, map_mul, apply_ite C, apply_ite <| mk W, mul_pow, ite_pow, mk_ψ₂_sq, map_one,
    one_pow, map_pow]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
simp_rw :
  HPow.hPow (α := CoordinateRing W) (β := ℕ)
      ((mk W : (a : R[X][Y]) → CoordinateRing W)
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ n) : R[X][Y])
            (if Even n then W.ψ₂ else 1)) :
        CoordinateRing W)
      2 =
    (mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) (W.ΨSq n))
⊢ HPow.hPow (α := CoordinateRing W) (β := ℕ) ((mk W : (a : R[X][Y]) → CoordinateRing W) (W.Ψ n)) 2 =
    (mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) (W.ΨSq n))
have simp_rw₁ : HPow.hPow (α := CoordinateRing W) (β := ℕ)
    ((mk W : (a : R[X][Y]) → CoordinateRing W)
        (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ n) : R[X][Y])
          (if Even n then W.ψ₂ else 1)) :
      CoordinateRing W)
    2 =
  (mk W : (a : R[X][Y]) → CoordinateRing W)
    ((C : (a : R[X]) → R[X][Y]) (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ n) 2 * if Even n then W.Ψ₂Sq else 1))
Tactic: simp_rw [Ψ, ΨSq, map_mul, apply_ite C, apply_ite <| mk W, mul_pow, ite_pow, mk_ψ₂_sq, map_one,
    one_pow, map_pow]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
simp_rw :
  HPow.hPow (α := CoordinateRing W) (β := ℕ)
      ((mk W : (a : R[X][Y]) → CoordinateRing W)
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ n) : R[X][Y])
            (if Even n then W.ψ₂ else 1)) :
        CoordinateRing W)
      2 =
    (mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) (W.ΨSq n))
simp_rw₁ :
  HPow.hPow (α := CoordinateRing W) (β := ℕ)
      ((mk W : (a : R[X][Y]) → CoordinateRing W)
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ n) : R[X][Y])
            (if Even n then W.ψ₂ else 1)) :
        CoordinateRing W)
      2 =
    (mk W : (a : R[X][Y]) → CoordinateRing W)
      ((C : (a : R[X]) → R[X][Y]) (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ n) 2 * if Even n then W.Ψ₂Sq else 1))
⊢ HPow.hPow (α := CoordinateRing W) (β := ℕ) ((mk W : (a : R[X][Y]) → CoordinateRing W) (W.Ψ n)) 2 =
    (mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) (W.ΨSq n))
have simp_rw₂ : HPow.hPow (β := ℕ)
    (HMul.hMul (α := CoordinateRing W) (β := CoordinateRing W)
      ((mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) (W.preΨ n)) : CoordinateRing W)
      ((mk W : (a : R[X][Y]) → CoordinateRing W) (if Even n then W.ψ₂ else 1)))
    2 =
  HMul.hMul (α := CoordinateRing W) (β := CoordinateRing W)
    ((mk W : (a : R[X][Y]) → CoordinateRing W)
        ((C : (a : R[X]) → R[X][Y]) (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ n) 2)) :
      CoordinateRing W)
    ((mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) (if Even n then W.Ψ₂Sq else 1)) :
      CoordinateRing W)
Tactic: simp_rw [Ψ, ΨSq, map_mul, apply_ite C, apply_ite <| mk W, mul_pow, ite_pow, mk_ψ₂_sq, map_one,
    one_pow, map_pow]