awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) : ℝ)
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) : ℝ)
⊢ 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).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) : ℝ)
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) : ℝ)
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) : ℝ)
⊢ 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).natDegree.choose 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]
-- 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) : ℝ)
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) : ℝ)
⊢ 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).natDegree.choose i • B ^ ((map f p).natDegree - i) ≤
  (↑((map f p).natDegree.choose i) : ℝ) * B ^ ((map f p).natDegree - 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) : ℝ)
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)
⊢ 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).natDegree.choose i) : ℝ) * B ^ ((map f p).natDegree - i) ≤
  (↑((map f p).natDegree.choose i) : ℝ) * B ^ ((map f p).natDegree - 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 (hypothesis)
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
⊢ r ≤ B ^ ((map f p).natDegree - i)
have hr₁ : ∃ (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
Cleared hypotheses: hr
-- 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
r : ℝ
hr : ∃ (a : K), (∃ a_1 ∈ powersetCard ((map f p).natDegree - i) (map f p).roots, a_1.prod = a) ∧ ‖a‖ = r
⊢ r ≤ B ^ ((map f p).natDegree - i)
have obtain : ∀ (s : Multiset K) (hs : s ∈ powersetCard ((map f p).natDegree - i) (map f p).roots),
  ‖s.prod‖ ≤ B ^ ((map f p).natDegree - i)
Tactic: obtain ⟨_, ⟨s, hs, rfl⟩, rfl⟩ := hr
Cleared hypotheses: r, hr
-- 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 : ℝ
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.prod‖ ≤ B ^ ((map f p).natDegree - i)
have hs₁ : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
Tactic: rw [mem_powersetCard] at hs
Cleared hypotheses: hs
-- 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
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
⊢ ‖s.prod‖ ≤ B ^ ((map f p).natDegree - i)
have lift : ∀ (B : ℝ≥0) (h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ (↑B : ℝ)), ‖s.prod‖ ≤ (↑B : ℝ) ^ ((map f p).natDegree - i)
Tactic: lift B to ℝ≥0 using hB
Cleared hypotheses: B, h3, 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
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ (↑B : ℝ)
⊢ ‖s.prod‖ ≤ (↑B : ℝ) ^ ((map f p).natDegree - i)
have rw : prod (Multiset.map (⇑(↑nnnormHom : K →* ℝ≥0) : (a : K) → ℝ≥0) s) ≤ B ^ ((map f p).natDegree - i)
Tactic: rw [← coe_nnnorm, ← NNReal.coe_pow, NNReal.coe_le_coe, ← nnnormHom_apply, ← MonoidHom.coe_coe,
    MonoidHom.map_multiset_prod]
-- 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
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ (↑B : ℝ)
⊢ B ^ card (α := ℝ≥0) (Multiset.map (⇑(↑nnnormHom : K →* ℝ≥0) : (a : K) → ℝ≥0) s) = B ^ ((map f p).natDegree - i)
have rw : B ^ s.card = B ^ ((map f p).natDegree - i)
Tactic: rw [card_map, hs.2]
-- 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
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ (↑B : ℝ)
rw : B ^ s.card = B ^ ((map f p).natDegree - i)
⊢ B ^ card (α := ℝ≥0) (Multiset.map (⇑(↑nnnormHom : K →* ℝ≥0) : (a : K) → ℝ≥0) s) = B ^ ((map f p).natDegree - i)
have rw₁ : B ^ ((map f p).natDegree - i) = B ^ ((map f p).natDegree - i)
Tactic: rw [card_map, hs.2]
-- 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
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ (↑B : ℝ)
⊢ prod (Multiset.map (⇑(↑nnnormHom : K →* ℝ≥0) : (a : K) → ℝ≥0) s) ≤ B ^ ((map f p).natDegree - i)
have refine : ∀ (x : ℝ≥0) (hx : Membership.mem (γ := Multiset ℝ≥0) (Multiset.map (⇑(↑nnnormHom : K →* ℝ≥0) : (a : K) → ℝ≥0) s) x),
  x ≤ B
Tactic: refine (prod_le_pow_card _ B fun x hx => ?_).trans_eq (by rw [card_map, hs.2])
-- 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
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ (↑B : ℝ)
x : ℝ≥0
hx : Membership.mem (γ := Multiset ℝ≥0) (Multiset.map (⇑(↑nnnormHom : K →* ℝ≥0) : (a : K) → ℝ≥0) s) x
⊢ x ≤ B
have obtain : ∀ (z : K) (hz : z ∈ s)
  (hx :
    Membership.mem (α := ℝ≥0) (γ := Multiset ℝ≥0) (Multiset.map (⇑(↑nnnormHom : K →* ℝ≥0) : (a : K) → ℝ≥0) s)
      ((((↑nnnormHom : K →* ℝ≥0) : K →* ℝ≥0) : (a : K) → ℝ≥0) z : ℝ≥0)),
  (((↑nnnormHom : K →* ℝ≥0) : K →* ℝ≥0) : (a : K) → ℝ≥0) z ≤ B
Tactic: obtain ⟨z, hz, rfl⟩ := Multiset.mem_map.1 hx
Cleared hypotheses: x, hx
-- 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
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
⊢ ‖(map f p).coeff i‖ ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
have inl : ∀ (hB : 0 ≤ B), ‖(map f p).coeff i‖ ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
Tactic: obtain hB | hB := le_or_gt 0 B
-- 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
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
inl : ∀ (hB : 0 ≤ B), ‖(map f p).coeff i‖ ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
⊢ ‖(map f p).coeff i‖ ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
have inr : ∀ (hB : B < 0), ‖(map f p).coeff i‖ ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
Tactic: obtain hB | hB := le_or_gt 0 B
-- 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
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ ‖(map f p).coeff i‖ ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
have inl : B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
Tactic: apply (coeff_le_of_roots_le i h1 h2 h4).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
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ)
have hbc : B ≤ max B 1
Tactic: gcongr
-- 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
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ max B 1 ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ d * (↑(p.natDegree.choose i) : ℝ)
have hbc : 1 ≤ max B 1
Tactic: gcongr
-- 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
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
hbc : 1 ≤ max B 1
⊢ max B 1 ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ d * (↑(p.natDegree.choose i) : ℝ)
have hbc₁ : p.natDegree - i ≤ d
Tactic: gcongr
-- 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
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ max B 1 ^ d * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
have hbc : p.natDegree.choose i ≤ d.choose (d / 2)
Tactic: gcongr
-- 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
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
have _ : B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ)
Tactic: 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)
-- 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
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
_ : B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ)
⊢ B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
have _₁ : max B 1 ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ d * (↑(p.natDegree.choose i) : ℝ)
Tactic: 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)
-- 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
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
_ : B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ)
_₁ : max B 1 ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ d * (↑(p.natDegree.choose i) : ℝ)
⊢ B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
have _₂ : max B 1 ^ d * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
Tactic: 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)
-- 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
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ ‖(map f p).coeff i‖ ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
have inr : norm.{u_4} (E := K) (if i = 0 then 1 else 0) ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
Tactic: rw [eq_one_of_roots_le hB h1 h2 h4, Polynomial.map_one, 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
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ norm.{u_4} (E := K) (if i = 0 then 1 else 0) ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
have inr : norm.{u_4} (E := K) (if i = 0 then 1 else 0) ≤ 1
Tactic: refine le_trans ?_ (one_le_mul_of_one_le_of_one_le (one_le_pow₀ (le_max_right B 1)) ?_)
-- 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
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : B < 0
inr : norm.{u_4} (E := K) (if i = 0 then 1 else 0) ≤ 1
⊢ norm.{u_4} (E := K) (if i = 0 then 1 else 0) ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
have inr₁ : LE.le (α := ℝ) 1 (↑(d.choose (d / 2)) : ℝ)
Tactic: refine le_trans ?_ (one_le_mul_of_one_le_of_one_le (one_le_pow₀ (le_max_right B 1)) ?_)
-- 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
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ norm.{u_4} (E := K) (if i = 0 then 1 else 0) ≤ 1
have pos : i = 0 → norm.{u_4} (E := K) 1 ≤ 1
Tactic: split_ifs
-- 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
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : B < 0
pos : i = 0 → norm.{u_4} (E := K) 1 ≤ 1
⊢ norm.{u_4} (E := K) (if i = 0 then 1 else 0) ≤ 1
have neg : ¬i = 0 → norm.{u_4} (E := K) 0 ≤ 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
⊢ ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
have refine : ∀ (n : ℕ), ∀ x ∈ Vn n, |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
Tactic: refine fun n x ↦ ⟨?_, fun hx ↦ ⟨Complex.arg x, hx, Circle.exp_arg x⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
n : ℕ
t : ℝ
ht : |t| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ |Complex.arg (↑((Circle.exp : (a : ℝ) → Circle) t) : ℂ)| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
have ht' : |t| < Real.pi
Tactic: have ht' := ht.trans_le (div_le_self Real.pi_nonneg (one_le_pow₀ one_le_two))
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
⊢ LocallyCompactSpace.{u_5} (PontryaginDual H)
have hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
Tactic: have hVn : ∀ n x, x ∈ Vn n ↔ |Complex.arg x| < Real.pi / 2 ^ (n + 1) := by
    refine fun n x ↦ ⟨?_, fun hx ↦ ⟨Complex.arg x, hx, Circle.exp_arg x⟩⟩
    rintro ⟨t, ht : |t| < _, rfl⟩
    have ht' := ht.trans_le (div_le_self Real.pi_nonneg (one_le_pow₀ one_le_two))
    rwa [Circle.arg_exp (neg_lt_of_abs_lt ht') (lt_of_abs_lt ht').le]