awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
h₁ :
  (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
        ((monomial d : (a : R) → R[X]) c : R[X])).nextCoeff =
    -(η * c)
h₂ :
  (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
        ((monomial d : (a : R) → R[X]) c : R[X])).eraseLead ≠
    0
⊢ signVariations.{u_1} (R := R) ((monomial d : (a : R) → R[X]) c) + 1 ≤
    (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
        ((monomial d : (a : R) → R[X]) c : R[X])).signVariations
have h₃ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType)
  ((SignType.sign : (a : R) → SignType) (-(η * c)) : SignType)
Tactic: have h₃ : SignType.sign c ≠ SignType.sign (-(η * c)) := by
    simp [hη, hc, Left.sign_neg, sign_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₂ : P.nextCoeff ≠ 0
⊢ ∃ (c₀ : R) (cs : List R),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
have h₃ : P ≠ 0
Tactic: have h₃ := leadingCoeff_ne_zero.mp h₁.ne'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₂ : P.nextCoeff ≠ 0
h₃ : P ≠ 0
⊢ ∃ (c₀ : R) (cs : List R),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
have h₄ : P.eraseLead.natDegree + 1 = P.natDegree
Tactic: have h₄ := natDegree_eraseLead_add_one h₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₂ : P.nextCoeff ≠ 0
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
⊢ ∃ (c₀ : R) (cs : List R),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
have h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
Tactic: have h₅ : (X - C η) ≠ 0 := X_sub_C_ne_zero η
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₂ : P.nextCoeff ≠ 0
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
⊢ ∃ (c₀ : R) (cs : List R),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
have h₆ : P.eraseLead ≠ 0
Tactic: have h₆ : P.eraseLead ≠ 0 := mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₂ : P.nextCoeff ≠ 0
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
⊢ ∃ (c₀ : R) (cs : List R),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
have obtain : ∀ (d : ℕ) (hd : P.natDegree = 0 + d + 1),
  ∃ (c₀ : R) (cs : List R),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
Tactic: obtain ⟨d, hd⟩ := Nat.exists_eq_add_of_lt (natDegree_pos_of_nextCoeff_ne_zero h₂)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₂ : P.nextCoeff ≠ 0
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
⊢ ∃ (c₀ : R) (cs : List R),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
have h₇ : P.eraseLead.leadingCoeff = P.nextCoeff
Tactic: apply leadingCoeff_eraseLead_eq_nextCoeff at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
⊢ ∃ (c₀ : R) (cs : List R),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
have h_cons : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).leadingCoeff ::
    (List.replicate
        ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree -
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.degree.succ)
        0 ++
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
Tactic: have h_cons := coeffList_eraseLead (mul_ne_zero h₅ h₆)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
h_cons :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).leadingCoeff ::
      (List.replicate
          ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree -
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.degree.succ)
          0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
⊢ ∃ (c₀ : R) (cs : List R),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
have generalize : ∀ (n : ℕ)
  (h_cons :
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).leadingCoeff ::
        (List.replicate n 0 ++
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)),
  ∃ (c₀ : R) (cs : List R),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
Tactic: generalize ((X - C η) * P.eraseLead).natDegree -
    ((X - C η) * P.eraseLead).eraseLead.degree.succ = n at h_cons ⊢
Cleared hypotheses: h_cons
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
⊢ ∃ (c₀ : R) (cs : List R),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
have h : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList =
    P.leadingCoeff ::
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff ::
        (List.replicate n 0 ++
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList) ∧
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
    P.nextCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
Tactic: use nextCoeff ((X - C η) * P), .replicate n 0 ++ coeffList ((X - C η) * P.eraseLead).eraseLead
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList =
      P.leadingCoeff ::
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff ::
          (List.replicate n 0 ++
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList) ∧
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
      P.nextCoeff ::
        (List.replicate n 0 ++
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
have h : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList =
  P.leadingCoeff ::
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
h :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList =
    P.leadingCoeff ::
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff ::
        (List.replicate n 0 ++
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList =
      P.leadingCoeff ::
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff ::
          (List.replicate n 0 ++
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList) ∧
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
      P.nextCoeff ::
        (List.replicate n 0 ++
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
have h₇ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
  P.nextCoeff ::
    (List.replicate n 0 ++
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
have rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X])).natDegree + P.natDegree = P.natDegree + 1
Tactic: rw [natDegree_mul h₅ h₃, natDegree_X_sub_C, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X])).natDegree + P.natDegree = P.natDegree + 1
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
have rw₁ : 1 + P.natDegree = P.natDegree + 1
Tactic: rw [natDegree_mul h₅ h₃, natDegree_X_sub_C, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X])).natDegree + P.natDegree = P.natDegree + 1
rw₁ : 1 + P.natDegree = P.natDegree + 1
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
have rw₂ : P.natDegree + 1 = P.natDegree + 1
Tactic: rw [natDegree_mul h₅ h₃, natDegree_X_sub_C, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList =
    P.leadingCoeff ::
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff ::
        (List.replicate n 0 ++
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
have h₇ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
Tactic: have h₇ : natDegree ((X - C η) * P) = P.natDegree + 1 := by
      rw [natDegree_mul h₅ h₃, natDegree_X_sub_C, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
h₇ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList =
    P.leadingCoeff ::
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff ::
        (List.replicate n 0 ++
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
have h₈ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead =
  HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead)
    ((monomial P.natDegree : (a : R) → R[X]) P.nextCoeff : R[X])
Tactic: have h₈ : ((X - C η) * P.eraseLead).eraseLead =
        (X - C η) * P.eraseLead - monomial P.natDegree P.nextCoeff := by
      simp [← self_sub_monomial_natDegree_leadingCoeff (_ * _), natDegree_mul,
        h₅, h₆, h₂, h₄, add_comm 1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
h₇ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
h₈ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead =
    HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead)
      ((monomial P.natDegree : (a : R) → R[X]) P.nextCoeff : R[X])
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList =
    P.leadingCoeff ::
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff ::
        (List.replicate n 0 ++
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
have this : P.eraseLead.natDegree + 2 =
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList.length
Tactic: have : P.eraseLead.natDegree + 2 = ((X - C η) * P.eraseLead).coeffList.length := by
      simp [h₅, h₆, natDegree_mul, add_comm 1]