awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ 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‖)
have 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‖
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ 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)
have 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‖)}
Tactic: apply Set.Finite.measure_zero _ MeasureTheory.volume
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ 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‖)}
have 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‖}
Tactic: simp only [Classical.not_imp]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ 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‖}
have 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
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)
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ (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
have 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}
Tactic: apply (p * q).roots.finite_toSet.subset
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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‖
⊢ Membership.mem (γ := Set ℂ) {x : ℂ | x ∈ (p * q).roots} a
have 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‖
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
s : Multiset ℂ[X]
⊢ s.prod.mahlerMeasure = Multiset.prod (Multiset.map (fun (p : ℂ[X]) ↦ p.mahlerMeasure) s)
have empty : mahlerMeasure (Multiset.prod 0) = Multiset.prod (Multiset.map (fun (p : ℂ[X]) ↦ p.mahlerMeasure) 0)
Tactic: induction s using Multiset.induction_on with
  | empty => simp
  | cons _ _ ih => simp [mahlerMeasure_mul, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
s : Multiset ℂ[X]
empty : mahlerMeasure (Multiset.prod 0) = Multiset.prod (Multiset.map (fun (p : ℂ[X]) ↦ p.mahlerMeasure) 0)
⊢ s.prod.mahlerMeasure = Multiset.prod (Multiset.map (fun (p : ℂ[X]) ↦ p.mahlerMeasure) s)
have 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))
Tactic: induction s using Multiset.induction_on with
  | empty => simp
  | cons _ _ ih => simp [mahlerMeasure_mul, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
a : ℂ
ha : a ≠ 0
p : ℂ[X]
hp : p ≠ 0
⊢ (HMul.hMul (α := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) a : ℂ[X]) p).logMahlerMeasure = log ‖a‖ + p.logMahlerMeasure
have rw : logMahlerMeasure ((C : (a : ℂ) → ℂ[X]) a) + p.logMahlerMeasure = log ‖a‖ + p.logMahlerMeasure
Tactic: rw [logMahlerMeasure_mul_eq_add_logMahlerMeasure (by simp [ha, hp]), logMahlerMeasure_const]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
a : ℂ
ha : a ≠ 0
p : ℂ[X]
hp : p ≠ 0
rw : logMahlerMeasure ((C : (a : ℂ) → ℂ[X]) a) + p.logMahlerMeasure = log ‖a‖ + p.logMahlerMeasure
⊢ (HMul.hMul (α := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) a : ℂ[X]) p).logMahlerMeasure = log ‖a‖ + p.logMahlerMeasure
have rw₁ : log ‖a‖ + p.logMahlerMeasure = log ‖a‖ + p.logMahlerMeasure
Tactic: rw [logMahlerMeasure_mul_eq_add_logMahlerMeasure (by simp [ha, hp]), logMahlerMeasure_const]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
a : ℂ
ha : a ≠ 0
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‖
have 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‖
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]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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‖
⊢ (HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) a : ℂ[X]) X)
        ((C : (a : ℂ) → ℂ[X]) b : ℂ[X])).logMahlerMeasure =
    log ‖a‖ + log⁺ ‖a⁻¹ * b‖
have rw₁ : log ‖a‖ + (HAdd.hAdd (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) (a⁻¹ * 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]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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‖
⊢ (HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) a : ℂ[X]) X)
        ((C : (a : ℂ) → ℂ[X]) b : ℂ[X])).logMahlerMeasure =
    log ‖a‖ + log⁺ ‖a⁻¹ * b‖
have rw₂ : log ‖a‖ + log⁺ ‖a⁻¹ * b‖ = 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]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
h : p.degree = 1
⊢ p.logMahlerMeasure = log ‖p.coeff 1‖ + log⁺ ‖(p.coeff 1)⁻¹ * p.coeff 0‖
have 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‖
Tactic: rw [eq_X_add_C_of_degree_le_one (le_of_eq h)]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
z : ℂ
⊢ (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = max 1 ‖z‖
have this : (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).logMahlerMeasure = log⁺ ‖z‖
Tactic: have := logMahlerMeasure_X_sub_C z
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
z : ℂ
this : (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).logMahlerMeasure = log⁺ ‖z‖
⊢ (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = max 1 ‖z‖
have this₁ : log (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = log⁺ ‖z‖
Tactic: rw [logMahlerMeasure_eq_log_MahlerMeasure] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
z : ℂ
this : log (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = log⁺ ‖z‖
⊢ (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = max 1 ‖z‖
have this₁ : rexp (log (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure) = rexp (log⁺ ‖z‖)
Tactic: apply_fun exp at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
z : ℂ
this : rexp (log (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure) = rexp (log⁺ ‖z‖)
⊢ (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = max 1 ‖z‖
have 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‖
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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‖
⊢ (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = max 1 ‖z‖
have 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‖
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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‖
⊢ (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])).mahlerMeasure = max 1 ‖z‖
have 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‖
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
a : ℂ
ha : a ≠ 0
b : ℂ
⊢ (HAdd.hAdd (β := ℂ[X]) (HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) a : ℂ[X]) X)
        ((C : (a : ℂ) → ℂ[X]) b : ℂ[X])).mahlerMeasure =
    max ‖a‖ ‖b‖
have simp : (↑‖a‖₊ : ℝ) * max 1 (↑‖a⁻¹ * b‖₊ : ℝ) = 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]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
a : ℂ
ha : a ≠ 0
b : ℂ
⊢ (↑‖a‖₊ : ℝ) * max 1 (↑‖a⁻¹ * b‖₊ : ℝ) = max (↑‖a‖₊ : ℝ) (↑‖b‖₊ : ℝ)
have norm_cast : ‖a‖₊ * max 1 ‖a⁻¹ * b‖₊ = max ‖a‖₊ ‖b‖₊
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
h : p.degree = 1
⊢ p.mahlerMeasure = max ‖p.coeff 1‖ ‖p.coeff 0‖
have 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‖
Tactic: rw [eq_X_add_C_of_degree_le_one (le_of_eq h)]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ p.logMahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)
have pos : ∀ (hp : p = 0), p.logMahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
pos :
  ∀ (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)
have neg : ∀ (hp : ¬p = 0),
  p.logMahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
p : ℂ[X]
hp : ¬p = 0
⊢ p.logMahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)
have this : ∀ (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]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
hp : ¬p = 0
this : ∀ (x : ℝ), Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (x : ℂ) ↦ max 1 ‖x‖) p.roots) x → x ≠ 0
⊢ p.logMahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)
have 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)
Tactic: nth_rw 1 [(IsAlgClosed.splits p).eq_prod_roots]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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])).logMahlerMeasure =
    log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)
have 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)
Tactic: rw [logMahlerMeasure_mul_eq_add_logMahlerMeasure (by simp [hp, X_sub_C_ne_zero])]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
have pos : ∀ (hp : p = 0), p.mahlerMeasure = ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
pos :
  ∀ (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)
have neg : ∀ (hp : ¬p = 0), p.mahlerMeasure = ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
p : ℂ[X]
hp : ¬p = 0
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
p : ℂ[X]
hp : ¬p = 0
this : p.logMahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
have this₁ : log p.mahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)
Tactic: rw [logMahlerMeasure_eq_log_MahlerMeasure] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
p : ℂ[X]
hp : ¬p = 0
this : log p.mahlerMeasure = log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots)
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
have this₁ : rexp (log p.mahlerMeasure) = rexp (log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots))
Tactic: apply_fun exp at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
p : ℂ[X]
hp : ¬p = 0
this :
  rexp (log p.mahlerMeasure) =
    rexp (log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots))
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
have this₁ : p.mahlerMeasure = ‖p.leadingCoeff‖ * rexp (Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots))
Tactic: rw [exp_add, exp_log <| mahlerMeasure_pos_of_ne_zero hp,
    exp_log <| norm_pos_iff.mpr <| leadingCoeff_ne_zero.mpr hp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ ‖p.leadingCoeff‖ ≤ p.mahlerMeasure
have rw : ‖p.leadingCoeff‖ * 1 ≤ ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
Tactic: rw [← mul_one ‖_‖, mahlerMeasure_eq_leadingCoeff_mul_prod_roots]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ ‖p.leadingCoeff‖ * 1 ≤ ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
have hbc : LE.le (α := ℝ) 1 (Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
hlc : 1 ≤ ‖p.leadingCoeff‖
⊢ Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots) ≤ p.mahlerMeasure
have rw : HMul.hMul (α := ℝ) 1 (Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)) ≤
  ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
Tactic: rw [← one_mul (Multiset.prod _), mahlerMeasure_eq_leadingCoeff_mul_prod_roots]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
hlc : 1 ≤ ‖p.leadingCoeff‖
⊢ HMul.hMul (α := ℝ) 1 (Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)) ≤
    ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
have ha : LE.le (α := ℝ) 0 (Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ p.mahlerMeasure ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖
have pos : ∀ (hp : p = 0), p.mahlerMeasure ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
pos : ∀ (hp : p = 0), p.mahlerMeasure ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖
⊢ p.mahlerMeasure ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖
have neg : ∀ (hp : ¬p = 0), p.mahlerMeasure ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
p : ℂ[X]
hp : ¬p = 0
⊢ p.mahlerMeasure ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖
have this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
Tactic: have : 0 < p.sum fun _ a ↦ ‖a‖ :=
    Finset.sum_pos' (fun i _ ↦ norm_nonneg (p.coeff i)) ⟨p.natDegree, by simp [hp]⟩
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
⊢ p.mahlerMeasure ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖
have neg : 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: rw [show (p.sum fun _ a ↦ ‖a‖) = rexp (circleAverage (fun _ ↦ log (p.sum fun _ a ↦ ‖a‖)) 0 1)
    by simp [circleAverage_def, mul_assoc, exp_log this], mahlerMeasure_def_of_ne_zero hp,
    circleAverage_def, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 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‖))
have neg : LE.le (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 x) p‖)
  (∫ (θ : ℝ) in 0..2 * π, log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖))
Tactic: gcongr