awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this :
  ∀ (x : Multiset ℂ) (hx : x ∈ S.toFinset),
    LE.le (α := ℝ) (∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
rw :
  HMul.hMul (α := ℝ) (∑ i ∈ S.toFinset, (↑(count i S) : ℝ)) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)) =
    HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
⊢ ∑ x ∈ S.toFinset, HMul.hMul (α := ℝ) (↑(count x S) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)) =
    HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))

Tactic:
rw [← Finset.sum_mul]

Premises used: Finset.sum_mul
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this :
  ∀ (x : Multiset ℂ) (hx : x ∈ S.toFinset),
    LE.le (α := ℝ) (∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
e_a : Eq (α := ℝ) (∑ i ∈ S.toFinset, (↑(count i S) : ℝ)) (↑(p.natDegree.choose n) : ℝ)
⊢ HMul.hMul (α := ℝ) (∑ i ∈ S.toFinset, (↑(count i S) : ℝ)) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)) =
    HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))

Tactic:
congr
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this :
  ∀ (x : Multiset ℂ) (hx : x ∈ S.toFinset),
    LE.le (α := ℝ) (∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
e_a : ∑ x ∈ S.toFinset, count x S = p.natDegree.choose n
⊢ Eq (α := ℝ) (∑ i ∈ S.toFinset, (↑(count i S) : ℝ)) (↑(p.natDegree.choose n) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this :
  ∀ (x : Multiset ℂ) (hx : x ∈ S.toFinset),
    LE.le (α := ℝ) (∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
e_a : p.roots.card.choose (p.natDegree - n) = p.natDegree.choose (p.natDegree - n)
⊢ ∑ x ∈ S.toFinset, count x S = p.natDegree.choose n

Tactic:
simp only [mem_powersetCard, mem_toFinset, imp_self, implies_true, sum_count_eq_card,
        card_powersetCard, S, ← Nat.choose_symm hn]

Premises used: Multiset.sum_count_eq_card, Multiset.mem_powersetCard, Multiset.card_powersetCard, Nat.choose_symm, imp_self, implies_true, Multiset.mem_toFinset
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this :
  ∀ (x : Multiset ℂ) (hx : x ∈ S.toFinset),
    LE.le (α := ℝ) (∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
e_a : p.roots.card = p.natDegree
⊢ p.roots.card.choose (p.natDegree - n) = p.natDegree.choose (p.natDegree - n)

Tactic:
congr
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this :
  ∀ (x : Multiset ℂ) (hx : x ∈ S.toFinset),
    LE.le (α := ℝ) (∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
⊢ p.roots.card = p.natDegree

Tactic:
splits_iff_card_roots.mp <| IsAlgClosed.splits p

Premises used: Polynomial.splits_iff_card_roots, Iff.mp, IsAlgClosed.splits
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this :
  ∀ (x : Multiset ℂ) (hx : x ∈ S.toFinset),
    LE.le (α := ℝ) (∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
⊢ p.roots.card = p.natDegree

Tactic:
exact splits_iff_card_roots.mp <| IsAlgClosed.splits p

Premises used: Polynomial.splits_iff_card_roots, Iff.mp, IsAlgClosed.splits
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this :
  ∀ (x : Multiset ℂ) (hx : x ∈ S.toFinset),
    LE.le (α := ℝ) (∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
calc :
  LE.le (α := ℝ) (∑ x ∈ S.toFinset, (↑(count x S) : ℝ) * ‖x.prod‖)
    (∑ x ∈ S.toFinset, HMul.hMul (α := ℝ) (↑(count x S) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)))
calc₁ :
  ∑ x ∈ S.toFinset, HMul.hMul (α := ℝ) (↑(count x S) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)) =
    HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
⊢ ∑ x ∈ (powersetCard (p.natDegree - n) p.roots).toFinset,
      (↑(count x (powersetCard (p.natDegree - n) p.roots)) : ℝ) * ‖x.prod‖ ≤
    HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))

Tactic:
calc ∑ x ∈ S.toFinset, count x S * ‖x.prod‖
    _ ≤ ∑ x ∈ S.toFinset, count x S * ((p.roots).map (fun a ↦ max 1 ‖a‖)).prod := by
      gcongr with x hx
      rw [Finset.prod_multiset_map_count, Finset.prod_multiset_count, norm_prod]
      simp_rw [norm_pow]
      exact this x hx
    _ = p.natDegree.choose n * (p.roots.map (fun a ↦ 1 ⊔ ‖a‖)).prod := by
      rw [← Finset.sum_mul]
      congr
      norm_cast
      simp only [mem_powersetCard, mem_toFinset, imp_self, implies_true, sum_count_eq_card,
        card_powersetCard, S, ← Nat.choose_symm hn]
      congr
      exact splits_iff_card_roots.mp <| IsAlgClosed.splits p

Premises used: Multiset.toFinset, Norm.norm, Polynomial.roots, Nat.choose, Multiset.map, Multiset.prod, Max.max, Polynomial.natDegree, OfNat.ofNat
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
obtain :
  ∀ (i : ℕ) (hi : p.supNorm = ‖p.coeff i‖), p.supNorm ≤ (↑(p.natDegree.choose (p.natDegree / 2)) : ℝ) * p.mahlerMeasure
⊢ p.supNorm ≤ (↑(p.natDegree.choose (p.natDegree / 2)) : ℝ) * p.mahlerMeasure

Tactic:
obtain ⟨i, hi⟩ := p.exists_eq_supNorm

Premises used: Polynomial.exists_eq_supNorm
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
i : ℕ
hi : p.supNorm = ‖p.coeff i‖
⊢ p.supNorm = ‖p.coeff i‖

Tactic:
hi
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
i : ℕ
hi : p.supNorm = ‖p.coeff i‖
⊢ ‖p.coeff i‖ ≤ (↑(p.natDegree.choose i) : ℝ) * p.mahlerMeasure

Tactic:
p.norm_coeff_le_choose_mul_mahlerMeasure i

Premises used: Polynomial.norm_coeff_le_choose_mul_mahlerMeasure
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
i : ℕ
hi : p.supNorm = ‖p.coeff i‖
⊢ LE.le (α := ℝ) (↑(p.natDegree.choose i) : ℝ) (↑(p.natDegree.choose (p.natDegree / 2)) : ℝ)

Tactic:
exact_mod_cast Nat.choose_le_middle i p.natDegree

Premises used: Nat.choose_le_middle, Polynomial.natDegree
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
i : ℕ
hi : p.supNorm = ‖p.coeff i‖
⊢ p.supNorm ≤ (↑(p.natDegree.choose (p.natDegree / 2)) : ℝ) * p.mahlerMeasure

Tactic:
calc p.supNorm = ‖p.coeff i‖ := hi
    _ ≤ (p.natDegree.choose i) * p.mahlerMeasure := p.norm_coeff_le_choose_mul_mahlerMeasure i
    _ ≤ (p.natDegree.choose (p.natDegree / 2)) * p.mahlerMeasure :=
      mul_le_mul_of_nonneg_right (by exact_mod_cast Nat.choose_le_middle i p.natDegree)
        p.mahlerMeasure_nonneg

Premises used: Nat.choose, Polynomial.mahlerMeasure_nonneg, HDiv.hDiv, Polynomial.coeff, mul_le_mul_of_nonneg_right, Polynomial.mahlerMeasure, Polynomial.supNorm, Polynomial.natDegree, OfNat.ofNat, Polynomial.norm_coeff_le_choose_mul_mahlerMeasure
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
g h : ℂ[X]
hh : 1 ≤ h.mahlerMeasure
hbc : g.mahlerMeasure ≤ (g * h).mahlerMeasure
⊢ (↑(g.natDegree.choose n) : ℝ) * g.mahlerMeasure ≤ (↑(g.natDegree.choose n) : ℝ) * (g * h).mahlerMeasure

Tactic:
gcongr
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
g h : ℂ[X]
hh : 1 ≤ h.mahlerMeasure
hbc : g.mahlerMeasure ≤ g.mahlerMeasure * h.mahlerMeasure
⊢ g.mahlerMeasure ≤ (g * h).mahlerMeasure

Tactic:
rw [mahlerMeasure_mul]

Premises used: Polynomial.mahlerMeasure_mul
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
g h : ℂ[X]
hh : 1 ≤ h.mahlerMeasure
⊢ g.mahlerMeasure ≤ g.mahlerMeasure * h.mahlerMeasure

Tactic:
le_mul_of_one_le_right g.mahlerMeasure_nonneg hh

Premises used: Polynomial.mahlerMeasure_nonneg, le_mul_of_one_le_right
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
g h : ℂ[X]
hh : 1 ≤ h.mahlerMeasure
⊢ g.mahlerMeasure ≤ g.mahlerMeasure * h.mahlerMeasure

Tactic:
exact le_mul_of_one_le_right g.mahlerMeasure_nonneg hh

Premises used: Polynomial.mahlerMeasure_nonneg, le_mul_of_one_le_right
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_1
inst : Semiring A
p : A[X]
v : A →+* ℂ
⊢ p.mapMahlerMeasure v = (map v p).mahlerMeasure

Tactic:
rfl

Premises used: Polynomial.mapMahlerMeasure, rfl
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_1
inst : Semiring A
v : A →+* ℂ
f g : A[X]
⊢ (f * g).mapMahlerMeasure v = f.mapMahlerMeasure v * g.mapMahlerMeasure v

Tactic:
simp [mapMahlerMeasure, mahlerMeasure_mul]

Premises used: Polynomial.mapMahlerMeasure, Polynomial.mahlerMeasure_mul
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_1
inst : Semiring A
p : A[X]
v : A →+* ℂ
⊢ 0 ≤ p.mapMahlerMeasure v

Tactic:
Polynomial.mahlerMeasure_nonneg _

Premises used: Polynomial.mahlerMeasure_nonneg, Polynomial.mapMahlerMeasure
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_1
inst : Semiring A
v : A →+* ℂ
⊢ mapMahlerMeasure 0 v = 0

Tactic:
simp [mapMahlerMeasure]

Premises used: Polynomial.mapMahlerMeasure
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_1
inst : Semiring A
v : A →+* ℂ
⊢ mapMahlerMeasure 1 v = 1

Tactic:
simp [mapMahlerMeasure]

Premises used: Polynomial.mapMahlerMeasure
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_2
inst : NormedRing A
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
z : A
⊢ mapMahlerMeasure ((C : (a : A) → A[X]) z) v = ‖z‖

Tactic:
simp [mapMahlerMeasure, hv.norm_map_of_map_zero (map_zero _)]

Premises used: Polynomial.mapMahlerMeasure, map_zero, Isometry.norm_map_of_map_zero
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
pos : ∀ (hp : p.leadingCoeff = 0), ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v
neg : ∀ (hp : ¬p.leadingCoeff = 0), ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v

Tactic:
by_cases hp : p.leadingCoeff = 0

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
hp : p.leadingCoeff = 0
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v

Tactic:
simp [hp, mapMahlerMeasure_nonneg]

Premises used: Polynomial.mapMahlerMeasure_nonneg
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
hp : ¬p.leadingCoeff = 0
⊢ Ne (α := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) (0 : ℂ)

Tactic:
have hv_ne : v p.leadingCoeff ≠ 0 :=
      fun h ↦ hp <| hv.injective <| h.trans (map_zero _).symm
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
hp : ¬p.leadingCoeff = 0
hv_ne : Ne (α := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) (0 : ℂ)
⊢ norm (E := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) = ‖p.leadingCoeff‖

Tactic:
have hv_norm : ‖v p.leadingCoeff‖ = ‖p.leadingCoeff‖ := hv.norm_map_of_map_zero (map_zero _) _
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
hp : ¬p.leadingCoeff = 0
hv_ne : Ne (α := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) (0 : ℂ)
hv_norm : norm (E := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) = ‖p.leadingCoeff‖
neg : norm (E := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) ≤ p.mapMahlerMeasure v
neg₁ : ‖(map v p).leadingCoeff‖ ≤ p.mapMahlerMeasure v
neg₂ : (map v p).mahlerMeasure ≤ p.mapMahlerMeasure v
neg₃ neg₄ : (map v p).mahlerMeasure ≤ (map v p).mahlerMeasure
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v

Tactic:
grw [← hv_norm, ← leadingCoeff_map_of_leadingCoeff_ne_zero v hv_ne,
      leadingCoeff_le_mahlerMeasure, mapMahlerMeasure]

Premises used: Polynomial.mapMahlerMeasure, Polynomial.leadingCoeff_le_mahlerMeasure, Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
inst_1 : NormOneClass A
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
hp : p.Monic
grw : 1 ≤ ‖p.leadingCoeff‖
grw₁ : 1 ≤ norm.{u_2} (E := A) 1
grw₂ grw₃ : LE.le (α := ℝ) 1 1
⊢ 1 ≤ p.mapMahlerMeasure v

Tactic:
grw [← p.leadingCoeff_le_mapMahlerMeasure v hv, hp.leadingCoeff, norm_one]

Premises used: Polynomial.leadingCoeff_le_mapMahlerMeasure, NormOneClass.norm_one, Polynomial.Monic.leadingCoeff
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
hp : p ≠ 0
⊢ 0 < p.mapMahlerMeasure v

Tactic:
mahlerMeasure_pos_of_ne_zero <| (Polynomial.map_eq_zero_iff hv.injective).not.mpr hp

Premises used: Iff.mpr, Polynomial.mapMahlerMeasure, Iff.not, Polynomial.mahlerMeasure_pos_of_ne_zero, Isometry.injective, Polynomial.map_eq_zero_iff
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
apply : Eq (α := ℝ) ((map v p).sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖) (p.sum fun (x : ℕ) (a : A) ↦ ‖a‖)
⊢ p.mapMahlerMeasure v ≤ p.sum fun (x : ℕ) (a : A) ↦ ‖a‖

Tactic:
apply mahlerMeasure_le_sum_norm_coeff _ |>.trans_eq

Premises used: LE.le.trans_eq, Polynomial.mahlerMeasure_le_sum_norm_coeff
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
rw : Eq (α := ℝ) (∑ n ∈ p.support, ‖(map v p).coeff n‖) (∑ n ∈ p.support, ‖p.coeff n‖)
⊢ Eq (α := ℝ) ((map v p).sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖) (p.sum fun (x : ℕ) (a : A) ↦ ‖a‖)

Tactic:
rw [sum_def, sum_def, support_map_of_injective _ hv.injective]

Premises used: Isometry.injective, Polynomial.sum_def, Polynomial.support_map_of_injective
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
x : ℕ
h : x ∈ p.support
⊢ ‖(map v p).coeff x‖ = ‖p.coeff x‖

Tactic:
simp [hv.norm_map_of_map_zero (map_zero _)]

Premises used: map_zero, Isometry.norm_map_of_map_zero
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
⊢ Eq (α := ℝ) (∑ n ∈ p.support, ‖(map v p).coeff n‖) (∑ n ∈ p.support, ‖p.coeff n‖)

Tactic:
exact Finset.sum_congr rfl fun x _ ↦ by
    simp [hv.norm_map_of_map_zero (map_zero _)]

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_2
inst : NormedRing A
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
n : ℕ
p : A[X]
⊢ ‖p.coeff n‖ = norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ)

Tactic:
have hv_norm : ‖p.coeff n‖ = ‖v (p.coeff n)‖ :=
    (hv.norm_map_of_map_zero (map_zero _) _).symm
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_2
inst : NormedRing A
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
n : ℕ
p : A[X]
hv_norm : ‖p.coeff n‖ = norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ)
⊢ norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ) = ‖(map v p).coeff n‖

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_2
inst : NormedRing A
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
n : ℕ
p : A[X]
hv_norm : ‖p.coeff n‖ = norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ)
⊢ norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ) = ‖(map v p).coeff n‖

Tactic:
have hcoeff : ‖v (p.coeff n)‖ = ‖(p.map v).coeff n‖ := by simp
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
A : Type u_2
inst : NormedRing A
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
n : ℕ
p : A[X]
hv_norm : ‖p.coeff n‖ = norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ)
hcoeff : norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ) = ‖(map v p).coeff n‖
grw : norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ) ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
grw₁ : ‖(map v p).coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
grw₂ :
  (↑((map v p).natDegree.choose n) : ℝ) * (map v p).mahlerMeasure ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
grw₃ : (↑(p.natDegree.choose n) : ℝ) * (map v p).mahlerMeasure ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
grw₄ grw₅ :
  (↑(p.natDegree.choose n) : ℝ) * (map v p).mahlerMeasure ≤ (↑(p.natDegree.choose n) : ℝ) * (map v p).mahlerMeasure
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v

Tactic:
grw [hv_norm, hcoeff, norm_coeff_le_choose_mul_mahlerMeasure,
    natDegree_map_eq_of_injective hv.injective, mapMahlerMeasure]

Premises used: Polynomial.mapMahlerMeasure, Isometry.injective, Polynomial.natDegree_map_eq_of_injective, Polynomial.norm_coeff_le_choose_mul_mahlerMeasure
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
p : A[X]
pos : ∀ (h : p.support.Nonempty), p.supNorm = p.support.sup' h (norm ∘ p.coeff)
neg : ∀ (h : ¬p.support.Nonempty), p.supNorm = 0
⊢ p.supNorm = if hp : p.support.Nonempty then p.support.sup' hp (norm ∘ p.coeff) else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
p : A[X]
h : p.support.Nonempty
pos :
  Eq (α := ℝ) (p.support.sup' ⋯ fun (x : ℕ) ↦ (SeminormedRing.toRingSeminorm A : (a : A) → ℝ) (p.coeff x))
    (p.support.sup' ⋯ fun (x : ℕ) ↦ ‖p.coeff x‖)
⊢ p.supNorm = p.support.sup' h (norm ∘ p.coeff)

Tactic:
simp only [supNorm, gaussNorm, h, ↓reduceDIte, one_pow, mul_one, Function.comp_apply]

Premises used: one_pow, reduceDIte, Polynomial.supNorm, Function.comp_apply, mul_one, Polynomial.gaussNorm
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
p : A[X]
h : p.support.Nonempty
⊢ Eq (α := ℝ) (p.support.sup' ⋯ fun (x : ℕ) ↦ (SeminormedRing.toRingSeminorm A : (a : A) → ℝ) (p.coeff x))
    (p.support.sup' ⋯ fun (x : ℕ) ↦ ‖p.coeff x‖)

Tactic:
congr
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
p : A[X]
h : ¬p.support.Nonempty
⊢ p.supNorm = 0

Tactic:
simp [supNorm, gaussNorm, h]

Premises used: Polynomial.supNorm, Polynomial.gaussNorm
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
⊢ supNorm.{u_1} (A := A) 0 = 0

Tactic:
gaussNorm_zero ..

Premises used: Polynomial.gaussNorm_zero, Polynomial.supNorm
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
p : A[X]
hc : LE.le (α := ℝ) 0 1
⊢ 0 ≤ p.supNorm

Tactic:
apply gaussNorm_nonneg

Premises used: Polynomial.gaussNorm_nonneg
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
p : A[X]
⊢ LE.le (α := ℝ) 0 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
a : A
⊢ supNorm.{u_1} (A := A) ((C : (a : A) → A[X]) a) = ‖a‖

Tactic:
gaussNorm_C ..

Premises used: Polynomial.gaussNorm_C, Polynomial.supNorm
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
n : ℕ
a : A
pos : ∀ (ha : a = 0), supNorm.{u_1} (A := A) ((monomial n : (a : A) → A[X]) a) = ‖a‖
neg : ∀ (ha : ¬a = 0), supNorm.{u_1} (A := A) ((monomial n : (a : A) → A[X]) a) = ‖a‖
⊢ supNorm.{u_1} (A := A) ((monomial n : (a : A) → A[X]) a) = ‖a‖

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
n : ℕ
a : A
ha : a = 0
⊢ supNorm.{u_1} (A := A) ((monomial n : (a : A) → A[X]) a) = ‖a‖

Tactic:
simp [ha]
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
n : ℕ
a : A
ha : ¬a = 0
⊢ supNorm.{u_1} (A := A) ((monomial n : (a : A) → A[X]) a) = ‖a‖

Tactic:
simp [supNorm, gaussNorm, support_monomial n ha]

Premises used: Polynomial.support_monomial, Polynomial.supNorm, Polynomial.gaussNorm
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
inst_1 : NormOneClass A
rw : supNorm.{u_1} (A := A) ((monomial 1 : (a : A) → A[X]) 1) = 1
rw₁ : norm.{u_1} (E := A) 1 = 1
rw₂ rw₃ : Eq (α := ℝ) 1 1
⊢ supNorm.{u_1} (A := A) X = 1

Tactic:
rw [← monomial_one_one_eq_X, supNorm_monomial, norm_one]

Premises used: Polynomial.monomial_one_one_eq_X, NormOneClass.norm_one, Polynomial.supNorm_monomial
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
p : A[X]
i : ℕ
⊢ LE.le (α := ℝ) 0 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
p : A[X]
i : ℕ
⊢ ‖p.coeff i‖ ≤ p.supNorm

Tactic:
simpa using le_gaussNorm (SeminormedRing.toRingSeminorm A) p (by norm_num : (0 : ℝ) ≤ 1) i

Premises used: Polynomial.le_gaussNorm, SeminormedRing.toRingSeminorm
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
p : A[X]
⊢ ∃ (i : ℕ), p.supNorm = ‖p.coeff i‖

Tactic:
simpa using p.exists_eq_gaussNorm (SeminormedRing.toRingSeminorm A) 1

Premises used: Polynomial.exists_eq_gaussNorm, SeminormedRing.toRingSeminorm, OfNat.ofNat
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
p : A[X]
⊢ Membership.mem (γ := Set ℝ) (Set.range fun (x : ℕ) ↦ ‖p.coeff x‖) p.supNorm

Tactic:
simpa [eq_comm] using exists_eq_supNorm p

Premises used: Polynomial.exists_eq_supNorm, eq_comm
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
p : A[X]
⊢ Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (x : ℕ) ↦ ‖p.coeff x‖)) p.supNorm

Tactic:
simpa [mem_upperBounds] using le_supNorm p

Premises used: Polynomial.le_supNorm, mem_upperBounds
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : SeminormedRing A
p : A[X]
⊢ p.supNorm = ⨆ (i : ℕ), ‖p.coeff i‖

Tactic:
p.isGreatest_supNorm.csSup_eq.symm

Premises used: iSup, Polynomial.isGreatest_supNorm, Eq.symm, IsGreatest.csSup_eq
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : NormedRing A
p : A[X]
⊢ ∀ (x : A), Eq (α := ℝ) ((SeminormedRing.toRingSeminorm A : (a : A) → ℝ) x : ℝ) (0 : ℝ) → x = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.Norm
Goal:
A : Type u_1
inst : NormedRing A
p : A[X]
⊢ LT.lt (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 ≤ P.leadingCoeff
contrapose! : ∀ (hroots : P.leadingCoeff ≤ 0), ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y
⊢ 0 < P.leadingCoeff

Tactic:
contrapose! hroots
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hlc : 0 ≤ P.leadingCoeff
hroots : P.leadingCoeff ≤ 0
⊢ P.IsRoot x

Tactic:
simp [leadingCoeff_eq_zero.mp <| eq_of_le_of_ge hroots hlc]

Premises used: Iff.mp, eq_of_le_of_ge, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hlc : 0 ≤ P.leadingCoeff
hroots : P.leadingCoeff ≤ 0
⊢ ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y

Tactic:
exact ⟨x, by simp [leadingCoeff_eq_zero.mp <| eq_of_le_of_ge hroots hlc], le_refl x⟩