awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
hP : ¬P = 0
⊢ IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q
have neg : Q.leadingCoeff ≠ 0
Tactic: refine isEquivalent_cobounded_leading_monomial.trans_isLittleO <|
      ((IsLittleO.const_mul_right ?_ ?_).const_mul_left _).trans_isEquivalent
        isEquivalent_cobounded_leading_monomial.symm
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
hP : ¬P = 0
neg : Q.leadingCoeff ≠ 0
⊢ IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q
have neg₁ : IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ P.natDegree) fun (x : R) ↦ x ^ Q.natDegree
Tactic: refine isEquivalent_cobounded_leading_monomial.trans_isLittleO <|
      ((IsLittleO.const_mul_right ?_ ?_).const_mul_left _).trans_isEquivalent
        isEquivalent_cobounded_leading_monomial.symm
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree ≤ Q.degree
⊢ IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q
have pos : ∀ (hQ : Q.leadingCoeff = 0), IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q
Tactic: by_cases hQ : Q.leadingCoeff = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree ≤ Q.degree
pos :
  ∀ (hQ : Q.leadingCoeff = 0), IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q
⊢ IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q
have neg : ∀ (hQ : ¬Q.leadingCoeff = 0), IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q
Tactic: by_cases hQ : Q.leadingCoeff = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree ≤ Q.degree
hQ : ¬Q.leadingCoeff = 0
⊢ IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q
have neg : IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ P.natDegree) fun (x : R) ↦ x ^ Q.natDegree
Tactic: refine isEquivalent_cobounded_leading_monomial.trans_isBigO <|
      ((IsBigO.const_mul_right hQ ?_).const_mul_left _).trans_isEquivalent
        isEquivalent_cobounded_leading_monomial.symm
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
Goal:
P Q : ℤ[X]
h : Q.degree < P.degree
⊢ Set.Finite (α := ℤ) {x : ℤ | |eval x P| ≤ |eval x Q|}
have o : IsLittleO (E := ℤ) (F := ℤ) (Bornology.cobounded ℤ) (fun (x : ℤ) ↦ eval x Q) fun (x : ℤ) ↦ eval x P
Tactic: have o := isLittleO_cobounded_of_degree_lt h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
Goal:
P Q : ℤ[X]
h : Q.degree < P.degree
o : IsLittleO (E := ℤ) (F := ℤ) (Bornology.cobounded ℤ) (fun (x : ℤ) ↦ eval x Q) fun (x : ℤ) ↦ eval x P
⊢ Set.Finite (α := ℤ) {x : ℤ | |eval x P| ≤ |eval x Q|}
have o₁ : IsLittleO (E := ℤ) (F := ℤ) cofinite (fun (x : ℤ) ↦ eval x Q) fun (x : ℤ) ↦ eval x P
Tactic: rw [IsOrderBornology.cobounded_eq, ← Int.cofinite_eq] at o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
Goal:
P Q : ℤ[X]
h : Q.degree < P.degree
o : IsLittleO (E := ℤ) (F := ℤ) cofinite (fun (x : ℤ) ↦ eval x Q) fun (x : ℤ) ↦ eval x P
⊢ Set.Finite (α := ℤ) {x : ℤ | |eval x P| ≤ |eval x Q|}
have nr : ∀ᶠ (x : ℤ) in cofinite, ¬P.IsRoot x
Tactic: have nr := eventually_cofinite_not_isRoot (ne_zero_of_degree_gt h)
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
Goal:
P Q : ℤ[X]
h : Q.degree < P.degree
o : IsLittleO (E := ℤ) (F := ℤ) cofinite (fun (x : ℤ) ↦ eval x Q) fun (x : ℤ) ↦ eval x P
nr : ∀ᶠ (x : ℤ) in cofinite, ¬P.IsRoot x
⊢ Set.Finite (α := ℤ) {x : ℤ | |eval x P| ≤ |eval x Q|}
have key : ∀ᶠ (x : ℤ) in cofinite, ‖eval x Q‖ < ‖eval x P‖
Tactic: have key := o.eventuallyLT_norm_of_eventually_pos (nr.congr (.of_forall (by simp)))
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
Goal:
P Q : ℤ[X]
h : Q.degree < P.degree
o : IsLittleO (E := ℤ) (F := ℤ) cofinite (fun (x : ℤ) ↦ eval x Q) fun (x : ℤ) ↦ eval x P
nr : ∀ᶠ (x : ℤ) in cofinite, ¬P.IsRoot x
key : ∀ᶠ (x : ℤ) in cofinite, ‖eval x Q‖ < ‖eval x P‖
⊢ Set.Finite (α := ℤ) {x : ℤ | |eval x P| ≤ |eval x Q|}
have key₁ : Set.Finite (α := ℤ) {x : ℤ | LE.le (α := ℝ) |(↑(eval x P) : ℝ)| |(↑(eval x Q) : ℝ)|}
Tactic: simp_rw [eventually_cofinite, not_lt, Int.norm_eq_abs] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
P Q : ℤ[X]
h : Q.degree < P.degree
o : IsLittleO (E := ℤ) (F := ℤ) cofinite (fun (x : ℤ) ↦ eval x Q) fun (x : ℤ) ↦ eval x P
nr : ∀ᶠ (x : ℤ) in cofinite, ¬P.IsRoot x
key : Set.Finite (α := ℤ) {x : ℤ | LE.le (α := ℝ) |(↑(eval x P) : ℝ)| |(↑(eval x Q) : ℝ)|}
⊢ Set.Finite (α := ℤ) {x : ℤ | |eval x P| ≤ |eval x Q|}
have norm_cast : ∀ (key : Set.Finite (α := ℤ) {x : ℤ | |eval x P| ≤ |eval x Q|}), Set.Finite (α := ℤ) {x : ℤ | |eval x P| ≤ |eval x Q|}
Tactic: norm_cast at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
Goal:
P Q : ℤ[X]
mQ : Q.Monic
h : Set.Infinite (α := ℤ) {a : ℤ | eval a Q ∣ eval a P}
⊢ Q ∣ P
have eqR : P %ₘ Q + Q * (P /ₘ Q) = P
Tactic: have eqR := modByMonic_add_div P Q
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
Goal:
P Q : ℤ[X]
mQ : Q.Monic
h : Set.Infinite (α := ℤ) {a : ℤ | eval a Q ∣ eval a P}
eqR : P %ₘ Q + Q * (P /ₘ Q) = P
⊢ Q ∣ P
have degR : (P %ₘ Q).degree < Q.degree
Tactic: have degR := degree_modByMonic_lt P mQ
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
P Q : ℤ[X]
mQ : Q.Monic
h : Set.Infinite (α := ℤ) {a : ℤ | eval a Q ∣ eval a P}
eqR : P %ₘ Q + Q * (P /ₘ Q) = P
degR : (P %ₘ Q).degree < Q.degree
⊢ Q ∣ P
have rw : P %ₘ Q = 0
Tactic: rw [← modByMonic_eq_zero_iff_dvd mQ]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
P Q : ℤ[X]
mQ : Q.Monic
h : Set.Infinite (α := ℤ) {a : ℤ | eval a Q ∣ eval a P}
eqR : P %ₘ Q + Q * (P /ₘ Q) = P
degR : (P %ₘ Q).degree < Q.degree
⊢ P %ₘ Q = 0
have set : let R := P %ₘ Q;
∀ (eqR : R + Q * (P /ₘ Q) = P) (degR : R.degree < Q.degree), R = 0
Tactic: set R := P %ₘ Q
Cleared hypotheses: eqR, degR
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
P Q : ℤ[X]
mQ : Q.Monic
h : Set.Infinite (α := ℤ) {a : ℤ | eval a Q ∣ eval a P}
R : ℤ[X] := P %ₘ Q
eqR : R + Q * (P /ₘ Q) = P
degR : R.degree < Q.degree
⊢ R = 0
have h₁ : Set.Infinite (α := ℤ) {x : ℤ | R.IsRoot x}
Tactic: apply eq_zero_of_infinite_isRoot
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
P Q : ℤ[X]
mQ : Q.Monic
h : Set.Infinite (α := ℤ) {a : ℤ | eval a Q ∣ eval a P}
R : ℤ[X] := P %ₘ Q
eqR : R + Q * (P /ₘ Q) = P
degR : R.degree < Q.degree
⊢ Set.Infinite (α := ℤ) {x : ℤ | R.IsRoot x}
have h₁ : ∀ (x : ℤ) (mx : Membership.mem (γ := Set ℤ) ({a : ℤ | eval a Q ∣ eval a P} \ {x : ℤ | |eval x Q| ≤ |eval x R|}) x),
  Membership.mem (γ := Set ℤ) {x : ℤ | R.IsRoot x} x
Tactic: refine (h.diff (finite_abs_eval_le_of_degree_lt degR)).mono fun x mx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
Goal:
P Q : ℤ[X]
mQ : Q.Monic
h : Set.Infinite (α := ℤ) {a : ℤ | eval a Q ∣ eval a P}
R : ℤ[X] := P %ₘ Q
eqR : R + Q * (P /ₘ Q) = P
degR : R.degree < Q.degree
x : ℤ
mx : Membership.mem (γ := Set ℤ) ({a : ℤ | eval a Q ∣ eval a P} \ {x : ℤ | |eval x Q| ≤ |eval x R|}) x
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | R.IsRoot x} x
have mx₁ : eval x Q ∣ eval x P ∧ |eval x R| < |eval x Q|
Tactic: simp only [Set.mem_diff, Set.mem_setOf_eq, not_le] at mx
Cleared hypotheses: mx
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
Goal:
P Q : ℤ[X]
mQ : Q.Monic
h : Set.Infinite (α := ℤ) {a : ℤ | eval a Q ∣ eval a P}
R : ℤ[X] := P %ₘ Q
eqR : R + Q * (P /ₘ Q) = P
degR : R.degree < Q.degree
x : ℤ
mx : eval x Q ∣ eval x P ∧ |eval x R| < |eval x Q|
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | R.IsRoot x} x
have mx₁ : |eval x Q| ∣ eval x R ∧ |eval x R| < |eval x Q|
Tactic: rw [← eqR, eval_add, eval_mul, Int.dvd_add_self_mul, ← abs_dvd] at mx
Cleared hypotheses: mx
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
x : K
hx : x ≠ 0
p : K[X]
⊢ (x • p).cauchyBound = p.cauchyBound
have simp : (‖x‖₊ * (range p.natDegree).sup fun (a : ℕ) ↦ ‖p.coeff a‖₊) / (‖x‖₊ * ‖p.leadingCoeff‖₊) =
  ((range p.natDegree).sup fun (a : ℕ) ↦ ‖p.coeff a‖₊) / ‖p.leadingCoeff‖₊
Tactic: simp only [cauchyBound, (IsRegular.of_ne_zero hx).left.isSMulRegular,
    natDegree_smul_of_smul_regular, coeff_smul, smul_eq_mul, nnnorm_mul, ← mul_finset_sup,
    leadingCoeff_smul_of_smul_regular, add_left_inj]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.CauchyBound (goal)
Goal:
K : Type u_1
inst : NormedDivisionRing K
x : K
hx : x ≠ 0
p : K[X]
⊢ (‖x‖₊ * (range p.natDegree).sup fun (a : ℕ) ↦ ‖p.coeff a‖₊) / (‖x‖₊ * ‖p.leadingCoeff‖₊) =
    ((range p.natDegree).sup fun (a : ℕ) ↦ ‖p.coeff a‖₊) / ‖p.leadingCoeff‖₊
have hc : ‖x‖₊ ≠ 0
Tactic: apply mul_div_mul_left
-- 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.IsRoot a
⊢ ‖a‖₊ < p.cauchyBound
have h₁ : Eq.{u_1 + 1} (α := K) (∑ i ∈ insert p.natDegree (range p.natDegree), p.coeff i * a ^ i) 0
Tactic: rw [IsRoot.def, eval_eq_sum_range, range_add_one] 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 : Eq.{u_1 + 1} (α := K) (∑ i ∈ insert p.natDegree (range p.natDegree), p.coeff i * a ^ i) 0
⊢ ‖a‖₊ < p.cauchyBound
have h₁ : p.leadingCoeff * a ^ p.natDegree = -∑ i ∈ range p.natDegree, p.coeff i * a ^ i
Tactic: simp only [mem_range, lt_self_iff_false, not_false_eq_true, sum_insert, coeff_natDegree,
    add_eq_zero_iff_eq_neg] 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 = -∑ i ∈ range p.natDegree, p.coeff i * a ^ i
⊢ ‖a‖₊ < p.cauchyBound
have h₁ : ‖p.leadingCoeff * a ^ p.natDegree‖₊ = nnnorm.{u_1} (E := K) (-∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
Tactic: apply_fun nnnorm 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.cauchyBound
have h₁ : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
Tactic: simp only [nnnorm_mul, nnnorm_pow, nnnorm_neg] at h
Cleared hypotheses: h
-- 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) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
⊢ ‖a‖₊ < p.cauchyBound
have inl : ∀ (ha : ‖a‖₊ = 1), ‖a‖₊ < p.cauchyBound
Tactic: rcases eq_or_ne ‖a‖₊ 1 with ha | ha
-- 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) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
inl : ∀ (ha : ‖a‖₊ = 1), ‖a‖₊ < p.cauchyBound
⊢ ‖a‖₊ < p.cauchyBound
have inr : ∀ (ha : ‖a‖₊ ≠ 1), ‖a‖₊ < p.cauchyBound
Tactic: rcases eq_or_ne ‖a‖₊ 1 with ha | ha
-- 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) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
ha : ‖a‖₊ = 1
⊢ ‖a‖₊ < p.cauchyBound
have inl : ∀ (this : 1 ≤ (p.cauchyBound - 1) * (↑p.natDegree : ℝ≥0)), 1 < p.cauchyBound
Tactic: simp only [ha, one_pow, sum_const, card_range, nsmul_eq_mul, mul_one, gt_iff_lt] at this ⊢
Cleared hypotheses: this
-- 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)
ha : ‖a‖₊ = 1
this : 1 ≤ (p.cauchyBound - 1) * (↑p.natDegree : ℝ≥0)
⊢ 1 < p.cauchyBound
have inl : 1 ≠ p.cauchyBound
Tactic: apply lt_of_le_of_ne (by 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)
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
ha : ‖a‖₊ ≠ 1
⊢ ‖a‖₊ < p.cauchyBound
have inr : ∀ (ha : ‖a‖₊ < 1), ‖a‖₊ < p.cauchyBound
Tactic: rcases lt_or_gt_of_ne ha with ha | ha
-- 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) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
ha : ‖a‖₊ ≠ 1
inr : ∀ (ha : ‖a‖₊ < 1), ‖a‖₊ < p.cauchyBound
⊢ ‖a‖₊ < p.cauchyBound
have inr₁ : ∀ (ha : 1 < ‖a‖₊), ‖a‖₊ < p.cauchyBound
Tactic: rcases lt_or_gt_of_ne ha with ha | ha
-- 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) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
ha_1 : ‖a‖₊ ≠ 1
ha : ‖a‖₊ < 1
⊢ ‖a‖₊ < p.cauchyBound
have inr : 1 ≤ p.cauchyBound
Tactic: apply ha.trans_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)
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
ha_1 : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
⊢ ‖a‖₊ < p.cauchyBound
have this₁ : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
Tactic: rw [geom_sum_of_one_lt ha] at this
Cleared hypotheses: this, ha_1, ha
-- 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‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 ≤
    (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1
have bc : 0 ≤ ‖a‖₊ ^ p.natDegree
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)
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha_1 : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
⊢ (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
have e_a : (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1) =
  (p.cauchyBound - 1) * (‖a‖₊ ^ p.natDegree - 1)
Tactic: congr 2
-- 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)
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha_1 : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
⊢ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1) =
    (p.cauchyBound - 1) * (‖a‖₊ ^ p.natDegree - 1)
have this₁ : ‖a‖₊ - 1 ≠ 0
Tactic: have : ‖a‖₊ - 1 ≠ 0 := fun nh ↦ (ha.trans_le (tsub_eq_zero_iff_le.mp nh)).false
-- 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‖₊
⊢ (p.cauchyBound - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1 <
    (p.cauchyBound - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1
have bc : 0 < p.cauchyBound - 1
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)
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha_1 : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
bc : 0 < p.cauchyBound - 1
⊢ (p.cauchyBound - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1 <
    (p.cauchyBound - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1
have bc₁ : ‖a‖₊ ^ p.natDegree - 1 < ‖a‖₊ ^ p.natDegree
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)
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha_1 : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
⊢ 0 < p.cauchyBound - 1
have bc : 0 ≠ p.cauchyBound - 1
Tactic: apply lt_of_le_of_ne (by 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)
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha_1 : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
⊢ 0 ≠ p.cauchyBound - 1
have bc : ∀ (this : 0 = p.cauchyBound - 1), (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) < ‖a‖₊ ^ p.natDegree
Tactic: contrapose! this
Cleared hypotheses: this
-- 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)
ha_1 : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
this : 0 = p.cauchyBound - 1
⊢ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) < ‖a‖₊ ^ p.natDegree
have bc : 0 < ‖a‖₊ ^ p.natDegree
Tactic: simp only [← this, zero_mul]
-- 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)
ha_1 : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
this : 0 = p.cauchyBound - 1
⊢ 0 < ‖a‖₊ ^ p.natDegree
have bc : 0 < ‖a‖₊
Tactic: apply pow_pos
-- 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‖₊ < p.cauchyBound
have _ : ‖a‖₊ - 1 + 1 = ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 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.cauchyBound
have _₁ : ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 ≤
  (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 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]