awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
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])
⊢ 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:
C_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ 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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ 3 = HAdd.hAdd (α := ℤ) (↑2 : ℤ) 1

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ Even (α := ℕ) 2

Tactic:
decide
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
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
rw₈ 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
⊢ W.Φ 3 = 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]

Premises used: even_two, WeierstrassCurve.preΨ'_three, if_pos, WeierstrassCurve.Φ_ofNat, mul_one, WeierstrassCurve.preΨ'_two, WeierstrassCurve.preΨ'_four
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ 4 = HAdd.hAdd (α := ℤ) (↑3 : ℤ) 1

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ ¬Even (α := ℕ) 3

Tactic:
decide
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ HAdd.hAdd (α := ℕ) 3 2 = HMul.hMul (α := ℕ) 2 2 + 1

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

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]

Premises used: Even.zero, WeierstrassCurve.preΨ'_one, WeierstrassCurve.preΨ'_three, if_pos, WeierstrassCurve.Φ_ofNat, WeierstrassCurve.preΨ'_odd, if_neg, WeierstrassCurve.preΨ'_two, WeierstrassCurve.preΨ'_four
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ 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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
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
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)

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]

Premises used: neg_add', neg_sub', WeierstrassCurve.preΨ_neg, neg_mul_neg, mul_comm, WeierstrassCurve.ΨSq_neg, WeierstrassCurve.preΨ, WeierstrassCurve.Φ, even_neg, sub_neg_eq_add
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ Eq (α := R[X][Y]) (W.ψ 0) 0

Tactic:
normEDS_zero ..

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

Tactic:
normEDS_one ..

Premises used: WeierstrassCurve.ψ, normEDS_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ Eq (α := R[X][Y]) (W.ψ 2) W.ψ₂

Tactic:
normEDS_two ..

Premises used: normEDS_two, WeierstrassCurve.ψ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ Eq (α := R[X][Y]) (W.ψ 3) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃)

Tactic:
normEDS_three ..

Premises used: WeierstrassCurve.ψ, normEDS_three
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ W.ψ 4 = HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y]) W.ψ₂

Tactic:
normEDS_four ..

Premises used: WeierstrassCurve.ψ, normEDS_four
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ Eq (α := R[X][Y]) (W.ψ (-n)) (-W.ψ n)

Tactic:
normEDS_neg ..

Premises used: WeierstrassCurve.ψ, normEDS_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
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

Tactic:
normEDS_even ..

Premises used: WeierstrassCurve.ψ, normEDS_even
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
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

Tactic:
normEDS_odd ..

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

Tactic:
simp [φ]

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

Tactic:
simp [φ]

Premises used: WeierstrassCurve.φ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ W.φ 2 =
    HSub.hSub (β := R[X][Y])
      (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) (HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2))
      ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y])

Tactic:
simp [φ]

Premises used: WeierstrassCurve.φ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ W.φ 3 =
    HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])
        (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) 2) -
      HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y]) (HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2)

Tactic:
simp [φ, mul_assoc, sq]

Premises used: mul_assoc, WeierstrassCurve.φ, sq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ HAdd.hAdd (α := ℤ) 4 1 = HMul.hMul (α := ℤ) 2 2 + 1

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ HSub.hSub (α := ℤ) 2 1 = 1

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ HSub.hSub (α := ℤ) 4 1 = 3

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
rw :
  HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])
        (HPow.hPow (β := ℕ)
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y]) W.ψ₂) 2) -
      HMul.hMul (β := R[X][Y])
        (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y]) W.ψ₂ *
            HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 3 -
          1 * HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) 3)
        ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) =
    HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y]) 2) *
          HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2 -
        HMul.hMul (β := R[X][Y])
          (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 4))
          ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) +
      HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) 4
⊢ W.φ 4 =
    HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y]) 2) *
          HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2 -
        HMul.hMul (β := R[X][Y])
          (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 4))
          ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) +
      HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) 4

Tactic:
rw [φ, ψ_four, show (4 + 1 : ℤ) = 2 * 2 + 1 by rfl, ψ_odd, two_add_two_eq_four, ψ_four,
    show (2 - 1 : ℤ) = 1 by rfl, ψ_two, ψ_one, two_add_one_eq_three, show (4 - 1 : ℤ) = 3 by rfl,
    ψ_three]

Premises used: WeierstrassCurve.ψ_two, WeierstrassCurve.φ, WeierstrassCurve.ψ_one, WeierstrassCurve.ψ_odd, WeierstrassCurve.ψ_three, two_add_one_eq_three, two_add_two_eq_four, WeierstrassCurve.ψ_four
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])
        (HPow.hPow (β := ℕ)
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y]) W.ψ₂) 2) -
      HMul.hMul (β := R[X][Y])
        (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y]) W.ψ₂ *
            HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 3 -
          1 * HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) 3)
        ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) =
    HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y]) 2) *
          HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2 -
        HMul.hMul (β := R[X][Y])
          (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 4))
          ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) +
      HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) 4

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
simp_rw :
  HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) (HPow.hPow (α := R[X][Y]) (β := ℕ) (-W.ψ n) 2) -
      HMul.hMul (α := R[X][Y]) (W.ψ (-n + 1)) (W.ψ (-n - 1)) =
    HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) (HPow.hPow (α := R[X][Y]) (β := ℕ) (W.ψ n) 2) -
      HMul.hMul (α := R[X][Y]) (W.ψ (n + 1)) (W.ψ (n - 1))
⊢ Eq (α := R[X][Y]) (W.φ (-n)) (W.φ n)

Tactic:
simp_rw [φ, ψ_neg, neg_sq, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add, ← neg_add', ψ_neg,
    neg_mul_neg, mul_comm <| W.ψ <| n - 1]

Premises used: WeierstrassCurve.ψ, neg_sq, WeierstrassCurve.φ, neg_add', neg_sub', WeierstrassCurve.ψ_neg, neg_mul_neg, mul_comm, sub_neg_eq_add
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
f : R →+* S
⊢ (W.map f).Ψ₂Sq = Polynomial.map f W.Ψ₂Sq

Tactic:
simp [Ψ₂Sq, map_ofNat]

Premises used: map_ofNat, WeierstrassCurve.Ψ₂Sq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
f : R →+* S
⊢ (W.map f).Ψ₃ = Polynomial.map f W.Ψ₃

Tactic:
simp [Ψ₃]

Premises used: WeierstrassCurve.Ψ₃
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
f : R →+* S
⊢ (W.map f).preΨ₄ = Polynomial.map f W.preΨ₄

Tactic:
simp [preΨ₄]

Premises used: WeierstrassCurve.preΨ₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℕ
⊢ (W.map f).preΨ' n = Polynomial.map f (W.preΨ' n)

Tactic:
simp [preΨ', ← coe_mapRingHom]

Premises used: Polynomial.coe_mapRingHom, WeierstrassCurve.preΨ'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).preΨ n = Polynomial.map f (W.preΨ n)

Tactic:
simp [preΨ, ← coe_mapRingHom]

Premises used: Polynomial.coe_mapRingHom, WeierstrassCurve.preΨ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).ΨSq n = Polynomial.map f (W.ΨSq n)

Tactic:
simp [ΨSq, ← coe_mapRingHom, apply_ite <| mapRingHom f]

Premises used: apply_ite, WeierstrassCurve.ΨSq, Polynomial.coe_mapRingHom, Polynomial.mapRingHom
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ Eq (α := S[X][Y]) ((W.map f).Ψ n) ((mapRingHom (mapRingHom f) : (a : R[X][Y]) → S[X][Y]) (W.Ψ n))

Tactic:
simp [Ψ, apply_ite <| mapRingHom _]

Premises used: apply_ite, WeierstrassCurve.Ψ, Polynomial.mapRingHom
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ Eq (α := S[X]) ((W.map f).Φ n) ((mapRingHom f : (a : R[X]) → S[X]) (W.Φ n))

Tactic:
simp [Φ, map_sub, apply_ite <| mapRingHom f]

Premises used: map_sub, apply_ite, Polynomial.mapRingHom, WeierstrassCurve.Φ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ Eq (α := S[X][Y]) ((W.map f).ψ n) ((mapRingHom (mapRingHom f) : (a : R[X][Y]) → S[X][Y]) (W.ψ n))

Tactic:
simp [ψ]

Premises used: WeierstrassCurve.ψ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).φ n = Polynomial.map (mapRingHom f) (W.φ n)

Tactic:
simp [φ]

Premises used: WeierstrassCurve.φ