awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
⊢ 0 ≤ B

Tactic:
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 : ℝ
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
lift : ∀ (B : ℝ≥0) (h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ (↑B : ℝ)), ‖s.prod‖ ≤ (↑B : ℝ) ^ ((map f p).natDegree - i)
⊢ ‖s.prod‖ ≤ B ^ ((map f p).natDegree - i)

Tactic:
lift B to ℝ≥0 using 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
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 : prod (Multiset.map (⇑(↑nnnormHom : K →* ℝ≥0) : (a : K) → ℝ≥0) s) ≤ B ^ ((map f p).natDegree - i)
⊢ ‖s.prod‖ ≤ (↑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]

Premises used: MonoidHom.coe_coe, coe_nnnorm, NNReal.coe_pow, nnnormHom_apply, MonoidHom.map_multiset_prod, NNReal.coe_le_coe
-- 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
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)
rw₁ rw₂ : B ^ ((map f p).natDegree - i) = B ^ ((map f p).natDegree - i)
⊢ B ^ card (α := ℝ≥0) (Multiset.map (⇑(↑nnnormHom : K →* ℝ≥0) : (a : K) → ℝ≥0) s) = B ^ ((map f p).natDegree - i)

Tactic:
rw [card_map, hs.2]

Premises used: And.right, 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
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 : ℝ)
refine :
  ∀ (x : ℝ≥0) (hx : Membership.mem (γ := Multiset ℝ≥0) (Multiset.map (⇑(↑nnnormHom : K →* ℝ≥0) : (a : K) → ℝ≥0) s) x),
    x ≤ B
⊢ prod (Multiset.map (⇑(↑nnnormHom : K →* ℝ≥0) : (a : K) → ℝ≥0) s) ≤ B ^ ((map f p).natDegree - i)

Tactic:
refine (prod_le_pow_card _ B fun x hx => ?_).trans_eq (by rw [card_map, hs.2])

Premises used: LE.le.trans_eq, Multiset.prod_le_pow_card
-- 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
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
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
⊢ x ≤ B

Tactic:
obtain ⟨z, hz, rfl⟩ := Multiset.mem_map.1 hx

Premises used: Multiset.mem_map, Iff.mp, 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
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 : ℝ)
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:
h3 z (mem_of_le hs.1 hz)

Premises used: Multiset.mem_of_le, And.left, NNReal.toReal
-- 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
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 : ℝ)
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:
exact h3 z (mem_of_le hs.1 hz)

Premises used: Multiset.mem_of_le, And.left
-- Module: Mathlib.Topology.Algebra.Polynomial
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)) : ℝ)
inr : ∀ (hB : B < 0), ‖(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)) : ℝ)

Tactic:
obtain hB | hB := le_or_gt 0 B

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Polynomial
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
inl : B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
⊢ ‖(map f p).coeff i‖ ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)

Tactic:
apply (coeff_le_of_roots_le i h1 h2 h4).trans

Premises used: Polynomial.coeff_le_of_roots_le, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Polynomial
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 : B ≤ max B 1
⊢ B ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.Polynomial
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 ≤ max B 1

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.Topology.Algebra.Polynomial
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
hbc₁ : p.natDegree - i ≤ d
⊢ max B 1 ^ (p.natDegree - i) * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ d * (↑(p.natDegree.choose i) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.Polynomial
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
⊢ 1 ≤ max B 1

Tactic:
apply le_max_right

Premises used: le_max_right
-- Module: Mathlib.Topology.Algebra.Polynomial
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
⊢ p.natDegree - i ≤ d

Tactic:
le_trans (Nat.sub_le _ _) h3

Premises used: Nat.sub_le, le_trans
-- Module: Mathlib.Topology.Algebra.Polynomial
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
⊢ p.natDegree - i ≤ d

Tactic:
exact le_trans (Nat.sub_le _ _) h3

Premises used: Nat.sub_le, le_trans
-- Module: Mathlib.Topology.Algebra.Polynomial
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 : p.natDegree.choose i ≤ d.choose (d / 2)
⊢ max B 1 ^ d * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.Polynomial
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
⊢ p.natDegree.choose i ≤ d.choose (d / 2)

Tactic:
(i.choose_mono h3).trans (i.choose_le_middle d)

Premises used: Nat.choose_mono, Nat.choose_le_middle, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Polynomial
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
⊢ p.natDegree.choose i ≤ d.choose (d / 2)

Tactic:
exact (i.choose_mono h3).trans (i.choose_le_middle d)

Premises used: Nat.choose_mono, Nat.choose_le_middle, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Polynomial
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) : ℝ)
_₂ : max B 1 ^ d * (↑(p.natDegree.choose i) : ℝ) ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
⊢ B ^ (p.natDegree - i) * (↑(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)

Premises used: Nat.choose, HSub.hSub, HDiv.hDiv, Max.max, Polynomial.natDegree, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Polynomial
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) ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)
⊢ ‖(map f p).coeff i‖ ≤ max B 1 ^ d * (↑(d.choose (d / 2)) : ℝ)

Tactic:
rw [eq_one_of_roots_le hB h1 h2 h4, Polynomial.map_one, coeff_one]

Premises used: Polynomial.map_one, Polynomial.coeff_one, Polynomial.eq_one_of_roots_le
-- Module: Mathlib.Topology.Algebra.Polynomial
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)) : ℝ)

Tactic:
le_trans ?_ (one_le_mul_of_one_le_of_one_le (one_le_pow₀ (le_max_right B 1)) ?_)

Premises used: le_max_right, one_le_pow₀, OfNat.ofNat, one_le_mul_of_one_le_of_one_le, le_trans
-- Module: Mathlib.Topology.Algebra.Polynomial
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
inr₁ : LE.le (α := ℝ) 1 (↑(d.choose (d / 2)) : ℝ)
⊢ norm.{u_4} (E := K) (if i = 0 then 1 else 0) ≤ max B 1 ^ d * (↑(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)) ?_)

Premises used: le_max_right, one_le_pow₀, OfNat.ofNat, one_le_mul_of_one_le_of_one_le, le_trans
-- Module: Mathlib.Topology.Algebra.Polynomial
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
neg : ¬i = 0 → norm.{u_4} (E := K) 0 ≤ 1
⊢ norm.{u_4} (E := K) (if i = 0 then 1 else 0) ≤ 1

Tactic:
split_ifs
-- Module: Mathlib.Topology.Algebra.Polynomial
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
h : i = 0
⊢ norm.{u_4} (E := K) 1 ≤ 1

Tactic:
norm_num
-- Module: Mathlib.Topology.Algebra.Polynomial
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
h : ¬i = 0
⊢ norm.{u_4} (E := K) 0 ≤ 1

Tactic:
norm_num
-- Module: Mathlib.Topology.Algebra.Polynomial
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
⊢ LE.le (α := ℝ) 1 (↑(d.choose (d / 2)) : ℝ)

Tactic:
mod_cast Nat.succ_le_iff.mpr (Nat.choose_pos (d.div_le_self 2))

Premises used: Iff.mpr, Nat.choose, congrArg, cast, HDiv.hDiv, Nat.div_le_self, Nat.cast_le._simp_1, LE.le, Nat.cast, Nat.choose_pos, congrFun', OfNat.ofNat, Eq.symm, Nat.succ_le_iff, Nat.cast_one, Eq.trans
-- Module: Mathlib.Topology.Algebra.Polynomial
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
⊢ LE.le (α := ℝ) 1 (↑(d.choose (d / 2)) : ℝ)

Tactic:
exact mod_cast Nat.succ_le_iff.mpr (Nat.choose_pos (d.div_le_self 2))

Premises used: Iff.mpr, Nat.div_le_self, Nat.choose_pos, OfNat.ofNat, Nat.succ_le_iff
-- Module: Mathlib.Topology.Algebra.PontryaginDual
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)

Tactic:
fun n x ↦ ⟨?_, fun hx ↦ ⟨Complex.arg x, hx, Circle.exp_arg x⟩⟩

Premises used: Circle.exp_arg, Complex.arg, And.intro, Iff.intro, Exists.intro, Subtype.val
-- Module: Mathlib.Topology.Algebra.PontryaginDual
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)}
refine : ∀ (n : ℕ), ∀ x ∈ Vn n, |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ ∀ (n : ℕ) (x : Circle), 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⟩⟩
-- Module: Mathlib.Topology.Algebra.PontryaginDual
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)
⊢ |t| < Real.pi

Tactic:
have ht' := ht.trans_le (div_le_self Real.pi_nonneg (one_le_pow₀ one_le_two))
-- Module: Mathlib.Topology.Algebra.PontryaginDual
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)
ht' : |t| < Real.pi
rwa rwa₁ rwa₂ rwa₃ : |t| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ |Complex.arg (↑((Circle.exp : (a : ℝ) → Circle) t) : ℂ)| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)

Tactic:
rwa [Circle.arg_exp (neg_lt_of_abs_lt ht') (lt_of_abs_lt ht').le]

Premises used: LT.lt.le, neg_lt_of_abs_lt, Circle.arg_exp, lt_of_abs_lt
-- Module: Mathlib.Topology.Algebra.PontryaginDual
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)

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]
-- Module: Mathlib.Topology.Algebra.PontryaginDual
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)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ LocallyCompactSpace.{u_5} (PontryaginDual H)

Tactic:
ContinuousMonoidHom.locallyCompactSpace_of_hasBasis Vn ?_ ?_

Premises used: PontryaginDual, ContinuousMonoidHom.locallyCompactSpace_of_hasBasis
-- Module: Mathlib.Topology.Algebra.PontryaginDual
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)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
refine_1 : ∀ {n : ℕ} {x : Circle}, x ∈ Vn n → x * x ∈ Vn n → x ∈ Vn (n + 1)
refine_2 : Filter.HasBasis (nhds 1) (fun (x : ℕ) ↦ True) Vn
⊢ LocallyCompactSpace.{u_5} (PontryaginDual H)

Tactic:
refine ContinuousMonoidHom.locallyCompactSpace_of_hasBasis Vn ?_ ?_

Premises used: ContinuousMonoidHom.locallyCompactSpace_of_hasBasis
-- Module: Mathlib.Topology.Algebra.PontryaginDual
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)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
n : ℕ
x : Circle
h1 : x ∈ Vn n
h2 : x * x ∈ Vn n
refine_1 :
  ∀ (h1 : |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1))
    (h2 : |(↑(x * x) : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)),
    |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1 + 1)
⊢ x ∈ Vn (n + 1)

Tactic:
rw [hVn] at h1 h2 ⊢
-- Module: Mathlib.Topology.Algebra.PontryaginDual
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)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
n : ℕ
x : Circle
h1 : |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
h2 : |(↑(x * x) : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
refine_1 :
  ∀ (h2 : |((↑x : ℂ) * (↑x : ℂ)).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)),
    (↑x : ℂ).arg + (↑x : ℂ).arg ∈ Set.Ioc (-Real.pi) Real.pi
⊢ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1 + 1)

Tactic:
rwa [Circle.coe_mul, Complex.arg_mul x.coe_ne_zero x.coe_ne_zero,
      ← two_mul, abs_mul, abs_two, ← lt_div_iff₀' two_pos, div_div, ← pow_succ] at h2

Premises used: lt_div_iff₀', pow_succ, abs_mul, two_mul, Circle.coe_mul, Circle.coe_ne_zero, Complex.arg_mul, div_div, abs_two