awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this_2 : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)),
    rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous (Y := ℝ) fun (x : ℝ) ↦ ‖eval (circleMap 0 1 x) p‖
⊢ √(⨍ (θ : ℝ) in 0..2 * π, HPow.hPow (β := ℕ) ‖eval (circleMap 0 1 θ) p‖ 2) =
    √(circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1)

Tactic:
simp [circleAverage_eq_intervalAverage]

Premises used: Real.circleAverage_eq_intervalAverage
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this_2 : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)),
    rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous (Y := ℝ) fun (x : ℝ) ↦ ‖eval (circleMap 0 1 x) p‖
⊢ √(circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1) =
    √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)

Tactic:
simp [p.sum_sq_norm_coeff_eq_circleAverage]

Premises used: Polynomial.sum_sq_norm_coeff_eq_circleAverage
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this_2 : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)),
    rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous (Y := ℝ) fun (x : ℝ) ↦ ‖eval (circleMap 0 1 x) p‖
calc :
  rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤
    ⨍ (θ : ℝ) in 0..2 * π, rexp (log ‖eval (circleMap 0 1 θ) p‖)
calc₁ :
  ⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖ =
    √(HPow.hPow (α := ℝ) (β := ℕ) (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) 2)
calc₂ :
  √(HPow.hPow (α := ℝ) (β := ℕ) (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) 2) ≤
    √(⨍ (θ : ℝ) in 0..2 * π, HPow.hPow (β := ℕ) ‖eval (circleMap 0 1 θ) p‖ 2)
calc₃ :
  √(⨍ (θ : ℝ) in 0..2 * π, HPow.hPow (β := ℕ) ‖eval (circleMap 0 1 θ) p‖ 2) =
    √(circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1)
calc₄ :
  √(circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1) =
    √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
⊢ rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)

Tactic:
calc exp (⨍ (θ : ℝ) in 0..(2 * π), log ‖p.eval (circleMap 0 1 θ)‖)
    ≤ ⨍ (θ : ℝ) in 0..(2 * π), exp (log ‖p.eval (circleMap 0 1 θ)‖) := by
        -- First Jensen's inequality invocation
        refine convexOn_exp.map_average_le continuousOn_exp isClosed_univ (by simp) ?_ ?_
        · rw [Set.uIoc_of_le (by positivity : 0 ≤ 2 * Real.pi)]
          exact ((analyticOnNhd_id.aeval_polynomial p).meromorphicOn.circleIntegrable_log_norm).1
        · exact (integrable_congr hlogAe).mpr hcont.integrableOn_uIoc
    _ = ⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖ := average_congr hlogAe
    _ = √((⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖) ^ 2) := by
        rw [sqrt_sq]; exact integral_nonneg (fun _ ↦ norm_nonneg _)
    _ ≤ √(⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖ ^ 2) := by
        -- Second Jensen's inequality invocation
        gcongr
        refine (convexOn_pow 2).map_average_le (continuousOn_pow 2)
            isClosed_Ici (by filter_upwards; simp) ?_ ?_
        · exact hcont.integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self
        · exact ((continuous_pow 2).comp hcont).integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self
    _ = √(circleAverage (fun θ ↦ ‖p.eval θ‖ ^ 2) 0 1) := by simp [circleAverage_eq_intervalAverage]
    _ = √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2) := by simp [p.sum_sq_norm_coeff_eq_circleAverage]

Premises used: Norm.norm, Polynomial.eval, Real.pi, HMul.hMul, Set.uIoc, MeasureTheory.Measure.restrict, circleMap, MeasureTheory.average, Real.exp, MeasureTheory.average_congr, Real.log, Polynomial.coeff, HPow.hPow, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, Polynomial.support, Finset.sum, Real.circleAverage
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
rw :
  √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1) * p.supNorm =
    √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1) * √(HPow.hPow (β := ℕ) p.supNorm 2)
rw₁ rw₂ :
  √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1) * p.supNorm = √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1) * p.supNorm
⊢ √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1) * p.supNorm =
    √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2)

Tactic:
rw [Real.sqrt_mul (by positivity), Real.sqrt_sq p.supNorm_nonneg]

Premises used: Real.sqrt_mul, Polynomial.supNorm_nonneg, Real.sqrt_sq
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
rw :
  √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2) ≤
    √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2)
⊢ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2) ≤ √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1) * p.supNorm

Tactic:
rw [show √(↑(p.natDegree) + 1) * p.supNorm = √((p.natDegree + 1) * p.supNorm ^ 2) from by
      rw [Real.sqrt_mul (by positivity), Real.sqrt_sq p.supNorm_nonneg]]
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
a :
  ∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2 ≤
    HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2
⊢ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2) ≤
    √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
⊢ ∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2 ≤
    HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2

Tactic:
(p.support.sum_le_card_nsmul _ (p.supNorm ^ 2) fun i _ ↦ ?_).trans ?_

Premises used: Finset.sum_le_card_nsmul, HPow.hPow, Polynomial.supNorm, LE.le.trans, OfNat.ofNat, Polynomial.support
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
a : ∀ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2 ≤ HPow.hPow (β := ℕ) p.supNorm 2
a₁ :
  p.support.card • HPow.hPow (β := ℕ) p.supNorm 2 ≤
    HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2
⊢ ∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2 ≤
    HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2

Tactic:
refine (p.support.sum_le_card_nsmul _ (p.supNorm ^ 2) fun i _ ↦ ?_).trans ?_

Premises used: Finset.sum_le_card_nsmul, HPow.hPow, Polynomial.supNorm, LE.le.trans, OfNat.ofNat, Polynomial.support
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
i : ℕ
h : i ∈ p.support
a : ‖p.coeff i‖ ≤ p.supNorm
⊢ HPow.hPow (β := ℕ) ‖p.coeff i‖ 2 ≤ HPow.hPow (β := ℕ) p.supNorm 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
i : ℕ
h : i ∈ p.support
⊢ ‖p.coeff i‖ ≤ p.supNorm

Tactic:
p.le_supNorm _

Premises used: Polynomial.le_supNorm
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
i : ℕ
h : i ∈ p.support
⊢ ‖p.coeff i‖ ≤ p.supNorm

Tactic:
exact p.le_supNorm _

Premises used: Polynomial.le_supNorm
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
a :
  (↑p.support.card : ℝ) * HPow.hPow (β := ℕ) p.supNorm 2 ≤
    HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2
⊢ p.support.card • HPow.hPow (β := ℕ) p.supNorm 2 ≤
    HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2

Tactic:
simp only [nsmul_eq_mul]

Premises used: nsmul_eq_mul
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
a : (↑p.support.card : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1
⊢ (↑p.support.card : ℝ) * HPow.hPow (β := ℕ) p.supNorm 2 ≤
    HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
⊢ (↑p.support.card : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1

Tactic:
mod_cast p.card_supp_le_succ_natDegree

Premises used: congrArg, Nat.cast_add._simp_1, cast, Nat.cast_le._simp_1, LE.le, Polynomial.card_supp_le_succ_natDegree, Nat.cast, HAdd.hAdd, Finset.card, Polynomial.natDegree, OfNat.ofNat, Eq.symm, Nat.cast_one, Polynomial.support, Eq.trans
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
⊢ (↑p.support.card : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1

Tactic:
exact mod_cast p.card_supp_le_succ_natDegree

Premises used: Polynomial.card_supp_le_succ_natDegree
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
p : ℂ[X]
pos : ∀ (hp : p = 0), ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure
neg : ∀ (hp : ¬p = 0), ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure

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

Tactic:
simp [hp]
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
neg : ∀ (hlt : p.natDegree < n), ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure
neg₁ : ∀ (hn : n ≤ p.natDegree), ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure

Tactic:
rcases lt_or_ge p.natDegree n with hlt | hn

Premises used: lt_or_ge, Polynomial.natDegree
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hlt : p.natDegree < n
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure

Tactic:
simp [coeff_eq_zero_of_natDegree_lt hlt, Nat.choose_eq_zero_of_lt hlt]

Premises used: Nat.choose_eq_zero_of_lt, Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
⊢ 0 < ‖p.leadingCoeff‖

Tactic:
simp [leadingCoeff_ne_zero.mpr hp]

Premises used: Iff.mpr, Polynomial.leadingCoeff_ne_zero
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
neg :
  Norm.norm (E := ℂ)
      (∑ m ∈ (powersetCard (p.natDegree - n) p.roots).toFinset,
        count m (powersetCard (p.natDegree - n) p.roots) • m.prod) ≤
    HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure

Tactic:
rw [mahlerMeasure_eq_leadingCoeff_mul_prod_roots, mul_left_comm,
    coeff_eq_esymm_roots_of_card (splits_iff_card_roots.mp (IsAlgClosed.splits p)) hn, mul_assoc,
    norm_mul, norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul,
    mul_le_mul_iff_right₀ (by simp [leadingCoeff_ne_zero.mpr hp]), esymm,
    Finset.sum_multiset_map_count]

Premises used: one_pow, Polynomial.mahlerMeasure_eq_leadingCoeff_mul_prod_roots, norm_pow, mul_assoc, NormOneClass.norm_one, norm_mul, mul_left_comm, Polynomial.splits_iff_card_roots, Finset.sum_multiset_map_count, norm_neg, Iff.mp, IsAlgClosed.splits, Multiset.esymm, Polynomial.coeff_eq_esymm_roots_of_card, one_mul, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
neg :
  ∑ i ∈ (powersetCard (p.natDegree - n) p.roots).toFinset, ‖count i (powersetCard (p.natDegree - n) p.roots) • i.prod‖ ≤
    HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
⊢ Norm.norm (E := ℂ)
      (∑ m ∈ (powersetCard (p.natDegree - n) p.roots).toFinset,
        count m (powersetCard (p.natDegree - n) p.roots) • m.prod) ≤
    HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))

Tactic:
apply le_trans <| norm_sum_le _ _

Premises used: norm_sum_le, le_trans
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
neg :
  ∑ 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))
⊢ ∑ i ∈ (powersetCard (p.natDegree - n) p.roots).toFinset, ‖count i (powersetCard (p.natDegree - n) p.roots) • i.prod‖ ≤
    HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))

Tactic:
simp_rw [nsmul_eq_mul, norm_mul, _root_.norm_natCast]

Premises used: norm_natCast, norm_mul, nsmul_eq_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
x : Multiset ℂ
hx : x ∈ S.toFinset
⊢ x ≤ p.roots ∧ x.card = p.natDegree - n

Tactic:
rw [mem_toFinset, mem_powersetCard] at hx

Premises used: Multiset.mem_powersetCard, 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
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
h1 : ∀ a ∈ x.toFinset, ‖a‖ ≤ max 1 ‖a‖
⊢ LE.le (α := ℝ) (∏ z ∈ x.toFinset, ‖z‖ ^ count z x) (∏ z ∈ x.toFinset, max 1 ‖z‖ ^ count z x)

Tactic:
gcongr with a
-- 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
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
a : ℂ
h : a ∈ x.toFinset
⊢ ‖a‖ ≤ max 1 ‖a‖

Tactic:
le_max_right 1 ‖a‖

Premises used: le_max_right, Norm.norm, OfNat.ofNat
-- 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
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
a : ℂ
h : a ∈ x.toFinset
⊢ ‖a‖ ≤ max 1 ‖a‖

Tactic:
exact le_max_right 1 ‖a‖

Premises used: le_max_right, Norm.norm, OfNat.ofNat
-- 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
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
norm_cast :
  LE.le (α := NNReal) (∏ x_1 ∈ x.toFinset, max 1 ‖x_1‖₊ ^ count x_1 x)
    (∏ x_1 ∈ p.roots.toFinset, max 1 ‖x_1‖₊ ^ count x_1 x)
⊢ LE.le (α := ℝ) (∏ x_1 ∈ x.toFinset, max 1 (↑‖x_1‖₊ : ℝ) ^ count x_1 x)
    (∏ x_1 ∈ p.roots.toFinset, max 1 (↑‖x_1‖₊ : ℝ) ^ count x_1 x)

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
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
⊢ LE.le (α := NNReal) (∏ x_1 ∈ x.toFinset, max 1 ‖x_1‖₊ ^ count x_1 x)
    (∏ x_1 ∈ p.roots.toFinset, max 1 ‖x_1‖₊ ^ count x_1 x)

Tactic:
Finset.prod_le_prod_of_subset_of_one_le' (toFinset_subset.mpr (subset_of_le hx.1))
        (fun a _ _ ↦ one_le_pow₀ (le_max_left 1 ‖a‖))

Premises used: Iff.mpr, Norm.norm, Multiset.subset_of_le, one_le_pow₀, Finset.prod_le_prod_of_subset_of_one_le', And.left, Multiset.toFinset_subset, OfNat.ofNat, le_max_left
-- 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
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
⊢ LE.le (α := NNReal) (∏ x_1 ∈ x.toFinset, max 1 ‖x_1‖₊ ^ count x_1 x)
    (∏ x_1 ∈ p.roots.toFinset, max 1 ‖x_1‖₊ ^ count x_1 x)

Tactic:
exact Finset.prod_le_prod_of_subset_of_one_le' (toFinset_subset.mpr (subset_of_le hx.1))
        (fun a _ _ ↦ one_le_pow₀ (le_max_left 1 ‖a‖))
-- 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
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
h1 : ∀ a ∈ p.roots.toFinset, 1 ≤ max 1 ‖a‖
h1₁ : ∀ a ∈ p.roots.toFinset, x ≤ p.roots
⊢ LE.le (α := ℝ) (∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z x) (∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z p.roots)

Tactic:
gcongr with a
-- 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
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
a : ℂ
h : a ∈ p.roots.toFinset
⊢ 1 ≤ max 1 ‖a‖

Tactic:
le_max_left 1 ‖a‖

Premises used: Norm.norm, OfNat.ofNat, le_max_left
-- 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
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
a : ℂ
h : a ∈ p.roots.toFinset
⊢ 1 ≤ max 1 ‖a‖

Tactic:
exact le_max_left 1 ‖a‖

Premises used: Norm.norm, OfNat.ofNat, le_max_left
-- 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
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
a : ℂ
h : a ∈ p.roots.toFinset
⊢ x ≤ p.roots

Tactic:
hx.1

Premises used: And.left
-- 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
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
a : ℂ
h : a ∈ p.roots.toFinset
⊢ x ≤ p.roots

Tactic:
exact hx.1

Premises used: And.left
-- 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
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
z : LE.le (α := ℝ) (∏ z ∈ x.toFinset, ‖z‖ ^ count z x) (∏ z ∈ x.toFinset, max 1 ‖z‖ ^ count z x)
z₁ : LE.le (α := ℝ) (∏ z ∈ x.toFinset, max 1 ‖z‖ ^ count z x) (∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z x)
z₂ :
  LE.le (α := ℝ) (∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z x) (∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z p.roots)
⊢ LE.le (α := ℝ) (∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)

Tactic:
calc
    ∏ z ∈ x.toFinset, ‖z‖ ^ count z x
      ≤ ∏ z ∈ x.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
      gcongr with a
      exact le_max_right 1 ‖a‖
    _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
      simp_rw [← coe_nnnorm]
      norm_cast
      exact Finset.prod_le_prod_of_subset_of_one_le' (toFinset_subset.mpr (subset_of_le hx.1))
        (fun a _ _ ↦ one_le_pow₀ (le_max_left 1 ‖a‖))
    _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z p.roots := by
      gcongr with a
      · exact le_max_left 1 ‖a‖
      · exact hx.1

Premises used: Multiset.toFinset, Polynomial.roots
-- 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
⊢ ∀ (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)

Tactic:
have (x : Multiset ℂ) (hx : x ∈ S.toFinset) : ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x
      ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots := by
    rw [mem_toFinset, mem_powersetCard] at hx
    calc
    ∏ z ∈ x.toFinset, ‖z‖ ^ count z x
      ≤ ∏ z ∈ x.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
      gcongr with a
      exact le_max_right 1 ‖a‖
    _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
      simp_rw [← coe_nnnorm]
      norm_cast
      exact Finset.prod_le_prod_of_subset_of_one_le' (toFinset_subset.mpr (subset_of_le hx.1))
        (fun a _ _ ↦ one_le_pow₀ (le_max_left 1 ‖a‖))
    _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z p.roots := by
      gcongr with a
      · exact le_max_left 1 ‖a‖
      · exact hx.1
-- 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)
h : ∀ (x : Multiset ℂ) (hx : x ∈ S.toFinset), ‖x.prod‖ ≤ prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
⊢ 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)))

Tactic:
gcongr with x hx
-- 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)
x : Multiset ℂ
hx : x ∈ S.toFinset
h : LE.le (α := ℝ) (∏ b ∈ x.toFinset, ‖b ^ count b x‖) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
⊢ ‖x.prod‖ ≤ prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)

Tactic:
rw [Finset.prod_multiset_map_count, Finset.prod_multiset_count, norm_prod]

Premises used: Finset.prod_multiset_map_count, norm_prod, Finset.prod_multiset_count
-- 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)
x : Multiset ℂ
hx : x ∈ S.toFinset
h : LE.le (α := ℝ) (∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
⊢ LE.le (α := ℝ) (∏ b ∈ x.toFinset, ‖b ^ count b x‖) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)

Tactic:
simp_rw [norm_pow]

Premises used: norm_pow
-- 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)
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)

Tactic:
this x hx
-- 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)
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)

Tactic:
exact this x hx