awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha_1 : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
_ : ‖a‖₊ - 1 + 1 = ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1
_₁ :
  ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 ≤
    (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1
⊢ ‖a‖₊ < p.cauchyBound
have _₂ : (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 =
  (p.cauchyBound - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1
Tactic: calc
        ‖a‖₊ = ‖a‖₊ - 1 + 1 := (tsub_add_cancel_of_le ha.le).symm
        _ = ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 := by field
        _ ≤ (cauchyBound p - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1)
            / ‖a‖₊ ^ p.natDegree + 1 := by gcongr
        _ = (cauchyBound p - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1 := by
          congr 2
          have : ‖a‖₊ - 1 ≠ 0 := fun nh ↦ (ha.trans_le (tsub_eq_zero_iff_le.mp nh)).false
          field
        _ < (cauchyBound p - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1 := by
          gcongr
          · apply lt_of_le_of_ne (by simp)
            contrapose! this
            simp only [← this, zero_mul]
            apply pow_pos
            exact zero_lt_one.trans ha
          simp [zero_lt_one.trans ha]
        _ = cauchyBound p := by simp [field, tsub_add_cancel_of_le]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha_1 : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
_ : ‖a‖₊ - 1 + 1 = ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1
_₁ :
  ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 ≤
    (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1
_₂ :
  (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 =
    (p.cauchyBound - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1
⊢ ‖a‖₊ < p.cauchyBound
have _₃ : (p.cauchyBound - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1 <
  (p.cauchyBound - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1
Tactic: calc
        ‖a‖₊ = ‖a‖₊ - 1 + 1 := (tsub_add_cancel_of_le ha.le).symm
        _ = ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 := by field
        _ ≤ (cauchyBound p - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1)
            / ‖a‖₊ ^ p.natDegree + 1 := by gcongr
        _ = (cauchyBound p - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1 := by
          congr 2
          have : ‖a‖₊ - 1 ≠ 0 := fun nh ↦ (ha.trans_le (tsub_eq_zero_iff_le.mp nh)).false
          field
        _ < (cauchyBound p - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1 := by
          gcongr
          · apply lt_of_le_of_ne (by simp)
            contrapose! this
            simp only [← this, zero_mul]
            apply pow_pos
            exact zero_lt_one.trans ha
          simp [zero_lt_one.trans ha]
        _ = cauchyBound p := by simp [field, tsub_add_cancel_of_le]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha_1 : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
_ : ‖a‖₊ - 1 + 1 = ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1
_₁ :
  ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 ≤
    (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1
_₂ :
  (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 =
    (p.cauchyBound - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1
_₃ :
  (p.cauchyBound - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1 <
    (p.cauchyBound - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1
⊢ ‖a‖₊ < p.cauchyBound
have _₄ : (p.cauchyBound - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1 = p.cauchyBound
Tactic: calc
        ‖a‖₊ = ‖a‖₊ - 1 + 1 := (tsub_add_cancel_of_le ha.le).symm
        _ = ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 := by field
        _ ≤ (cauchyBound p - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1)
            / ‖a‖₊ ^ p.natDegree + 1 := by gcongr
        _ = (cauchyBound p - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1 := by
          congr 2
          have : ‖a‖₊ - 1 ≠ 0 := fun nh ↦ (ha.trans_le (tsub_eq_zero_iff_le.mp nh)).false
          field
        _ < (cauchyBound p - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1 := by
          gcongr
          · apply lt_of_le_of_ne (by simp)
            contrapose! this
            simp only [← this, zero_mul]
            apply pow_pos
            exact zero_lt_one.trans ha
          simp [zero_lt_one.trans ha]
        _ = cauchyBound p := by simp [field, tsub_add_cancel_of_le]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
⊢ ‖a‖₊ < p.cauchyBound
have suffices : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
Tactic: suffices ‖a‖₊ ^ p.natDegree ≤ (cauchyBound p - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x by
    rcases eq_or_ne ‖a‖₊ 1 with ha | ha
    · simp only [ha, one_pow, sum_const, card_range, nsmul_eq_mul, mul_one, gt_iff_lt] at this ⊢
      apply lt_of_le_of_ne (by simp)
      intro nh
      simp [← nh, tsub_self] at this
    rcases lt_or_gt_of_ne ha with ha | ha
    · apply ha.trans_le
      simp
    · rw [geom_sum_of_one_lt ha] at this
      calc
        ‖a‖₊ = ‖a‖₊ - 1 + 1 := (tsub_add_cancel_of_le ha.le).symm
        _ = ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 := by field
        _ ≤ (cauchyBound p - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1)
            / ‖a‖₊ ^ p.natDegree + 1 := by gcongr
        _ = (cauchyBound p - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1 := by
          congr 2
          have : ‖a‖₊ - 1 ≠ 0 := fun nh ↦ (ha.trans_le (tsub_eq_zero_iff_le.mp nh)).false
          field
        _ < (cauchyBound p - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1 := by
          gcongr
          · apply lt_of_le_of_ne (by simp)
            contrapose! this
            simp only [← this, zero_mul]
            apply pow_pos
            exact zero_lt_one.trans ha
          simp [zero_lt_one.trans ha]
        _ = cauchyBound p := by simp [field, tsub_add_cancel_of_le]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (hypothesis)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
⊢ ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
have h₁ : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
Tactic: apply le_of_eq at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (hypothesis)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
⊢ ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
have pld : ‖p.leadingCoeff‖₊ ≠ 0
Tactic: have pld : ‖p.leadingCoeff‖₊ ≠ 0 := by simpa
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ ≤
    nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) / ‖p.leadingCoeff‖₊
have hc : 0 ≤ ‖p.leadingCoeff‖₊
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) / ‖p.leadingCoeff‖₊ ≤
    (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊
have hab : nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) ≤ ∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ ≤
    (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (p.cauchyBound - 1) * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊
have hab : ∀ i ∈ range p.natDegree, ‖p.coeff i‖₊ ≤ ‖p.leadingCoeff‖₊ * (p.cauchyBound - 1)
Tactic: gcongr (∑ x ∈ _, ?_ * _) / _
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
i : ℕ
h_1 : i ∈ range p.natDegree
⊢ ‖p.coeff i‖₊ ≤ ‖p.leadingCoeff‖₊ * (p.cauchyBound - 1)
have hab : ‖p.coeff i‖₊ ≤ ‖p.leadingCoeff‖₊ * (((range p.natDegree).sup fun (x : ℕ) ↦ ‖p.coeff x‖₊) / ‖p.leadingCoeff‖₊)
Tactic: rw [cauchyBound, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
i : ℕ
h_1 : i ∈ range p.natDegree
⊢ ‖p.coeff i‖₊ ≤ ‖p.leadingCoeff‖₊ * (((range p.natDegree).sup fun (x : ℕ) ↦ ‖p.coeff x‖₊) / ‖p.leadingCoeff‖₊)
have hab : ‖p.coeff i‖₊ ≤ (range p.natDegree).sup fun (x : ℕ) ↦ ‖p.coeff x‖₊
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (p.cauchyBound - 1) * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ =
    (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
have simp : (‖p.leadingCoeff‖₊ * (p.cauchyBound - 1) * ∑ i ∈ range p.natDegree, ‖a‖₊ ^ i) / ‖p.leadingCoeff‖₊ =
  (p.cauchyBound - 1) * ∑ i ∈ range p.natDegree, ‖a‖₊ ^ i
Tactic: simp only [← mul_sum]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
have calc : ‖a‖₊ ^ p.natDegree = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊
Tactic: calc ‖a‖₊ ^ p.natDegree
    _ = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ := by
      rw [mul_div_cancel_left₀]
      simpa
    _ ≤ ‖∑ x ∈ range p.natDegree, p.coeff x * a ^ x‖₊ / ‖p.leadingCoeff‖₊ := by gcongr
    _ ≤ (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊ := by
      gcongr
      apply nnnorm_sum_le
    _ = (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ := by simp
    _ ≤ (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (cauchyBound p - 1) * ‖a‖₊ ^ x) /
        ‖p.leadingCoeff‖₊ := by
      gcongr (∑ x ∈ _, ?_ * _) / _
      rw [cauchyBound, add_tsub_cancel_right]
      field_simp
      apply le_sup (f := (‖p.coeff ·‖₊)) ‹_›
    _ = (cauchyBound p - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x := by
      simp only [← mul_sum]
      field
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
calc : ‖a‖₊ ^ p.natDegree = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊
⊢ ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
have calc₁ : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ ≤
  nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) / ‖p.leadingCoeff‖₊
Tactic: calc ‖a‖₊ ^ p.natDegree
    _ = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ := by
      rw [mul_div_cancel_left₀]
      simpa
    _ ≤ ‖∑ x ∈ range p.natDegree, p.coeff x * a ^ x‖₊ / ‖p.leadingCoeff‖₊ := by gcongr
    _ ≤ (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊ := by
      gcongr
      apply nnnorm_sum_le
    _ = (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ := by simp
    _ ≤ (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (cauchyBound p - 1) * ‖a‖₊ ^ x) /
        ‖p.leadingCoeff‖₊ := by
      gcongr (∑ x ∈ _, ?_ * _) / _
      rw [cauchyBound, add_tsub_cancel_right]
      field_simp
      apply le_sup (f := (‖p.coeff ·‖₊)) ‹_›
    _ = (cauchyBound p - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x := by
      simp only [← mul_sum]
      field
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
calc : ‖a‖₊ ^ p.natDegree = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊
calc₁ :
  ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ ≤
    nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) / ‖p.leadingCoeff‖₊
⊢ ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
have calc₂ : nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) / ‖p.leadingCoeff‖₊ ≤
  (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊
Tactic: calc ‖a‖₊ ^ p.natDegree
    _ = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ := by
      rw [mul_div_cancel_left₀]
      simpa
    _ ≤ ‖∑ x ∈ range p.natDegree, p.coeff x * a ^ x‖₊ / ‖p.leadingCoeff‖₊ := by gcongr
    _ ≤ (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊ := by
      gcongr
      apply nnnorm_sum_le
    _ = (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ := by simp
    _ ≤ (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (cauchyBound p - 1) * ‖a‖₊ ^ x) /
        ‖p.leadingCoeff‖₊ := by
      gcongr (∑ x ∈ _, ?_ * _) / _
      rw [cauchyBound, add_tsub_cancel_right]
      field_simp
      apply le_sup (f := (‖p.coeff ·‖₊)) ‹_›
    _ = (cauchyBound p - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x := by
      simp only [← mul_sum]
      field
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
calc : ‖a‖₊ ^ p.natDegree = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊
calc₁ :
  ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ ≤
    nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) / ‖p.leadingCoeff‖₊
calc₂ :
  nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) / ‖p.leadingCoeff‖₊ ≤
    (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊
⊢ ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
have calc₃ : (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊ =
  (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊
Tactic: calc ‖a‖₊ ^ p.natDegree
    _ = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ := by
      rw [mul_div_cancel_left₀]
      simpa
    _ ≤ ‖∑ x ∈ range p.natDegree, p.coeff x * a ^ x‖₊ / ‖p.leadingCoeff‖₊ := by gcongr
    _ ≤ (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊ := by
      gcongr
      apply nnnorm_sum_le
    _ = (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ := by simp
    _ ≤ (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (cauchyBound p - 1) * ‖a‖₊ ^ x) /
        ‖p.leadingCoeff‖₊ := by
      gcongr (∑ x ∈ _, ?_ * _) / _
      rw [cauchyBound, add_tsub_cancel_right]
      field_simp
      apply le_sup (f := (‖p.coeff ·‖₊)) ‹_›
    _ = (cauchyBound p - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x := by
      simp only [← mul_sum]
      field
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
calc : ‖a‖₊ ^ p.natDegree = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊
calc₁ :
  ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ ≤
    nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) / ‖p.leadingCoeff‖₊
calc₂ :
  nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) / ‖p.leadingCoeff‖₊ ≤
    (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊
calc₃ :
  (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊ =
    (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊
⊢ ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
have calc₄ : (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ ≤
  (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (p.cauchyBound - 1) * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊
Tactic: calc ‖a‖₊ ^ p.natDegree
    _ = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ := by
      rw [mul_div_cancel_left₀]
      simpa
    _ ≤ ‖∑ x ∈ range p.natDegree, p.coeff x * a ^ x‖₊ / ‖p.leadingCoeff‖₊ := by gcongr
    _ ≤ (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊ := by
      gcongr
      apply nnnorm_sum_le
    _ = (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ := by simp
    _ ≤ (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (cauchyBound p - 1) * ‖a‖₊ ^ x) /
        ‖p.leadingCoeff‖₊ := by
      gcongr (∑ x ∈ _, ?_ * _) / _
      rw [cauchyBound, add_tsub_cancel_right]
      field_simp
      apply le_sup (f := (‖p.coeff ·‖₊)) ‹_›
    _ = (cauchyBound p - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x := by
      simp only [← mul_sum]
      field
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
calc : ‖a‖₊ ^ p.natDegree = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊
calc₁ :
  ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ ≤
    nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) / ‖p.leadingCoeff‖₊
calc₂ :
  nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) / ‖p.leadingCoeff‖₊ ≤
    (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊
calc₃ :
  (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊ =
    (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊
calc₄ :
  (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ ≤
    (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (p.cauchyBound - 1) * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊
⊢ ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
have calc₅ : (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (p.cauchyBound - 1) * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ =
  (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
Tactic: calc ‖a‖₊ ^ p.natDegree
    _ = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ := by
      rw [mul_div_cancel_left₀]
      simpa
    _ ≤ ‖∑ x ∈ range p.natDegree, p.coeff x * a ^ x‖₊ / ‖p.leadingCoeff‖₊ := by gcongr
    _ ≤ (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊ := by
      gcongr
      apply nnnorm_sum_le
    _ = (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ := by simp
    _ ≤ (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (cauchyBound p - 1) * ‖a‖₊ ^ x) /
        ‖p.leadingCoeff‖₊ := by
      gcongr (∑ x ∈ _, ?_ * _) / _
      rw [cauchyBound, add_tsub_cancel_right]
      field_simp
      apply le_sup (f := (‖p.coeff ·‖₊)) ‹_›
    _ = (cauchyBound p - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x := by
      simp only [← mul_sum]
      field
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsAlgClosed F
f : F[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
⊢ ∃ (f₁ : F[X]) (f₂ : F[X]), f₁.IsMonicOfDegree 1 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
have obtain : ∀ (f₁ : F[X]) (hf₁m : f₁.Monic) (hf₁i : Irreducible f₁) (f₂ : F[X]) (hf₂ : f = f₁ * f₂),
  ∃ (f₁ : F[X]) (f₂ : F[X]), f₁.IsMonicOfDegree 1 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
Tactic: obtain ⟨f₁, hf₁m, hf₁i, f₂, hf₂⟩ :=
    exists_monic_irreducible_factor f <| not_isUnit_of_natDegree_pos f <|
      by grind [IsMonicOfDegree.natDegree_eq]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsAlgClosed F
f : F[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : F[X]
hf₁m : f₁.Monic
hf₁i : Irreducible f₁
f₂ : F[X]
hf₂ : f = f₁ * f₂
⊢ ∃ (f₁ : F[X]) (f₂ : F[X]), f₁.IsMonicOfDegree 1 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
have hf₁ : (f₁ * f₂).IsMonicOfDegree (1 + n)
Tactic: rw [hf₂, add_comm] at hf
Cleared hypotheses: hf, hf₂
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : IsAlgClosed F
f : F[X]
n : ℕ
f₁ : F[X]
hf₁m : f₁.Monic
hf₁i : Irreducible f₁
f₂ : F[X]
hf : (f₁ * f₂).IsMonicOfDegree (1 + n)
hf₂ : f = f₁ * f₂
⊢ ∃ (f₁ : F[X]) (f₂ : F[X]), f₁.IsMonicOfDegree 1 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
have hf₁ : f₁.IsMonicOfDegree 1
Tactic: have hf₁ : IsMonicOfDegree f₁ 1 :=
    ⟨natDegree_eq_of_degree_eq_some <| IsAlgClosed.degree_eq_one_of_irreducible F hf₁i, hf₁m⟩
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (goal)
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), (f₁.IsMonicOfDegree 1 ∨ f₁.IsMonicOfDegree 2) ∧ f = f₁ * f₂
have obtain : ∀ (f₁ : ℝ[X]) (hm : f₁.Monic) (hirr : Irreducible f₁) (f₂ : ℝ[X]) (hf₂ : f = f₁ * f₂),
  ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), (f₁.IsMonicOfDegree 1 ∨ f₁.IsMonicOfDegree 2) ∧ f = f₁ * f₂
Tactic: obtain ⟨f₁, hm, hirr, f₂, hf₂⟩ :=
    exists_monic_irreducible_factor f <| not_isUnit_of_natDegree_pos f <|
      by grind [IsMonicOfDegree.natDegree_eq]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (goal)
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : ℝ[X]
hm : f₁.Monic
hirr : Irreducible f₁
f₂ : ℝ[X]
hf₂ : f = f₁ * f₂
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), (f₁.IsMonicOfDegree 1 ∨ f₁.IsMonicOfDegree 2) ∧ f = f₁ * f₂
have refine : f₁.IsMonicOfDegree 1 ∨ f₁.IsMonicOfDegree 2
Tactic: refine ⟨f₁, f₂, ?_, hf₂⟩