awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
p : R[X]
hd : 0 < p.degree
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) 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) p)) l atTop
have refine_1 : ∀ {a : R},
  a ≠ 0 →
    ∀
      (hf :
        Ne.{u_2 + 1} (α := S)
          ((f : (a : R) → S) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).leadingCoeff : S)
          (0 : S)),
      Tendsto.{u_4, u_3} (β := k)
        (fun (x : α) ↦ abv (eval₂ f (z x) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X))) l
        atTop
Tactic: refine degree_pos_induction_on p hd ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
p : R[X]
hd : 0 < p.degree
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
refine_1 :
  ∀ {a : R},
    a ≠ 0 →
      ∀
        (hf :
          Ne.{u_2 + 1} (α := S)
            ((f : (a : R) → S) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).leadingCoeff : S)
            (0 : S)),
        Tendsto.{u_4, u_3} (β := k)
          (fun (x : α) ↦ abv (eval₂ f (z x) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X))) 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) p)) l atTop
have refine_2 : ∀ {p : R[X]},
  0 < p.degree →
    (∀ (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 * X).leadingCoeff : S) (0 : S)),
        Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) (p * X))) l atTop
Tactic: refine degree_pos_induction_on p hd ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
p : R[X]
hd : 0 < p.degree
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
refine_1 :
  ∀ {a : R},
    a ≠ 0 →
      ∀
        (hf :
          Ne.{u_2 + 1} (α := S)
            ((f : (a : R) → S) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).leadingCoeff : S)
            (0 : S)),
        Tendsto.{u_4, u_3} (β := k)
          (fun (x : α) ↦ abv (eval₂ f (z x) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X))) l
          atTop
refine_2 :
  ∀ {p : R[X]},
    0 < p.degree →
      (∀ (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 * X).leadingCoeff : S) (0 : S)),
          Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) (p * X))) 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) p)) l atTop
have refine_3 : ∀ {p : R[X]} {a : R},
  0 < p.degree →
    (∀ (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) (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).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: refine degree_pos_induction_on p hd ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (hypothesis)
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
a : R
hc :
  Ne.{u_2 + 1} (α := S)
    ((f : (a : R) → S) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).leadingCoeff : S) (0 : S)
⊢ Tendsto.{u_4, u_3} (β := k)
    (fun (x : α) ↦ abv (eval₂ f (z x) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X))) l atTop
have hc₁ : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
Tactic: rw [leadingCoeff_mul_X, leadingCoeff_C] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (hypothesis)
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]
h : 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 * X).leadingCoeff : S) (0 : S)
⊢ Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) (p * X))) l atTop
have hf₁ : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
Tactic: rw [leadingCoeff_mul_X] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (hypothesis)
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) (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).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
have hf₁ : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
Tactic: rw [add_comm, leadingCoeff_add_of_degree_lt (degree_C_le.trans_lt hd)] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
have 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
Tactic: refine .atTop_of_add_const (abv (-f a)) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
have 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
Tactic: refine tendsto_atTop_mono (fun _ => abv_add abv _ _) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
⊢ Tendsto.{u_3, u_2} (β := k) (fun (x : α) ↦ abv (eval (z x) p)) l atTop
have apply : Ne (α := R) ((RingHom.id R : (a : R) → R) p.leadingCoeff : R) (0 : R)
Tactic: apply tendsto_abv_eval₂_atTop _ _ _ h _ hz
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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), ‖eval (p.coeff 0) p‖ ≤ ‖eval y p‖
have 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))‖
Tactic: rw [eq_C_of_degree_le_zero (le_of_not_gt hp0)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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) (cocompact R) (cocompact R)
have rw : Tendsto (β := ℝ) (fun (x : R) ↦ ‖eval x p‖) (Bornology.cobounded R) atTop
Tactic: rw [← Metric.cobounded_eq_cocompact, ← tendsto_norm_atTop_iff_cobounded]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : IsAbsoluteValue.{0, u_2} (R := R) norm
inst_2 : ProperSpace R
p : R[X]
⊢ IsClosedMap (Y := R) fun (x : R) ↦ eval x p
have inl : ∀ (h : p.degree ≤ 0), IsClosedMap (Y := R) fun (x : R) ↦ eval x p
Tactic: obtain h | h := le_or_gt p.degree 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
⊢ IsClosedMap (Y := R) fun (x : R) ↦ eval x p
have inr : ∀ (h : 0 < p.degree), IsClosedMap (Y := R) fun (x : R) ↦ eval x p
Tactic: obtain h | h := le_or_gt p.degree 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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 p
have inl : IsClosedMap (Y := R) fun (x : R) ↦ eval x ((C : (a : R) → R[X]) (p.coeff 0))
Tactic: rw [degree_le_zero_iff.mp h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
⊢ p.natDegree = 0
have contrapose! : ∀ (hB : p.natDegree ≠ 0), 0 ≤ B
Tactic: contrapose! hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (hypothesis)
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
⊢ 0 ≤ B
have hB₁ : (map f p).roots.card ≠ 0
Tactic: rw [← h1.natDegree_map f, Splits.natDegree_eq_card_roots h2] at hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
⊢ 0 ≤ B
have obtain : ∀ (z : K) (hz : z ∈ (map f p).roots), 0 ≤ B
Tactic: obtain ⟨z, hz⟩ := card_pos_iff_exists_mem.mp (zero_lt_iff.mpr hB)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
⊢ ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ)
have inl : ∀ (hB : B < 0), ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ)
Tactic: obtain hB | hB := lt_or_ge B 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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) : ℝ)
⊢ ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ)
have inr : ∀ (hB : 0 ≤ B), ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ)
Tactic: obtain hB | hB := lt_or_ge B 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
⊢ ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ)
have inl : norm.{u_4} (E := K) (if i = 0 then 1 else 0) ≤ (↑(Nat.choose 0 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
⊢ norm.{u_4} (E := K) (if i = 0 then 1 else 0) ≤ (↑(Nat.choose 0 i) : ℝ)
have pos : ∀ (h : i = 0), norm.{u_4} (E := K) 1 ≤ (↑(Nat.choose 0 i) : ℝ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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) : ℝ)
⊢ norm.{u_4} (E := K) (if i = 0 then 1 else 0) ≤ (↑(Nat.choose 0 i) : ℝ)
have neg : ∀ (h : ¬i = 0), norm.{u_4} (E := K) 0 ≤ (↑(Nat.choose 0 i) : ℝ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
⊢ ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ)
have inr : ‖(map f p).coeff i‖ ≤ B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
Tactic: rw [← h1.natDegree_map f]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
⊢ ‖(map f p).coeff i‖ ≤ B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
have inr : ∀ (hi : (map f p).natDegree < 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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) : ℝ)
⊢ ‖(map f p).coeff i‖ ≤ B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
have inr₁ : ∀ (hi : i ≤ (map f p).natDegree),
  ‖(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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
⊢ ‖(map f p).coeff i‖ ≤ B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
have inr : 0 ≤ B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
Tactic: rw [coeff_eq_zero_of_natDegree_lt hi, norm_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
⊢ ‖(map f p).coeff i‖ ≤ B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
have inr : ‖(map f p).roots.esymm ((map f p).natDegree - 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
⊢ ‖(map f p).roots.esymm ((map f p).natDegree - i)‖ ≤
    B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
have 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: apply ((norm_multiset_sum_le _).trans <| sum_le_card_nsmul _ _ fun r hr => _).trans
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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 : ℝ
⊢ ‖(map f p).roots.esymm ((map f p).natDegree - i)‖ ≤
    B ^ ((map f p).natDegree - i) * (↑((map f p).natDegree.choose i) : ℝ)
have 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)
Tactic: apply ((norm_multiset_sum_le _).trans <| sum_le_card_nsmul _ _ fun r hr => _).trans
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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
⊢ 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) : ℝ)
have 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) : ℝ)
Tactic: rw [Multiset.map_map, card_map, card_powersetCard, ← Splits.natDegree_eq_card_roots h2,
      Nat.choose_symm hi, mul_comm, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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) : ℝ)
⊢ 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) : ℝ)
have 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) : ℝ)
Tactic: rw [Multiset.map_map, card_map, card_powersetCard, ← Splits.natDegree_eq_card_roots h2,
      Nat.choose_symm hi, mul_comm, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
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) : ℝ)
⊢ 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) : ℝ)
have 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) : ℝ)
Tactic: rw [Multiset.map_map, card_map, card_powersetCard, ← Splits.natDegree_eq_card_roots h2,
      Nat.choose_symm hi, mul_comm, nsmul_eq_mul]