awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst : Semiring R
inst_1 : Ring S
inst_2 : Field k
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst_5 : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p : R[X]
a : R
hd : 0 < p.degree
ihp :
  ∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)),
    Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop
hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ Tendsto.{u_4, u_3} (β := k)
    (fun (x : α) ↦ abv (eval₂ f (z x) (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])))) l atTop

Tactic:
.atTop_of_add_const (abv (-f a)) ?_

Premises used: Filter.Tendsto.atTop_of_add_const, DFunLike.coe, Neg.neg
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst : Semiring R
inst_1 : Ring S
inst_2 : Field k
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst_5 : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p : R[X]
a : R
hd : 0 < p.degree
ihp :
  ∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)),
    Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop
hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
refine_3 :
  Tendsto.{u_4, u_3} (β := k)
    (fun (x : α) ↦
      abv (eval₂ f (z x) (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))) + abv (-(f : (a : R) → S) a))
    l atTop
⊢ Tendsto.{u_4, u_3} (β := k)
    (fun (x : α) ↦ abv (eval₂ f (z x) (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])))) l atTop

Tactic:
refine .atTop_of_add_const (abv (-f a)) ?_
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst : Semiring R
inst_1 : Ring S
inst_2 : Field k
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst_5 : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p : R[X]
a : R
hd : 0 < p.degree
ihp :
  ∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)),
    Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop
hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ Tendsto.{u_4, u_3} (β := k)
    (fun (x : α) ↦
      abv (eval₂ f (z x) (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))) + abv (-(f : (a : R) → S) a))
    l atTop

Tactic:
tendsto_atTop_mono (fun _ => abv_add abv _ _) ?_

Premises used: Polynomial.C, Filter.tendsto_atTop_mono, Polynomial.eval₂, HAdd.hAdd, IsAbsoluteValue.abv_add, DFunLike.coe, Neg.neg
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst : Semiring R
inst_1 : Ring S
inst_2 : Field k
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst_5 : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p : R[X]
a : R
hd : 0 < p.degree
ihp :
  ∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)),
    Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop
hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
refine_3 :
  Tendsto.{u_4, u_3} (β := k)
    (fun (x : α) ↦
      abv
        (HAdd.hAdd (β := S) (eval₂ f (z x) (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])))
          (-(f : (a : R) → S) a : S)))
    l atTop
⊢ Tendsto.{u_4, u_3} (β := k)
    (fun (x : α) ↦
      abv (eval₂ f (z x) (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))) + abv (-(f : (a : R) → S) a))
    l atTop

Tactic:
refine tendsto_atTop_mono (fun _ => abv_add abv _ _) ?_

Premises used: Filter.tendsto_atTop_mono, IsAbsoluteValue.abv_add
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst : Semiring R
inst_1 : Ring S
inst_2 : Field k
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst_5 : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p : R[X]
a : R
hd : 0 < p.degree
ihp :
  ∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)),
    Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop
hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ Tendsto.{u_4, u_3} (β := k)
    (fun (x : α) ↦
      abv
        (HAdd.hAdd (β := S) (eval₂ f (z x) (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])))
          (-(f : (a : R) → S) a : S)))
    l atTop

Tactic:
simpa using ihp hf
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
k : Type u_2
α : Type u_3
inst : Ring R
inst_1 : Field k
inst_2 : LinearOrder k
inst_3 : IsStrictOrderedRing k
abv : R → k
inst_4 : IsAbsoluteValue abv
p : R[X]
h : 0 < p.degree
l : Filter α
z : α → R
hz : Tendsto (abv ∘ z) l atTop
apply : Ne (α := R) ((RingHom.id R : (a : R) → R) p.leadingCoeff : R) (0 : R)
⊢ Tendsto.{u_3, u_2} (β := k) (fun (x : α) ↦ abv (eval (z x) p)) l atTop

Tactic:
apply tendsto_abv_eval₂_atTop _ _ _ h _ hz

Premises used: Polynomial.tendsto_abv_eval₂_atTop
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
k : Type u_2
α : Type u_3
inst : Ring R
inst_1 : Field k
inst_2 : LinearOrder k
inst_3 : IsStrictOrderedRing k
abv : R → k
inst_4 : IsAbsoluteValue abv
p : R[X]
h : 0 < p.degree
l : Filter α
z : α → R
hz : Tendsto (abv ∘ z) l atTop
⊢ Ne (α := R) ((RingHom.id R : (a : R) → R) p.leadingCoeff : R) (0 : R)

Tactic:
mt leadingCoeff_eq_zero.1 (ne_zero_of_degree_gt h)

Premises used: Polynomial.ne_zero_of_degree_gt, mt, Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
k : Type u_2
α : Type u_3
inst : Ring R
inst_1 : Field k
inst_2 : LinearOrder k
inst_3 : IsStrictOrderedRing k
abv : R → k
inst_4 : IsAbsoluteValue abv
p : R[X]
h : 0 < p.degree
l : Filter α
z : α → R
hz : Tendsto (abv ∘ z) l atTop
⊢ Ne (α := R) ((RingHom.id R : (a : R) → R) p.leadingCoeff : R) (0 : R)

Tactic:
exact mt leadingCoeff_eq_zero.1 (ne_zero_of_degree_gt h)

Premises used: Polynomial.ne_zero_of_degree_gt, mt, Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
A : Type u_2
k : Type u_3
α : Type u_4
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Field k
inst_4 : LinearOrder k
inst_5 : IsStrictOrderedRing k
abv : A → k
inst_6 : IsAbsoluteValue abv
p : R[X]
hd : 0 < p.degree
h₀ : Ne.{u_2 + 1} (α := A) ((algebraMap R A : (a : R) → A) p.leadingCoeff : A) (0 : A)
l : Filter α
z : α → A
hz : Tendsto (abv ∘ z) l atTop
⊢ Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv ((aeval (z x) : (a : R[X]) → A) p)) l atTop

Tactic:
tendsto_abv_eval₂_atTop _ abv p hd h₀ hz

Premises used: Polynomial.tendsto_abv_eval₂_atTop, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
α : Type u_1
R : Type u_2
inst : NormedRing R
inst_1 : IsAbsoluteValue.{0, u_2} (R := R) norm
p : R[X]
h : 0 < p.degree
l : Filter α
z : α → R
hz : Tendsto (β := ℝ) (fun (x : α) ↦ ‖z x‖) l atTop
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖eval (z x) p‖) l atTop

Tactic:
p.tendsto_abv_atTop norm h hz

Premises used: Norm.norm, Polynomial.tendsto_abv_atTop
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : IsAbsoluteValue.{0, u_2} (R := R) norm
inst_2 : ProperSpace R
p : R[X]
hp0 : ¬0 < p.degree
rw :
  ∀ (y : R),
    norm.{u_2} (E := R) (eval (coeff ((C : (a : R) → R[X]) (p.coeff 0)) 0) ((C : (a : R) → R[X]) (p.coeff 0))) ≤
      ‖eval y ((C : (a : R) → R[X]) (p.coeff 0))‖
⊢ ∀ (y : R), ‖eval (p.coeff 0) p‖ ≤ ‖eval y p‖

Tactic:
rw [eq_C_of_degree_le_zero (le_of_not_gt hp0)]

Premises used: le_of_not_gt, Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : IsAbsoluteValue.{0, u_2} (R := R) norm
inst_2 : ProperSpace R
p : R[X]
hp0 : ¬0 < p.degree
⊢ ∀ (y : R),
    norm.{u_2} (E := R) (eval (coeff ((C : (a : R) → R[X]) (p.coeff 0)) 0) ((C : (a : R) → R[X]) (p.coeff 0))) ≤
      ‖eval y ((C : (a : R) → R[X]) (p.coeff 0))‖

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : IsAbsoluteValue.{0, u_2} (R := R) norm
inst_2 : ProperSpace R
p : R[X]
h : 0 < p.degree
⊢ Continuous (Y := R) fun (x : R) ↦ eval x p

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : IsAbsoluteValue.{0, u_2} (R := R) norm
inst_2 : ProperSpace R
p : R[X]
h : 0 < p.degree
rw : Tendsto (β := ℝ) (fun (x : R) ↦ ‖eval x p‖) (Bornology.cobounded R) atTop
⊢ Tendsto (fun (x : R) ↦ eval x p) (cocompact R) (cocompact R)

Tactic:
rw [← Metric.cobounded_eq_cocompact, ← tendsto_norm_atTop_iff_cobounded]

Premises used: Metric.cobounded_eq_cocompact, tendsto_norm_atTop_iff_cobounded
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : IsAbsoluteValue.{0, u_2} (R := R) norm
inst_2 : ProperSpace R
p : R[X]
h : 0 < p.degree
⊢ Tendsto (β := ℝ) (fun (x : R) ↦ ‖eval x p‖) (Bornology.cobounded R) atTop

Tactic:
p.tendsto_norm_atTop h tendsto_norm_cobounded_atTop

Premises used: Polynomial.tendsto_norm_atTop, tendsto_norm_cobounded_atTop
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : IsAbsoluteValue.{0, u_2} (R := R) norm
inst_2 : ProperSpace R
p : R[X]
h : 0 < p.degree
⊢ Tendsto (β := ℝ) (fun (x : R) ↦ ‖eval x p‖) (Bornology.cobounded R) atTop

Tactic:
exact p.tendsto_norm_atTop h tendsto_norm_cobounded_atTop

Premises used: Polynomial.tendsto_norm_atTop, tendsto_norm_cobounded_atTop
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : IsAbsoluteValue.{0, u_2} (R := R) norm
inst_2 : ProperSpace R
p : R[X]
inl : ∀ (h : p.degree ≤ 0), IsClosedMap (Y := R) fun (x : R) ↦ eval x p
inr : ∀ (h : 0 < p.degree), IsClosedMap (Y := R) fun (x : R) ↦ eval x p
⊢ IsClosedMap (Y := R) fun (x : R) ↦ eval x p

Tactic:
obtain h | h := le_or_gt p.degree 0

Premises used: Polynomial.degree, le_or_gt, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : IsAbsoluteValue.{0, u_2} (R := R) norm
inst_2 : ProperSpace R
p : R[X]
h : p.degree ≤ 0
inl : IsClosedMap (Y := R) fun (x : R) ↦ eval x ((C : (a : R) → R[X]) (p.coeff 0))
⊢ IsClosedMap (Y := R) fun (x : R) ↦ eval x p

Tactic:
rw [degree_le_zero_iff.mp h]

Premises used: Iff.mp, Polynomial.degree_le_zero_iff
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : IsAbsoluteValue.{0, u_2} (R := R) norm
inst_2 : ProperSpace R
p : R[X]
h : p.degree ≤ 0
⊢ IsClosedMap (Y := R) fun (x : R) ↦ eval x ((C : (a : R) → R[X]) (p.coeff 0))

Tactic:
simpa using isClosedMap_const

Premises used: isClosedMap_const
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : IsAbsoluteValue.{0, u_2} (R := R) norm
inst_2 : ProperSpace R
p : R[X]
h : 0 < p.degree
⊢ IsClosedMap (Y := R) fun (x : R) ↦ eval x p

Tactic:
(p.isProperMap_eval h).isClosedMap

Premises used: IsProperMap.isClosedMap, Polynomial.isProperMap_eval
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : IsAbsoluteValue.{0, u_2} (R := R) norm
inst_2 : ProperSpace R
p : R[X]
h : 0 < p.degree
⊢ IsClosedMap (Y := R) fun (x : R) ↦ eval x p

Tactic:
exact (p.isProperMap_eval h).isClosedMap

Premises used: IsProperMap.isClosedMap, Polynomial.isProperMap_eval
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : IsAbsoluteValue.{0, u_2} (R := R) norm
inst_2 : ProperSpace R
n : ℕ
⊢ IsClosedMap (Y := R) fun (x : R) ↦ x ^ n

Tactic:
simpa [eval_X_pow] using (X ^ n).isClosedMap_eval

Premises used: Polynomial.eval_X_pow, Polynomial.isClosedMap_eval, HPow.hPow, Polynomial.X
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
hB : B < 0
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
contrapose! : ∀ (hB : p.natDegree ≠ 0), 0 ≤ B
⊢ p.natDegree = 0

Tactic:
contrapose! hB
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : p.natDegree ≠ 0
⊢ (map f p).roots.card ≠ 0

Tactic:
rw [← h1.natDegree_map f, Splits.natDegree_eq_card_roots h2] at hB

Premises used: Polynomial.Splits.natDegree_eq_card_roots, Polynomial.Monic.natDegree_map
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : (map f p).roots.card ≠ 0
obtain : ∀ (z : K) (hz : z ∈ (map f p).roots), 0 ≤ B
⊢ 0 ≤ B

Tactic:
obtain ⟨z, hz⟩ := card_pos_iff_exists_mem.mp (zero_lt_iff.mpr hB)

Premises used: Iff.mpr, Iff.mp, zero_lt_iff, Multiset.card_pos_iff_exists_mem
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : (map f p).roots.card ≠ 0
z : K
hz : z ∈ (map f p).roots
⊢ 0 ≤ B

Tactic:
le_trans (norm_nonneg _) (h3 z hz)

Premises used: norm_nonneg, le_trans
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : (map f p).roots.card ≠ 0
z : K
hz : z ∈ (map f p).roots
⊢ 0 ≤ B

Tactic:
exact le_trans (norm_nonneg _) (h3 z hz)

Premises used: norm_nonneg, le_trans
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
inl : ∀ (hB : B < 0), ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ)
inr : ∀ (hB : 0 ≤ B), ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ)
⊢ ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ)

Tactic:
obtain hB | hB := lt_or_ge B 0

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : B < 0
inl : norm.{u_4} (E := K) (if i = 0 then 1 else 0) ≤ (↑(Nat.choose 0 i) : ℝ)
⊢ ‖(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]

Premises used: Polynomial.map_one, Polynomial.coeff_one, Polynomial.eq_one_of_roots_le, pow_zero, Polynomial.natDegree_one, one_mul, zero_tsub
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : B < 0
pos : ∀ (h : i = 0), norm.{u_4} (E := K) 1 ≤ (↑(Nat.choose 0 i) : ℝ)
neg : ∀ (h : ¬i = 0), norm.{u_4} (E := K) 0 ≤ (↑(Nat.choose 0 i) : ℝ)
⊢ norm.{u_4} (E := K) (if i = 0 then 1 else 0) ≤ (↑(Nat.choose 0 i) : ℝ)

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : B < 0
h : i = 0
⊢ norm.{u_4} (E := K) 1 ≤ (↑(Nat.choose 0 i) : ℝ)

Tactic:
simp [h]
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : B < 0
h : ¬i = 0
⊢ norm.{u_4} (E := K) 0 ≤ (↑(Nat.choose 0 i) : ℝ)

Tactic:
simp [h]
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
inr : ‖(map f p).coeff i‖ ≤ B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
⊢ ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ)

Tactic:
rw [← h1.natDegree_map f]

Premises used: Polynomial.Monic.natDegree_map
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
inr :
  ∀ (hi : (map f p).natDegree < i),
    ‖(map f p).coeff i‖ ≤ B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
inr₁ :
  ∀ (hi : i ≤ (map f p).natDegree),
    ‖(map f p).coeff i‖ ≤ B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
⊢ ‖(map f p).coeff i‖ ≤ B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)

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

Premises used: Polynomial.map, lt_or_ge, Polynomial.natDegree
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : (map f p).natDegree < i
inr : 0 ≤ B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose 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]

Premises used: norm_zero, Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
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) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
inr :
  ‖(map f p).roots.esymm ((map f p).natDegree - i)‖ ≤
    B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
⊢ ‖(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 h2 hi, (h1.map _).leadingCoeff,
    one_mul, norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul]

Premises used: one_pow, norm_pow, NormOneClass.norm_one, norm_mul, norm_neg, Polynomial.coeff_eq_esymm_roots_of_splits, Polynomial.Monic.leadingCoeff, Polynomial.Monic.map, one_mul
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
inr :
  card (α := ℝ)
        (Multiset.map (fun (x : K) ↦ ‖x‖)
          (Multiset.map prod (powersetCard ((map f p).natDegree - i) (map f p).roots))) •
      B ^ ((map f p).natDegree - i) ≤
    B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
apply : ℝ
apply₁ :
  ∀ (r : ℝ)
    (hr :
      Membership.mem (γ := Multiset ℝ)
        (Multiset.map (fun (x : K) ↦ ‖x‖) (Multiset.map prod (powersetCard ((map f p).natDegree - i) (map f p).roots)))
        r),
    r ≤ B ^ ((map f p).natDegree - i)
⊢ ‖(map f p).roots.esymm ((map f p).natDegree - i)‖ ≤
    B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)

Tactic:
apply ((norm_multiset_sum_le _).trans <| sum_le_card_nsmul _ _ fun r hr => _).trans

Premises used: norm_multiset_sum_le, Multiset.sum_le_card_nsmul, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
inr :
  card (α := ℝ) (Multiset.map ((fun (x : K) ↦ ‖x‖) ∘ prod) (powersetCard ((map f p).natDegree - i) (map f p).roots)) •
      B ^ ((map f p).natDegree - i) ≤
    B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
inr₁ :
  (powersetCard ((map f p).natDegree - i) (map f p).roots).card • B ^ ((map f p).natDegree - i) ≤
    B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
inr₂ :
  (map f p).roots.card.choose ((map f p).natDegree - i) • B ^ ((map f p).natDegree - i) ≤
    B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
inr₃ :
  (map f p).natDegree.choose ((map f p).natDegree - i) • B ^ ((map f p).natDegree - i) ≤
    B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
inr₄ :
  (map f p).natDegree.choose i • B ^ ((map f p).natDegree - i) ≤
    B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
inr₅ :
  (map f p).natDegree.choose i • B ^ ((map f p).natDegree - i) ≤
    (↑((map f p).natDegree.choose i) : ℝ) * B ^ ((map f p).natDegree - i)
inr₆ :
  (↑((map f p).natDegree.choose i) : ℝ) * B ^ ((map f p).natDegree - i) ≤
    (↑((map f p).natDegree.choose i) : ℝ) * B ^ ((map f p).natDegree - i)
inr₇ : ℝ
inr₈ :
  (↑((map f p).natDegree.choose i) : ℝ) * B ^ ((map f p).natDegree - i) ≤
    (↑((map f p).natDegree.choose i) : ℝ) * B ^ ((map f p).natDegree - i)
inr₉ : ℝ
⊢ card (α := ℝ)
        (Multiset.map (fun (x : K) ↦ ‖x‖)
          (Multiset.map prod (powersetCard ((map f p).natDegree - i) (map f p).roots))) •
      B ^ ((map f p).natDegree - i) ≤
    B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)

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

Premises used: Multiset.card_powersetCard, Nat.choose_symm, Polynomial.Splits.natDegree_eq_card_roots, mul_comm, nsmul_eq_mul, Multiset.map_map, Multiset.card_map
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
r : ℝ
hr :
  Membership.mem (γ := Multiset ℝ)
    (Multiset.map (fun (x : K) ↦ ‖x‖) (Multiset.map prod (powersetCard ((map f p).natDegree - i) (map f p).roots))) r
⊢ ∃ (a : K), (∃ a_1 ∈ powersetCard ((map f p).natDegree - i) (map f p).roots, a_1.prod = a) ∧ ‖a‖ = r

Tactic:
simp_rw [Multiset.mem_map] at hr

Premises used: Multiset.mem_map
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
r : ℝ
hr : ∃ (a : K), (∃ a_1 ∈ powersetCard ((map f p).natDegree - i) (map f p).roots, a_1.prod = a) ∧ ‖a‖ = r
obtain :
  ∀ (s : Multiset K) (hs : s ∈ powersetCard ((map f p).natDegree - i) (map f p).roots),
    ‖s.prod‖ ≤ B ^ ((map f p).natDegree - i)
⊢ r ≤ B ^ ((map f p).natDegree - i)

Tactic:
obtain ⟨_, ⟨s, hs, rfl⟩, rfl⟩ := hr

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
F : Type u_3
K : Type u_4
inst : CommRing F
inst_1 : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ∈ powersetCard ((map f p).natDegree - i) (map f p).roots
⊢ s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i

Tactic:
rw [mem_powersetCard] at hs

Premises used: Multiset.mem_powersetCard