awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 ≤ P.leadingCoeff
⊢ 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⟩
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 < P.leadingCoeff
pos : ∀ (hdeg : P.degree ≤ 0), 0 < eval x P
neg : ∀ (hdeg : 0 < P.degree), 0 < eval x P
⊢ 0 < eval x P

Tactic:
by_cases! hdeg : P.degree ≤ 0

Premises used: Polynomial.degree
-- Module: Mathlib.Analysis.Polynomial.Order
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))
pos₂ pos₃ pos₄ pos₅ : 0 < P.coeff P.natDegree
⊢ 0 < eval x P

Tactic:
rwa [eq_C_of_degree_le_zero hdeg, ← natDegree_eq_zero_iff_degree_le_zero.mpr hdeg, eval_C]

Premises used: Iff.mpr, Polynomial.eval_C, Polynomial.eq_C_of_degree_le_zero, Polynomial.natDegree_eq_zero_iff_degree_le_zero
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 < P.leadingCoeff
hdeg : 0 < P.degree
neg : ∀ (hroots : eval x P ≤ 0), ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y
⊢ 0 < eval x P

Tactic:
contrapose! hroots
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hlc : 0 < P.leadingCoeff
hdeg : 0 < P.degree
hroots : eval x P ≤ 0
neg : ∀ (z : ℝ) (hz : ∀ b ≥ z, 0 < eval b P), ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y
⊢ ∃ (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

Premises used: LT.lt.le, Polynomial.tendsto_atTop_of_leadingCoeff_nonneg, OfNat.ofNat, Filter.Tendsto.eventually_gt_atTop, Filter.Eventually.exists_forall_of_atTop
-- Module: Mathlib.Analysis.Polynomial.Order
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
⊢ x ≤ w ∧ 0 < eval w P

Tactic:
have hw : x ≤ w ∧ 0 < P.eval w := ⟨le_max_left .., hz w (le_max_right ..)⟩
-- Module: Mathlib.Analysis.Polynomial.Order
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
⊢ 0 ∈ Set.Icc (eval x P) (eval w P)

Tactic:
grind
-- Module: Mathlib.Analysis.Polynomial.Order
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
neg : ∀ (y : ℝ) (hy : y ∈ Set.Icc x w ∧ eval y P = 0), ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y
⊢ ∃ (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))

Premises used: Polynomial.continuous, Continuous.continuousOn, Set.mem_image, And.left, intermediate_value_Icc, Iff.mp
-- Module: Mathlib.Analysis.Polynomial.Order
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 : ℝ
hy : y ∈ Set.Icc x w ∧ eval y P = 0
⊢ x ≤ y

Tactic:
grind
-- Module: Mathlib.Analysis.Polynomial.Order
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 : ℝ
hy : y ∈ Set.Icc x w ∧ eval y P = 0
⊢ ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y

Tactic:
exact ⟨y, ⟨hy.2, by grind⟩⟩
-- Module: Mathlib.Analysis.Polynomial.Order
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
neg : ∀ (hroots' : ∀ (y : ℝ) (_ : P.IsRoot y), y < x), 0 ≤ eval x P
⊢ 0 ≤ eval x P

Tactic:
by_cases! hroots' : ∃ y, P.IsRoot y ∧ x ≤ y
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : 0 ≤ P.leadingCoeff
hroots' : ∃ (y : ℝ), P.IsRoot y ∧ x ≤ y
pos : ∀ (y : ℝ) (hroot : P.IsRoot y) (hle : x ≤ y), 0 ≤ eval x P
⊢ 0 ≤ eval x P

Tactic:
obtain ⟨y, hroot, hle⟩ := hroots'
-- Module: Mathlib.Analysis.Polynomial.Order
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
pos₁ pos₂ : LE.le (α := ℝ) 0 0
⊢ 0 ≤ eval x P

Tactic:
rw [eq_of_le_of_ge hle (hroots y hroot), hroot]

Premises used: eq_of_le_of_ge
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (_ : P.IsRoot y), y < x
⊢ 0 ≤ eval x P

Tactic:
(zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg hroots' hlc).le

Premises used: Polynomial.zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg, LT.lt.le
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (_ : P.IsRoot y), y < x
⊢ 0 ≤ eval x P

Tactic:
exact (zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg hroots' hlc).le

Premises used: Polynomial.zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg, LT.lt.le
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
this : 0 < eval x (-P)
apply : 0 < -eval x P
⊢ eval x P < 0

Tactic:
apply neg_pos.mp

Premises used: neg_pos, Iff.mp
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
this : 0 < eval x (-P)
rwa rwa₁ rwa₂ rwa₃ : 0 < eval x (-P)
⊢ 0 < -eval x P

Tactic:
rwa [← eval_neg]

Premises used: Polynomial.eval_neg
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
suffices : 0 < eval x (-P)
⊢ eval x P < 0

Tactic:
suffices 0 < (-P).eval x by apply neg_pos.mp; rwa [← eval_neg]
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
⊢ 0 < eval x (-P)

Tactic:
zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_

Premises used: Polynomial.zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg
-- Module: Mathlib.Analysis.Polynomial.Order
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
refine_2 : 0 ≤ (-P).leadingCoeff
⊢ 0 < eval x (-P)

Tactic:
refine zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_

Premises used: Polynomial.zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg
-- Module: Mathlib.Analysis.Polynomial.Order
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
refine_1₃ refine_1₄ refine_1₅ refine_1₆ : eval y (-P) = 0
⊢ P.IsRoot y

Tactic:
rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]

Premises used: Polynomial.IsRoot, neg_eq_iff_eq_neg, Polynomial.eval_neg, neg_zero
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
refine_2 : 0 ≤ -P.leadingCoeff
refine_2₁ : P.leadingCoeff ≤ -0
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : P.leadingCoeff ≤ 0
⊢ 0 ≤ (-P).leadingCoeff

Tactic:
rwa [leadingCoeff_neg, le_neg, neg_zero]

Premises used: le_neg, neg_zero, Polynomial.leadingCoeff_neg
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
this : 0 ≤ eval x (-P)
apply : 0 ≤ -eval x P
⊢ eval x P ≤ 0

Tactic:
apply neg_nonneg.mp

Premises used: neg_nonneg, Iff.mp
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
this : 0 ≤ eval x (-P)
rwa rwa₁ rwa₂ rwa₃ : 0 ≤ eval x (-P)
⊢ 0 ≤ -eval x P

Tactic:
rwa [← eval_neg]

Premises used: Polynomial.eval_neg
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
suffices : 0 ≤ eval x (-P)
⊢ eval x P ≤ 0

Tactic:
suffices 0 ≤ (-P).eval x by apply neg_nonneg.mp; rwa [← eval_neg]
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
⊢ 0 ≤ eval x (-P)

Tactic:
zero_le_eval_of_roots_le_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_

Premises used: Polynomial.zero_le_eval_of_roots_le_of_leadingCoeff_nonneg
-- Module: Mathlib.Analysis.Polynomial.Order
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
refine_2 : 0 ≤ (-P).leadingCoeff
⊢ 0 ≤ eval x (-P)

Tactic:
refine zero_le_eval_of_roots_le_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_

Premises used: Polynomial.zero_le_eval_of_roots_le_of_leadingCoeff_nonneg
-- Module: Mathlib.Analysis.Polynomial.Order
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
refine_1₃ refine_1₄ refine_1₅ refine_1₆ : eval y (-P) = 0
⊢ P.IsRoot y

Tactic:
rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]

Premises used: Polynomial.IsRoot, neg_eq_iff_eq_neg, Polynomial.eval_neg, neg_zero
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
refine_2 : 0 ≤ -P.leadingCoeff
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : P.leadingCoeff ≤ 0
⊢ 0 ≤ (-P).leadingCoeff

Tactic:
rwa [leadingCoeff_neg, neg_nonneg]

Premises used: neg_nonneg, Polynomial.leadingCoeff_neg
-- Module: Mathlib.Analysis.Polynomial.Order
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)
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (hy : P.IsRoot (-y)), P.IsRoot (-y)
⊢ P.IsRoot (-y)

Tactic:
rwa [IsRoot.def, eval_comp, eval_neg, eval_X, ← IsRoot.def] at hy

Premises used: Polynomial.eval_X, Polynomial.IsRoot.def, Polynomial.eval_comp, Polynomial.eval_neg
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
y : ℝ
hy : (P.comp (-X)).IsRoot y
⊢ y < -x

Tactic:
grind [show P.IsRoot (-y) by rwa [IsRoot.def, eval_comp, eval_neg, eval_X, ← IsRoot.def] at hy]
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
⊢ ∀ (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]
-- Module: Mathlib.Analysis.Polynomial.Order
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
simp : HPow.hPow (α := ℝ) (-1) P.natDegree * P.leadingCoeff = P.leadingCoeff * HPow.hPow (α := ℝ) (-1) P.natDegree
⊢ (P.comp (-X)).leadingCoeff = P.leadingCoeff * (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.Order
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
⊢ HPow.hPow (α := ℝ) (-1) P.natDegree * P.leadingCoeff = P.leadingCoeff * HPow.hPow (α := ℝ) (-1) P.natDegree

Tactic:
ring
-- Module: Mathlib.Analysis.Polynomial.Order
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)).natDegree = P.natDegree

Tactic:
simp [natDegree_comp]

Premises used: Polynomial.natDegree_comp
-- Module: Mathlib.Analysis.Polynomial.Order
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
rw :
  0 ≤
    P.leadingCoeff *
      HMul.hMul (α := ℝ) (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ)
        (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ)
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑(P.comp (-X)).natDegree : ℤ)) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff

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]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Analysis.Polynomial.Order
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 ≤
    P.leadingCoeff *
      HMul.hMul (α := ℝ) (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ)
        (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ)

Tactic:
simpa [Int.cast_negOnePow_natCast, pow_right_comm]

Premises used: pow_right_comm, Int.cast_negOnePow_natCast
-- Module: Mathlib.Analysis.Polynomial.Order
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

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]
-- Module: Mathlib.Analysis.Polynomial.Order
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
inr : Odd P.natDegree → 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
⊢ 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P

Tactic:
cases P.natDegree.even_or_odd

Premises used: Polynomial.natDegree, Nat.even_or_odd
-- Module: Mathlib.Analysis.Polynomial.Order
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 : ℤ)
hn₁ : Even (α := ℤ) (↑(P.comp (-X)).natDegree : ℤ)
⊢ 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P

Tactic:
rw [Int.negOnePow_even] at hlc' ⊢

Premises used: Int.negOnePow_even
-- Module: Mathlib.Analysis.Polynomial.Order
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 ≤ (↑(↑1 : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff
h : Even P.natDegree
push_cast : ∀ (hlc' : 0 ≤ 1 * (P.comp (-X)).leadingCoeff), 0 < 1 * eval x P
⊢ 0 < (↑(↑1 : ℤ) : ℝ) * eval x P

Tactic:
push_cast at hlc' ⊢
-- Module: Mathlib.Analysis.Polynomial.Order
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
h : Even P.natDegree
hlc' : 0 ≤ 1 * (P.comp (-X)).leadingCoeff
rw : ∀ (hlc' : 0 ≤ (P.comp (-X)).leadingCoeff), 0 < eval x P
⊢ 0 < 1 * eval x P

Tactic:
rw [one_mul] at hlc' ⊢

Premises used: one_mul
-- Module: Mathlib.Analysis.Polynomial.Order
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
h : Even P.natDegree
hlc' : 0 ≤ (P.comp (-X)).leadingCoeff
⊢ 0 < eval (-x) (P.comp (-X))

Tactic:
have := zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg hroots' hlc'
-- Module: Mathlib.Analysis.Polynomial.Order
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
h : Even P.natDegree
hlc' : 0 ≤ (P.comp (-X)).leadingCoeff
this : 0 < eval (-x) (P.comp (-X))
⊢ 0 < eval x P

Tactic:
simpa using this
-- Module: Mathlib.Analysis.Polynomial.Order
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 ≤ (↑(↑1 : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff
h : Even P.natDegree
⊢ Even (α := ℤ) (↑P.natDegree : ℤ)

Tactic:
simpa
-- Module: Mathlib.Analysis.Polynomial.Order
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
⊢ Even (α := ℤ) (↑(P.comp (-X)).natDegree : ℤ)

Tactic:
simpa [natDegree_comp]

Premises used: Polynomial.natDegree_comp
-- Module: Mathlib.Analysis.Polynomial.Order
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

Tactic:
case inl h =>
    rw [Int.negOnePow_even] at hlc' ⊢
    · push_cast at hlc' ⊢; rw [one_mul] at hlc' ⊢
      have := zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg hroots' hlc'
      simpa using this
    · simpa
    · simpa [natDegree_comp]

Premises used: Polynomial.natDegree_comp, Int.negOnePow_even, one_mul
-- Module: Mathlib.Analysis.Polynomial.Order
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 : Odd P.natDegree
rw :
  ∀ (hlc' : 0 ≤ (↑(↑(-1) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff) (h : Odd P.natDegree),
    0 < (↑(↑(-1) : ℤ) : ℝ) * eval x P
hn :
  ∀ (hlc' : 0 ≤ (↑(↑(-1) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff) (h : Odd P.natDegree), Odd (α := ℤ) (↑P.natDegree : ℤ)
hn₁ : Odd (α := ℤ) (↑(P.comp (-X)).natDegree : ℤ)
⊢ 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P

Tactic:
rw [Int.negOnePow_odd] at hlc' ⊢

Premises used: Int.negOnePow_odd
-- Module: Mathlib.Analysis.Polynomial.Order
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 ≤ (↑(↑(-1) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff
h : Odd P.natDegree
push_cast : ∀ (hlc' : 0 ≤ -1 * (P.comp (-X)).leadingCoeff), 0 < -1 * eval x P
⊢ 0 < (↑(↑(-1) : ℤ) : ℝ) * eval x P

Tactic:
push_cast at hlc' ⊢
-- Module: Mathlib.Analysis.Polynomial.Order
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
h : Odd P.natDegree
hlc' : 0 ≤ -1 * (P.comp (-X)).leadingCoeff
rw : ∀ (hlc' : 0 ≤ -(P.comp (-X)).leadingCoeff), 0 < -eval x P
⊢ 0 < -1 * eval x P

Tactic:
rw [neg_one_mul] at hlc' ⊢

Premises used: neg_one_mul
-- Module: Mathlib.Analysis.Polynomial.Order
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
h : Odd P.natDegree
hlc' : 0 ≤ -(P.comp (-X)).leadingCoeff
⊢ eval (-x) (P.comp (-X)) < 0

Tactic:
have := eval_lt_zero_of_roots_lt_of_leadingCoeff_nonpos hroots' (nonpos_of_neg_nonneg hlc')
-- Module: Mathlib.Analysis.Polynomial.Order
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
h : Odd P.natDegree
hlc' : 0 ≤ -(P.comp (-X)).leadingCoeff
this : eval (-x) (P.comp (-X)) < 0
⊢ eval x P < 0

Tactic:
simpa using this
-- Module: Mathlib.Analysis.Polynomial.Order
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
h : Odd P.natDegree
hlc' : 0 ≤ -(P.comp (-X)).leadingCoeff
this : eval (-x) (P.comp (-X)) < 0
⊢ 0 < -eval x P

Tactic:
exact neg_pos.mpr (by simpa using this)

Premises used: Iff.mpr, neg_pos
-- Module: Mathlib.Analysis.Polynomial.Order
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 ≤ (↑(↑(-1) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff
h : Odd P.natDegree
⊢ Odd (α := ℤ) (↑P.natDegree : ℤ)

Tactic:
simpa
-- Module: Mathlib.Analysis.Polynomial.Order
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 : Odd P.natDegree
⊢ Odd (α := ℤ) (↑(P.comp (-X)).natDegree : ℤ)

Tactic:
simpa [natDegree_comp]

Premises used: Polynomial.natDegree_comp
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : 0 ≤ P.leadingCoeff
pos : ∀ (hroots' : ∃ (y : ℝ), P.IsRoot y ∧ y ≤ x), 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
neg : ∀ (hroots' : ∀ (y : ℝ) (_ : P.IsRoot y), x < y), 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P

Tactic:
by_cases! hroots' : ∃ y, P.IsRoot y ∧ y ≤ x
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∃ (y : ℝ), P.IsRoot y ∧ y ≤ x
pos : ∀ (y : ℝ) (hroot : P.IsRoot y) (hle : y ≤ x), 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P

Tactic:
obtain ⟨y, hroot, hle⟩ := hroots'
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : 0 ≤ P.leadingCoeff
y : ℝ
hroot : P.IsRoot y
hle : y ≤ x
pos : 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval y P
pos₁ : 0 ≤ HMul.hMul (α := ℝ) (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) 0
pos₂ pos₃ : LE.le (α := ℝ) 0 0
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P

Tactic:
rw [eq_of_ge_of_le hle (hroots y hroot), hroot, mul_zero]

Premises used: eq_of_ge_of_le, MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (_ : P.IsRoot y), x < y
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P

Tactic:
(zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg hroots' hlc).le

Premises used: LT.lt.le, Polynomial.zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (_ : P.IsRoot y), x < y
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P

Tactic:
exact (zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg hroots' hlc).le

Premises used: LT.lt.le, Polynomial.zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
this : 0 < (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)
apply : 0 < -((↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P)
⊢ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P < 0

Tactic:
apply neg_pos.mp

Premises used: neg_pos, Iff.mp