awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < HPow.hPow (α := ℝ) (-1) i * c i
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
x : ℝ
hx : Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1))) x
hPx : eval x P ≠ eval x (T ℝ (↑n : ℤ))
i_1 : ℕ
hix : node n i_1 = x
hi_1 : i_1 ∈ Finset.Iic n
i : ℕ
hi : i ∈ Finset.Iic n
⊢ HPow.hPow (α := ℝ) (-1) i * eval (node n i) P * (HPow.hPow (α := ℝ) (-1) i * c i) ≤
    HPow.hPow (α := ℝ) (-1) i * eval (node n i) (T ℝ (↑n : ℤ)) * (HPow.hPow (α := ℝ) (-1) i * c i)

Tactic:
mul_le_mul_of_nonneg_right ?_ (le_of_lt (hcpos i (Finset.mem_Iic.mp hi)))

Premises used: Finset.mem_Iic, le_of_lt, mul_le_mul_of_nonneg_right, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < HPow.hPow (α := ℝ) (-1) i * c i
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
x : ℝ
hx : Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1))) x
hPx : eval x P ≠ eval x (T ℝ (↑n : ℤ))
i_1 : ℕ
hix : node n i_1 = x
hi_1 : i_1 ∈ Finset.Iic n
i : ℕ
hi : i ∈ Finset.Iic n
refine : HPow.hPow (α := ℝ) (-1) i * eval (node n i) P ≤ HPow.hPow (α := ℝ) (-1) i * eval (node n i) (T ℝ (↑n : ℤ))
⊢ HPow.hPow (α := ℝ) (-1) i * eval (node n i) P * (HPow.hPow (α := ℝ) (-1) i * c i) ≤
    HPow.hPow (α := ℝ) (-1) i * eval (node n i) (T ℝ (↑n : ℤ)) * (HPow.hPow (α := ℝ) (-1) i * c i)

Tactic:
refine mul_le_mul_of_nonneg_right ?_ (le_of_lt (hcpos i (Finset.mem_Iic.mp hi)))

Premises used: Finset.mem_Iic, le_of_lt, mul_le_mul_of_nonneg_right, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < HPow.hPow (α := ℝ) (-1) i * c i
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
x : ℝ
hx : Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1))) x
hPx : eval x P ≠ eval x (T ℝ (↑n : ℤ))
i_1 : ℕ
hix : node n i_1 = x
hi_1 : i_1 ∈ Finset.Iic n
i : ℕ
hi : i ∈ Finset.Iic n
rw : HPow.hPow (α := ℝ) (-1) i * eval (node n i) P ≤ 1
⊢ HPow.hPow (α := ℝ) (-1) i * eval (node n i) P ≤ HPow.hPow (α := ℝ) (-1) i * eval (node n i) (T ℝ (↑n : ℤ))

Tactic:
rw [eval_T_real_node hi, ← neg_pow', neg_neg, one_pow]

Premises used: one_pow, Polynomial.Chebyshev.eval_T_real_node, neg_neg, neg_pow'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < HPow.hPow (α := ℝ) (-1) i * c i
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
x : ℝ
hx : Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1))) x
hPx : eval x P ≠ eval x (T ℝ (↑n : ℤ))
i_1 : ℕ
hix : node n i_1 = x
hi_1 : i_1 ∈ Finset.Iic n
i : ℕ
hi : i ∈ Finset.Iic n
⊢ HPow.hPow (α := ℝ) (-1) i * eval (node n i) P ≤ 1

Tactic:
negOnePow_mul_le (hPbnd _ node_mem_Icc)

Premises used: _private.0.Polynomial.Chebyshev.negOnePow_mul_le, Polynomial.Chebyshev.node_mem_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < HPow.hPow (α := ℝ) (-1) i * c i
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
x : ℝ
hx : Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1))) x
hPx : eval x P ≠ eval x (T ℝ (↑n : ℤ))
i_1 : ℕ
hix : node n i_1 = x
hi_1 : i_1 ∈ Finset.Iic n
i : ℕ
hi : i ∈ Finset.Iic n
⊢ HPow.hPow (α := ℝ) (-1) i * eval (node n i) P ≤ 1

Tactic:
exact negOnePow_mul_le (hPbnd _ node_mem_Icc)

Premises used: _private.0.Polynomial.Chebyshev.negOnePow_mul_le, Polynomial.Chebyshev.node_mem_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < HPow.hPow (α := ℝ) (-1) i * c i
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
x : ℝ
hx : Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1))) x
hPx : eval x P ≠ eval x (T ℝ (↑n : ℤ))
i : ℕ
hix : node n i = x
hi : i ∈ Finset.Iic n
⊢ ∀ {i : ℕ} (hi : i ∈ Finset.Iic n),
    HPow.hPow (α := ℝ) (-1) i * eval (node n i) P * (HPow.hPow (α := ℝ) (-1) i * c i) ≤
      HPow.hPow (α := ℝ) (-1) i * eval (node n i) (T ℝ (↑n : ℤ)) * (HPow.hPow (α := ℝ) (-1) i * c i)

Tactic:
have h_le {i : ℕ} (hi : i ∈ Finset.Iic n) :
    (-1) ^ i * P.eval (node n i) * ((-1) ^ i * c i) ≤
    (-1) ^ i * (T ℝ n).eval (node n i) * ((-1) ^ i * c i) := by
    refine mul_le_mul_of_nonneg_right ?_ (le_of_lt (hcpos i (Finset.mem_Iic.mp hi)))
    rw [eval_T_real_node hi, ← neg_pow', neg_neg, one_pow]
    exact negOnePow_mul_le (hPbnd _ node_mem_Icc)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < HPow.hPow (α := ℝ) (-1) i * c i
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
x : ℝ
hx : Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1))) x
hPx : eval x P ≠ eval x (T ℝ (↑n : ℤ))
i : ℕ
hix : node n i = x
hi : i ∈ Finset.Iic n
h_le :
  ∀ {i : ℕ} (hi : i ∈ Finset.Iic n),
    HPow.hPow (α := ℝ) (-1) i * eval (node n i) P * (HPow.hPow (α := ℝ) (-1) i * c i) ≤
      HPow.hPow (α := ℝ) (-1) i * eval (node n i) (T ℝ (↑n : ℤ)) * (HPow.hPow (α := ℝ) (-1) i * c i)
⊢ LT.lt (α := ℝ) (∑ i ∈ Finset.Iic n, HPow.hPow (α := ℝ) (-1) i * eval (node n i) P * (HPow.hPow (α := ℝ) (-1) i * c i))
    (∑ i ∈ Finset.Iic n, HPow.hPow (α := ℝ) (-1) i * eval (node n i) (T ℝ (↑n : ℤ)) * (HPow.hPow (α := ℝ) (-1) i * c i))

Tactic:
Finset.sum_lt_sum (fun i hi => h_le hi) ⟨i, hi, lt_of_le_of_ne (h_le hi) ?_⟩

Premises used: And.intro, Exists.intro, Finset.sum_lt_sum, lt_of_le_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < HPow.hPow (α := ℝ) (-1) i * c i
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
x : ℝ
hx : Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1))) x
hPx : eval x P ≠ eval x (T ℝ (↑n : ℤ))
i : ℕ
hix : node n i = x
hi : i ∈ Finset.Iic n
h_le :
  ∀ {i : ℕ} (hi : i ∈ Finset.Iic n),
    HPow.hPow (α := ℝ) (-1) i * eval (node n i) P * (HPow.hPow (α := ℝ) (-1) i * c i) ≤
      HPow.hPow (α := ℝ) (-1) i * eval (node n i) (T ℝ (↑n : ℤ)) * (HPow.hPow (α := ℝ) (-1) i * c i)
eval_fg :
  HPow.hPow (α := ℝ) (-1) i * eval (node n i) P * (HPow.hPow (α := ℝ) (-1) i * c i) ≠
    HPow.hPow (α := ℝ) (-1) i * eval (node n i) (T ℝ (↑n : ℤ)) * (HPow.hPow (α := ℝ) (-1) i * c i)
⊢ LT.lt (α := ℝ) (∑ i ∈ Finset.Iic n, HPow.hPow (α := ℝ) (-1) i * eval (node n i) P * (HPow.hPow (α := ℝ) (-1) i * c i))
    (∑ i ∈ Finset.Iic n, HPow.hPow (α := ℝ) (-1) i * eval (node n i) (T ℝ (↑n : ℤ)) * (HPow.hPow (α := ℝ) (-1) i * c i))

Tactic:
refine Finset.sum_lt_sum (fun i hi => h_le hi) ⟨i, hi, lt_of_le_of_ne (h_le hi) ?_⟩

Premises used: And.intro, Exists.intro, Finset.sum_lt_sum, lt_of_le_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < HPow.hPow (α := ℝ) (-1) i * c i
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
x : ℝ
hx : Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1))) x
hPx : eval x P ≠ eval x (T ℝ (↑n : ℤ))
i : ℕ
hix : node n i = x
hi : i ∈ Finset.Iic n
h_le :
  ∀ {i : ℕ} (hi : i ∈ Finset.Iic n),
    HPow.hPow (α := ℝ) (-1) i * eval (node n i) P * (HPow.hPow (α := ℝ) (-1) i * c i) ≤
      HPow.hPow (α := ℝ) (-1) i * eval (node n i) (T ℝ (↑n : ℤ)) * (HPow.hPow (α := ℝ) (-1) i * c i)
⊢ 0 ≠ HPow.hPow (α := ℝ) (-1) i * c i

Tactic:
have := ne_of_lt (hcpos i (Finset.mem_Iic.mp hi))
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
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 : ℕ
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 : ℕ
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 : ℕ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
⊢ n < n + 1

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

Tactic:
have : 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 : ℕ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
this : P.degree < (↑(Finset.range (n + 1)).card : WithBot ℕ)
⊢ ∑ i ∈ Finset.range (n + 1), eval (node n i) P / ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j) =
    P.coeff ((Finset.range (n + 1)).card - 1)

Tactic:
(Lagrange.coeff_eq_sum (strictAntiOn_node n).injOn this).symm

Premises used: Lagrange.coeff_eq_sum, Polynomial.Chebyshev.strictAntiOn_node, StrictAntiOn.injOn, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
this : P.degree < (↑(Finset.range (n + 1)).card : WithBot ℕ)
h : Finset.Iic n = Finset.range (n + 1)
h₁ : n = (Finset.range (n + 1)).card - 1
⊢ ∑ x ∈ Finset.Iic n, eval (node n x) P * (∏ j ∈ (Finset.range (n + 1)).erase x, (node n x - node n j))⁻¹ = P.coeff n

Tactic:
convert! (Lagrange.coeff_eq_sum (strictAntiOn_node n).injOn this).symm using 2

Premises used: Lagrange.coeff_eq_sum, Polynomial.Chebyshev.strictAntiOn_node, StrictAntiOn.injOn, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
this : P.degree < (↑(Finset.range (n + 1)).card : WithBot ℕ)
⊢ Finset.Iic n = Finset.range (n + 1)

Tactic:
Eq.symm (Nat.range_succ_eq_Iic n)

Premises used: Nat.range_succ_eq_Iic, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
this : P.degree < (↑(Finset.range (n + 1)).card : WithBot ℕ)
⊢ Finset.Iic n = Finset.range (n + 1)

Tactic:
exact Eq.symm (Nat.range_succ_eq_Iic n)

Premises used: Nat.range_succ_eq_Iic, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
this : P.degree < (↑(Finset.range (n + 1)).card : WithBot ℕ)
⊢ n = (Finset.range (n + 1)).card - 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
⊢ degree (T ℝ (↑n : ℤ)) ≤ (↑n : WithBot ℕ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
rw : coeff (T ℝ (↑n : ℤ)) n = HPow.hPow (α := ℝ) 2 (n - 1)
⊢ sumNodes n (leadingCoeffC n) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) 2 (n - 1)

Tactic:
rw [sumNodes_eq_coeff (by simp)]

Premises used: _private.0.Polynomial.Chebyshev.sumNodes_eq_coeff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
trans : coeff (T ℝ (↑n : ℤ)) n = leadingCoeff (T ℝ (↑n : ℤ))
trans₁ : leadingCoeff (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) 2 (n - 1)
⊢ coeff (T ℝ (↑n : ℤ)) n = HPow.hPow (α := ℝ) 2 (n - 1)

Tactic:
trans (T ℝ n).leadingCoeff

Premises used: Real, Polynomial.Chebyshev.T, Polynomial.leadingCoeff, Nat.cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
⊢ coeff (T ℝ (↑n : ℤ)) n = leadingCoeff (T ℝ (↑n : ℤ))

Tactic:
simp [leadingCoeff]

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
⊢ leadingCoeff (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) 2 (n - 1)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n i : ℕ
hi : i ≤ n
⊢ 0 < (HPow.hPow (α := ℝ) (-1) i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹

Tactic:
have := inv_pos_of_pos <| zero_lt_prod_node_sub_node hi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n i : ℕ
hi : i ≤ n
this : 0 < (HPow.hPow (α := ℝ) (-1) i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
rwa :
  ∀ (this : 0 < (HPow.hPow (α := ℝ) (-1) i)⁻¹ * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹),
    0 < HPow.hPow (α := ℝ) (-1) i * leadingCoeffC n i
rwa₁ :
  ∀ (this : 0 < HPow.hPow (α := ℝ) (-1)⁻¹ i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹),
    0 < HPow.hPow (α := ℝ) (-1) i * leadingCoeffC n i
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (this : 0 < HPow.hPow (α := ℝ) (-1) i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹),
    0 < HPow.hPow (α := ℝ) (-1) i * leadingCoeffC n i
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * leadingCoeffC n i

Tactic:
rwa [mul_inv, ← inv_pow, inv_neg_one] at this

Premises used: mul_inv, inv_pow, inv_neg_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
⊢ sumNodes n (fun (i : ℕ) ↦ leadingCoeffC n i) P ≤ sumNodes n (fun (i : ℕ) ↦ leadingCoeffC n i) (T ℝ (↑n : ℤ))

Tactic:
sumNodes_le_sumNodes_T (fun i hi => le_of_lt <| negOnePow_mul_leadingCoeffC_pos hi) hPbnd

Premises used: Polynomial.Chebyshev.sumNodes_le_sumNodes_T, le_of_lt, _private.0.Polynomial.Chebyshev.negOnePow_mul_leadingCoeffC_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
h : P.coeff n = sumNodes n (fun (i : ℕ) ↦ leadingCoeffC n i) P
h₁ : HPow.hPow (α := ℝ) 2 (n - 1) = sumNodes n (fun (i : ℕ) ↦ leadingCoeffC n i) (T ℝ (↑n : ℤ))
convert! : ℕ
⊢ P.coeff n ≤ HPow.hPow (α := ℝ) 2 (n - 1)

Tactic:
convert! sumNodes_le_sumNodes_T (fun i hi => le_of_lt <| negOnePow_mul_leadingCoeffC_pos hi) hPbnd

Premises used: Polynomial.Chebyshev.sumNodes_le_sumNodes_T, le_of_lt, _private.0.Polynomial.Chebyshev.negOnePow_mul_leadingCoeffC_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
h h₁ : P.coeff n = P.coeff n
⊢ P.coeff n = sumNodes n (fun (i : ℕ) ↦ leadingCoeffC n i) P

Tactic:
rw [sumNodes_eq_coeff hPdeg]

Premises used: _private.0.Polynomial.Chebyshev.sumNodes_eq_coeff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
h h₁ : HPow.hPow (α := ℝ) 2 (n - 1) = HPow.hPow (α := ℝ) 2 (n - 1)
⊢ HPow.hPow (α := ℝ) 2 (n - 1) = sumNodes n (fun (i : ℕ) ↦ leadingCoeffC n i) (T ℝ (↑n : ℤ))

Tactic:
rw [sumNodes_T_eq]

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

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

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

Tactic:
case pos hP => simp [hP]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hP : ¬P = 0
⊢ P.degree ≠ ⊥

Tactic:
degree_ne_bot.mpr hP

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

Tactic:
lift P.degree to ℕ using degree_ne_bot.mpr hP with d hd

Premises used: Iff.mpr, Polynomial.degree, Polynomial.degree_ne_bot
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hP : ¬P = 0
d : ℕ
hd : (↑d : WithBot ℕ) = P.degree
hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)
⊢ d ≤ n

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

Tactic:
rw [leadingCoeff, natDegree_eq_of_degree_eq_some hd.symm]

Premises used: Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hP : ¬P = 0
d : ℕ
hd : (↑d : WithBot ℕ) = P.degree
hPdeg : d ≤ n
h₁ : LE.le (α := ℝ) 1 2
⊢ P.coeff d ≤ HPow.hPow (α := ℝ) 2 (n - 1)

Tactic:
grw [coeff_le_of_forall_abs_le_one (le_of_eq hd.symm) hPbnd, hPdeg]

Premises used: le_of_eq, Polynomial.Chebyshev.coeff_le_of_forall_abs_le_one, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hP : ¬P = 0
d : ℕ
hd : (↑d : WithBot ℕ) = P.degree
hPdeg : d ≤ n
⊢ LE.le (α := ℝ) 1 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
⊢ sumNodes n (fun (i : ℕ) ↦ leadingCoeffC n i) P = sumNodes n (fun (i : ℕ) ↦ leadingCoeffC n i) (T ℝ (↑n : ℤ)) ↔
    P = T ℝ (↑n : ℤ)

Tactic:
sumNodes_eq_sumNodes_T_iff (fun i hi => negOnePow_mul_leadingCoeffC_pos hi) hPdeg hPbnd

Premises used: Polynomial.Chebyshev.sumNodes_eq_sumNodes_T_iff, _private.0.Polynomial.Chebyshev.negOnePow_mul_leadingCoeffC_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
h : P.coeff n = sumNodes n (fun (i : ℕ) ↦ leadingCoeffC n i) P
h₁ : HPow.hPow (α := ℝ) 2 (n - 1) = sumNodes n (fun (i : ℕ) ↦ leadingCoeffC n i) (T ℝ (↑n : ℤ))
⊢ P.coeff n = HPow.hPow (α := ℝ) 2 (n - 1) ↔ P = T ℝ (↑n : ℤ)

Tactic:
convert! sumNodes_eq_sumNodes_T_iff (fun i hi => negOnePow_mul_leadingCoeffC_pos hi) hPdeg hPbnd

Premises used: Polynomial.Chebyshev.sumNodes_eq_sumNodes_T_iff, _private.0.Polynomial.Chebyshev.negOnePow_mul_leadingCoeffC_pos
-- 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 = T ℝ (↑n : ℤ)
⊢ P.leadingCoeff = HPow.hPow (α := ℝ) 2 (n - 1)

Tactic:
simp [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
refine : ∀ (hP : P.leadingCoeff = HPow.hPow (α := ℝ) 2 (n - 1)), P = T ℝ (↑n : ℤ)
⊢ P.leadingCoeff = HPow.hPow (α := ℝ) 2 (n - 1) ↔ P = T ℝ (↑n : ℤ)

Tactic:
refine ⟨fun hP => ?_, fun hP => by simp [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.leadingCoeff = HPow.hPow (α := ℝ) 2 (n - 1)
apply : P.coeff n = HPow.hPow (α := ℝ) 2 (n - 1)
⊢ P = T ℝ (↑n : ℤ)

Tactic:
apply (coeff_eq_iff_of_forall_abs_le_one hPdeg hPbnd).mp

Premises used: Polynomial.Chebyshev.coeff_eq_iff_of_forall_abs_le_one, Iff.mp
-- 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)
hPdeg' : (↑n : WithBot ℕ) ≤ P.degree
⊢ P.degree = (↑n : WithBot ℕ)

Tactic:
replace hPdeg' : P.degree = n := eq_of_le_of_ge hPdeg hPdeg'
-- 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)
hPdeg' : P.degree = (↑n : WithBot ℕ)
rwa :
  ∀ (hP : P.coeff P.natDegree = HPow.hPow (α := ℝ) 2 (n - 1)) (hPdeg' : P.degree = (↑n : WithBot ℕ)),
    P.coeff n = HPow.hPow (α := ℝ) 2 (n - 1)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hP : P.coeff n = HPow.hPow (α := ℝ) 2 (n - 1)) (hPdeg' : P.degree = (↑n : WithBot ℕ)),
    P.coeff n = HPow.hPow (α := ℝ) 2 (n - 1)
⊢ P.coeff n = HPow.hPow (α := ℝ) 2 (n - 1)

Tactic:
rwa [leadingCoeff, natDegree_eq_of_degree_eq_some hPdeg'] at hP

Premises used: Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some
-- 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)
suffices : (↑n : WithBot ℕ) ≤ P.degree
⊢ P.coeff n = HPow.hPow (α := ℝ) 2 (n - 1)

Tactic:
suffices hPdeg' : n ≤ P.degree by
    replace hPdeg' : P.degree = n := eq_of_le_of_ge hPdeg hPdeg'
    rwa [leadingCoeff, natDegree_eq_of_degree_eq_some hPdeg'] at hP