awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
h : ¬Even m
⊢ 2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2 =
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 2 * (HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
        (HAdd.hAdd (α := ℚ) (↑m : ℚ) 5 / 2) -
      HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2 * (HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) *
        HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 4) 2

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
h : Even m
⊢ 2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 + 1 =
    HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 / 2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 / 2) 3 * 16 -
      HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 3) 3 * 1

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
m : ℕ
h : ¬Even m
⊢ 2 * HAdd.hAdd (α := ℚ) (↑m : ℚ) 2 + 1 =
    HAdd.hAdd (α := ℚ) (↑m : ℚ) 4 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 2) 3 * 1 -
      HAdd.hAdd (α := ℚ) (↑m : ℚ) 1 / 2 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℚ) (↑m : ℚ) 3 / 2) 3 * 16

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
⊢ natDegree (W.preΨ' 0) ≤ expDegree 0 ∧ coeff (W.preΨ' 0) (expDegree 0) = (↑(expCoeff 0) : R)

Tactic:
simpa only [preΨ'_zero] using ⟨natDegree_zero.le, Int.cast_zero.symm⟩

Premises used: WeierstrassCurve.preΨ'_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
⊢ natDegree (W.preΨ' 1) ≤ expDegree 1 ∧ coeff (W.preΨ' 1) (expDegree 1) = (↑(expCoeff 1) : R)

Tactic:
simpa only [preΨ'_one] using ⟨natDegree_one.le, coeff_one_zero.trans Int.cast_one.symm⟩

Premises used: WeierstrassCurve.preΨ'_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
⊢ natDegree (W.preΨ' 2) ≤ expDegree 2 ∧ coeff (W.preΨ' 2) (expDegree 2) = (↑(expCoeff 2) : R)

Tactic:
simpa only [preΨ'_two] using ⟨natDegree_one.le, coeff_one_zero.trans Int.cast_one.symm⟩

Premises used: WeierstrassCurve.preΨ'_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
⊢ natDegree (W.preΨ' 3) ≤ expDegree 3 ∧ coeff (W.preΨ' 3) (expDegree 3) = (↑(expCoeff 3) : R)

Tactic:
simpa only [preΨ'_three] using ⟨W.natDegree_Ψ₃_le, W.coeff_Ψ₃ ▸ Int.cast_three.symm⟩

Premises used: WeierstrassCurve.preΨ'_three
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
⊢ natDegree (W.preΨ' 4) ≤ expDegree 4 ∧ coeff (W.preΨ' 4) (expDegree 4) = (↑(expCoeff 4) : R)

Tactic:
simpa only [preΨ'_four] using ⟨W.natDegree_preΨ₄_le, W.coeff_preΨ₄ ▸ Int.cast_two.symm⟩

Premises used: WeierstrassCurve.preΨ'_four
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
h₅ :
  natDegree (W.preΨ' (m + 5)) ≤ expDegree (m + 5) ∧
    coeff (W.preΨ' (m + 5)) (expDegree (m + 5)) = (↑(expCoeff (m + 5)) : R)
even : natDegree (W.preΨ' (2 * (m + 3))) ≤ expDegree (2 * (m + 3))
even₁ : coeff (W.preΨ' (2 * (m + 3))) (expDegree (2 * (m + 3))) = (↑(expCoeff (2 * (m + 3))) : R)
⊢ natDegree (W.preΨ' (2 * (m + 3))) ≤ expDegree (2 * (m + 3)) ∧
    coeff (W.preΨ' (2 * (m + 3))) (expDegree (2 * (m + 3))) = (↑(expCoeff (2 * (m + 3))) : R)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
h₅ :
  natDegree (W.preΨ' (m + 5)) ≤ expDegree (m + 5) ∧
    coeff (W.preΨ' (m + 5)) (expDegree (m + 5)) = (↑(expCoeff (m + 5)) : R)
even :
  (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).natDegree ≤
    max (2 * expDegree (m + 2) + expDegree (m + 3) + expDegree (m + 5))
      (expDegree (m + 1) + expDegree (m + 3) + 2 * expDegree (m + 4))
⊢ natDegree (W.preΨ' (2 * (m + 3))) ≤ expDegree (2 * (m + 3))

Tactic:
nth_rw 1 [preΨ'_even, ← max_self <| expDegree _, (expDegree_rec m).1.1, (expDegree_rec m).1.2]

Premises used: _private.0.WeierstrassCurve.expDegree, WeierstrassCurve.preΨ'_even, max_self, _private.0.WeierstrassCurve.expDegree_rec, And.right, And.left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
h₅ :
  natDegree (W.preΨ' (m + 5)) ≤ expDegree (m + 5) ∧
    coeff (W.preΨ' (m + 5)) (expDegree (m + 5)) = (↑(expCoeff (m + 5)) : R)
⊢ (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).natDegree ≤
    max (2 * expDegree (m + 2) + expDegree (m + 3) + expDegree (m + 5))
      (expDegree (m + 1) + expDegree (m + 3) + 2 * expDegree (m + 4))

Tactic:
natDegree_sub_le_of_le (dm (dm (dp h₂.1) h₃.1) h₅.1) (dm (dm h₁.1 h₃.1) (dp h₄.1))

Premises used: Polynomial.natDegree_sub_le_of_le, And.left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
h₅ :
  natDegree (W.preΨ' (m + 5)) ≤ expDegree (m + 5) ∧
    coeff (W.preΨ' (m + 5)) (expDegree (m + 5)) = (↑(expCoeff (m + 5)) : R)
⊢ (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).natDegree ≤
    max (2 * expDegree (m + 2) + expDegree (m + 3) + expDegree (m + 5))
      (expDegree (m + 1) + expDegree (m + 3) + 2 * expDegree (m + 4))

Tactic:
exact natDegree_sub_le_of_le (dm (dm (dp h₂.1) h₃.1) h₅.1) (dm (dm h₁.1 h₃.1) (dp h₄.1))

Premises used: Polynomial.natDegree_sub_le_of_le, And.left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
h₅ :
  natDegree (W.preΨ' (m + 5)) ≤ expDegree (m + 5) ∧
    coeff (W.preΨ' (m + 5)) (expDegree (m + 5)) = (↑(expCoeff (m + 5)) : R)
even :
  HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (m + 2)) : R) 2 * (↑(expCoeff (m + 3)) : R) * (↑(expCoeff (m + 5)) : R) -
      HMul.hMul (α := R) (↑(expCoeff (m + 1)) : R) (↑(expCoeff (m + 3)) : R) *
        HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (m + 4)) : R) 2 =
    (↑(HPow.hPow (β := ℕ) (expCoeff (m + 2)) 2 * expCoeff (m + 3) * expCoeff (m + 5) -
          expCoeff (m + 1) * expCoeff (m + 3) * HPow.hPow (β := ℕ) (expCoeff (m + 4)) 2) :
      R)
⊢ coeff (W.preΨ' (2 * (m + 3))) (expDegree (2 * (m + 3))) = (↑(expCoeff (2 * (m + 3))) : R)

Tactic:
nth_rw 1 [preΨ'_even, coeff_sub, (expDegree_rec m).1.1, cm (dm (dp h₂.1) h₃.1) h₅.1,
        cm (dp h₂.1) h₃.1, cp h₂.1, h₂.2, h₃.2, h₅.2, (expDegree_rec m).1.2,
        cm (dm h₁.1 h₃.1) (dp h₄.1), cm h₁.1 h₃.1, h₁.2, cp h₄.1, h₃.2, h₄.2, (expCoeff_rec m).1]

Premises used: WeierstrassCurve.preΨ'_even, _private.0.WeierstrassCurve.expDegree_rec, And.right, And.left, Polynomial.coeff_sub, _private.0.WeierstrassCurve.expCoeff_rec
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
h₅ :
  natDegree (W.preΨ' (m + 5)) ≤ expDegree (m + 5) ∧
    coeff (W.preΨ' (m + 5)) (expDegree (m + 5)) = (↑(expCoeff (m + 5)) : R)
even even₁ even₂ even₃ :
  Eq.{u + 1} (α := R)
    (↑(HPow.hPow (β := ℕ) (expCoeff (m + 2)) 2 * expCoeff (m + 3) * expCoeff (m + 5) -
          expCoeff (m + 1) * expCoeff (m + 3) * HPow.hPow (β := ℕ) (expCoeff (m + 4)) 2) :
      R)
    (↑(HPow.hPow (β := ℕ) (expCoeff (m + 2)) 2 * expCoeff (m + 3) * expCoeff (m + 5) -
          expCoeff (m + 1) * expCoeff (m + 3) * HPow.hPow (β := ℕ) (expCoeff (m + 4)) 2) :
      R)
⊢ HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (m + 2)) : R) 2 * (↑(expCoeff (m + 3)) : R) * (↑(expCoeff (m + 5)) : R) -
      HMul.hMul (α := R) (↑(expCoeff (m + 1)) : R) (↑(expCoeff (m + 3)) : R) *
        HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (m + 4)) : R) 2 =
    (↑(HPow.hPow (β := ℕ) (expCoeff (m + 2)) 2 * expCoeff (m + 3) * expCoeff (m + 5) -
          expCoeff (m + 1) * expCoeff (m + 3) * HPow.hPow (β := ℕ) (expCoeff (m + 4)) 2) :
      R)

Tactic:
norm_cast
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
odd :
  ((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).natDegree ≤
      expDegree (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).coeff
        (expDegree (2 * (m + 2) + 1)) =
      (↑(expCoeff (2 * (m + 2) + 1)) : R)
⊢ natDegree (W.preΨ' (2 * (m + 2) + 1)) ≤ expDegree (2 * (m + 2) + 1) ∧
    coeff (W.preΨ' (2 * (m + 2) + 1)) (expDegree (2 * (m + 2) + 1)) = (↑(expCoeff (2 * (m + 2) + 1)) : R)

Tactic:
rw [preΨ'_odd]

Premises used: WeierstrassCurve.preΨ'_odd
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
odd :
  ((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).natDegree ≤
    expDegree (2 * (m + 2) + 1)
odd₁ :
  ((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).coeff
      (expDegree (2 * (m + 2) + 1)) =
    (↑(expCoeff (2 * (m + 2) + 1)) : R)
⊢ ((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).natDegree ≤
      expDegree (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).coeff
        (expDegree (2 * (m + 2) + 1)) =
      (↑(expCoeff (2 * (m + 2) + 1)) : R)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ :
  natDegree (W.preΨ' (m + 1)) ≤ expDegree (m + 1) ∧
    coeff (W.preΨ' (m + 1)) (expDegree (m + 1)) = (↑(expCoeff (m + 1)) : R)
h₂ :
  natDegree (W.preΨ' (m + 2)) ≤ expDegree (m + 2) ∧
    coeff (W.preΨ' (m + 2)) (expDegree (m + 2)) = (↑(expCoeff (m + 2)) : R)
h₃ :
  natDegree (W.preΨ' (m + 3)) ≤ expDegree (m + 3) ∧
    coeff (W.preΨ' (m + 3)) (expDegree (m + 3)) = (↑(expCoeff (m + 3)) : R)
h₄ :
  natDegree (W.preΨ' (m + 4)) ≤ expDegree (m + 4) ∧
    coeff (W.preΨ' (m + 4)) (expDegree (m + 4)) = (↑(expCoeff (m + 4)) : R)
odd :
  ((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).natDegree ≤
    max (expDegree (m + 4) + 3 * expDegree (m + 2) + if Even m then HMul.hMul (α := ℕ) 2 3 else 0)
      (expDegree (m + 1) + 3 * expDegree (m + 3) + if Even m then 0 else HMul.hMul (α := ℕ) 2 3)
⊢ ((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).natDegree ≤
    expDegree (2 * (m + 2) + 1)

Tactic:
nth_rw 1 [← max_self <| expDegree _, (expDegree_rec m).2.1, (expDegree_rec m).2.2]

Premises used: _private.0.WeierstrassCurve.expDegree, max_self, _private.0.WeierstrassCurve.expDegree_rec, And.right, And.left