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

case inr
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ ‖coeff (map f p) i‖ ≤ max B 1 ^ d * ↑(Nat.choose d (d / 2))
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
⊢ ‖coeff (map f p) i‖ ≤ max B 1 ^ d * ↑(Nat.choose d (d / 2))
obtain hB | hB := le_or_lt 0 B
case inl
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ B ^ (natDegree p - i) * ↑(Nat.choose (natDegree p) i) ≤ max B 1 ^ d * ↑(Nat.choose d (d / 2))
case inl
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ ‖coeff (map f p) i‖ ≤ max B 1 ^ d * ↑(Nat.choose d (d / 2))
apply (coeff_le_of_roots_le i h1 h2 h4).trans
no goals
case inl
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ B ^ (natDegree p - i) * ↑(Nat.choose (natDegree p) i) ≤ max B 1 ^ d * ↑(Nat.choose d (d / 2))
calc
  _ ≤ max B 1 ^ (p.natDegree - i) * p.natDegree.choose i := by gcongr; apply le_max_left
  _ ≤ max B 1 ^ d * p.natDegree.choose i := by
    gcongr; apply le_max_right; exact le_trans (Nat.sub_le _ _) h3
  _ ≤ max B 1 ^ d * d.choose (d / 2) := by
    gcongr; exact (i.choose_mono h3).trans (i.choose_le_middle d)
case h.hab
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ B ≤ max B 1
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ B ^ (natDegree p - i) * ↑(Nat.choose (natDegree p) i) ≤ max B 1 ^ (natDegree p - i) * ↑(Nat.choose (natDegree p) i)
gcongr
no goals
case h.hab
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ B ≤ max B 1
apply le_max_left
case h.ha
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ 1 ≤ max B 1

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

case h.h
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ natDegree p - i ≤ d
apply le_max_right
no goals
case h.h
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ natDegree p - i ≤ d
exact le_trans (Nat.sub_le _ _) h3
case h.h
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ Nat.choose (natDegree p) i ≤ Nat.choose d (d / 2)
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ max B 1 ^ d * ↑(Nat.choose (natDegree p) i) ≤ max B 1 ^ d * ↑(Nat.choose d (d / 2))
gcongr
no goals
case h.h
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ Nat.choose (natDegree p) i ≤ Nat.choose d (d / 2)
exact (i.choose_mono h3).trans (i.choose_le_middle d)
case inr
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ ‖if 0 = i then 1 else 0‖ ≤ max B 1 ^ d * ↑(Nat.choose d (d / 2))
case inr
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ ‖coeff (map f p) i‖ ≤ max B 1 ^ d * ↑(Nat.choose d (d / 2))
rw [eq_one_of_roots_le hB h1 h2 h4, Polynomial.map_one, coeff_one]
case inr.refine'_1
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ ‖if 0 = i then 1 else 0‖ ≤ 1

case inr.refine'_2
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ 1 ≤ ↑(Nat.choose d (d / 2))
case inr
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ ‖if 0 = i then 1 else 0‖ ≤ max B 1 ^ d * ↑(Nat.choose d (d / 2))
refine' _root_.trans _
  (one_le_mul_of_one_le_of_one_le (one_le_pow_of_one_le (le_max_right B 1) d) _)
no goals
case inr.refine'_1
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ ‖if 0 = i then 1 else 0‖ ≤ 1
split_ifs <;> norm_num
no goals
case inr.refine'_2
α : Type ?u.202389
R : Type ?u.202392
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ 1 ≤ ↑(Nat.choose d (d / 2))
exact_mod_cast Nat.succ_le_iff.mpr (Nat.choose_pos (d.div_le_self 2))