awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hP : P.leadingCoeff = HPow.hPow (α := ℝ) 2 (n - 1)
lift : P.degree ≠ ⊥
lift₁ :
  ∀ (d : ℕ) (hd : (↑d : WithBot ℕ) = P.degree) (hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)),
    (↑n : WithBot ℕ) ≤ (↑d : WithBot ℕ)
⊢ (↑n : WithBot ℕ) ≤ P.degree

Tactic:
lift P.degree to ℕ with d hd

Premises used: Polynomial.degree
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hP : P.leadingCoeff = HPow.hPow (α := ℝ) 2 (n - 1)
contrapose! : ∀ (hP : P.degree = ⊥), P.leadingCoeff ≠ HPow.hPow (α := ℝ) 2 (n - 1)
⊢ P.degree ≠ ⊥

Tactic:
contrapose! hP
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hP : P.degree = ⊥
rw : 0 ≠ HPow.hPow (α := ℝ) 2 (n - 1)
⊢ P.leadingCoeff ≠ HPow.hPow (α := ℝ) 2 (n - 1)

Tactic:
rw [degree_eq_bot.mp hP, leadingCoeff_zero]

Premises used: Polynomial.leadingCoeff_zero, Iff.mp, Polynomial.degree_eq_bot
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hP : P.degree = ⊥
⊢ 0 ≠ HPow.hPow (α := ℝ) 2 (n - 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hP : P.leadingCoeff = HPow.hPow (α := ℝ) 2 (n - 1)
d : ℕ
hd : (↑d : WithBot ℕ) = P.degree
hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)
⊢ HPow.hPow (α := ℝ) 2 (n - 1) ≤ P.leadingCoeff

Tactic:
replace hP := ge_of_eq hP
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
d : ℕ
hd : (↑d : WithBot ℕ) = P.degree
hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)
hP : HPow.hPow (α := ℝ) 2 (n - 1) ≤ P.leadingCoeff
contrapose! : ∀ (hP : (↑d : WithBot ℕ) < (↑n : WithBot ℕ)), P.leadingCoeff < HPow.hPow (α := ℝ) 2 (n - 1)
⊢ (↑n : WithBot ℕ) ≤ (↑d : WithBot ℕ)

Tactic:
contrapose! hP
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
d : ℕ
hd : (↑d : WithBot ℕ) = P.degree
hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)
hP : (↑d : WithBot ℕ) < (↑n : WithBot ℕ)
⊢ d - 1 < n - 1

Tactic:
grind [Nat.cast_withBot, WithBot.coe_le_coe, WithBot.coe_lt_coe]

Premises used: WithBot.coe_le_coe, WithBot.coe_lt_coe, Nat.cast_withBot
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
d : ℕ
hd : (↑d : WithBot ℕ) = P.degree
hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)
hP : (↑d : WithBot ℕ) < (↑n : WithBot ℕ)
⊢ d - 1 < n - 1

Tactic:
have : d - 1 < n - 1 := by grind [Nat.cast_withBot, WithBot.coe_le_coe, WithBot.coe_lt_coe]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
d : ℕ
hd : (↑d : WithBot ℕ) = P.degree
hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)
hP : (↑d : WithBot ℕ) < (↑n : WithBot ℕ)
this : d - 1 < n - 1
⊢ P.leadingCoeff ≤ HPow.hPow (α := ℝ) 2 (d - 1)

Tactic:
leadingCoeff_le_of_forall_abs_le_one (le_of_eq hd.symm) hPbnd

Premises used: Polynomial.Chebyshev.leadingCoeff_le_of_forall_abs_le_one, le_of_eq, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
d : ℕ
hd : (↑d : WithBot ℕ) = P.degree
hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)
hP : (↑d : WithBot ℕ) < (↑n : WithBot ℕ)
this : d - 1 < n - 1
h : LT.lt (α := ℝ) 1 2
⊢ HPow.hPow (α := ℝ) 2 (d - 1) < HPow.hPow (α := ℝ) 2 (n - 1)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
d : ℕ
hd : (↑d : WithBot ℕ) = P.degree
hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)
hP : (↑d : WithBot ℕ) < (↑n : WithBot ℕ)
this : d - 1 < n - 1
⊢ LT.lt (α := ℝ) 1 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
d : ℕ
hd : (↑d : WithBot ℕ) = P.degree
hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)
hP : (↑d : WithBot ℕ) < (↑n : WithBot ℕ)
this : d - 1 < n - 1
calc : HPow.hPow (α := ℝ) 2 (d - 1) < HPow.hPow (α := ℝ) 2 (n - 1)
⊢ P.leadingCoeff < HPow.hPow (α := ℝ) 2 (n - 1)

Tactic:
calc P.leadingCoeff ≤ 2 ^ (d - 1) := leadingCoeff_le_of_forall_abs_le_one (le_of_eq hd.symm) hPbnd
  _ < 2 ^ (n - 1) := by gcongr; norm_num

Premises used: HSub.hSub, Polynomial.Chebyshev.leadingCoeff_le_of_forall_abs_le_one, Polynomial.leadingCoeff, le_of_eq, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
rw : P.degree < (↑(n + 1) : WithBot ℕ)
⊢ P.degree < (↑(Finset.range (n + 1)).card : WithBot ℕ)

Tactic:
rw [Finset.card_range]

Premises used: Finset.card_range
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
grw : LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑(n + 1) : WithBot ℕ)
⊢ P.degree < (↑(n + 1) : WithBot ℕ)

Tactic:
grw [hP]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
norm_cast : n < n + 1
⊢ LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑(n + 1) : WithBot ℕ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
⊢ n < n + 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
⊢ P.degree < (↑(Finset.range (n + 1)).card : WithBot ℕ)

Tactic:
have h₁ : P.degree < (Finset.range (n + 1)).card := by
    rw [Finset.card_range]; grw [hP]; norm_cast; simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
h₁ : P.degree < (↑(Finset.range (n + 1)).card : WithBot ℕ)
⊢ k < (Finset.range (n + 1)).card

Tactic:
simp [hk]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
h₁ : P.degree < (↑(Finset.range (n + 1)).card : WithBot ℕ)
h :
  ∑ x_1 ∈ Finset.Iic n,
      eval (node n x_1) P *
        (HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase x_1, (node n x_1 - node n j))⁻¹ *
          ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase x_1), ∏ a ∈ t, (x - node n a)) =
    HMul.hMul (α := ℝ) (↑k.factorial : ℝ)
      (∑ i ∈ Finset.range (n + 1),
        (eval (node n i) P / ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)) *
          ∑ t ∈ Finset.powersetCard ((Finset.range (n + 1)).card - (k + 1)) ((Finset.range (n + 1)).erase i),
            ∏ a ∈ t, (x - node n a))
⊢ ∑ x_1 ∈ Finset.Iic n,
      eval (node n x_1) P *
        (HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase x_1, (node n x_1 - node n j))⁻¹ *
          ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase x_1), ∏ a ∈ t, (x - node n a)) =
    eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P)

Tactic:
convert!
    (Lagrange.eval_iterate_derivative_eq_sum (strictAntiOn_node n).injOn h₁
        (show k < _ by simp [hk]) x).symm

Premises used: Lagrange.eval_iterate_derivative_eq_sum, Polynomial.Chebyshev.strictAntiOn_node, StrictAntiOn.injOn, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
h₁ : P.degree < (↑(Finset.range (n + 1)).card : WithBot ℕ)
h :
  Eq (α := ℝ)
    (∑ x_1 ∈ Finset.Iic n,
      eval (node n x_1) P *
        (HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase x_1, (node n x_1 - node n j))⁻¹ *
          ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase x_1), ∏ a ∈ t, (x - node n a)))
    (∑ i ∈ Finset.range (n + 1),
      (↑k.factorial : ℝ) *
        ((eval (node n i) P / ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)) *
          ∑ t ∈ Finset.powersetCard ((Finset.range (n + 1)).card - (k + 1)) ((Finset.range (n + 1)).erase i),
            ∏ a ∈ t, (x - node n a)))
⊢ ∑ x_1 ∈ Finset.Iic n,
      eval (node n x_1) P *
        (HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase x_1, (node n x_1 - node n j))⁻¹ *
          ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase x_1), ∏ a ∈ t, (x - node n a)) =
    HMul.hMul (α := ℝ) (↑k.factorial : ℝ)
      (∑ i ∈ Finset.range (n + 1),
        (eval (node n i) P / ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)) *
          ∑ t ∈ Finset.powersetCard ((Finset.range (n + 1)).card - (k + 1)) ((Finset.range (n + 1)).erase i),
            ∏ a ∈ t, (x - node n a))

Tactic:
rw [Finset.mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
h₁ : P.degree < (↑(Finset.range (n + 1)).card : WithBot ℕ)
⊢ Eq (α := ℝ)
    (∑ x_1 ∈ Finset.Iic n,
      eval (node n x_1) P *
        (HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase x_1, (node n x_1 - node n j))⁻¹ *
          ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase x_1), ∏ a ∈ t, (x - node n a)))
    (∑ i ∈ Finset.range (n + 1),
      (↑k.factorial : ℝ) *
        ((eval (node n i) P / ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)) *
          ∑ t ∈ Finset.powersetCard ((Finset.range (n + 1)).card - (k + 1)) ((Finset.range (n + 1)).erase i),
            ∏ a ∈ t, (x - node n a)))

Tactic:
grind [Nat.range_succ_eq_Iic, Nat.card_Iic]

Premises used: Nat.range_succ_eq_Iic, Nat.card_Iic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
rw :
  0 ≤
    HPow.hPow (α := ℝ) (-1) i *
        HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)
⊢ 0 ≤ HPow.hPow (α := ℝ) (-1) i * iterateDerivativeC n k x i

Tactic:
rw [iterateDerivativeC, ← mul_assoc]

Premises used: _private.0.Polynomial.Chebyshev.iterateDerivativeC, mul_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤
    HPow.hPow (α := ℝ) (-1) i *
        HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)

Tactic:
mul_nonneg ?_ (Finset.sum_nonneg' ?_)

Premises used: mul_nonneg, Finset.sum_nonneg'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
refine_1 :
  0 ≤
    HPow.hPow (α := ℝ) (-1) i *
      HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
refine_2 : ∀ (i : Finset ℕ), LE.le (α := ℝ) 0 (∏ a ∈ i, (x - node n a))
⊢ 0 ≤
    HPow.hPow (α := ℝ) (-1) i *
        HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)

Tactic:
refine mul_nonneg ?_ (Finset.sum_nonneg' ?_)

Premises used: mul_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
refine_1 :
  0 ≤ (↑k.factorial : ℝ) * (HPow.hPow (α := ℝ) (-1) i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)
⊢ 0 ≤
    HPow.hPow (α := ℝ) (-1) i *
      HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹

Tactic:
rw [← mul_assoc, mul_comm (a := (-1) ^ i), mul_assoc]

Premises used: mul_assoc, HPow.hPow, mul_comm, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ (↑k.factorial : ℝ) * (HPow.hPow (α := ℝ) (-1) i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)

Tactic:
le_of_lt <| mul_pos (Nat.cast_pos.mpr <| Nat.factorial_pos k)
      (negOnePow_mul_leadingCoeffC_pos hi)

Premises used: Iff.mpr, Nat.cast_pos, le_of_lt, mul_pos, _private.0.Polynomial.Chebyshev.negOnePow_mul_leadingCoeffC_pos, Nat.factorial_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ (↑k.factorial : ℝ) * (HPow.hPow (α := ℝ) (-1) i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)

Tactic:
exact le_of_lt <| mul_pos (Nat.cast_pos.mpr <| Nat.factorial_pos k)
      (negOnePow_mul_leadingCoeffC_pos hi)

Premises used: Iff.mpr, Nat.cast_pos, le_of_lt, mul_pos, _private.0.Polynomial.Chebyshev.negOnePow_mul_leadingCoeffC_pos, Nat.factorial_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
t : Finset ℕ
a : ℕ
h : a ∈ t
⊢ 0 ≤ x - node n a

Tactic:
grind [show node n a ≤ 1 from cos_le_one _]

Premises used: Real.pi, HMul.hMul, HDiv.hDiv, Nat.cast, Real.cos_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∀ (i : Finset ℕ), LE.le (α := ℝ) 0 (∏ a ∈ i, (x - node n a))

Tactic:
exact fun t => Finset.prod_nonneg (fun a _ => by grind [show node n a ≤ 1 from cos_le_one _])

Premises used: Finset.prod_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
rw :
  0 <
    HPow.hPow (α := ℝ) (-1) i *
        HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * iterateDerivativeC n k x i

Tactic:
rw [iterateDerivativeC, ← mul_assoc]

Premises used: _private.0.Polynomial.Chebyshev.iterateDerivativeC, mul_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 <
    HPow.hPow (α := ℝ) (-1) i *
        HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)

Tactic:
mul_pos ?_ (Finset.sum_pos' ?_ ?_)

Premises used: Finset.sum_pos', mul_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
refine_1 :
  0 <
    HPow.hPow (α := ℝ) (-1) i *
      HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
refine_2 :
  ∀ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), LE.le (α := ℝ) 0 (∏ a ∈ i_1, (x - node n a))
refine_3 :
  ∃ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), LT.lt (α := ℝ) 0 (∏ a ∈ i_1, (x - node n a))
⊢ 0 <
    HPow.hPow (α := ℝ) (-1) i *
        HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)

Tactic:
refine mul_pos ?_ (Finset.sum_pos' ?_ ?_)

Premises used: mul_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
refine_1 :
  0 < (↑k.factorial : ℝ) * (HPow.hPow (α := ℝ) (-1) i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)
⊢ 0 <
    HPow.hPow (α := ℝ) (-1) i *
      HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹

Tactic:
rw [← mul_assoc, mul_comm (a := (-1) ^ i), mul_assoc]

Premises used: mul_assoc, HPow.hPow, mul_comm, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 < (↑k.factorial : ℝ) * (HPow.hPow (α := ℝ) (-1) i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)

Tactic:
mul_pos (Nat.cast_pos.mpr <| Nat.factorial_pos k) (negOnePow_mul_leadingCoeffC_pos hi)

Premises used: Iff.mpr, Nat.cast_pos, mul_pos, _private.0.Polynomial.Chebyshev.negOnePow_mul_leadingCoeffC_pos, Nat.factorial_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 < (↑k.factorial : ℝ) * (HPow.hPow (α := ℝ) (-1) i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)

Tactic:
exact mul_pos (Nat.cast_pos.mpr <| Nat.factorial_pos k) (negOnePow_mul_leadingCoeffC_pos hi)

Premises used: Iff.mpr, Nat.cast_pos, mul_pos, _private.0.Polynomial.Chebyshev.negOnePow_mul_leadingCoeffC_pos, Nat.factorial_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
t : Finset ℕ
h : t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i)
a : ℕ
h_1 : a ∈ t
⊢ 0 ≤ x - node n a

Tactic:
grind [show node n a ≤ 1 from cos_le_one _]

Premises used: Real.pi, HMul.hMul, HDiv.hDiv, Nat.cast, Real.cos_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∀ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), LE.le (α := ℝ) 0 (∏ a ∈ i_1, (x - node n a))

Tactic:
exact fun t _ => Finset.prod_nonneg (fun a _ => by grind [show node n a ≤ 1 from cos_le_one _])

Premises used: Finset.prod_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
by_cases : 1 ≤ i ∧ i ≤ n - k → ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s
by_cases₁ : ¬(1 ≤ i ∧ i ≤ n - k) → ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s
⊢ ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s

Tactic:
by_cases 1 ≤ i ∧ i ≤ n - k
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
h : ¬(1 ≤ i ∧ i ≤ n - k)
⊢ Finset.Icc 1 (n - k) ⊆ (Finset.range (n + 1)).erase i

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
h : ¬(1 ≤ i ∧ i ≤ n - k)
⊢ (Finset.Icc 1 (n - k)).card = n - k

Tactic:
grind [Nat.card_Icc]

Premises used: Nat.card_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
h : ¬(1 ≤ i ∧ i ≤ n - k)
⊢ 0 ∉ Finset.Icc 1 (n - k)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
h : ¬(1 ≤ i ∧ i ≤ n - k)
⊢ ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s

Tactic:
exact ⟨Finset.Icc 1 (n - k), by grind, by grind [Nat.card_Icc], by simp⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
h : ¬(1 ≤ i ∧ i ≤ n - k)
⊢ ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s

Tactic:
case neg => exact ⟨Finset.Icc 1 (n - k), by grind, by grind [Nat.card_Icc], by simp⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
h : 1 ≤ i ∧ i ≤ n - k
⊢ (Finset.Icc 1 (n - k + 1)).erase i ⊆ (Finset.range (n + 1)).erase i

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
h : 1 ≤ i ∧ i ≤ n - k
⊢ ((Finset.Icc 1 (n - k + 1)).erase i).card = n - k

Tactic:
grind [Nat.card_Icc]

Premises used: Nat.card_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
h : 1 ≤ i ∧ i ≤ n - k
⊢ 0 ∉ (Finset.Icc 1 (n - k + 1)).erase i

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
h : 1 ≤ i ∧ i ≤ n - k
⊢ ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s

Tactic:
exact ⟨(Finset.Icc 1 (n - k + 1)).erase i, by grind, by grind [Nat.card_Icc],
        by simp⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
h : 1 ≤ i ∧ i ≤ n - k
⊢ ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s

Tactic:
case pos => exact ⟨(Finset.Icc 1 (n - k + 1)).erase i, by grind, by grind [Nat.card_Icc],
        by simp⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s

Tactic:
have : ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s := by
      by_cases 1 ≤ i ∧ i ≤ n - k
      case neg => exact ⟨Finset.Icc 1 (n - k), by grind, by grind [Nat.card_Icc], by simp⟩
      case pos => exact ⟨(Finset.Icc 1 (n - k + 1)).erase i, by grind, by grind [Nat.card_Icc],
        by simp⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
this : ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s
refine_3 :
  ∀ (s : Finset ℕ) (hs : s ⊆ (Finset.range (n + 1)).erase i) (hscard : s.card = n - k) (hsn : 0 ∉ s),
    ∃ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), LT.lt (α := ℝ) 0 (∏ a ∈ i_1, (x - node n a))
⊢ ∃ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), LT.lt (α := ℝ) 0 (∏ a ∈ i_1, (x - node n a))

Tactic:
obtain ⟨s, hs, hscard, hsn⟩ := this
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
⊢ s ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i)

Tactic:
simp [hs, hscard]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
refine_3 : ∀ (a : ℕ) (ha : a ∈ s), 0 < x - node n a
⊢ ∃ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), LT.lt (α := ℝ) 0 (∏ a ∈ i_1, (x - node n a))

Tactic:
refine ⟨s, by simp [hs, hscard], Finset.prod_pos (fun a ha => ?_)⟩