awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℕ
⊢ W.preΨ' (2 * (m + 3)) =
    HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 2)) 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) -
      HMul.hMul (α := R[X]) (W.preΨ' (m + 1)) (W.preΨ' (m + 3)) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 4)) 2

Tactic:
preNormEDS'_even ..

Premises used: preNormEDS'_even, WeierstrassCurve.preΨ'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℕ
⊢ W.preΨ' (2 * (m + 2) + 1) =
    (W.preΨ' (m + 4) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (m + 2)) 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 + 3)) 3 *
        if Even m then 1 else HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2

Tactic:
preNormEDS'_odd ..

Premises used: preNormEDS'_odd, WeierstrassCurve.preΨ'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ Eq (α := R[X]) (W.preΨ (↑n : ℤ)) (W.preΨ' n)

Tactic:
preNormEDS_ofNat ..

Premises used: preNormEDS_ofNat, WeierstrassCurve.preΨ', WeierstrassCurve.preΨ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ Eq (α := R[X]) (W.preΨ 0) 0

Tactic:
preNormEDS_zero ..

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

Tactic:
preNormEDS_one ..

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

Tactic:
preNormEDS_two ..

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

Tactic:
preNormEDS_three ..

Premises used: preNormEDS_three, WeierstrassCurve.preΨ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ Eq (α := R[X]) (W.preΨ 4) W.preΨ₄

Tactic:
preNormEDS_four ..

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

Tactic:
preNormEDS_neg ..

Premises used: preNormEDS_neg, WeierstrassCurve.preΨ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ W.preΨ (2 * m) =
    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

Tactic:
preNormEDS_even ..

Premises used: preNormEDS_even, WeierstrassCurve.preΨ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ W.preΨ (2 * m + 1) =
    (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

Tactic:
preNormEDS_odd ..

Premises used: preNormEDS_odd, WeierstrassCurve.preΨ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ W.ΨSq (↑n : ℤ) = HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' n) 2 * if Even n then W.Ψ₂Sq else 1

Tactic:
simp [ΨSq]

Premises used: WeierstrassCurve.ΨSq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ Eq (α := R[X]) (W.ΨSq 0) 0

Tactic:
simp [ΨSq]

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

Tactic:
simp [ΨSq]

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

Tactic:
simp [ΨSq]

Premises used: WeierstrassCurve.ΨSq
-- 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
⊢ W.ΨSq 3 = HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₃ 2

Tactic:
simp [ΨSq, show ¬Even (3 : ℤ) by decide]

Premises used: WeierstrassCurve.ΨSq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ ¬Odd (α := ℤ) 4

Tactic:
decide
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ W.ΨSq 4 = HPow.hPow (α := R[X]) (β := ℕ) W.preΨ₄ 2 * W.Ψ₂Sq

Tactic:
simp [ΨSq, show ¬Odd (4 : ℤ) by decide]

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

Tactic:
simp [ΨSq]

Premises used: WeierstrassCurve.ΨSq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
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
rw₂ 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
⊢ 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

Tactic:
rw [ΨSq, preΨ_even, if_pos <| even_two_mul m]

Premises used: WeierstrassCurve.ΨSq, if_pos, even_two_mul, WeierstrassCurve.preΨ_even
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
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
rw₃ 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
⊢ 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

Tactic:
rw [ΨSq, preΨ_odd, if_neg m.not_even_two_mul_add_one, mul_one]

Premises used: WeierstrassCurve.preΨ_odd, WeierstrassCurve.ΨSq, Int.not_even_two_mul_add_one, mul_one, if_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ W.Ψ (↑n : ℤ) =
    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 [Ψ]

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

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) 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.Ψ 2) W.ψ₂

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.Ψ 3) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃)

Tactic:
simp [Ψ, show ¬Even (3 : ℤ) by decide]

Premises used: WeierstrassCurve.Ψ
-- 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:
simp [Ψ, show ¬Odd (4 : ℤ) by decide]

Premises used: WeierstrassCurve.Ψ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
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)
⊢ Eq (α := R[X][Y]) (W.Ψ (-n)) (-W.Ψ n)

Tactic:
simp_rw [Ψ, preΨ_neg, C_neg, neg_mul, even_neg]

Premises used: WeierstrassCurve.Ψ, WeierstrassCurve.preΨ_neg, neg_mul, Polynomial.C_neg, even_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
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
⊢ 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:
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]

Premises used: iff_false, even_two, Int.not_even_one, iff_true, WeierstrassCurve.Ψ, if_pos, Int.even_add, even_two_mul, Int.even_sub, WeierstrassCurve.preΨ_even
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
h : Even m
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
⊢ 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:
C_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
h : ¬Even m
neg :
  (HMul.hMul (β := R[X][Y])
            (HMul.hMul (β := R[X][Y])
              (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) 2)
              ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]))
            ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) -
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 2)) : R[X][Y])
              ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) *
            HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) 2) *
        W.ψ₂ *
      W.ψ₂ =
    HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) W.ψ₂) 2 *
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) (1 : R[X][Y]) *
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) (1 : R[X][Y]) -
      HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 2)) : R[X][Y]) (1 : R[X][Y]) *
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) (1 : R[X][Y]) *
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) W.ψ₂) 2
⊢ HMul.hMul (α := R[X][Y]) (β := R[X][Y])
        ((C : (a : R[X]) → R[X][Y])
            (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m - 1)) 2 * W.preΨ m * W.preΨ (m + 2) -
              HMul.hMul (α := R[X]) (W.preΨ (m - 2)) (W.preΨ m) * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ (m + 1)) 2) :
          R[X][Y])
        W.ψ₂ *
      W.ψ₂ =
    HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) W.ψ₂) 2 *
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) (1 : R[X][Y]) *
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) (1 : R[X][Y]) -
      HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 2)) : R[X][Y]) (1 : R[X][Y]) *
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) (1 : R[X][Y]) *
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) W.ψ₂) 2

Tactic:
C_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
h : Even m
⊢ (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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
m : ℤ
h : ¬Even m
⊢ (HMul.hMul (β := R[X][Y])
            (HMul.hMul (β := R[X][Y])
              (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) 2)
              ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]))
            ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) -
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 2)) : R[X][Y])
              ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) *
            HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) 2) *
        W.ψ₂ *
      W.ψ₂ =
    HPow.hPow (β := ℕ)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 1)) : R[X][Y]) W.ψ₂) 2 *
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) (1 : R[X][Y]) *
        HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 2)) : R[X][Y]) (1 : R[X][Y]) -
      HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m - 2)) : R[X][Y]) (1 : R[X][Y]) *
          HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ m) : R[X][Y]) (1 : R[X][Y]) *
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ (m + 1)) : R[X][Y]) W.ψ₂) 2

Tactic:
ring1