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
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))
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)
⊢ 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)
        (if Even n then (C : (a : R[X]) → R[X][Y]) W.Ψ₂Sq else (C : (a : R[X]) → R[X][Y]) 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ 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
have 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
Tactic: rw [Φ, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (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
have 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
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (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
have 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
Tactic: simp_rw [ΨSq_ofNat, Nat.even_add_one, ite_not, ← mul_assoc, preΨ_ofNat]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
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
⊢ (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
have 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
Tactic: simp_rw [ΨSq_ofNat, Nat.even_add_one, ite_not, ← mul_assoc, preΨ_ofNat]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
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
⊢ (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
have 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
Tactic: simp_rw [ΨSq_ofNat, Nat.even_add_one, ite_not, ← mul_assoc, preΨ_ofNat]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
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
⊢ (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
have 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
Tactic: simp_rw [ΨSq_ofNat, Nat.even_add_one, ite_not, ← mul_assoc, preΨ_ofNat]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ 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])
have 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])
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, Ψ₃]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ 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])
have C_simp : X * HPow.hPow (α := R[X]) (β := ℕ) 1 2 *
      HAdd.hAdd (β := 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]) (2 : R[X]) ((C : (a : R) → R[X]) 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]) (2 : R[X]) ((C : (a : R) → R[X]) W.b₆ : R[X]) * X)
    ((C : (a : R) → R[X]) W.b₈ : R[X])
Tactic: C_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 3 = X * HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2 - HMul.hMul (α := R[X]) W.preΨ₄ W.Ψ₂Sq
have rw : W.Φ (HAdd.hAdd (α := ℤ) (↑2 : ℤ) 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
⊢ 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.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
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
⊢ 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 * 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
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
⊢ 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 * 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
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
⊢ 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Ψ' (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
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
⊢ 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.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
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]