awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
push_cast :
  (HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 6)) : ℤ) =
        2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 2)) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 5)) : ℤ) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 6)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) + 3 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 2)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) + 3 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)
⊢ (expDegree (2 * (m + 3)) = 2 * expDegree (m + 2) + expDegree (m + 3) + expDegree (m + 5) ∧
      expDegree (2 * (m + 3)) = expDegree (m + 1) + expDegree (m + 3) + 2 * expDegree (m + 4)) ∧
    (expDegree (2 * (m + 2) + 1) =
        expDegree (m + 4) + 3 * expDegree (m + 2) + if Even m then HMul.hMul (α := ℕ) 2 3 else 0) ∧
      expDegree (2 * (m + 2) + 1) =
        expDegree (m + 1) + 3 * expDegree (m + 3) + if Even m then 0 else HMul.hMul (α := ℕ) 2 3

Tactic:
push_cast [← @Nat.cast_inj ℤ, ← mul_left_cancel_iff_of_pos (b := (expDegree _ : ℤ)) two_pos,
    mul_add, mul_left_comm (2 : ℤ)]

Premises used: two_pos, Nat.cast_inj, mul_left_comm, mul_add, OfNat.ofNat, mul_left_cancel_iff_of_pos
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
⊢ 2 * m + 6 ≠ 0

Tactic:
lia
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
rw :
  ((HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 2)) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 5)) : ℤ) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) + 3 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 2)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) + 3 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)
⊢ (HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 6)) : ℤ) =
        2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 2)) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 5)) : ℤ) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 6)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) + 3 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 2)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) + 3 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)

Tactic:
rw [expDegree_cast <| by lia]

Premises used: _private.0.WeierstrassCurve.expDegree_cast
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
⊢ m + 2 ≠ 0

Tactic:
lia
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
rw :
  ((HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
            HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 5)) : ℤ) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) + 3 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)
⊢ ((HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 2)) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 5)) : ℤ) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) + 3 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 2)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) + 3 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)

Tactic:
rw [expDegree_cast <| by lia]

Premises used: _private.0.WeierstrassCurve.expDegree_cast
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
⊢ m + 3 ≠ 0

Tactic:
lia
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
rw :
  ((HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 5)) : ℤ) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)
⊢ ((HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
            HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 5)) : ℤ) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) + 3 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)

Tactic:
rw [expDegree_cast <| by lia]

Premises used: _private.0.WeierstrassCurve.expDegree_cast
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
⊢ m + 5 ≠ 0

Tactic:
lia
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
rw :
  ((HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 5) : ℤ) 2 - if Even (m + 5) then 4 else 1) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)
⊢ ((HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 5)) : ℤ) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)

Tactic:
rw [expDegree_cast <| by lia]

Premises used: _private.0.WeierstrassCurve.expDegree_cast
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
⊢ m + 1 ≠ 0

Tactic:
lia
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
rw :
  ((HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 5) : ℤ) 2 - if Even (m + 5) then 4 else 1) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 1) : ℤ) 2 - if Even (m + 1) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 1) : ℤ) 2 - if Even (m + 1) then 4 else 1) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)
⊢ ((HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 5) : ℤ) 2 - if Even (m + 5) then 4 else 1) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)

Tactic:
rw [expDegree_cast <| by lia]

Premises used: _private.0.WeierstrassCurve.expDegree_cast
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
⊢ m + 4 ≠ 0

Tactic:
lia
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
rw :
  ((HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 5) : ℤ) 2 - if Even (m + 5) then 4 else 1) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 1) : ℤ) 2 - if Even (m + 1) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 4) : ℤ) 2 - if Even (m + 4) then 4 else 1)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 4) : ℤ) 2 - if Even (m + 4) then 4 else 1) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 1) : ℤ) 2 - if Even (m + 1) then 4 else 1) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)
⊢ ((HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 5) : ℤ) 2 - if Even (m + 5) then 4 else 1) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 1) : ℤ) 2 - if Even (m + 1) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 1) : ℤ) 2 - if Even (m + 1) then 4 else 1) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)

Tactic:
rw [expDegree_cast <| by lia]

Premises used: _private.0.WeierstrassCurve.expDegree_cast
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
⊢ 2 * m + 4 + 1 ≠ 0

Tactic:
lia
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
rw :
  ((HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 5) : ℤ) 2 - if Even (m + 5) then 4 else 1) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 1) : ℤ) 2 - if Even (m + 1) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 4) : ℤ) 2 - if Even (m + 4) then 4 else 1)) ∧
    (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 4 + 1) : ℤ) 2 - if Even (2 * m + 4 + 1) then 4 else 1) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 4) : ℤ) 2 - if Even (m + 4) then 4 else 1) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 4 + 1) : ℤ) 2 - if Even (2 * m + 4 + 1) then 4 else 1) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 1) : ℤ) 2 - if Even (m + 1) then 4 else 1) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)
⊢ ((HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 5) : ℤ) 2 - if Even (m + 5) then 4 else 1) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 1) : ℤ) 2 - if Even (m + 1) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 4) : ℤ) 2 - if Even (m + 4) then 4 else 1)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 4) : ℤ) 2 - if Even (m + 4) then 4 else 1) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 1) : ℤ) 2 - if Even (m + 1) then 4 else 1) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)

Tactic:
rw [expDegree_cast <| by lia]

Premises used: _private.0.WeierstrassCurve.expDegree_cast
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
repeat :
  ((HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 5) : ℤ) 2 - if Even (m + 5) then 4 else 1) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 6) : ℤ) 2 - if Even (2 * m + 6) then 4 else 1) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 1) : ℤ) 2 - if Even (m + 1) then 4 else 1) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          2 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 4) : ℤ) 2 - if Even (m + 4) then 4 else 1)) ∧
    (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 4 + 1) : ℤ) 2 - if Even (2 * m + 4 + 1) then 4 else 1) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 4) : ℤ) 2 - if Even (m + 4) then 4 else 1) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 2) : ℤ) 2 - if Even (m + 2) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(2 * m + 4 + 1) : ℤ) 2 - if Even (2 * m + 4 + 1) then 4 else 1) =
        (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 1) : ℤ) 2 - if Even (m + 1) then 4 else 1) +
            3 * (HPow.hPow (α := ℤ) (β := ℕ) (↑(m + 3) : ℤ) 2 - if Even (m + 3) then 4 else 1) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)
⊢ (HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 6)) : ℤ) =
        2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 2)) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 5)) : ℤ) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 6)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          2 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ)) ∧
    HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 4)) : ℤ) + 3 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 2)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (if Even m then 6 else 0) ∧
      HMul.hMul (α := ℤ) 2 (↑(expDegree (2 * m + 4 + 1)) : ℤ) =
        HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 1)) : ℤ) + 3 * HMul.hMul (α := ℤ) 2 (↑(expDegree (m + 3)) : ℤ) +
          HMul.hMul (α := ℤ) 2 (if Even m then 0 else 6)

Tactic:
repeat rw [expDegree_cast <| by lia]

Premises used: _private.0.WeierstrassCurve.expDegree_cast