[GOAL]
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
p✝ : R[X]
inst✝ : Semiring S
p : S[X]
f : S →+* R
⊢ Continuous fun x => eval₂ f x p
[PROOFSTEP]
simp only [eval₂_eq_sum, Finsupp.sum]
[GOAL]
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
p✝ : R[X]
inst✝ : Semiring S
p : S[X]
f : S →+* R
⊢ Continuous fun x => sum p fun e a => ↑f a * x ^ e
[PROOFSTEP]
exact continuous_finset_sum _ fun c _ => continuous_const.mul (continuous_pow _)
[GOAL]
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < degree p
hf : ↑f (leadingCoeff p) ≠ 0
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop
[PROOFSTEP]
revert hf
[GOAL]
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < degree p
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ↑f (leadingCoeff p) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop
[PROOFSTEP]
refine' degree_pos_induction_on p hd _ _ _
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < degree p
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {a : R}, a ≠ 0 → ↑f (leadingCoeff (↑C a * X)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (↑C a * X))) l atTop
[PROOFSTEP]
clear hd p
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < degree p
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]},
    0 < degree p →
      (↑f (leadingCoeff p) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) →
        ↑f (leadingCoeff (p * X)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (p * X))) l atTop
[PROOFSTEP]
clear hd p
[GOAL]
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < degree p
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]} {a : R},
    0 < degree p →
      (↑f (leadingCoeff p) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) →
        ↑f (leadingCoeff (p + ↑C a)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (p + ↑C a))) l atTop
[PROOFSTEP]
clear hd p
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {a : R}, a ≠ 0 → ↑f (leadingCoeff (↑C a * X)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (↑C a * X))) l atTop
[PROOFSTEP]
rintro _ - hc
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
a✝ : R
hc : ↑f (leadingCoeff (↑C a✝ * X)) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (↑C a✝ * X))) l atTop
[PROOFSTEP]
rw [leadingCoeff_mul_X, leadingCoeff_C] at hc 
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
a✝ : R
hc : ↑f a✝ ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (↑C a✝ * X))) l atTop
[PROOFSTEP]
simpa [abv_mul abv] using hz.const_mul_atTop ((abv_pos abv).2 hc)
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]},
    0 < degree p →
      (↑f (leadingCoeff p) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) →
        ↑f (leadingCoeff (p * X)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (p * X))) l atTop
[PROOFSTEP]
intro _ _ ihp hf
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a✝ : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff (p✝ * X)) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ * X))) l atTop
[PROOFSTEP]
rw [leadingCoeff_mul_X] at hf 
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a✝ : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff p✝) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ * X))) l atTop
[PROOFSTEP]
simpa [abv_mul abv] using (ihp hf).atTop_mul_atTop hz
[GOAL]
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]} {a : R},
    0 < degree p →
      (↑f (leadingCoeff p) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) →
        ↑f (leadingCoeff (p + ↑C a)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (p + ↑C a))) l atTop
[PROOFSTEP]
intro _ a hd ihp hf
[GOAL]
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff (p✝ + ↑C a)) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + ↑C a))) l atTop
[PROOFSTEP]
rw [add_comm, leadingCoeff_add_of_degree_lt (degree_C_le.trans_lt hd)] at hf 
[GOAL]
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff p✝) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + ↑C a))) l atTop
[PROOFSTEP]
refine' tendsto_atTop_of_add_const_right (abv (-f a)) _
[GOAL]
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff p✝) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + ↑C a)) + abv (-↑f a)) l atTop
[PROOFSTEP]
refine' tendsto_atTop_mono (fun _ => abv_add abv _ _) _
[GOAL]
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff p✝) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + ↑C a) + -↑f a)) l atTop
[PROOFSTEP]
simpa using ihp hf
[GOAL]
R : Type u_1
k : Type u_2
α : Type u_3
inst✝² : Ring R
inst✝¹ : LinearOrderedField k
abv : R → k
inst✝ : IsAbsoluteValue abv
p : R[X]
h : 0 < degree p
l : Filter α
z : α → R
hz : Tendsto (abv ∘ z) l atTop
⊢ Tendsto (fun x => abv (eval (z x) p)) l atTop
[PROOFSTEP]
apply tendsto_abv_eval₂_atTop _ _ _ h _ hz
[GOAL]
R : Type u_1
k : Type u_2
α : Type u_3
inst✝² : Ring R
inst✝¹ : LinearOrderedField k
abv : R → k
inst✝ : IsAbsoluteValue abv
p : R[X]
h : 0 < degree p
l : Filter α
z : α → R
hz : Tendsto (abv ∘ z) l atTop
⊢ ↑(RingHom.id R) (leadingCoeff p) ≠ 0
[PROOFSTEP]
exact (mt leadingCoeff_eq_zero.1 (ne_zero_of_degree_gt h))
[GOAL]
α : Type u_1
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
hp0 : ¬0 < degree p
⊢ ∀ (y : R), ‖eval (coeff p 0) p‖ ≤ ‖eval y p‖
[PROOFSTEP]
rw [eq_C_of_degree_le_zero (le_of_not_gt hp0)]
[GOAL]
α : Type u_1
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
hp0 : ¬0 < degree p
⊢ ∀ (y : R), ‖eval (coeff (↑C (coeff p 0)) 0) (↑C (coeff p 0))‖ ≤ ‖eval y (↑C (coeff p 0))‖
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
hB : B < 0
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
⊢ natDegree p = 0
[PROOFSTEP]
contrapose! hB
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : natDegree p ≠ 0
⊢ 0 ≤ B
[PROOFSTEP]
rw [← h1.natDegree_map f, natDegree_eq_card_roots' h2] at hB 
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : ↑card (roots (map f p)) ≠ 0
⊢ 0 ≤ B
[PROOFSTEP]
obtain ⟨z, hz⟩ := card_pos_iff_exists_mem.mp (zero_lt_iff.mpr hB)
[GOAL]
case intro
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : ↑card (roots (map f p)) ≠ 0
z : K
hz : z ∈ roots (map f p)
⊢ 0 ≤ B
[PROOFSTEP]
exact le_trans (norm_nonneg _) (h3 z hz)
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
obtain hB | hB := lt_or_le B 0
[GOAL]
case inl
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
rw [eq_one_of_roots_le hB h1 h2 h3, Polynomial.map_one, natDegree_one, zero_tsub, pow_zero, one_mul, coeff_one]
[GOAL]
case inl
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
norm_num [h]
[GOAL]
case neg
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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
⊢ ‖0‖ ≤ ↑(Nat.choose 0 i)
[PROOFSTEP]
norm_num [h]
[GOAL]
case pos
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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
[PROOFSTEP]
simp [‹0 = i›]
[GOAL]
case inr
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
rw [← h1.natDegree_map f]
[GOAL]
case inr
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
obtain hi | hi := lt_or_le (map f p).natDegree i
[GOAL]
case inr.inl
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt hi, norm_zero]
[GOAL]
case inr.inl
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
positivity
[GOAL]
case inr.inr
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
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]
[GOAL]
case inr.inr
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
apply ((norm_multiset_sum_le _).trans <| sum_le_card_nsmul _ _ fun r hr => _).trans
[GOAL]
case inr.inr
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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.209879 ≤
    B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
[PROOFSTEP]
rw [Multiset.map_map, card_map, card_powersetLen, ← natDegree_eq_card_roots' h2, Nat.choose_symm hi, mul_comm,
  nsmul_eq_mul]
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
intro r hr
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
simp_rw [Multiset.mem_map] at hr 
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
obtain ⟨_, ⟨s, hs, rfl⟩, rfl⟩ := hr
[GOAL]
case intro.intro.intro.intro
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
rw [mem_powersetLen] at hs 
[GOAL]
case intro.intro.intro.intro
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
lift B to ℝ≥0 using hB
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
rw [← coe_nnnorm, ← NNReal.coe_pow, NNReal.coe_le_coe, ← nnnormHom_apply, ← MonoidHom.coe_coe,
  MonoidHom.map_multiset_prod]
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
refine' (prod_le_pow_card _ B fun x hx => _).trans_eq (by rw [card_map, hs.2])
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
rw [card_map, hs.2]
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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
[PROOFSTEP]
obtain ⟨z, hz, rfl⟩ := Multiset.mem_map.1 hx
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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
[PROOFSTEP]
exact h3 z (mem_of_le hs.1 hz)
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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))
[PROOFSTEP]
obtain hB | hB := le_or_lt 0 B
[GOAL]
case inl
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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))
[PROOFSTEP]
apply (coeff_le_of_roots_le i h1 h2 h4).trans
[GOAL]
case inl
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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))
[PROOFSTEP]
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)
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
gcongr
[GOAL]
case h.hab
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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
[PROOFSTEP]
apply le_max_left
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
gcongr
[GOAL]
case h.ha
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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
[PROOFSTEP]
apply le_max_right
[GOAL]
case h.h
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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
[PROOFSTEP]
exact le_trans (Nat.sub_le _ _) h3
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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))
[PROOFSTEP]
gcongr
[GOAL]
case h.h
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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)
[PROOFSTEP]
exact (i.choose_mono h3).trans (i.choose_le_middle d)
[GOAL]
case inr
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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))
[PROOFSTEP]
rw [eq_one_of_roots_le hB h1 h2 h4, Polynomial.map_one, coeff_one]
[GOAL]
case inr
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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))
[PROOFSTEP]
refine' _root_.trans _ (one_le_mul_of_one_le_of_one_le (one_le_pow_of_one_le (le_max_right B 1) d) _)
[GOAL]
case inr.refine'_1
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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
h✝ : 0 = i
⊢ ‖1‖ ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
case neg
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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
h✝ : ¬0 = i
⊢ ‖0‖ ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
case inr.refine'_2
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
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))
[PROOFSTEP]
exact_mod_cast Nat.succ_le_iff.mpr (Nat.choose_pos (d.div_le_self 2))
