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
rw :
  W.Φ (HAdd.hAdd (α := ℤ) (↑2 : ℤ) 1) = X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₁ :
  ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (HAdd.hAdd (α := ℕ) 2 1)) 2 * if Even (α := ℕ) 2 then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (HAdd.hAdd (α := ℕ) 2 2)) (W.preΨ' 2) * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₂ :
  ((X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 * if Even (α := ℕ) 2 then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (HAdd.hAdd (α := ℕ) 2 2)) (W.preΨ' 2) * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₃ :
  (X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 * 1 -
      HMul.hMul (α := R[X]) (W.preΨ' (HAdd.hAdd (α := ℕ) 2 2)) (W.preΨ' 2) * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₄ :
  (X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 -
      HMul.hMul (α := R[X]) (W.preΨ' (HAdd.hAdd (α := ℕ) 2 2)) (W.preΨ' 2) * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₅ :
  (X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 -
      HMul.hMul (α := R[X]) W.preΨ₄ (W.preΨ' 2) * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
⊢ W.Φ 3 = X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
have rw₆ : (X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ 1 * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
  X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
Tactic: rw [show 3 = ((2 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_three, if_pos <| by decide, mul_one,
    preΨ'_four, preΨ'_two, mul_one, if_pos even_two]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
rw :
  W.Φ (HAdd.hAdd (α := ℤ) (↑2 : ℤ) 1) = X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₁ :
  ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (HAdd.hAdd (α := ℕ) 2 1)) 2 * if Even (α := ℕ) 2 then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (HAdd.hAdd (α := ℕ) 2 2)) (W.preΨ' 2) * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₂ :
  ((X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 * if Even (α := ℕ) 2 then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (HAdd.hAdd (α := ℕ) 2 2)) (W.preΨ' 2) * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₃ :
  (X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 * 1 -
      HMul.hMul (α := R[X]) (W.preΨ' (HAdd.hAdd (α := ℕ) 2 2)) (W.preΨ' 2) * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₄ :
  (X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 -
      HMul.hMul (α := R[X]) (W.preΨ' (HAdd.hAdd (α := ℕ) 2 2)) (W.preΨ' 2) * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₅ :
  (X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 -
      HMul.hMul (α := R[X]) W.preΨ₄ (W.preΨ' 2) * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₆ :
  (X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 -
      HMul.hMul (α := R[X]) W.preΨ₄ 1 * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
⊢ W.Φ 3 = X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
have rw₇ : X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ (if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
  X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
Tactic: rw [show 3 = ((2 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_three, if_pos <| by decide, mul_one,
    preΨ'_four, preΨ'_two, mul_one, if_pos even_two]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
rw :
  W.Φ (HAdd.hAdd (α := ℤ) (↑2 : ℤ) 1) = X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₁ :
  ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (HAdd.hAdd (α := ℕ) 2 1)) 2 * if Even (α := ℕ) 2 then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (HAdd.hAdd (α := ℕ) 2 2)) (W.preΨ' 2) * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₂ :
  ((X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 * if Even (α := ℕ) 2 then 1 else W.Ψ₂Sq) -
      HMul.hMul (α := R[X]) (W.preΨ' (HAdd.hAdd (α := ℕ) 2 2)) (W.preΨ' 2) * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₃ :
  (X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 * 1 -
      HMul.hMul (α := R[X]) (W.preΨ' (HAdd.hAdd (α := ℕ) 2 2)) (W.preΨ' 2) * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₄ :
  (X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 -
      HMul.hMul (α := R[X]) (W.preΨ' (HAdd.hAdd (α := ℕ) 2 2)) (W.preΨ' 2) * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₅ :
  (X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 -
      HMul.hMul (α := R[X]) W.preΨ₄ (W.preΨ' 2) * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₆ :
  (X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 -
      HMul.hMul (α := R[X]) W.preΨ₄ 1 * if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
rw₇ :
  X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ (if Even (α := ℕ) 2 then W.Ψ₂Sq else 1) =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
⊢ W.Φ 3 = X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
have rw₈ : X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq =
  X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
Tactic: rw [show 3 = ((2 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_three, if_pos <| by decide, mul_one,
    preΨ'_four, preΨ'_two, mul_one, if_pos even_two]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 4 =
    X * HPow.hPow (α := R[X]) (β := ℕ) W.preΨ₄ 2 * W.Ψ₂Sq -
      W.Ψ₃ * (W.preΨ₄ * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 - HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 3)
have rw : X * HPow.hPow (α := R[X]) (β := ℕ) W.preΨ₄ 2 * W.Ψ₂Sq -
    (W.preΨ₄ * HPow.hPow (α := R[X]) (β := ℕ) 1 3 * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 -
          1 * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 3 * 1) *
        W.Ψ₃ *
      1 =
  X * HPow.hPow (α := R[X]) (β := ℕ) W.preΨ₄ 2 * W.Ψ₂Sq -
    W.Ψ₃ * (W.preΨ₄ * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2 - HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 3)
Tactic: rw [show 4 = ((3 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_four, if_neg <| by decide,
    show 3 + 2 = 2 * 2 + 1 by rfl, preΨ'_odd, preΨ'_four, preΨ'_two, if_pos Even.zero, preΨ'_one,
    preΨ'_three, if_pos Even.zero, if_neg <| by decide]
-- 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]) (W.Φ (-n)) (W.Φ n)
have simp_rw : (HMul.hMul (α := R[X]) X (W.ΨSq (-n)) -
    HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
  HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
Tactic: simp_rw [Φ, ΨSq_neg, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add, ← neg_add', preΨ_neg,
    neg_mul_neg, mul_comm <| W.preΨ <| n - 1, even_neg]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
simp_rw :
  (HMul.hMul (α := R[X]) X (W.ΨSq (-n)) -
      HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
⊢ Eq (α := R[X]) (W.Φ (-n)) (W.Φ n)
have simp_rw₁ : (HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
  HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
Tactic: simp_rw [Φ, ΨSq_neg, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add, ← neg_add', preΨ_neg,
    neg_mul_neg, mul_comm <| W.preΨ <| n - 1, even_neg]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
simp_rw :
  (HMul.hMul (α := R[X]) X (W.ΨSq (-n)) -
      HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₁ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
⊢ Eq (α := R[X]) (W.Φ (-n)) (W.Φ n)
have simp_rw₂ : (HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (W.preΨ (-n - -1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
  HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (W.preΨ (n - -1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
Tactic: simp_rw [Φ, ΨSq_neg, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add, ← neg_add', preΨ_neg,
    neg_mul_neg, mul_comm <| W.preΨ <| n - 1, even_neg]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
simp_rw :
  (HMul.hMul (α := R[X]) X (W.ΨSq (-n)) -
      HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₁ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₂ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-n - -1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n - -1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
⊢ Eq (α := R[X]) (W.Φ (-n)) (W.Φ n)
have simp_rw₃ : (HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (W.preΨ (-(n - 1))) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
  HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (W.preΨ (n - -1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
Tactic: simp_rw [Φ, ΨSq_neg, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add, ← neg_add', preΨ_neg,
    neg_mul_neg, mul_comm <| W.preΨ <| n - 1, even_neg]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
simp_rw :
  (HMul.hMul (α := R[X]) X (W.ΨSq (-n)) -
      HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₁ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₂ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-n - -1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n - -1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₃ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-(n - 1))) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n - -1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
⊢ Eq (α := R[X]) (W.Φ (-n)) (W.Φ n)
have simp_rw₄ : (HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (W.preΨ (-(n - 1))) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
  HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
Tactic: simp_rw [Φ, ΨSq_neg, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add, ← neg_add', preΨ_neg,
    neg_mul_neg, mul_comm <| W.preΨ <| n - 1, even_neg]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
simp_rw :
  (HMul.hMul (α := R[X]) X (W.ΨSq (-n)) -
      HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₁ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₂ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-n - -1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n - -1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₃ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-(n - 1))) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n - -1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₄ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-(n - 1))) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
⊢ Eq (α := R[X]) (W.Φ (-n)) (W.Φ n)
have simp_rw₅ : (HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (W.preΨ (-(n - 1))) (W.preΨ (-(n + 1))) * if Even (-n) then 1 else W.Ψ₂Sq) =
  HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
Tactic: simp_rw [Φ, ΨSq_neg, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add, ← neg_add', preΨ_neg,
    neg_mul_neg, mul_comm <| W.preΨ <| n - 1, even_neg]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
simp_rw :
  (HMul.hMul (α := R[X]) X (W.ΨSq (-n)) -
      HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₁ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₂ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-n - -1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n - -1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₃ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-(n - 1))) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n - -1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₄ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-(n - 1))) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₅ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-(n - 1))) (W.preΨ (-(n + 1))) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
⊢ Eq (α := R[X]) (W.Φ (-n)) (W.Φ n)
have simp_rw₆ : (HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (-W.preΨ (n - 1)) (-W.preΨ (n + 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
  HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
Tactic: simp_rw [Φ, ΨSq_neg, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add, ← neg_add', preΨ_neg,
    neg_mul_neg, mul_comm <| W.preΨ <| n - 1, even_neg]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
simp_rw :
  (HMul.hMul (α := R[X]) X (W.ΨSq (-n)) -
      HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₁ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₂ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-n - -1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n - -1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₃ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-(n - 1))) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n - -1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₄ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-(n - 1))) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₅ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-(n - 1))) (W.preΨ (-(n + 1))) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₆ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (-W.preΨ (n - 1)) (-W.preΨ (n + 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
⊢ Eq (α := R[X]) (W.Φ (-n)) (W.Φ n)
have simp_rw₇ : (HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (W.preΨ (n - 1)) (W.preΨ (n + 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
  HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
Tactic: simp_rw [Φ, ΨSq_neg, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add, ← neg_add', preΨ_neg,
    neg_mul_neg, mul_comm <| W.preΨ <| n - 1, even_neg]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
simp_rw :
  (HMul.hMul (α := R[X]) X (W.ΨSq (-n)) -
      HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₁ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-n + 1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₂ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-n - -1)) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n - -1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₃ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-(n - 1))) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n - -1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₄ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-(n - 1))) (W.preΨ (-n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₅ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (-(n - 1))) (W.preΨ (-(n + 1))) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₆ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (-W.preΨ (n - 1)) (-W.preΨ (n + 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
simp_rw₇ :
  (HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n - 1)) (W.preΨ (n + 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
    HMul.hMul (α := R[X]) X (W.ΨSq n) -
      HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
⊢ Eq (α := R[X]) (W.Φ (-n)) (W.Φ n)
have simp_rw₈ : (HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even (-n) then 1 else W.Ψ₂Sq) =
  HMul.hMul (α := R[X]) X (W.ΨSq n) -
    HMul.hMul (α := R[X]) (W.preΨ (n + 1)) (W.preΨ (n - 1)) * if Even n then 1 else W.Ψ₂Sq
Tactic: simp_rw [Φ, ΨSq_neg, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add, ← neg_add', preΨ_neg,
    neg_mul_neg, mul_comm <| W.preΨ <| n - 1, even_neg]