awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
neg :
  ∫ (θ : ℝ) in 0..2 * π, log (‖eval (circleMap 0 1 θ) p‖ * ‖eval (circleMap 0 1 θ) q‖) =
    HAdd.hAdd (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖)
      (∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) q‖)
⊢ rexp (π⁻¹ * 2⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log (‖eval (circleMap 0 1 θ) p‖ * ‖eval (circleMap 0 1 θ) q‖)) =
    rexp
      (π⁻¹ * 2⁻¹ *
        HAdd.hAdd (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖)
          (∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) q‖))

Tactic:
congr
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
neg :
  Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log (‖eval (circleMap 0 1 θ) p‖ * ‖eval (circleMap 0 1 θ) q‖))
    (∫ (x : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 x) p‖ + log ‖eval (circleMap 0 1 x) q‖)
⊢ ∫ (θ : ℝ) in 0..2 * π, log (‖eval (circleMap 0 1 θ) p‖ * ‖eval (circleMap 0 1 θ) q‖) =
    HAdd.hAdd (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖)
      (∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) q‖)

Tactic:
rw [← integral_add p.intervalIntegrable_mahlerMeasure q.intervalIntegrable_mahlerMeasure]

Premises used: Polynomial.intervalIntegrable_mahlerMeasure, intervalIntegral.integral_add
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
neg :
  ∀ᵐ (x : ℝ),
    x ∈ Set.uIoc 0 (2 * π) →
      log (‖eval (circleMap 0 1 x) p‖ * ‖eval (circleMap 0 1 x) q‖) =
        log ‖eval (circleMap 0 1 x) p‖ + log ‖eval (circleMap 0 1 x) q‖
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log (‖eval (circleMap 0 1 θ) p‖ * ‖eval (circleMap 0 1 θ) q‖))
    (∫ (x : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 x) p‖ + log ‖eval (circleMap 0 1 x) q‖)

Tactic:
apply integral_congr_ae

Premises used: intervalIntegral.integral_congr_ae
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
apply :
  Set.Finite (α := ℝ)
    {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‖)}
⊢ Eq (α := ENNReal)
    ((MeasureTheory.volume : (a : Set ℝ) → ENNReal)
        {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‖)} :
      ENNReal)
    (0 : ENNReal)

Tactic:
apply Set.Finite.measure_zero _ MeasureTheory.volume

Premises used: Set.Finite.measure_zero, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
simp :
  Set.Finite (α := ℝ)
    {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‖}
⊢ Set.Finite (α := ℝ)
    {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‖)}

Tactic:
simp only [Classical.not_imp]

Premises used: Classical.not_imp
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ |0 - 2 * π| ≤ 2 * π

Tactic:
simp [le_of_eq, pi_nonneg]

Premises used: Real.pi_nonneg, le_of_eq
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
apply :
  (circleMap 0 1 ''
      {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‖}).Finite
⊢ Set.Finite (α := ℝ)
    {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‖}

Tactic:
apply Set.Finite.of_finite_image (f := circleMap 0 1) _ <|
    (injOn_circleMap_of_abs_sub_le one_ne_zero (by simp [le_of_eq, pi_nonneg])).mono (fun _ h ↦ h.1)

Premises used: Set.Finite.of_finite_image, injOn_circleMap_of_abs_sub_le, Set.InjOn.mono, one_ne_zero
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
apply :
  circleMap 0 1 ''
      {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‖} ⊆
    {x : ℂ | x ∈ (p * q).roots}
⊢ (circleMap 0 1 ''
      {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‖}).Finite

Tactic:
apply (p * q).roots.finite_toSet.subset

Premises used: Polynomial.roots, HMul.hMul, Set.Finite.subset, Multiset.finite_toSet
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
a : ℂ
w : ℝ
right : circleMap 0 1 w = a
left : w ∈ Set.uIoc 0 (2 * π)
h :
  ¬log (‖eval (circleMap 0 1 w) p‖ * ‖eval (circleMap 0 1 w) q‖) =
      log ‖eval (circleMap 0 1 w) p‖ + log ‖eval (circleMap 0 1 w) q‖
contrapose :
  ∀ (h : a ∉ {x : ℂ | x ∈ (p * q).roots}),
    log (‖eval (circleMap 0 1 w) p‖ * ‖eval (circleMap 0 1 w) q‖) =
      log ‖eval (circleMap 0 1 w) p‖ + log ‖eval (circleMap 0 1 w) q‖
⊢ Membership.mem (γ := Set ℂ) {x : ℂ | x ∈ (p * q).roots} a

Tactic:
contrapose h
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
a : ℂ
w : ℝ
right : circleMap 0 1 w = a
left : w ∈ Set.uIoc 0 (2 * π)
h : a ∉ {x : ℂ | x ∈ (p * q).roots}
⊢ log (‖eval (circleMap 0 1 w) p‖ * ‖eval (circleMap 0 1 w) q‖) =
    log ‖eval (circleMap 0 1 w) p‖ + log ‖eval (circleMap 0 1 w) q‖

Tactic:
simp_all [log_mul]

Premises used: Real.log_mul
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
⊢ mahlerMeasure (Multiset.prod 0) = Multiset.prod (Multiset.map (fun (p : ℂ[X]) ↦ p.mahlerMeasure) 0)

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
a : ℂ[X]
s : Multiset ℂ[X]
ih : s.prod.mahlerMeasure = Multiset.prod (Multiset.map (fun (p : ℂ[X]) ↦ p.mahlerMeasure) s)
⊢ (a ::ₘ s).prod.mahlerMeasure = Multiset.prod (Multiset.map (fun (p : ℂ[X]) ↦ p.mahlerMeasure) (a ::ₘ s))

Tactic:
simp [mahlerMeasure_mul, ih]

Premises used: Polynomial.mahlerMeasure_mul
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
s : Multiset ℂ[X]
empty : mahlerMeasure (Multiset.prod 0) = Multiset.prod (Multiset.map (fun (p : ℂ[X]) ↦ p.mahlerMeasure) 0)
cons :
  ∀ (a : ℂ[X]) (s : Multiset ℂ[X])
    (ih : s.prod.mahlerMeasure = Multiset.prod (Multiset.map (fun (p : ℂ[X]) ↦ p.mahlerMeasure) s)),
    (a ::ₘ s).prod.mahlerMeasure = Multiset.prod (Multiset.map (fun (p : ℂ[X]) ↦ p.mahlerMeasure) (a ::ₘ s))
⊢ s.prod.mahlerMeasure = Multiset.prod (Multiset.map (fun (p : ℂ[X]) ↦ p.mahlerMeasure) s)

Tactic:
induction s using Multiset.induction_on with
  | empty => simp
  | cons _ _ ih => simp [mahlerMeasure_mul, ih]

Premises used: Polynomial.mahlerMeasure_mul
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p q : ℂ[X]
hpq : p * q ≠ 0
⊢ (p * q).logMahlerMeasure = p.logMahlerMeasure + q.logMahlerMeasure

Tactic:
simp_all [logMahlerMeasure_eq_log_MahlerMeasure, mahlerMeasure_mul, log_mul]

Premises used: Polynomial.mahlerMeasure_mul, Polynomial.logMahlerMeasure_eq_log_MahlerMeasure, Real.log_mul
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
a : ℂ
ha : a ≠ 0
p : ℂ[X]
hp : p ≠ 0
⊢ HMul.hMul (α := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) a : ℂ[X]) p ≠ 0

Tactic:
simp [ha, hp]
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
a : ℂ
ha : a ≠ 0
p : ℂ[X]
hp : p ≠ 0
rw : logMahlerMeasure ((C : (a : ℂ) → ℂ[X]) a) + p.logMahlerMeasure = log ‖a‖ + p.logMahlerMeasure
rw₁ rw₂ : log ‖a‖ + p.logMahlerMeasure = log ‖a‖ + p.logMahlerMeasure
⊢ (HMul.hMul (α := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) a : ℂ[X]) p).logMahlerMeasure = log ‖a‖ + p.logMahlerMeasure

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

Premises used: Polynomial.logMahlerMeasure_mul_eq_add_logMahlerMeasure, Polynomial.logMahlerMeasure_const
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
z : ℂ
⊢ (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).logMahlerMeasure = log⁺ ‖z‖

Tactic:
simp [logMahlerMeasure_def]

Premises used: Polynomial.logMahlerMeasure_def
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
z : ℂ
⊢ (HAdd.hAdd (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).logMahlerMeasure = log⁺ ‖z‖

Tactic:
simp [← sub_neg_eq_add, ← map_neg]

Premises used: map_neg, sub_neg_eq_add
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
a : ℂ
ha : a ≠ 0
b : ℂ
⊢ HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) a : ℂ[X]) X)
      ((C : (a : ℂ) → ℂ[X]) b : ℂ[X]) =
    HMul.hMul (α := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) a : ℂ[X])
      (HAdd.hAdd (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) (a⁻¹ * b) : ℂ[X]))

Tactic:
simp [mul_add, ← map_mul, ha]

Premises used: map_mul, mul_add
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
a : ℂ
ha : a ≠ 0
b : ℂ
rw :
  (HMul.hMul (α := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) a : ℂ[X])
        (HAdd.hAdd (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) (a⁻¹ * b) : ℂ[X]))).logMahlerMeasure =
    log ‖a‖ + log⁺ ‖a⁻¹ * b‖
rw₁ :
  log ‖a‖ + (HAdd.hAdd (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) (a⁻¹ * b) : ℂ[X])).logMahlerMeasure =
    log ‖a‖ + log⁺ ‖a⁻¹ * b‖
rw₂ rw₃ : log ‖a‖ + log⁺ ‖a⁻¹ * b‖ = log ‖a‖ + log⁺ ‖a⁻¹ * b‖
⊢ (HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) a : ℂ[X]) X)
        ((C : (a : ℂ) → ℂ[X]) b : ℂ[X])).logMahlerMeasure =
    log ‖a‖ + log⁺ ‖a⁻¹ * b‖

Tactic:
rw [show C a * X + C b = C a * (X + C (a⁻¹ * b)) by simp [mul_add, ← map_mul, ha],
    logMahlerMeasure_C_mul ha (X_add_C_ne_zero (a⁻¹ * b)), logMahlerMeasure_X_add_C]

Premises used: Polynomial.logMahlerMeasure_C_mul, HMul.hMul, Polynomial.X_add_C_ne_zero, Polynomial.logMahlerMeasure_X_add_C, Inv.inv
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
h : p.degree = 1
rw :
  (HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (p.coeff 1) : ℂ[X]) X)
        ((C : (a : ℂ) → ℂ[X]) (p.coeff 0) : ℂ[X])).logMahlerMeasure =
    log
        ‖(HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (p.coeff 1) : ℂ[X]) X)
                ((C : (a : ℂ) → ℂ[X]) (p.coeff 0) : ℂ[X])).coeff
            1‖ +
      log⁺
        ‖((HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (p.coeff 1) : ℂ[X]) X)
                    ((C : (a : ℂ) → ℂ[X]) (p.coeff 0) : ℂ[X])).coeff
                1)⁻¹ *
            (HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (p.coeff 1) : ℂ[X]) X)
                  ((C : (a : ℂ) → ℂ[X]) (p.coeff 0) : ℂ[X])).coeff
              0‖
⊢ p.logMahlerMeasure = log ‖p.coeff 1‖ + log⁺ ‖(p.coeff 1)⁻¹ * p.coeff 0‖

Tactic:
rw [eq_X_add_C_of_degree_le_one (le_of_eq h)]

Premises used: Polynomial.eq_X_add_C_of_degree_le_one, le_of_eq
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
h : p.degree = 1
⊢ p.coeff 1 ≠ 0

Tactic:
coeff_ne_zero_of_eq_degree h

Premises used: Polynomial.coeff_ne_zero_of_eq_degree
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
h : p.degree = 1
⊢ p.coeff 1 ≠ 0

Tactic:
exact coeff_ne_zero_of_eq_degree h

Premises used: Polynomial.coeff_ne_zero_of_eq_degree
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
h : p.degree = 1
⊢ (HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (p.coeff 1) : ℂ[X]) X)
        ((C : (a : ℂ) → ℂ[X]) (p.coeff 0) : ℂ[X])).logMahlerMeasure =
    log
        ‖(HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (p.coeff 1) : ℂ[X]) X)
                ((C : (a : ℂ) → ℂ[X]) (p.coeff 0) : ℂ[X])).coeff
            1‖ +
      log⁺
        ‖((HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (p.coeff 1) : ℂ[X]) X)
                    ((C : (a : ℂ) → ℂ[X]) (p.coeff 0) : ℂ[X])).coeff
                1)⁻¹ *
            (HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (p.coeff 1) : ℂ[X]) X)
                  ((C : (a : ℂ) → ℂ[X]) (p.coeff 0) : ℂ[X])).coeff
              0‖

Tactic:
simp [logMahlerMeasure_C_mul_X_add_C (show p.coeff 1 ≠ 0 by exact coeff_ne_zero_of_eq_degree h)]

Premises used: Polynomial.logMahlerMeasure_C_mul_X_add_C
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
z : ℂ
⊢ (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).logMahlerMeasure = log⁺ ‖z‖

Tactic:
have := logMahlerMeasure_X_sub_C z
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
z : ℂ
this : (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).logMahlerMeasure = log⁺ ‖z‖
⊢ log (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = log⁺ ‖z‖

Tactic:
rw [logMahlerMeasure_eq_log_MahlerMeasure] at this

Premises used: Polynomial.logMahlerMeasure_eq_log_MahlerMeasure
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
z : ℂ
this : log (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = log⁺ ‖z‖
⊢ rexp (log (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure) = rexp (log⁺ ‖z‖)

Tactic:
apply_fun exp at this

Premises used: Real.exp
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
z : ℂ
this : rexp (log (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure) = rexp (log⁺ ‖z‖)
rwa :
  ∀
    (this :
      rexp (log (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure) =
        rexp (log (max 1 ‖z‖))),
    (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = max 1 ‖z‖
rwa₁ :
  ∀
    (this :
      (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = rexp (log (max 1 ‖z‖))),
    (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = max 1 ‖z‖
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (this : (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = max 1 ‖z‖),
    (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = max 1 ‖z‖
⊢ (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = max 1 ‖z‖

Tactic:
rwa [posLog_eq_log_max_one (norm_nonneg z),
    exp_log (mahlerMeasure_pos_of_ne_zero <| X_sub_C_ne_zero z),
    exp_log (lt_of_lt_of_le zero_lt_one <| le_max_left 1 ‖z‖)] at this

Premises used: Norm.norm, Polynomial.mahlerMeasure_pos_of_ne_zero, Real.exp_log, zero_lt_one, Real.posLog_eq_log_max_one, Polynomial.X_sub_C_ne_zero, OfNat.ofNat, le_max_left, norm_nonneg, lt_of_lt_of_le
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
z : ℂ
⊢ (HAdd.hAdd (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = max 1 ‖z‖

Tactic:
simp [← sub_neg_eq_add, ← map_neg]

Premises used: map_neg, sub_neg_eq_add
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
a : ℂ
ha : a ≠ 0
b : ℂ
simp : (↑‖a‖₊ : ℝ) * max 1 (↑‖a⁻¹ * b‖₊ : ℝ) = max (↑‖a‖₊ : ℝ) (↑‖b‖₊ : ℝ)
⊢ (HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) a : ℂ[X]) X)
        ((C : (a : ℂ) → ℂ[X]) b : ℂ[X])).mahlerMeasure =
    max ‖a‖ ‖b‖

Tactic:
simp only [show C a * X + C b = C a * (X + C (a⁻¹ * b)) by simp [mul_add, ← map_mul, ha],
    mahlerMeasure_mul, mahlerMeasure_const, ← coe_nnnorm, mahlerMeasure_X_add_C]

Premises used: Polynomial.mahlerMeasure_const, Polynomial.mahlerMeasure_X_add_C, Polynomial.mahlerMeasure_mul, coe_nnnorm
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
a : ℂ
ha : a ≠ 0
b : ℂ
norm_cast : ‖a‖₊ * max 1 ‖a⁻¹ * b‖₊ = max ‖a‖₊ ‖b‖₊
⊢ (↑‖a‖₊ : ℝ) * max 1 (↑‖a⁻¹ * b‖₊ : ℝ) = max (↑‖a‖₊ : ℝ) (↑‖b‖₊ : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
a : ℂ
ha : a ≠ 0
b : ℂ
⊢ ‖a‖₊ * max 1 ‖a⁻¹ * b‖₊ = max ‖a‖₊ ‖b‖₊

Tactic:
simp [mul_max, ha]

Premises used: mul_max
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
h : p.degree = 1
rw :
  (HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (p.coeff 1) : ℂ[X]) X)
        ((C : (a : ℂ) → ℂ[X]) (p.coeff 0) : ℂ[X])).mahlerMeasure =
    max
      ‖(HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (p.coeff 1) : ℂ[X]) X)
              ((C : (a : ℂ) → ℂ[X]) (p.coeff 0) : ℂ[X])).coeff
          1‖
      ‖(HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (p.coeff 1) : ℂ[X]) X)
              ((C : (a : ℂ) → ℂ[X]) (p.coeff 0) : ℂ[X])).coeff
          0‖
⊢ p.mahlerMeasure = max ‖p.coeff 1‖ ‖p.coeff 0‖

Tactic:
rw [eq_X_add_C_of_degree_le_one (le_of_eq h)]

Premises used: Polynomial.eq_X_add_C_of_degree_le_one, le_of_eq
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
h : p.degree = 1
⊢ (HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (p.coeff 1) : ℂ[X]) X)
        ((C : (a : ℂ) → ℂ[X]) (p.coeff 0) : ℂ[X])).mahlerMeasure =
    max
      ‖(HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (p.coeff 1) : ℂ[X]) X)
              ((C : (a : ℂ) → ℂ[X]) (p.coeff 0) : ℂ[X])).coeff
          1‖
      ‖(HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (p.coeff 1) : ℂ[X]) X)
              ((C : (a : ℂ) → ℂ[X]) (p.coeff 0) : ℂ[X])).coeff
          0‖

Tactic:
simp [mahlerMeasure_C_mul_X_add_C (show p.coeff 1 ≠ 0 by exact coeff_ne_zero_of_eq_degree h)]

Premises used: Polynomial.mahlerMeasure_C_mul_X_add_C
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
pos :
  ∀ (hp : p = 0),
    p.logMahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)
neg :
  ∀ (hp : ¬p = 0),
    p.logMahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)
⊢ p.logMahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : p = 0
⊢ p.logMahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)

Tactic:
simp [hp]
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
⊢ ∀ (x : ℝ), Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (x : ℂ) ↦ max 1 ‖x‖) p.roots) x → x ≠ 0

Tactic:
grind [Multiset.mem_map]

Premises used: Multiset.mem_map
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
⊢ ∀ (x : ℝ), Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (x : ℂ) ↦ max 1 ‖x‖) p.roots) x → x ≠ 0

Tactic:
have : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0 := by grind [Multiset.mem_map]
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : ∀ (x : ℝ), Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (x : ℂ) ↦ max 1 ‖x‖) p.roots) x → x ≠ 0
neg :
  (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) p.leadingCoeff : ℂ[X])
        (Multiset.prod
            (Multiset.map (fun (x : ℂ) ↦ HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) x : ℂ[X])) p.roots) :
          ℂ[X])).logMahlerMeasure =
    log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)
⊢ p.logMahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)

Tactic:
nth_rw 1 [(IsAlgClosed.splits p).eq_prod_roots]

Premises used: Polynomial.Splits.eq_prod_roots, IsAlgClosed.splits
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : ∀ (x : ℝ), Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (x : ℂ) ↦ max 1 ‖x‖) p.roots) x → x ≠ 0
⊢ HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) p.leadingCoeff : ℂ[X])
      (Multiset.prod
          (Multiset.map (fun (x : ℂ) ↦ HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) x : ℂ[X])) p.roots) :
        ℂ[X]) ≠
    0

Tactic:
simp [hp, X_sub_C_ne_zero]

Premises used: Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : ∀ (x : ℝ), Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (x : ℂ) ↦ max 1 ‖x‖) p.roots) x → x ≠ 0
neg :
  logMahlerMeasure ((C : (a : ℂ) → ℂ[X]) p.leadingCoeff) +
      logMahlerMeasure
        (Multiset.prod
          (Multiset.map (fun (x : ℂ) ↦ HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) x : ℂ[X])) p.roots)) =
    log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)
⊢ (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) p.leadingCoeff : ℂ[X])
        (Multiset.prod
            (Multiset.map (fun (x : ℂ) ↦ HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) x : ℂ[X])) p.roots) :
          ℂ[X])).logMahlerMeasure =
    log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)

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

Premises used: Polynomial.logMahlerMeasure_mul_eq_add_logMahlerMeasure
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : ∀ (x : ℝ), Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (x : ℂ) ↦ max 1 ‖x‖) p.roots) x → x ≠ 0
⊢ logMahlerMeasure ((C : (a : ℂ) → ℂ[X]) p.leadingCoeff) +
      logMahlerMeasure
        (Multiset.prod
          (Multiset.map (fun (x : ℂ) ↦ HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) x : ℂ[X])) p.roots)) =
    log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)

Tactic:
simp [posLog_eq_log_max_one, logMahlerMeasure_eq_log_MahlerMeasure,
    prod_mahlerMeasure_eq_mahlerMeasure_prod, log_multiset_prod this]

Premises used: Polynomial.prod_mahlerMeasure_eq_mahlerMeasure_prod, Polynomial.logMahlerMeasure_eq_log_MahlerMeasure, Real.log_multiset_prod, Real.posLog_eq_log_max_one
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
pos :
  ∀ (hp : p = 0), p.mahlerMeasure = ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
neg :
  ∀ (hp : ¬p = 0), p.mahlerMeasure = ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : p = 0
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)

Tactic:
simp [hp]
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
⊢ p.logMahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)

Tactic:
have := logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots p
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : p.logMahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)
⊢ log p.mahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)

Tactic:
rw [logMahlerMeasure_eq_log_MahlerMeasure] at this

Premises used: Polynomial.logMahlerMeasure_eq_log_MahlerMeasure
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : log p.mahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)
⊢ rexp (log p.mahlerMeasure) =
    rexp (log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots))

Tactic:
apply_fun exp at this

Premises used: Real.exp