-- Mathlib/Topology/Algebra/Polynomial.lean
theorem coeff_le_of_roots_le {p : F[X]} {f : F →+* K} {B : ℝ} (i : ℕ) (h1 : p.Monic)
    (h2 : Splits f p) (h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B) :
    ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * p.natDegree.choose i

Proof state:
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
⊢ ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * ↑(p.natDegree.choose i)

Tactic:
obtain hB | hB := lt_or_le B 0

Result:
case inl
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : B < 0
⊢ ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * ↑(p.natDegree.choose i)

case inr
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
⊢ ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * ↑(p.natDegree.choose i)

Proof state:
case inr.inl
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : (map f p).natDegree < i
⊢ ‖(map f p).coeff i‖ ≤ B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)

Tactic:
rw [coeff_eq_zero_of_natDegree_lt hi, norm_zero]

Result:
case inr.inl
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : (map f p).natDegree < i
⊢ 0 ≤ B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)

Proof state:
case inr.inr
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
⊢ ‖(map f p).coeff i‖ ≤ B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)

Tactic:
rw [coeff_eq_esymm_roots_of_splits ((splits_id_iff_splits f).2 h2) hi, (h1.map _).leadingCoeff,
  one_mul, norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul]

Result:
case inr.inr
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
⊢ ‖(map f p).roots.esymm ((map f p).natDegree - i)‖ ≤ B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)

Proof state:
case intro.intro.intro.intro
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
⊢ ‖s.prod‖ ≤ B ^ ((map f p).natDegree - i)

Tactic:
lift B to ℝ≥0 using hB

Result:
case intro.intro.intro.intro.intro
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : p.Monic
h2 : Splits f p
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ ↑B
⊢ ‖s.prod‖ ≤ ↑B ^ ((map f p).natDegree - i)

Proof state:
case inr.inr
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
⊢ (Multiset.map (fun x => ‖x‖) (Multiset.map prod (powersetCard ((map f p).natDegree - i) (map f p).roots))).card •
      ?m.42576 ≤
    B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)

Tactic:
rw [Multiset.map_map, card_map, card_powersetCard, ← natDegree_eq_card_roots' h2,
  Nat.choose_symm hi, mul_comm, nsmul_eq_mul]

Result:
no goals

Proof state:
case inl
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : B < 0
⊢ ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * ↑(p.natDegree.choose i)

Tactic:
rw [eq_one_of_roots_le hB h1 h2 h3, Polynomial.map_one, natDegree_one, zero_tsub, pow_zero,
  one_mul, coeff_one]

Result:
case inl
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : B < 0
⊢ ‖if i = 0 then 1 else 0‖ ≤ ↑(Nat.choose 0 i)

Proof state:
case inr
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
⊢ ‖(map f p).coeff i‖ ≤ B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)

Tactic:
obtain hi | hi := lt_or_le (map f p).natDegree i

Result:
case inr.inl
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : (map f p).natDegree < i
⊢ ‖(map f p).coeff i‖ ≤ B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)

case inr.inr
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
⊢ ‖(map f p).coeff i‖ ≤ B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)

Proof state:
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
⊢ ∀ r ∈ Multiset.map (fun x => ‖x‖) (Multiset.map prod (powersetCard ((map f p).natDegree - i) (map f p).roots)),
    r ≤ B ^ ((map f p).natDegree - i)

Tactic:
intro r hr

Result:
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
r : ℝ
hr : r ∈ Multiset.map (fun x => ‖x‖) (Multiset.map prod (powersetCard ((map f p).natDegree - i) (map f p).roots))
⊢ r ≤ B ^ ((map f p).natDegree - i)

Proof state:
case intro.intro.intro.intro.intro
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : p.Monic
h2 : Splits f p
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ ↑B
⊢ (Multiset.map (⇑↑nnnormHom) s).prod ≤ B ^ ((map f p).natDegree - i)

Tactic:
refine (prod_le_pow_card _ B fun x hx => ?_).trans_eq (by rw [card_map, hs.2])

Result:
case intro.intro.intro.intro.intro
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : p.Monic
h2 : Splits f p
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ ↑B
x : ℝ≥0
hx : x ∈ Multiset.map (⇑↑nnnormHom) s
⊢ x ≤ B