awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Polynomial.Basic
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) : ℝ)|}
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  ∀ (key : Set.Finite (α := ℤ) {x : ℤ | |eval x P| ≤ |eval x Q|}), Set.Finite (α := ℤ) {x : ℤ | |eval x P| ≤ |eval x Q|}
⊢ Set.Finite (α := ℤ) {x : ℤ | |eval x P| ≤ |eval x Q|}

Tactic:
norm_cast at key
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
P Q : ℤ[X]
mQ : Q.Monic
h : Set.Infinite (α := ℤ) {a : ℤ | eval a Q ∣ eval a P}
⊢ P %ₘ Q + Q * (P /ₘ Q) = P

Tactic:
have eqR := modByMonic_add_div P Q
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
P Q : ℤ[X]
mQ : Q.Monic
h : Set.Infinite (α := ℤ) {a : ℤ | eval a Q ∣ eval a P}
eqR : P %ₘ Q + Q * (P /ₘ Q) = P
⊢ (P %ₘ Q).degree < Q.degree

Tactic:
have degR := degree_modByMonic_lt P mQ
-- Module: Mathlib.Analysis.Polynomial.Basic
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
rw : P %ₘ Q = 0
⊢ Q ∣ P

Tactic:
rw [← modByMonic_eq_zero_iff_dvd mQ]

Premises used: Polynomial.modByMonic_eq_zero_iff_dvd
-- Module: Mathlib.Analysis.Polynomial.Basic
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
set :
  let R := P %ₘ Q;
  ∀ (eqR : R + Q * (P /ₘ Q) = P) (degR : R.degree < Q.degree), R = 0
⊢ P %ₘ Q = 0

Tactic:
set R := P %ₘ Q
-- Module: Mathlib.Analysis.Polynomial.Basic
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
h₁ : Set.Infinite (α := ℤ) {x : ℤ | R.IsRoot x}
⊢ R = 0

Tactic:
apply eq_zero_of_infinite_isRoot

Premises used: Polynomial.eq_zero_of_infinite_isRoot
-- Module: Mathlib.Analysis.Polynomial.Basic
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}

Tactic:
(h.diff (finite_abs_eval_le_of_degree_lt degR)).mono fun x mx ↦ ?_

Premises used: Set.Infinite.mono, Polynomial.finite_abs_eval_le_of_degree_lt, Set.Infinite.diff
-- Module: Mathlib.Analysis.Polynomial.Basic
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
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
⊢ Set.Infinite (α := ℤ) {x : ℤ | R.IsRoot x}

Tactic:
refine (h.diff (finite_abs_eval_le_of_degree_lt degR)).mono fun x mx ↦ ?_

Premises used: Set.Infinite.mono, Polynomial.finite_abs_eval_le_of_degree_lt, Set.Infinite.diff
-- Module: Mathlib.Analysis.Polynomial.Basic
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
⊢ 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

Premises used: not_le, Set.mem_setOf_eq, Set.mem_diff
-- Module: Mathlib.Analysis.Polynomial.Basic
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|
⊢ |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

Premises used: abs_dvd, Int.dvd_add_self_mul, Polynomial.eval_mul, Polynomial.eval_add
-- Module: Mathlib.Analysis.Polynomial.Basic
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 R ∧ |eval x R| < |eval x Q|
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | R.IsRoot x} x

Tactic:
Int.eq_zero_of_abs_lt_dvd mx.1 mx.2

Premises used: Set.Mem, Polynomial.IsRoot, setOf, And.right, And.left, Int.eq_zero_of_abs_lt_dvd
-- Module: Mathlib.Analysis.Polynomial.Basic
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 R ∧ |eval x R| < |eval x Q|
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | R.IsRoot x} x

Tactic:
exact Int.eq_zero_of_abs_lt_dvd mx.1 mx.2

Premises used: And.right, And.left, Int.eq_zero_of_abs_lt_dvd
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
⊢ 1 ≤ p.cauchyBound

Tactic:
simp [cauchyBound]

Premises used: Polynomial.cauchyBound
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
⊢ cauchyBound.{u_1} (K := K) 0 = 1

Tactic:
simp [cauchyBound]

Premises used: Polynomial.cauchyBound
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
x : K
⊢ cauchyBound.{u_1} (K := K) ((C : (a : K) → K[X]) x) = 1

Tactic:
simp [cauchyBound]

Premises used: Polynomial.cauchyBound
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
⊢ cauchyBound.{u_1} (K := K) 1 = 1

Tactic:
cauchyBound_C 1

Premises used: Polynomial.cauchyBound_C, OfNat.ofNat
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
⊢ cauchyBound.{u_1} (K := K) X = 1

Tactic:
simp [cauchyBound]

Premises used: Polynomial.cauchyBound
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
x : K
⊢ (HAdd.hAdd (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])).cauchyBound = ‖x‖₊ + 1

Tactic:
simp [cauchyBound]

Premises used: Polynomial.cauchyBound
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
x : K
⊢ (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])).cauchyBound = ‖x‖₊ + 1

Tactic:
simp [cauchyBound]

Premises used: Polynomial.cauchyBound
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
x : K
hx : x ≠ 0
p : K[X]
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‖₊
⊢ (x • p).cauchyBound = p.cauchyBound

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]

Premises used: IsRegular.of_ne_zero, Polynomial.natDegree_smul_of_smul_regular, IsLeftRegular.isSMulRegular, add_left_inj, NNReal.mul_finset_sup, Polynomial.leadingCoeff_smul_of_smul_regular, Polynomial.cauchyBound, Polynomial.coeff_smul, nnnorm_mul, smul_eq_mul, IsRegular.left
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
x : K
hx : x ≠ 0
p : K[X]
hc : ‖x‖₊ ≠ 0
⊢ (‖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:
apply mul_div_mul_left

Premises used: mul_div_mul_left
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
x : K
hx : x ≠ 0
p : K[X]
⊢ ‖x‖₊ ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : p.IsRoot a
⊢ 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

Premises used: Polynomial.IsRoot.def, Finset.range_add_one, Polynomial.eval_eq_sum_range
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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
⊢ 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

Premises used: Polynomial.coeff_natDegree, add_eq_zero_iff_eq_neg, Finset.mem_range, lt_self_iff_false, Finset.sum_insert, not_false_eq_true
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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
⊢ ‖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

Premises used: NNNorm.nnnorm
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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)
⊢ ‖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

Premises used: nnnorm_pow, nnnorm_neg, nnnorm_mul
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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
inr : ∀ (ha : ‖a‖₊ ≠ 1), ‖a‖₊ < p.cauchyBound
⊢ ‖a‖₊ < p.cauchyBound

Tactic:
rcases eq_or_ne ‖a‖₊ 1 with ha | ha

Premises used: NNNorm.nnnorm, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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
inl : ∀ (this : 1 ≤ (p.cauchyBound - 1) * (↑p.natDegree : ℝ≥0)), 1 < p.cauchyBound
⊢ ‖a‖₊ < p.cauchyBound

Tactic:
simp only [ha, one_pow, sum_const, card_range, nsmul_eq_mul, mul_one, gt_iff_lt] at this ⊢

Premises used: one_pow, Finset.card_range, gt_iff_lt, nsmul_eq_mul, mul_one, Finset.sum_const
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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)
inl : 1 ≠ p.cauchyBound
⊢ 1 < p.cauchyBound

Tactic:
apply lt_of_le_of_ne (by simp)

Premises used: lt_of_le_of_ne
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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)
nh : 1 = p.cauchyBound
⊢ False

Tactic:
simp [← nh, tsub_self] at this

Premises used: tsub_self
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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
inr₁ : ∀ (ha : 1 < ‖a‖₊), ‖a‖₊ < p.cauchyBound
⊢ ‖a‖₊ < p.cauchyBound

Tactic:
rcases lt_or_gt_of_ne ha with ha | ha

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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
inr : 1 ≤ p.cauchyBound
⊢ ‖a‖₊ < p.cauchyBound

Tactic:
apply ha.trans_le

Premises used: LT.lt.trans_le
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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
⊢ 1 ≤ p.cauchyBound

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))

Tactic:
rw [geom_sum_of_one_lt ha] at this

Premises used: geom_sum_of_one_lt
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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‖₊
this₁ : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
⊢ ‖a‖₊ ≠ 1

Tactic:
rw [geom_sum_of_one_lt ha] at this

Premises used: geom_sum_of_one_lt
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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‖₊
this₁ : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha₁ : ‖a‖₊ ≠ 1
⊢ 1 < ‖a‖₊

Tactic:
rw [geom_sum_of_one_lt ha] at this

Premises used: geom_sum_of_one_lt
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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‖₊ = ‖a‖₊ - 1 + 1

Tactic:
(tsub_add_cancel_of_le ha.le).symm

Premises used: tsub_add_cancel_of_le, LT.lt.le, Eq.symm
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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

Tactic:
field
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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 ≤ ‖a‖₊ ^ p.natDegree
⊢ ‖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:
gcongr
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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‖₊
e_a :
  (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1) =
    (p.cauchyBound - 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

Tactic:
congr 2
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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 ≠ 0

Tactic:
have : ‖a‖₊ - 1 ≠ 0 := fun nh ↦ (ha.trans_le (tsub_eq_zero_iff_le.mp nh)).false
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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_1 : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha_1 : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
this : ‖a‖₊ - 1 ≠ 0
⊢ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1) =
    (p.cauchyBound - 1) * (‖a‖₊ ^ p.natDegree - 1)

Tactic:
field
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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
bc₁ : ‖a‖₊ ^ p.natDegree - 1 < ‖a‖₊ ^ p.natDegree
⊢ (p.cauchyBound - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1 <
    (p.cauchyBound - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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
⊢ 0 < p.cauchyBound - 1

Tactic:
apply lt_of_le_of_ne (by simp)

Premises used: lt_of_le_of_ne
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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 :
  ∀ (this : 0 = p.cauchyBound - 1), (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) < ‖a‖₊ ^ p.natDegree
⊢ 0 ≠ p.cauchyBound - 1

Tactic:
contrapose! this
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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
bc : 0 < ‖a‖₊ ^ p.natDegree
⊢ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) < ‖a‖₊ ^ p.natDegree

Tactic:
simp only [← this, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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
bc : 0 < ‖a‖₊
⊢ 0 < ‖a‖₊ ^ p.natDegree

Tactic:
apply pow_pos

Premises used: pow_pos
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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‖₊

Tactic:
zero_lt_one.trans ha

Premises used: zero_lt_one, LT.lt.trans
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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‖₊

Tactic:
exact zero_lt_one.trans ha

Premises used: zero_lt_one, LT.lt.trans
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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 - 1 < ‖a‖₊ ^ p.natDegree

Tactic:
simp [zero_lt_one.trans ha]

Premises used: zero_lt_one, LT.lt.trans
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
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 / ‖a‖₊ ^ p.natDegree + 1 = p.cauchyBound

Tactic:
simp [field, tsub_add_cancel_of_le]

Premises used: tsub_add_cancel_of_le