case inl
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : B < 0
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree p - i) * ↑(Nat.choose (natDegree p) i)

case inr
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree p - i) * ↑(Nat.choose (natDegree p) i)
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree p - i) * ↑(Nat.choose (natDegree p) i)
obtain hB | hB := lt_or_le B 0
case inr
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
case inr
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree p - i) * ↑(Nat.choose (natDegree p) i)
rw [← h1.natDegree_map f]
case inr.inl
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : natDegree (map f p) < i
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)

case inr.inr
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
case inr
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
obtain hi | hi := lt_or_le (map f p).natDegree i
case inr.inr
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
⊢ ‖esymm (roots (map f p)) (natDegree (map f p) - i)‖ ≤
    B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
case inr.inr
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
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]
case inr.inr
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
⊢ ↑card (Multiset.map (fun x => ‖x‖) (Multiset.map prod (powersetLen (natDegree (map f p) - i) (roots (map f p))))) •
      ?m.198217 ≤
    B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)

α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
⊢ ℝ

α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
⊢ ∀ (r : ℝ),
    r ∈ Multiset.map (fun x => ‖x‖) (Multiset.map prod (powersetLen (natDegree (map f p) - i) (roots (map f p)))) →
      r ≤ ?m.198217
case inr.inr
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
⊢ ‖esymm (roots (map f p)) (natDegree (map f p) - i)‖ ≤
    B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
apply ((norm_multiset_sum_le _).trans <| sum_le_card_nsmul _ _ fun r hr => _).trans
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
r : ℝ
hr : r ∈ Multiset.map (fun x => ‖x‖) (Multiset.map prod (powersetLen (natDegree (map f p) - i) (roots (map f p))))
⊢ r ≤ B ^ (natDegree (map f p) - i)
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
⊢ ∀ (r : ℝ),
    r ∈ Multiset.map (fun x => ‖x‖) (Multiset.map prod (powersetLen (natDegree (map f p) - i) (roots (map f p)))) →
      r ≤ B ^ (natDegree (map f p) - i)
intro r hr
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
r : ℝ
hr : ∃ a, (∃ a_1, a_1 ∈ powersetLen (natDegree (map f p) - i) (roots (map f p)) ∧ prod a_1 = a) ∧ ‖a‖ = r
⊢ r ≤ B ^ (natDegree (map f p) - i)
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
r : ℝ
hr : r ∈ Multiset.map (fun x => ‖x‖) (Multiset.map prod (powersetLen (natDegree (map f p) - i) (roots (map f p))))
⊢ r ≤ B ^ (natDegree (map f p) - i)
simp_rw [Multiset.mem_map] at hr
case intro.intro.intro.intro
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ∈ powersetLen (natDegree (map f p) - i) (roots (map f p))
⊢ ‖prod s‖ ≤ B ^ (natDegree (map f p) - i)
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
r : ℝ
hr : ∃ a, (∃ a_1, a_1 ∈ powersetLen (natDegree (map f p) - i) (roots (map f p)) ∧ prod a_1 = a) ∧ ‖a‖ = r
⊢ r ≤ B ^ (natDegree (map f p) - i)
obtain ⟨_, ⟨s, hs, rfl⟩, rfl⟩ := hr
case intro.intro.intro.intro
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
⊢ ‖prod s‖ ≤ B ^ (natDegree (map f p) - i)
case intro.intro.intro.intro
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ∈ powersetLen (natDegree (map f p) - i) (roots (map f p))
⊢ ‖prod s‖ ≤ B ^ (natDegree (map f p) - i)
rw [mem_powersetLen] at hs
case intro.intro.intro.intro.intro
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : Monic p
h2 : Splits f p
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
B : ℝ≥0
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ ↑B
⊢ ‖prod s‖ ≤ ↑B ^ (natDegree (map f p) - i)
case intro.intro.intro.intro
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
⊢ ‖prod s‖ ≤ B ^ (natDegree (map f p) - i)
lift B to ℝ≥0 using hB
case intro.intro.intro.intro.intro
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : Monic p
h2 : Splits f p
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
B : ℝ≥0
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ ↑B
⊢ prod (Multiset.map (↑↑nnnormHom) s) ≤ B ^ (natDegree (map f p) - i)
case intro.intro.intro.intro.intro
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : Monic p
h2 : Splits f p
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
B : ℝ≥0
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ ↑B
⊢ ‖prod s‖ ≤ ↑B ^ (natDegree (map f p) - i)
rw [← coe_nnnorm, ← NNReal.coe_pow, NNReal.coe_le_coe, ← nnnormHom_apply, ← MonoidHom.coe_coe,
  MonoidHom.map_multiset_prod]
case intro.intro.intro.intro.intro
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : Monic p
h2 : Splits f p
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
B : ℝ≥0
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ ↑B
x : ℝ≥0
hx : x ∈ Multiset.map (↑↑nnnormHom) s
⊢ x ≤ B
case intro.intro.intro.intro.intro
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : Monic p
h2 : Splits f p
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
B : ℝ≥0
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ ↑B
⊢ prod (Multiset.map (↑↑nnnormHom) s) ≤ B ^ (natDegree (map f p) - i)
refine' (prod_le_pow_card _ B fun x hx => _).trans_eq (by rw [card_map, hs.2])
case intro.intro.intro.intro.intro.intro.intro
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : Monic p
h2 : Splits f p
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
B : ℝ≥0
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ ↑B
z : K
hz : z ∈ s
hx : ↑↑nnnormHom z ∈ Multiset.map (↑↑nnnormHom) s
⊢ ↑↑nnnormHom z ≤ B
case intro.intro.intro.intro.intro
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : Monic p
h2 : Splits f p
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
B : ℝ≥0
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ ↑B
x : ℝ≥0
hx : x ∈ Multiset.map (↑↑nnnormHom) s
⊢ x ≤ B
obtain ⟨z, hz, rfl⟩ := Multiset.mem_map.1 hx
no goals
case intro.intro.intro.intro.intro.intro.intro
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : Monic p
h2 : Splits f p
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
B : ℝ≥0
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ ↑B
z : K
hz : z ∈ s
hx : ↑↑nnnormHom z ∈ Multiset.map (↑↑nnnormHom) s
⊢ ↑↑nnnormHom z ≤ B
exact h3 z (mem_of_le hs.1 hz)
case inl
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : B < 0
⊢ ‖if 0 = i then 1 else 0‖ ≤ ↑(Nat.choose 0 i)
case inl
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : B < 0
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree p - i) * ↑(Nat.choose (natDegree p) i)
rw [eq_one_of_roots_le hB h1 h2 h3, Polynomial.map_one, natDegree_one, zero_tsub, pow_zero,
  one_mul, coeff_one]
case inl.inl
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : B < 0
h✝ : 0 = i
⊢ 1 ≤ Nat.choose 0 i
case inl
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : B < 0
⊢ ‖if 0 = i then 1 else 0‖ ≤ ↑(Nat.choose 0 i)
split_ifs <;> norm_num [h]
no goals
case inl.inl
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : B < 0
h✝ : 0 = i
⊢ 1 ≤ Nat.choose 0 i
simp [‹0 = i›]
case inr.inl
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : natDegree (map f p) < i
⊢ 0 ≤ B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
case inr.inl
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : natDegree (map f p) < i
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
rw [coeff_eq_zero_of_natDegree_lt hi, norm_zero]
no goals
case inr.inl
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : natDegree (map f p) < i
⊢ 0 ≤ B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
positivity
no goals
case inr.inr
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
⊢ ↑card (Multiset.map (fun x => ‖x‖) (Multiset.map prod (powersetLen (natDegree (map f p) - i) (roots (map f p))))) •
      ?m.198217 ≤
    B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
rw [Multiset.map_map, card_map, card_powersetLen, ← natDegree_eq_card_roots' h2,
  Nat.choose_symm hi, mul_comm, nsmul_eq_mul]
no goals
α : Type ?u.183469
R : Type ?u.183472
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : Monic p
h2 : Splits f p
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
B : ℝ≥0
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ ↑B
⊢ B ^ ↑card (Multiset.map (↑↑nnnormHom) s) = B ^ (natDegree (map f p) - i)
rw [card_map, hs.2]