mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg.e_a
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ MeasureTheory.volume
      {a |
        ¬(a ∈ Set.uIoc 0 (2 * π) →
            log (‖eval (circleMap 0 1 a) p‖ * ‖eval (circleMap 0 1 a) q‖) =
              log ‖eval (circleMap 0 1 a) p‖ + log ‖eval (circleMap 0 1 a) q‖)} =
    0

Tactic:
]

Goal state after:
case neg.e_a
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ MeasureTheory.volume
      {a |
        ¬(a ∈ Set.uIoc 0 (2 * π) →
            log (‖eval (circleMap 0 1 a) p‖ * ‖eval (circleMap 0 1 a) q‖) =
              log ‖eval (circleMap 0 1 a) p‖ + log ‖eval (circleMap 0 1 a) q‖)} =
    0
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case refine_2
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
⊢ P.leadingCoeff ≤ 0

Tactic:
]

Goal state after:
case refine_2
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
⊢ P.leadingCoeff ≤ 0
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ eval y (-P) = 0

Tactic:
]

Goal state after:
case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ eval y (-P) = 0
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case refine_2
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
⊢ P.leadingCoeff ≤ 0

Tactic:
]

Goal state after:
case refine_2
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
⊢ P.leadingCoeff ≤ 0
Module: Mathlib.Analysis.RCLike.BoundedContinuous

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : PseudoEMetricSpace E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
g : C(E, ℝ)
x : E →ᵇ 𝕜
hxA : x ∈ A
hxg : (toContinuousMapStarₐ 𝕜) x = (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) g
hg_apply : ∀ (a : E), x a = ↑(g a)
h_comp_eq : (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) (comp ⇑reCLM ⋯ x) = x
⊢ x ∈ A

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : PseudoEMetricSpace E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
g : C(E, ℝ)
x : E →ᵇ 𝕜
hxA : x ∈ A
hxg : (toContinuousMapStarₐ 𝕜) x = (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) g
hg_apply : ∀ (a : E), x a = ↑(g a)
h_comp_eq : (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) (comp ⇑reCLM ⋯ x) = x
⊢ x ∈ A
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: a : ℂ
ha : a ≠ 0
p : ℂ[X]
hp : p ≠ 0
⊢ log ‖a‖ + p.logMahlerMeasure = log ‖a‖ + p.logMahlerMeasure

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case cons
α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s✝ : Finset ι
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
j : ι
s : Finset ι
hj : j ∉ s
hs✝ : s.Nonempty
IH : ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)
⊢ g (f j + ∑ i ∈ s, f i) ≤ g (f j) ∨ ∃ a ∈ s, g (f j + ∑ i ∈ s, f i) ≤ g (f a)

Tactic:
refine (le_total (g (∑ i ∈ s, f i)) (g (f j))).imp ?_ ?_

Goal state after:
case cons.refine_1
α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s✝ : Finset ι
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
j : ι
s : Finset ι
hj : j ∉ s
hs✝ : s.Nonempty
IH : ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)
⊢ g (∑ i ∈ s, f i) ≤ g (f j) → g (f j + ∑ i ∈ s, f i) ≤ g (f j)

case cons.refine_2
α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s✝ : Finset ι
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
j : ι
s : Finset ι
hj : j ∉ s
hs✝ : s.Nonempty
IH : ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)
⊢ g (f j) ≤ g (∑ i ∈ s, f i) → ∃ a ∈ s, g (f j + ∑ i ∈ s, f i) ≤ g (f a)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: a : ℂ
ha : a ≠ 0
p : ℂ[X]
hp : p ≠ 0
⊢ (C a * p).logMahlerMeasure = log ‖a‖ + p.logMahlerMeasure

Tactic:
rw [logMahlerMeasure_mul_eq_add_logMahlerMeasure (by simp [ha, hp]), logMahlerMeasure_const]

Goal state after:
Module: Mathlib.Data.Rat.NatSqrt.Defs

Goal state before:
pp: x prec : ℕ
h : 0 < prec
⊢ ↑(x * prec ^ 2).sqrt ^ 2 ≤ ↑x * ↑prec ^ 2

Tactic:
]

Goal state after:
x prec : ℕ
h : 0 < prec
⊢ ↑(x * prec ^ 2).sqrt ^ 2 ≤ ↑x * ↑prec ^ 2
Module: Mathlib.Data.Rat.NatSqrt.Defs

Goal state before:
pp: x prec : ℕ
h : 0 < prec
⊢ ↑x * ↑prec ^ 2 < (↑(x * prec ^ 2).sqrt / ↑prec + 1 / ↑prec) ^ 2 * ↑prec ^ 2

Tactic:
]

Goal state after:
x prec : ℕ
h : 0 < prec
⊢ ↑x * ↑prec ^ 2 < (↑(x * prec ^ 2).sqrt / ↑prec + 1 / ↑prec) ^ 2 * ↑prec ^ 2
Module: Mathlib.Data.Rat.NatSqrt.Defs

Goal state before:
pp: x prec : ℕ
h : 0 < prec
⊢ ↑x * ↑prec ^ 2 < (↑(x * prec ^ 2).sqrt / ↑prec * ↑prec + 1 / ↑prec * ↑prec) ^ 2

Tactic:
]

Goal state after:
x prec : ℕ
h : 0 < prec
⊢ ↑x * ↑prec ^ 2 < (↑(x * prec ^ 2).sqrt / ↑prec * ↑prec + 1 / ↑prec * ↑prec) ^ 2
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: a : ℂ
ha : a ≠ 0
b : ℂ
⊢ log ‖a‖ + log⁺ ‖a⁻¹ * b‖ = log ‖a‖ + log⁺ ‖a⁻¹ * b‖

Tactic:
]

Goal state after:
Module: Mathlib.Data.Rat.NatSqrt.Defs

Goal state before:
pp: x prec : ℕ
h : 0 < prec
⊢ ↑x * ↑prec ^ 2 < (↑(x * prec ^ 2).sqrt + 1) ^ 2

pp: case h
x prec : ℕ
h : 0 < prec
⊢ ↑prec ≠ 0

pp: case h
x prec : ℕ
h : 0 < prec
⊢ ↑prec ≠ 0

Tactic:
]

Goal state after:
x prec : ℕ
h : 0 < prec
⊢ ↑x * ↑prec ^ 2 < (↑(x * prec ^ 2).sqrt + 1) ^ 2

case h
x prec : ℕ
h : 0 < prec
⊢ ↑prec ≠ 0

case h
x prec : ℕ
h : 0 < prec
⊢ ↑prec ≠ 0
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
h : p.degree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).logMahlerMeasure =
    log ‖(C (p.coeff 1) * X + C (p.coeff 0)).coeff 1‖ +
      log⁺ ‖((C (p.coeff 1) * X + C (p.coeff 0)).coeff 1)⁻¹ * (C (p.coeff 1) * X + C (p.coeff 0)).coeff 0‖

Tactic:
]

Goal state after:
p : ℂ[X]
h : p.degree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).logMahlerMeasure =
    log ‖(C (p.coeff 1) * X + C (p.coeff 0)).coeff 1‖ +
      log⁺ ‖((C (p.coeff 1) * X + C (p.coeff 0)).coeff 1)⁻¹ * (C (p.coeff 1) * X + C (p.coeff 0)).coeff 0‖
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: z : ℂ
this : log (X - C z).mahlerMeasure = log⁺ ‖z‖
⊢ (X - C z).mahlerMeasure = max 1 ‖z‖

Tactic:
]

Goal state after:
z : ℂ
this : log (X - C z).mahlerMeasure = log⁺ ‖z‖
⊢ (X - C z).mahlerMeasure = max 1 ‖z‖
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
i j : σ →₀ ℕ
vna : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v a = v (-a)
hdom : ∀ p ∈ Finset.antidiagonal (i + j), p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f * (coeff j) g)
⊢ v ((coeff (i + j)) (f * g)) = v ((coeff i) f * (coeff j) g)

Tactic:
]

Goal state after:
R : Type u_1
σ : Type u_2
v : R → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
i j : σ →₀ ℕ
vna : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v a = v (-a)
hdom : ∀ p ∈ Finset.antidiagonal (i + j), p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f * (coeff j) g)
⊢ v ((coeff (i + j)) (f * g)) = v ((coeff i) f * (coeff j) g)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: z : ℂ
this : (X - C z).mahlerMeasure = max 1 ‖z‖
⊢ (X - C z).mahlerMeasure = max 1 ‖z‖

Tactic:
]

Goal state after:
z : ℂ
this : (X - C z).mahlerMeasure = max 1 ‖z‖
⊢ (X - C z).mahlerMeasure = max 1 ‖z‖
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
i j : σ →₀ ℕ
vna : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v a = v (-a)
hdom : ∀ p ∈ Finset.antidiagonal (i + j), p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f * (coeff j) g)
⊢ v ((coeff (i, j).1) f * (coeff (i, j).2) g) = v ((coeff i) f * (coeff j) g)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
h : p.degree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).mahlerMeasure =
    max ‖(C (p.coeff 1) * X + C (p.coeff 0)).coeff 1‖ ‖(C (p.coeff 1) * X + C (p.coeff 0)).coeff 0‖

Tactic:
]

Goal state after:
p : ℂ[X]
h : p.degree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).mahlerMeasure =
    max ‖(C (p.coeff 1) * X + C (p.coeff 0)).coeff 1‖ ‖(C (p.coeff 1) * X + C (p.coeff 0)).coeff 0‖
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vna : IsNonarchimedean v
vNeg : ∀ (a : R), v a = v (-a)
hbfg : HasGaussNorm v c (f * g)
i₀ j₀ : σ →₀ ℕ
hi₀ : (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c f
hj₀ : (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c g
hdom' :
  ∀ p ∈ Finset.antidiagonal (i₀ + j₀),
    p ≠ (i₀, j₀) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i₀) f) * v ((coeff j₀) g)
⊢ (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) * (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2) =
    (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) * (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vna : IsNonarchimedean v
vNeg : ∀ (a : R), v a = v (-a)
hbfg : HasGaussNorm v c (f * g)
i₀ j₀ : σ →₀ ℕ
hi₀ : (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c f
hj₀ : (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c g
hdom' :
  ∀ p ∈ Finset.antidiagonal (i₀ + j₀),
    p ≠ (i₀, j₀) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i₀) f) * v ((coeff j₀) g)
hprod : ((i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2) = (i₀.prod fun x1 x2 ↦ c x1 ^ x2) * j₀.prod fun x1 x2 ↦ c x1 ^ x2
⊢ (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) * (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2) =
    v ((coeff i₀) f) * v ((coeff j₀) g) * ((i₀.prod fun x1 x2 ↦ c x1 ^ x2) * j₀.prod fun x1 x2 ↦ c x1 ^ x2)

Tactic:
]

Goal state after:
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vna : IsNonarchimedean v
vNeg : ∀ (a : R), v a = v (-a)
hbfg : HasGaussNorm v c (f * g)
i₀ j₀ : σ →₀ ℕ
hi₀ : (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c f
hj₀ : (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c g
hdom' :
  ∀ p ∈ Finset.antidiagonal (i₀ + j₀),
    p ≠ (i₀, j₀) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i₀) f) * v ((coeff j₀) g)
hprod : ((i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2) = (i₀.prod fun x1 x2 ↦ c x1 ^ x2) * j₀.prod fun x1 x2 ↦ c x1 ^ x2
⊢ (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) * (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2) =
    v ((coeff i₀) f) * v ((coeff j₀) g) * ((i₀.prod fun x1 x2 ↦ c x1 ^ x2) * j₀.prod fun x1 x2 ↦ c x1 ^ x2)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
hp : ¬p = 0
this : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0
⊢ (C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) p.roots).prod).logMahlerMeasure =
    log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum

Tactic:
]

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
this : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0
⊢ (C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) p.roots).prod).logMahlerMeasure =
    log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vna : IsNonarchimedean v
vNeg : ∀ (a : R), v a = v (-a)
hbfg : HasGaussNorm v c (f * g)
i₀ j₀ : σ →₀ ℕ
hi₀ : (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c f
hj₀ : (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c g
hdom' :
  ∀ p ∈ Finset.antidiagonal (i₀ + j₀),
    p ≠ (i₀, j₀) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i₀) f) * v ((coeff j₀) g)
⊢ (v ((coeff i₀) f) * v ((coeff j₀) g) * (i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2) =
    v ((coeff i₀) f) * v ((coeff j₀) g) * (i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vna : IsNonarchimedean v
vNeg : ∀ (a : R), v a = v (-a)
hbfg : HasGaussNorm v c (f * g)
i₀ j₀ : σ →₀ ℕ
hi₀ : (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c f
hj₀ : (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c g
hdom' :
  ∀ p ∈ Finset.antidiagonal (i₀ + j₀),
    p ≠ (i₀, j₀) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i₀) f) * v ((coeff j₀) g)
⊢ (v ((coeff i₀) f * (coeff j₀) g) * (i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2) =
    v ((coeff i₀) f * (coeff j₀) g) * (i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
hp : ¬p = 0
this : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0
⊢ (C p.leadingCoeff).logMahlerMeasure + (Multiset.map (fun x ↦ X - C x) p.roots).prod.logMahlerMeasure =
    log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum

Tactic:
]

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
this : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0
⊢ (C p.leadingCoeff).logMahlerMeasure + (Multiset.map (fun x ↦ X - C x) p.roots).prod.logMahlerMeasure =
    log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
hp : ¬p = 0
this : log p.mahlerMeasure = log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
]

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
this : log p.mahlerMeasure = log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
hp : ¬p = 0
this : p.mahlerMeasure = ‖p.leadingCoeff‖ * rexp (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
]

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
this : p.mahlerMeasure = ‖p.leadingCoeff‖ * rexp (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
⊢ ‖p.leadingCoeff‖ * 1 ≤ ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
]

Goal state after:
p : ℂ[X]
⊢ ‖p.leadingCoeff‖ * 1 ≤ ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
hlc : 1 ≤ ‖p.leadingCoeff‖
⊢ 1 * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod ≤
    ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
]

Goal state after:
p : ℂ[X]
hlc : 1 ≤ ‖p.leadingCoeff‖
⊢ 1 * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod ≤
    ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ rexp ((2 * π)⁻¹ * ∫ (x : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 x) p‖) ≤
    rexp ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log (p.sum fun x a ↦ ‖a‖))

Tactic:
]

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ rexp ((2 * π)⁻¹ * ∫ (x : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 x) p‖) ≤
    rexp ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log (p.sum fun x a ↦ ‖a‖))
Module: Mathlib.Analysis.Rat.NatSqrt.Real

Goal state before:
pp: x prec : ℕ
h : 0 < prec
this✝¹ : x.ratSqrt prec ^ 2 ≤ ↑x
this✝ : ↑(x.ratSqrt prec) ^ 2 ≤ ↑x
this : ↑(x.ratSqrt prec) ≤ √↑x
⊢ ↑(x.ratSqrt prec) ≤ √↑x

pp: x prec : ℕ
h : 0 < prec
this✝¹ : x.ratSqrt prec ^ 2 ≤ ↑x
this✝ : ↑(x.ratSqrt prec) ^ 2 ≤ ↑x
this : √(↑(x.ratSqrt prec) ^ 2) ≤ √↑x
⊢ 0 ≤ ↑(x.ratSqrt prec)

Tactic:
]

Goal state after:
x prec : ℕ
h : 0 < prec
this✝¹ : x.ratSqrt prec ^ 2 ≤ ↑x
this✝ : ↑(x.ratSqrt prec) ^ 2 ≤ ↑x
this : ↑(x.ratSqrt prec) ≤ √↑x
⊢ ↑(x.ratSqrt prec) ≤ √↑x

x prec : ℕ
h : 0 < prec
this✝¹ : x.ratSqrt prec ^ 2 ≤ ↑x
this✝ : ↑(x.ratSqrt prec) ^ 2 ≤ ↑x
this : √(↑(x.ratSqrt prec) ^ 2) ≤ √↑x
⊢ 0 ≤ ↑(x.ratSqrt prec)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case hbc
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ ∃ v ∈ ae (volume.restrict (Icc 0 (2 * π))), ∀ y ∈ v, log ‖eval (circleMap 0 1 y) p‖ ≤ log (p.sum fun x a ↦ ‖a‖)

Tactic:
]

Goal state after:
case hbc
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ ∃ v ∈ ae (volume.restrict (Icc 0 (2 * π))), ∀ y ∈ v, log ‖eval (circleMap 0 1 y) p‖ ≤ log (p.sum fun x a ↦ ‖a‖)
Module: Mathlib.Analysis.Rat.NatSqrt.Real

Goal state before:
pp: x prec : ℕ
h : 0 < prec
this✝¹ : ↑x < (x.ratSqrt prec + 1 / ↑prec) ^ 2
this✝ : ↑x < ↑((x.ratSqrt prec + 1 / ↑prec) ^ 2)
this : √↑x < ↑(x.ratSqrt prec + 1 / ↑prec)
⊢ √↑x < ↑(x.ratSqrt prec) + 1 / ↑prec

pp: x prec : ℕ
h : 0 < prec
this✝¹ : ↑x < (x.ratSqrt prec + 1 / ↑prec) ^ 2
this✝ : ↑x < ↑((x.ratSqrt prec + 1 / ↑prec) ^ 2)
this : √↑x < √(↑(x.ratSqrt prec + 1 / ↑prec) ^ 2)
⊢ 0 ≤ ↑(x.ratSqrt prec + 1 / ↑prec)

Tactic:
]

Goal state after:
x prec : ℕ
h : 0 < prec
this✝¹ : ↑x < (x.ratSqrt prec + 1 / ↑prec) ^ 2
this✝ : ↑x < ↑((x.ratSqrt prec + 1 / ↑prec) ^ 2)
this : √↑x < ↑(x.ratSqrt prec + 1 / ↑prec)
⊢ √↑x < ↑(x.ratSqrt prec) + 1 / ↑prec

x prec : ℕ
h : 0 < prec
this✝¹ : ↑x < (x.ratSqrt prec + 1 / ↑prec) ^ 2
this✝ : ↑x < ↑((x.ratSqrt prec + 1 / ↑prec) ^ 2)
this : √↑x < √(↑(x.ratSqrt prec + 1 / ↑prec) ^ 2)
⊢ 0 ≤ ↑(x.ratSqrt prec + 1 / ↑prec)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case h.left
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ volume ({x | x ∉ {x | eval (circleMap 0 1 x) p ≠ 0}} ∩ Icc 0 (2 * π)) = 0

Tactic:
]

Goal state after:
case h.left
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ volume ({x | x ∉ {x | eval (circleMap 0 1 x) p ≠ 0}} ∩ Icc 0 (2 * π)) = 0
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ {a | a ∈ Ico 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0}.Finite

Tactic:
]

Goal state after:
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ {a | a ∈ Ico 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0}.Finite
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case hxy
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
y✝ : ℝ
a✝ : y✝ ∈ {x | eval (circleMap 0 1 x) p ≠ 0}
⊢ ‖p.sum fun e a ↦ a * circleMap 0 1 y✝ ^ e‖ ≤ p.sum fun x a ↦ ‖a‖

Tactic:
]

Goal state after:
case hxy
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
y✝ : ℝ
a✝ : y✝ ∈ {x | eval (circleMap 0 1 x) p ≠ 0}
⊢ ‖p.sum fun e a ↦ a * circleMap 0 1 y✝ ^ e‖ ≤ p.sum fun x a ↦ ‖a‖
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
⊢ IsFiniteMeasure (volume.restrict (Ioc 0 (2 * π)))

Tactic:
]

Goal state after:
p : ℂ[X]
⊢ IsFiniteMeasure (volume.restrict (Ioc 0 (2 * π)))
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
this✝ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → 0 < ‖eval (circleMap 0 1 x) p‖

Tactic:
]

Goal state after:
p : ℂ[X]
this✝ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → 0 < ‖eval (circleMap 0 1 x) p‖
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case refine_2
p : ℂ[X]
this✝ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
⊢ InjOn (circleMap 0 1) {a | a ∈ uIoc 0 (2 * π)}

Tactic:
]

Goal state after:
case refine_2
p : ℂ[X]
this✝ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
⊢ InjOn (circleMap 0 1) {a | a ∈ uIoc 0 (2 * π)}
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)

Tactic:
]

Goal state after:
case neg
p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case refine_1
p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ Integrable (fun θ ↦ log ‖eval (circleMap 0 1 θ) p‖) (volume.restrict (Ioc 0 (2 * π)))

Tactic:
]

Goal state after:
case refine_1
p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ Integrable (fun θ ↦ log ‖eval (circleMap 0 1 θ) p‖) (volume.restrict (Ioc 0 (2 * π)))