awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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 := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
pos : Even (n + 1) → natDegree.{u} (R := R) 1 ≤ 0
⊢ natDegree (if Even (n + 1) then 1 else W.Ψ₂Sq) ≤ if Even (n + 1) then 0 else 3
have neg : ¬Even (n + 1) → natDegree W.Ψ₂Sq ≤ 3
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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 := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ natDegree (if Even (n + 1) then W.Ψ₂Sq else 1) ≤ if Even (n + 1) then 3 else 0
have pos : Even (n + 1) → natDegree W.Ψ₂Sq ≤ 3
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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 := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
pos : Even (n + 1) → natDegree W.Ψ₂Sq ≤ 3
⊢ natDegree (if Even (n + 1) then W.Ψ₂Sq else 1) ≤ if Even (n + 1) then 3 else 0
have neg : ¬Even (n + 1) → natDegree.{u} (R := R) 1 ≤ 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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 := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1 + 1)) 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
          HMul.hMul (α := R[X]) (W.preΨ' (n + 1 + 2)) (W.preΨ' (n + 1)) * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
      (HPow.hPow (β := ℕ) (n + 1 + 1) 2) =
    1
have succ : ((1 * HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (n + 1 + 1)) : R) 2 * if Even (n + 1) then 1 else 4) -
    HMul.hMul (α := R) (↑(expCoeff (n + 1 + 2)) : R) (↑(expCoeff (n + 1)) : R) * if Even (n + 1) then 4 else 1) =
  1
Tactic: nth_rw 1 [coeff_sub, hd, hd', cm (dm natDegree_X_le (dp h.1)), cm natDegree_X_le (dp h.1),
      coeff_X_one, coeff_pow_of_natDegree_le h.1, h.2, apply_ite₂ coeff, coeff_one_zero, coeff_Ψ₂Sq,
      cm (dm h.1 h.1), cm h.1 h.1, h.2, h.2, apply_ite₂ coeff, coeff_one_zero, coeff_Ψ₂Sq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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 := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
succ :
  ((1 * HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (n + 1 + 1)) : R) 2 * if Even (n + 1) then 1 else 4) -
      HMul.hMul (α := R) (↑(expCoeff (n + 1 + 2)) : R) (↑(expCoeff (n + 1)) : R) * if Even (n + 1) then 4 else 1) =
    1
⊢ ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1 + 1)) 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
          HMul.hMul (α := R[X]) (W.preΨ' (n + 1 + 2)) (W.preΨ' (n + 1)) * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
      (HPow.hPow (β := ℕ) (n + 1 + 1) 2) =
    1
have succ₁ : natDegree (if Even (n + 1) then W.Ψ₂Sq else 1) ≤ if Even (n + 1) then 3 else 0
Tactic: nth_rw 1 [coeff_sub, hd, hd', cm (dm natDegree_X_le (dp h.1)), cm natDegree_X_le (dp h.1),
      coeff_X_one, coeff_pow_of_natDegree_le h.1, h.2, apply_ite₂ coeff, coeff_one_zero, coeff_Ψ₂Sq,
      cm (dm h.1 h.1), cm h.1 h.1, h.2, h.2, apply_ite₂ coeff, coeff_one_zero, coeff_Ψ₂Sq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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 := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
succ :
  ((1 * HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (n + 1 + 1)) : R) 2 * if Even (n + 1) then 1 else 4) -
      HMul.hMul (α := R) (↑(expCoeff (n + 1 + 2)) : R) (↑(expCoeff (n + 1)) : R) * if Even (n + 1) then 4 else 1) =
    1
succ₁ : natDegree (if Even (n + 1) then W.Ψ₂Sq else 1) ≤ if Even (n + 1) then 3 else 0
⊢ ((X * HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ' (n + 1 + 1)) 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
          HMul.hMul (α := R[X]) (W.preΨ' (n + 1 + 2)) (W.preΨ' (n + 1)) * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
      (HPow.hPow (β := ℕ) (n + 1 + 1) 2) =
    1
have succ₂ : natDegree (if Even (n + 1) then 1 else W.Ψ₂Sq) ≤ if Even (n + 1) then 0 else 3
Tactic: nth_rw 1 [coeff_sub, hd, hd', cm (dm natDegree_X_le (dp h.1)), cm natDegree_X_le (dp h.1),
      coeff_X_one, coeff_pow_of_natDegree_le h.1, h.2, apply_ite₂ coeff, coeff_one_zero, coeff_Ψ₂Sq,
      cm (dm h.1 h.1), cm h.1 h.1, h.2, h.2, apply_ite₂ coeff, coeff_one_zero, coeff_Ψ₂Sq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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 := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
| 1
have rw : (↑((1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1) :
  R)
Tactic: rw [← Int.cast_one, hc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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 := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ ((1 * HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (n + 1 + 1)) : R) 2 * if Even (n + 1) then 1 else 4) -
      HMul.hMul (α := R) (↑(expCoeff (n + 1 + 2)) : R) (↑(expCoeff (n + 1)) : R) * if Even (n + 1) then 4 else 1) =
    1
have succ : ((1 * HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (n + 1 + 1)) : R) 2 * if Even (n + 1) then 1 else 4) -
    HMul.hMul (α := R) (↑(expCoeff (n + 1 + 2)) : R) (↑(expCoeff (n + 1)) : R) * if Even (n + 1) then 4 else 1) =
  (↑((1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
        expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1) :
    R)
Tactic: conv_rhs => rw [← Int.cast_one, hc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
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 := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ ((1 * HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (n + 1 + 1)) : R) 2 * if Even (n + 1) then 1 else 4) -
      HMul.hMul (α := R) (↑(expCoeff (n + 1 + 2)) : R) (↑(expCoeff (n + 1)) : R) * if Even (n + 1) then 4 else 1) =
    (↑((1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * if Even (n + 1) then 1 else 4) -
          expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1) :
      R)
have succ : Eq.{u + 1} (α := R)
  (↑(1 * HPow.hPow (β := ℕ) (expCoeff (n + 1 + 1)) 2 * (↑(if Even (n + 1) then 1 else 4) : ℤ) -
        expCoeff (n + 1 + 2) * expCoeff (n + 1) * (↑(if Even (n + 1) then 4 else 1) : ℤ)) :
    R)
  (↑(1 * HPow.hPow (β := ℕ) (expCoeff (n + 2)) 2 * (↑(if Even (n + 1) then 1 else 4) : ℤ) -
        expCoeff (n + 3) * expCoeff (n + 1) * (↑(if Even (n + 1) then 4 else 1) : ℤ)) :
    R)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2
n : ℕ
⊢ natDegree (W.Φ (-(↑n : ℤ))) ≤ HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2
have neg : natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2
Tactic: simp_rw [Φ_neg, Int.natAbs_neg, ih]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2
n : ℕ
neg : natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2
⊢ natDegree (W.Φ (-(↑n : ℤ))) ≤ HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2
have neg₁ : natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2
Tactic: simp_rw [Φ_neg, Int.natAbs_neg, ih]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ natDegree (W.Φ n) ≤ HPow.hPow (β := ℕ) n.natAbs 2
have nat : ∀ (n : ℕ), natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2
Tactic: induction n using Int.negInduction with
  | nat n => exact (W.natDegree_coeff_Φ_ofNat n).left
  | neg ih => simp_rw [Φ_neg, Int.natAbs_neg, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
nat : ∀ (n : ℕ), natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2
⊢ natDegree (W.Φ n) ≤ HPow.hPow (β := ℕ) n.natAbs 2
have neg : ∀ (ih : ∀ (n : ℕ), natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2) (n : ℕ),
  natDegree (W.Φ (-(↑n : ℤ))) ≤ HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2
Tactic: induction n using Int.negInduction with
  | nat n => exact (W.natDegree_coeff_Φ_ofNat n).left
  | neg ih => simp_rw [Φ_neg, Int.natAbs_neg, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2) = 1
n : ℕ
⊢ coeff (W.Φ (-(↑n : ℤ))) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2) = 1
have neg : coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2) = 1
Tactic: rw [Φ_neg, Int.natAbs_neg, ih]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2) = 1
n : ℕ
neg : coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2) = 1
⊢ coeff (W.Φ (-(↑n : ℤ))) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2) = 1
have neg₁ : coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2) = 1
Tactic: rw [Φ_neg, Int.natAbs_neg, ih]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2) = 1
n : ℕ
neg : coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2) = 1
neg₁ : coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2) = 1
⊢ coeff (W.Φ (-(↑n : ℤ))) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2) = 1
have neg₂ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [Φ_neg, Int.natAbs_neg, ih]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ coeff (W.Φ n) (HPow.hPow (β := ℕ) n.natAbs 2) = 1
have nat : ∀ (n : ℕ), coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2) = 1
Tactic: induction n using Int.negInduction with
  | nat n => exact (W.natDegree_coeff_Φ_ofNat n).right
  | neg ih => rw [Φ_neg, Int.natAbs_neg, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
nat : ∀ (n : ℕ), coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2) = 1
⊢ coeff (W.Φ n) (HPow.hPow (β := ℕ) n.natAbs 2) = 1
have neg : ∀ (ih : ∀ (n : ℕ), coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2) = 1) (n : ℕ),
  coeff (W.Φ (-(↑n : ℤ))) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2) = 1
Tactic: induction n using Int.negInduction with
  | nat n => exact (W.natDegree_coeff_Φ_ofNat n).right
  | neg ih => rw [Φ_neg, Int.natAbs_neg, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
n : ℤ
⊢ leadingCoeff (W.Φ n) = 1
have rw : coeff (W.Φ n) (natDegree (W.Φ n)) = 1
Tactic: rw [leadingCoeff, natDegree_Φ, coeff_Φ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
n : ℤ
rw : coeff (W.Φ n) (natDegree (W.Φ n)) = 1
⊢ leadingCoeff (W.Φ n) = 1
have rw₁ : coeff (W.Φ n) (HPow.hPow (β := ℕ) n.natAbs 2) = 1
Tactic: rw [leadingCoeff, natDegree_Φ, coeff_Φ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
n : ℤ
rw : coeff (W.Φ n) (natDegree (W.Φ n)) = 1
rw₁ : coeff (W.Φ n) (HPow.hPow (β := ℕ) n.natAbs 2) = 1
⊢ leadingCoeff (W.Φ n) = 1
have rw₂ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [leadingCoeff, natDegree_Φ, coeff_Φ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
n : ℤ
⊢ Ne (α := R[X]) (W.Φ n) 0
have pos : ∀ (hn : n = 0), Ne (α := R[X]) (W.Φ n) 0
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
n : ℤ
pos : ∀ (hn : n = 0), Ne (α := R[X]) (W.Φ n) 0
⊢ Ne (α := R[X]) (W.Φ n) 0
have neg : ∀ (hn : ¬n = 0), Ne (α := R[X]) (W.Φ n) 0
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
⊢ ∃ (C : VariableChange F), C • E = E'
have obtain : ∀ (s : F) (hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0), ∃ (C : VariableChange F), C • E = E'
Tactic: obtain ⟨s, hs⟩ := IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C' 2 2
    1 1 (E.a₂ + E'.a₂) (by simp) (by simp) one_ne_zero
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ ∃ (C : VariableChange F), C • E = E'
have h : HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E = E'
Tactic: use ⟨1, 0, s, 0⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E = E'
have h : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₁ = E'.a₁
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
h : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₁ = E'.a₁
⊢ HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E = E'
have h₁ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₂ = E'.a₂
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
h : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₁ = E'.a₁
h₁ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₂ = E'.a₂
⊢ HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E = E'
have h₂ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₃ = E'.a₃
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
h : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₁ = E'.a₁
h₁ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₂ = E'.a₂
h₂ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₃ = E'.a₃
⊢ HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E = E'
have h₃ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₄ = E'.a₄
Tactic: ext