awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
A : Type u_2
inst : NormedRing A
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
n : ℕ
p : A[X]
hv_norm : ‖p.coeff n‖ = norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ)
hcoeff : norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ) = ‖(map v p).coeff n‖
grw : norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ) ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
grw₁ : ‖(map v p).coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
grw₂ :
  (↑((map v p).natDegree.choose n) : ℝ) * (map v p).mahlerMeasure ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
have grw₃ : (↑(p.natDegree.choose n) : ℝ) * (map v p).mahlerMeasure ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
Tactic: grw [hv_norm, hcoeff, norm_coeff_le_choose_mul_mahlerMeasure,
    natDegree_map_eq_of_injective hv.injective, mapMahlerMeasure]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
A : Type u_2
inst : NormedRing A
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
n : ℕ
p : A[X]
hv_norm : ‖p.coeff n‖ = norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ)
hcoeff : norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ) = ‖(map v p).coeff n‖
grw : norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ) ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
grw₁ : ‖(map v p).coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
grw₂ :
  (↑((map v p).natDegree.choose n) : ℝ) * (map v p).mahlerMeasure ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
grw₃ : (↑(p.natDegree.choose n) : ℝ) * (map v p).mahlerMeasure ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
have grw₄ : (↑(p.natDegree.choose n) : ℝ) * (map v p).mahlerMeasure ≤ (↑(p.natDegree.choose n) : ℝ) * (map v p).mahlerMeasure
Tactic: grw [hv_norm, hcoeff, norm_coeff_le_choose_mul_mahlerMeasure,
    natDegree_map_eq_of_injective hv.injective, mapMahlerMeasure]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Norm (goal)
Goal:
A : Type u_1
inst : SeminormedRing A
p : A[X]
⊢ p.supNorm = if hp : p.support.Nonempty then p.support.sup' hp (norm ∘ p.coeff) else 0
have pos : ∀ (h : p.support.Nonempty), p.supNorm = p.support.sup' h (norm ∘ p.coeff)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Norm (goal)
Goal:
A : Type u_1
inst : SeminormedRing A
p : A[X]
pos : ∀ (h : p.support.Nonempty), p.supNorm = p.support.sup' h (norm ∘ p.coeff)
⊢ p.supNorm = if hp : p.support.Nonempty then p.support.sup' hp (norm ∘ p.coeff) else 0
have neg : ∀ (h : ¬p.support.Nonempty), p.supNorm = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Norm (goal)
Goal:
A : Type u_1
inst : SeminormedRing A
p : A[X]
h : p.support.Nonempty
⊢ p.supNorm = p.support.sup' h (norm ∘ p.coeff)
have pos : Eq (α := ℝ) (p.support.sup' sorry fun (x : ℕ) ↦ (SeminormedRing.toRingSeminorm A : (a : A) → ℝ) (p.coeff x))
  (p.support.sup' sorry fun (x : ℕ) ↦ ‖p.coeff x‖)
Tactic: simp only [supNorm, gaussNorm, h, ↓reduceDIte, one_pow, mul_one, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Norm (goal)
Goal:
A : Type u_1
inst : SeminormedRing A
p : A[X]
⊢ 0 ≤ p.supNorm
have hc : LE.le (α := ℝ) 0 1
Tactic: apply gaussNorm_nonneg
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Norm (goal)
Goal:
A : Type u_1
inst : SeminormedRing A
n : ℕ
a : A
⊢ supNorm.{u_1} (A := A) ((monomial n : (a : A) → A[X]) a) = ‖a‖
have pos : ∀ (ha : a = 0), supNorm.{u_1} (A := A) ((monomial n : (a : A) → A[X]) a) = ‖a‖
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Norm (goal)
Goal:
A : Type u_1
inst : SeminormedRing A
n : ℕ
a : A
pos : ∀ (ha : a = 0), supNorm.{u_1} (A := A) ((monomial n : (a : A) → A[X]) a) = ‖a‖
⊢ supNorm.{u_1} (A := A) ((monomial n : (a : A) → A[X]) a) = ‖a‖
have neg : ∀ (ha : ¬a = 0), supNorm.{u_1} (A := A) ((monomial n : (a : A) → A[X]) a) = ‖a‖
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Norm (goal)
Goal:
A : Type u_1
inst : SeminormedRing A
inst_1 : NormOneClass A
⊢ supNorm.{u_1} (A := A) X = 1
have rw : supNorm.{u_1} (A := A) ((monomial 1 : (a : A) → A[X]) 1) = 1
Tactic: rw [← monomial_one_one_eq_X, supNorm_monomial, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Norm (goal)
Goal:
A : Type u_1
inst : SeminormedRing A
inst_1 : NormOneClass A
rw : supNorm.{u_1} (A := A) ((monomial 1 : (a : A) → A[X]) 1) = 1
⊢ supNorm.{u_1} (A := A) X = 1
have rw₁ : norm.{u_1} (E := A) 1 = 1
Tactic: rw [← monomial_one_one_eq_X, supNorm_monomial, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Norm (goal)
Goal:
A : Type u_1
inst : SeminormedRing A
inst_1 : NormOneClass A
rw : supNorm.{u_1} (A := A) ((monomial 1 : (a : A) → A[X]) 1) = 1
rw₁ : norm.{u_1} (E := A) 1 = 1
⊢ supNorm.{u_1} (A := A) X = 1
have rw₂ : Eq (α := ℝ) 1 1
Tactic: rw [← monomial_one_one_eq_X, supNorm_monomial, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 ≤ P.leadingCoeff
⊢ 0 < P.leadingCoeff
have contrapose! : ∀ (hroots : P.leadingCoeff ≤ 0), ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y
Tactic: contrapose! hroots
Cleared hypotheses: hroots
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (hypothesis)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 ≤ P.leadingCoeff
⊢ 0 < eval x P
have hlc₁ : 0 < P.leadingCoeff
Tactic: replace hlc : 0 < P.leadingCoeff := by
    contrapose! hroots
    exact ⟨x, by simp [leadingCoeff_eq_zero.mp <| eq_of_le_of_ge hroots hlc], le_refl x⟩
Cleared hypotheses: hlc
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 < P.leadingCoeff
⊢ 0 < eval x P
have pos : ∀ (hdeg : P.degree ≤ 0), 0 < eval x P
Tactic: by_cases! hdeg : P.degree ≤ 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 < P.leadingCoeff
pos : ∀ (hdeg : P.degree ≤ 0), 0 < eval x P
⊢ 0 < eval x P
have neg : ∀ (hdeg : 0 < P.degree), 0 < eval x P
Tactic: by_cases! hdeg : P.degree ≤ 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 < P.leadingCoeff
hdeg : P.degree ≤ 0
⊢ 0 < eval x P
have pos : 0 < eval x ((C : (a : ℝ) → ℝ[X]) (P.coeff 0))
Tactic: rwa [eq_C_of_degree_le_zero hdeg, ← natDegree_eq_zero_iff_degree_le_zero.mpr hdeg, eval_C]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 < P.leadingCoeff
hdeg : P.degree ≤ 0
pos : 0 < eval x ((C : (a : ℝ) → ℝ[X]) (P.coeff 0))
⊢ 0 < eval x P
have pos₁ : 0 < eval x ((C : (a : ℝ) → ℝ[X]) (P.coeff P.natDegree))
Tactic: rwa [eq_C_of_degree_le_zero hdeg, ← natDegree_eq_zero_iff_degree_le_zero.mpr hdeg, eval_C]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 < P.leadingCoeff
hdeg : P.degree ≤ 0
pos : 0 < eval x ((C : (a : ℝ) → ℝ[X]) (P.coeff 0))
pos₁ : 0 < eval x ((C : (a : ℝ) → ℝ[X]) (P.coeff P.natDegree))
⊢ 0 < eval x P
have pos₂ : 0 < P.coeff P.natDegree
Tactic: rwa [eq_C_of_degree_le_zero hdeg, ← natDegree_eq_zero_iff_degree_le_zero.mpr hdeg, eval_C]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 < P.leadingCoeff
hdeg : 0 < P.degree
⊢ 0 < eval x P
have neg : ∀ (hroots : eval x P ≤ 0), ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y
Tactic: contrapose! hroots
Cleared hypotheses: hroots
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hlc : 0 < P.leadingCoeff
hdeg : 0 < P.degree
hroots : eval x P ≤ 0
⊢ ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y
have neg : ∀ (z : ℝ) (hz : ∀ b ≥ z, 0 < eval b P), ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y
Tactic: obtain ⟨z, hz⟩ := Filter.Eventually.exists_forall_of_atTop <|
    (P.tendsto_atTop_of_leadingCoeff_nonneg hdeg hlc.le).eventually_gt_atTop 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (hypothesis)
Goal:
P : ℝ[X]
x : ℝ
hlc : 0 < P.leadingCoeff
hdeg : 0 < P.degree
hroots : eval x P ≤ 0
z : ℝ
hz : ∀ b ≥ z, 0 < eval b P
w : ℝ := max x z
⊢ ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y
have hw : x ≤ w ∧ 0 < eval w P
Tactic: have hw : x ≤ w ∧ 0 < P.eval w := ⟨le_max_left .., hz w (le_max_right ..)⟩
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hlc : 0 < P.leadingCoeff
hdeg : 0 < P.degree
hroots : eval x P ≤ 0
z : ℝ
hz : ∀ b ≥ z, 0 < eval b P
w : ℝ := max x z
hw : x ≤ w ∧ 0 < eval w P
⊢ ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y
have neg : ∀ (y : ℝ) (hy : y ∈ Set.Icc x w ∧ eval y P = 0), ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y
Tactic: obtain ⟨y, hy⟩ := (Set.mem_image ..).mp
    (intermediate_value_Icc hw.1 P.continuous.continuousOn (show 0 ∈ _ by grind))
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : 0 ≤ P.leadingCoeff
⊢ 0 ≤ eval x P
have pos : ∀ (hroots' : ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y), 0 ≤ eval x P
Tactic: by_cases! hroots' : ∃ y, P.IsRoot y ∧ x ≤ y
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : 0 ≤ P.leadingCoeff
pos : ∀ (hroots' : ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y), 0 ≤ eval x P
⊢ 0 ≤ eval x P
have neg : ∀ (hroots' : ∀ (y : ℝ) (_ : P.IsRoot y), y < x), 0 ≤ eval x P
Tactic: by_cases! hroots' : ∃ y, P.IsRoot y ∧ x ≤ y
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : 0 ≤ P.leadingCoeff
hroots' : ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y
⊢ 0 ≤ eval x P
have pos : ∀ (y : ℝ) (hroot : P.IsRoot y) (hle : x ≤ y), 0 ≤ eval x P
Tactic: obtain ⟨y, hroot, hle⟩ := hroots'
Cleared hypotheses: hroots'
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : 0 ≤ P.leadingCoeff
y : ℝ
hroot : P.IsRoot y
hle : x ≤ y
⊢ 0 ≤ eval x P
have pos : 0 ≤ eval y P
Tactic: rw [eq_of_le_of_ge hle (hroots y hroot), hroot]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : 0 ≤ P.leadingCoeff
y : ℝ
hroot : P.IsRoot y
hle : x ≤ y
pos : 0 ≤ eval y P
⊢ 0 ≤ eval x P
have pos₁ : LE.le (α := ℝ) 0 0
Tactic: rw [eq_of_le_of_ge hle (hroots y hroot), hroot]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
this : 0 < eval x (-P)
⊢ eval x P < 0
have apply : 0 < -eval x P
Tactic: apply neg_pos.mp
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
⊢ eval x P < 0
have suffices : 0 < eval x (-P)
Tactic: suffices 0 < (-P).eval x by apply neg_pos.mp; rwa [← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
⊢ 0 < eval x (-P)
have refine_1 : ∀ (y : ℝ) (hy : (-P).IsRoot y), P.IsRoot y
Tactic: refine zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
refine_1 : ∀ (y : ℝ) (hy : (-P).IsRoot y), P.IsRoot y
⊢ 0 < eval x (-P)
have refine_2 : 0 ≤ (-P).leadingCoeff
Tactic: refine zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ P.IsRoot y
have refine_1 : eval y P = 0
Tactic: rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
refine_1 : eval y P = 0
⊢ P.IsRoot y
have refine_1₁ : eval y P = -0
Tactic: rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
refine_1 : eval y P = 0
refine_1₁ : eval y P = -0
⊢ P.IsRoot y
have refine_1₂ : -eval y P = 0
Tactic: rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
refine_1 : eval y P = 0
refine_1₁ : eval y P = -0
refine_1₂ : -eval y P = 0
⊢ P.IsRoot y
have refine_1₃ : eval y (-P) = 0
Tactic: rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
⊢ 0 ≤ (-P).leadingCoeff
have refine_2 : 0 ≤ -P.leadingCoeff
Tactic: rwa [leadingCoeff_neg, le_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
refine_2 : 0 ≤ -P.leadingCoeff
⊢ 0 ≤ (-P).leadingCoeff
have refine_2₁ : P.leadingCoeff ≤ -0
Tactic: rwa [leadingCoeff_neg, le_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
this : 0 ≤ eval x (-P)
⊢ eval x P ≤ 0
have apply : 0 ≤ -eval x P
Tactic: apply neg_nonneg.mp
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
⊢ eval x P ≤ 0
have suffices : 0 ≤ eval x (-P)
Tactic: suffices 0 ≤ (-P).eval x by apply neg_nonneg.mp; rwa [← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
⊢ 0 ≤ eval x (-P)
have refine_1 : ∀ (y : ℝ) (hy : (-P).IsRoot y), P.IsRoot y
Tactic: refine zero_le_eval_of_roots_le_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
refine_1 : ∀ (y : ℝ) (hy : (-P).IsRoot y), P.IsRoot y
⊢ 0 ≤ eval x (-P)
have refine_2 : 0 ≤ (-P).leadingCoeff
Tactic: refine zero_le_eval_of_roots_le_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ P.IsRoot y
have refine_1 : eval y P = 0
Tactic: rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
refine_1 : eval y P = 0
⊢ P.IsRoot y
have refine_1₁ : eval y P = -0
Tactic: rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
refine_1 : eval y P = 0
refine_1₁ : eval y P = -0
⊢ P.IsRoot y
have refine_1₂ : -eval y P = 0
Tactic: rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
refine_1 : eval y P = 0
refine_1₁ : eval y P = -0
refine_1₂ : -eval y P = 0
⊢ P.IsRoot y
have refine_1₃ : eval y (-P) = 0
Tactic: rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
⊢ 0 ≤ (-P).leadingCoeff
have refine_2 : 0 ≤ -P.leadingCoeff
Tactic: rwa [leadingCoeff_neg, neg_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
y : ℝ
hy : (P.comp (-X)).IsRoot y
⊢ P.IsRoot (-y)
have rwa : ∀ (hy : eval y (P.comp (-X)) = 0), P.IsRoot (-y)
Tactic: rwa [IsRoot.def, eval_comp, eval_neg, eval_X, ← IsRoot.def] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
y : ℝ
hy : (P.comp (-X)).IsRoot y
rwa : ∀ (hy : eval y (P.comp (-X)) = 0), P.IsRoot (-y)
⊢ P.IsRoot (-y)
have rwa₁ : ∀ (hy : eval (eval y (-X)) P = 0), P.IsRoot (-y)
Tactic: rwa [IsRoot.def, eval_comp, eval_neg, eval_X, ← IsRoot.def] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
y : ℝ
hy : (P.comp (-X)).IsRoot y
rwa : ∀ (hy : eval y (P.comp (-X)) = 0), P.IsRoot (-y)
rwa₁ : ∀ (hy : eval (eval y (-X)) P = 0), P.IsRoot (-y)
⊢ P.IsRoot (-y)
have rwa₂ : ∀ (hy : eval (-eval y X) P = 0), P.IsRoot (-y)
Tactic: rwa [IsRoot.def, eval_comp, eval_neg, eval_X, ← IsRoot.def] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
y : ℝ
hy : (P.comp (-X)).IsRoot y
rwa : ∀ (hy : eval y (P.comp (-X)) = 0), P.IsRoot (-y)
rwa₁ : ∀ (hy : eval (eval y (-X)) P = 0), P.IsRoot (-y)
rwa₂ : ∀ (hy : eval (-eval y X) P = 0), P.IsRoot (-y)
⊢ P.IsRoot (-y)
have rwa₃ : ∀ (hy : eval (-y) P = 0), P.IsRoot (-y)
Tactic: rwa [IsRoot.def, eval_comp, eval_neg, eval_X, ← IsRoot.def] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
y : ℝ
hy : (P.comp (-X)).IsRoot y
rwa : ∀ (hy : eval y (P.comp (-X)) = 0), P.IsRoot (-y)
rwa₁ : ∀ (hy : eval (eval y (-X)) P = 0), P.IsRoot (-y)
rwa₂ : ∀ (hy : eval (-eval y X) P = 0), P.IsRoot (-y)
rwa₃ : ∀ (hy : eval (-y) P = 0), P.IsRoot (-y)
⊢ P.IsRoot (-y)
have rwa₄ : ∀ (hy : P.IsRoot (-y)), P.IsRoot (-y)
Tactic: rwa [IsRoot.def, eval_comp, eval_neg, eval_X, ← IsRoot.def] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (hypothesis)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
⊢ 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
have hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
Tactic: have hroots' y (hy : (P.comp (-X)).IsRoot y) : y < -x := by
    grind [show P.IsRoot (-y) by rwa [IsRoot.def, eval_comp, eval_neg, eval_X, ← IsRoot.def] at hy]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
⊢ (P.comp (-X)).leadingCoeff = P.leadingCoeff * (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ)
have simp : HPow.hPow (α := ℝ) (-1) P.natDegree * P.leadingCoeff = P.leadingCoeff * HPow.hPow (α := ℝ) (-1) P.natDegree
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑(P.comp (-X)).natDegree : ℤ)) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff
have rw : 0 ≤
  P.leadingCoeff *
    HMul.hMul (α := ℝ) (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ)
Tactic: rw [show (P.comp (-X)).leadingCoeff = P.leadingCoeff * Int.negOnePow P.natDegree by simp; ring,
      show (P.comp (-X)).natDegree = P.natDegree by simp [natDegree_comp], mul_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (hypothesis)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
⊢ 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
have hlc' : 0 ≤ (↑(↑(Int.negOnePow (↑(P.comp (-X)).natDegree : ℤ)) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff
Tactic: have hlc' : 0 ≤ Int.negOnePow (P.comp (-X)).natDegree * (P.comp (-X)).leadingCoeff := by
    rw [show (P.comp (-X)).leadingCoeff = P.leadingCoeff * Int.negOnePow P.natDegree by simp; ring,
      show (P.comp (-X)).natDegree = P.natDegree by simp [natDegree_comp], mul_comm, mul_assoc]
    simpa [Int.cast_negOnePow_natCast, pow_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
hlc' : 0 ≤ (↑(↑(Int.negOnePow (↑(P.comp (-X)).natDegree : ℤ)) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff
⊢ 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
have inl : Even P.natDegree → 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
Tactic: cases P.natDegree.even_or_odd
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
hlc' : 0 ≤ (↑(↑(Int.negOnePow (↑(P.comp (-X)).natDegree : ℤ)) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff
inl : Even P.natDegree → 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
⊢ 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
have inr : Odd P.natDegree → 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
Tactic: cases P.natDegree.even_or_odd
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
hlc' : 0 ≤ (↑(↑(Int.negOnePow (↑(P.comp (-X)).natDegree : ℤ)) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff
h : Even P.natDegree
⊢ 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
have rw : ∀ (hlc' : 0 ≤ (↑(↑1 : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff) (h : Even P.natDegree), 0 < (↑(↑1 : ℤ) : ℝ) * eval x P
Tactic: rw [Int.negOnePow_even] at hlc' ⊢
Cleared hypotheses: hlc', h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
hlc' : 0 ≤ (↑(↑(Int.negOnePow (↑(P.comp (-X)).natDegree : ℤ)) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff
h : Even P.natDegree
rw : ∀ (hlc' : 0 ≤ (↑(↑1 : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff) (h : Even P.natDegree), 0 < (↑(↑1 : ℤ) : ℝ) * eval x P
⊢ 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
have hn : ∀ (hlc' : 0 ≤ (↑(↑1 : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff) (h : Even P.natDegree), Even (α := ℤ) (↑P.natDegree : ℤ)
Tactic: rw [Int.negOnePow_even] at hlc' ⊢
Cleared hypotheses: hlc', h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
hlc' : 0 ≤ (↑(↑(Int.negOnePow (↑(P.comp (-X)).natDegree : ℤ)) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff
h : Even P.natDegree
rw : ∀ (hlc' : 0 ≤ (↑(↑1 : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff) (h : Even P.natDegree), 0 < (↑(↑1 : ℤ) : ℝ) * eval x P
hn :
  ∀ (hlc' : 0 ≤ (↑(↑1 : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff) (h : Even P.natDegree), Even (α := ℤ) (↑P.natDegree : ℤ)
⊢ 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
have hn₁ : Even (α := ℤ) (↑(P.comp (-X)).natDegree : ℤ)
Tactic: rw [Int.negOnePow_even] at hlc' ⊢