awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
F : Type u
inst : Field F
W : Affine F
P Q : W.Point
x₁ y : F
h_1 : W.Nonsingular x₁ y
x₂ y_1 : F
h_2 : W.Nonsingular x₂ y_1
h : (some x₁ y h_1).xRep = (some x₂ y_1 h_2).xRep
⊢ some x₁ y h_1 = some x₂ y_1 h_2 ∨ some x₁ y h_1 = -some x₂ y_1 h_2
have h₁ : x₁ = x₂
Tactic: simp only [xRep, Matrix.vecCons_inj, and_true] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
P Q : W.Point
⊢ P.xRep = Q.xRep ↔ P = Q ∨ P = -Q
have refine : ∀ (H : P = Q ∨ P = -Q), P.xRep = Q.xRep
Tactic: refine ⟨eq_or_eq_neg_of_xRep_eq_xRep, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
P Q : W.Point
H : P = Q ∨ P = -Q
⊢ P.xRep = Q.xRep
have inl : P.xRep = P.xRep
Tactic: rcases H with rfl | rfl
Cleared hypotheses: Q, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
P Q : W.Point
H : P = Q ∨ P = -Q
inl : P.xRep = P.xRep
⊢ P.xRep = Q.xRep
have inr : (-Q).xRep = Q.xRep
Tactic: rcases H with rfl | rfl
Cleared hypotheses: P, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ (C : (a : R[X]) → R[X][Y]) W.Ψ₂Sq =
    HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2 - HMul.hMul (α := R[X][Y]) 4 W.toAffine.polynomial
have rw : (C : (a : R[X]) → R[X][Y])
    (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]) (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) : R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (2 * (2 * W.a₄ + W.a₁ * W.a₃)) : R[X]) X)
      ((C : (a : R) → R[X]) (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆) : R[X])) =
  HPow.hPow (β := ℕ)
      (HAdd.hAdd (β := R[X][Y])
        (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) 2) : R[X][Y]) Y)
        ((C : (a : R[X]) → R[X][Y])
            (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.toAffine.a₁ : R[X]) X)
              ((C : (a : R) → R[X]) W.toAffine.a₃ : R[X])) :
          R[X][Y]))
      2 -
    4 *
      HSub.hSub (β := R[X][Y])
        (HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
          HMul.hMul (α := R[X][Y]) (β := R[X][Y])
            ((C : (a : R[X]) → R[X][Y])
                (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.toAffine.a₁ : R[X]) X)
                  ((C : (a : R) → R[X]) W.toAffine.a₃ : R[X])) :
              R[X][Y])
            Y)
        ((C : (a : R[X]) → R[X][Y])
            (HAdd.hAdd (β := R[X])
              (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W.toAffine.a₂ : R[X])
                    (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.toAffine.a₄ : R[X]) X)
              ((C : (a : R) → R[X]) W.toAffine.a₆ : R[X])) :
          R[X][Y])
Tactic: rw [Ψ₂Sq, ψ₂, b₂, b₄, b₆, Affine.polynomialY, Affine.polynomial]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ W.ΨSq (2 * m) =
    HPow.hPow (β := ℕ)
        (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)
        2 *
      W.Ψ₂Sq
have rw : (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (2 * m)) 2 * if Even (2 * m) then W.Ψ₂Sq else 1) =
  HPow.hPow (β := ℕ)
      (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)
      2 *
    W.Ψ₂Sq
Tactic: rw [ΨSq, preΨ_even, if_pos <| even_two_mul m]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
rw :
  (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (2 * m)) 2 * if Even (2 * m) then W.Ψ₂Sq else 1) =
    HPow.hPow (β := ℕ)
        (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)
        2 *
      W.Ψ₂Sq
⊢ W.ΨSq (2 * m) =
    HPow.hPow (β := ℕ)
        (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)
        2 *
      W.Ψ₂Sq
have rw₁ : (HPow.hPow (β := ℕ)
      (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)
      2 *
    if Even (2 * m) then W.Ψ₂Sq else 1) =
  HPow.hPow (β := ℕ)
      (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)
      2 *
    W.Ψ₂Sq
Tactic: rw [ΨSq, preΨ_even, if_pos <| even_two_mul m]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
rw :
  (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (2 * m)) 2 * if Even (2 * m) then W.Ψ₂Sq else 1) =
    HPow.hPow (β := ℕ)
        (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)
        2 *
      W.Ψ₂Sq
rw₁ :
  (HPow.hPow (β := ℕ)
        (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)
        2 *
      if Even (2 * m) then W.Ψ₂Sq else 1) =
    HPow.hPow (β := ℕ)
        (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)
        2 *
      W.Ψ₂Sq
⊢ W.ΨSq (2 * m) =
    HPow.hPow (β := ℕ)
        (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)
        2 *
      W.Ψ₂Sq
have rw₂ : HPow.hPow (β := ℕ)
      (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)
      2 *
    W.Ψ₂Sq =
  HPow.hPow (β := ℕ)
      (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)
      2 *
    W.Ψ₂Sq
Tactic: rw [ΨSq, preΨ_even, if_pos <| even_two_mul m]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ W.ΨSq (2 * m + 1) =
    HPow.hPow (β := ℕ)
      ((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)
      2
have rw : (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (2 * m + 1)) 2 * if Even (2 * m + 1) then W.Ψ₂Sq else 1) =
  HPow.hPow (β := ℕ)
    ((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)
    2
Tactic: rw [ΨSq, preΨ_odd, if_neg m.not_even_two_mul_add_one, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
rw :
  (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (2 * m + 1)) 2 * if Even (2 * m + 1) then W.Ψ₂Sq else 1) =
    HPow.hPow (β := ℕ)
      ((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)
      2
⊢ W.ΨSq (2 * m + 1) =
    HPow.hPow (β := ℕ)
      ((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)
      2
have rw₁ : (HPow.hPow (β := ℕ)
      ((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)
      2 *
    if Even (2 * m + 1) then W.Ψ₂Sq else 1) =
  HPow.hPow (β := ℕ)
    ((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)
    2
Tactic: rw [ΨSq, preΨ_odd, if_neg m.not_even_two_mul_add_one, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
rw :
  (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (2 * m + 1)) 2 * if Even (2 * m + 1) then W.Ψ₂Sq else 1) =
    HPow.hPow (β := ℕ)
      ((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)
      2
rw₁ :
  (HPow.hPow (β := ℕ)
        ((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)
        2 *
      if Even (2 * m + 1) then W.Ψ₂Sq else 1) =
    HPow.hPow (β := ℕ)
      ((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)
      2
⊢ W.ΨSq (2 * m + 1) =
    HPow.hPow (β := ℕ)
      ((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)
      2
have rw₂ : HPow.hPow (β := ℕ)
      ((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)
      2 *
    1 =
  HPow.hPow (β := ℕ)
    ((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)
    2
Tactic: rw [ΨSq, preΨ_odd, if_neg m.not_even_two_mul_add_one, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
rw :
  (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (2 * m + 1)) 2 * if Even (2 * m + 1) then W.Ψ₂Sq else 1) =
    HPow.hPow (β := ℕ)
      ((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)
      2
rw₁ :
  (HPow.hPow (β := ℕ)
        ((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)
        2 *
      if Even (2 * m + 1) then W.Ψ₂Sq else 1) =
    HPow.hPow (β := ℕ)
      ((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)
      2
rw₂ :
  HPow.hPow (β := ℕ)
        ((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)
        2 *
      1 =
    HPow.hPow (β := ℕ)
      ((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)
      2
⊢ W.ΨSq (2 * m + 1) =
    HPow.hPow (β := ℕ)
      ((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)
      2
have rw₃ : HPow.hPow (β := ℕ)
    ((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)
    2 =
  HPow.hPow (β := ℕ)
    ((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)
    2
Tactic: rw [ΨSq, preΨ_odd, if_neg m.not_even_two_mul_add_one, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ Eq (α := R[X][Y]) (W.Ψ (-n)) (-W.Ψ n)
have simp_rw : 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) =
  -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)
Tactic: simp_rw [Ψ, preΨ_neg, C_neg, neg_mul, even_neg]
-- 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]) (W.Ψ (2 * m)) W.ψ₂ =
    HPow.hPow (α := R[X][Y]) (β := ℕ) (W.Ψ (m - 1)) 2 * W.Ψ m * W.Ψ (m + 2) -
      HMul.hMul (α := R[X][Y]) (W.Ψ (m - 2)) (W.Ψ m) * HPow.hPow (α := R[X][Y]) (β := ℕ) (W.Ψ (m + 1)) 2
have simp_rw : 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])
            (if ¬Even m then W.ψ₂ else 1))
          2 *
        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) *
      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) -
    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) *
        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) *
      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))
        2
Tactic: simp_rw [Ψ, preΨ_even, if_pos <| even_two_mul m, 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])
            (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])
              (if ¬Even m then W.ψ₂ else 1))
            2 *
          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) *
        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) -
      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) *
          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) *
        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))
          2
have pos : 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])
              (1 : R[X][Y]))
            2 *
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) W.ψ₂ *
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) W.ψ₂ -
      HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 2)) : R[X][Y]) W.ψ₂ *
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : 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])
            (1 : R[X][Y]))
          2
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])
            (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])
              (1 : R[X][Y]))
            2 *
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) W.ψ₂ *
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) W.ψ₂ -
      HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 2)) : R[X][Y]) W.ψ₂ *
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : 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])
            (1 : R[X][Y]))
          2
have pos : (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])
            (1 : R[X][Y]))
          2 *
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) W.ψ₂ *
      HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) W.ψ₂ -
    HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 2)) : R[X][Y]) W.ψ₂ *
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : 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]) (1 : R[X][Y]))
        2
Tactic: C_simp