awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℕ
hx : x ≤ n
⊢ (↑x : ℝ) * (π / (↑n : ℝ)) ≤ π
have inr : (↑x : ℝ) * (π / (↑n : ℝ)) ≤ (↑n : ℝ) * (π / (↑n : ℝ))
Tactic: nth_rewrite 2 [← mul_div_cancel₀ π (Nat.cast_ne_zero.mpr hn)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℕ
hx : x ≤ n
⊢ (↑x : ℝ) * (π / (↑n : ℝ)) ≤ (↑n : ℝ) * (π / (↑n : ℝ))
have inr : 0 ≤ π / (↑n : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n i : ℕ
hi : i ≤ n
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)
have inl : ∀ (hi : i ≤ 0),
  0 < HPow.hPow (α := ℝ) (-1) i * ∏ j ∈ (Finset.range (HAdd.hAdd (α := ℕ) 0 1)).erase i, (node 0 i - node 0 j)
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n, hi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n i : ℕ
hi : i ≤ n
inl :
  ∀ (hi : i ≤ 0),
    0 < HPow.hPow (α := ℝ) (-1) i * ∏ j ∈ (Finset.range (HAdd.hAdd (α := ℕ) 0 1)).erase i, (node 0 i - node 0 j)
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)
have inr : ∀ (hn : n ≠ 0), 0 < HPow.hPow (α := ℝ) (-1) i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (hypothesis)
Goal:
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)
have h₁ : LT.lt (α := ℝ) 0 (∏ j ∈ Finset.range i, -1 * (node n i - node n j))
Tactic: have h₁ : 0 < ∏ j ∈ Finset.range i, ((-1) * (node n i - node n j)) :=
    Finset.prod_pos (fun j hj => mul_pos_of_neg_of_neg neg_one_lt_zero <| sub_neg.mpr <|
    node_lt hi (Finset.mem_range.mp hj))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (hypothesis)
Goal:
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : LT.lt (α := ℝ) 0 (∏ j ∈ Finset.range i, -1 * (node n i - node n j))
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)
have h₂ : 0 < HPow.hPow (α := ℝ) (-1) i * ∏ x ∈ Finset.range i, (node n i - node n x)
Tactic: rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (hypothesis)
Goal:
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < HPow.hPow (α := ℝ) (-1) i * ∏ x ∈ Finset.range i, (node n i - node n x)
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)
have h₂ : LT.lt (α := ℝ) 0 (∏ j ∈ Finset.Ioc i n, (node n i - node n j))
Tactic: have h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (node n i - node n j) :=
    Finset.prod_pos (fun j hj => sub_pos.mpr <|
      node_lt (Finset.mem_Ioc.mp hj).2 (Finset.mem_Ioc.mp hj).1)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (hypothesis)
Goal:
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < HPow.hPow (α := ℝ) (-1) i * ∏ x ∈ Finset.range i, (node n i - node n x)
h₂ : LT.lt (α := ℝ) 0 (∏ j ∈ Finset.Ioc i n, (node n i - node n j))
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)
have union : (Finset.range (n + 1)).erase i = Finset.range i ∪ Finset.Ioc i n
Tactic: have union : (Finset.range (n + 1)).erase i = (Finset.range i) ∪ Finset.Ioc i n := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (hypothesis)
Goal:
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < HPow.hPow (α := ℝ) (-1) i * ∏ x ∈ Finset.range i, (node n i - node n x)
h₂ : LT.lt (α := ℝ) 0 (∏ j ∈ Finset.Ioc i n, (node n i - node n j))
union : (Finset.range (n + 1)).erase i = Finset.range i ∪ Finset.Ioc i n
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)
have disjoint : Disjoint (Finset.range i) (Finset.Ioc i n)
Tactic: have disjoint : Disjoint (Finset.range i) (Finset.Ioc i n) := by grind [Finset.disjoint_iff_ne]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < HPow.hPow (α := ℝ) (-1) i * ∏ x ∈ Finset.range i, (node n i - node n x)
h₂ : LT.lt (α := ℝ) 0 (∏ j ∈ Finset.Ioc i n, (node n i - node n j))
union : (Finset.range (n + 1)).erase i = Finset.range i ∪ Finset.Ioc i n
disjoint : Disjoint (Finset.range i) (Finset.Ioc i n)
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)
have inr : 0 <
  (HPow.hPow (α := ℝ) (-1) i * ∏ x ∈ Finset.range i, (node n i - node n x)) *
    ∏ x ∈ Finset.Ioc i n, (node n i - node n x)
Tactic: rw [union, Finset.prod_union disjoint, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
α : ℝ
i : ℕ
hα : |α| ≤ 1
⊢ HPow.hPow (α := ℝ) (-1) i * α ≤ 1
have h : |HPow.hPow (α := ℝ) (-1) i * α| ≤ 1
Tactic: apply le_of_abs_le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
α : ℝ
i : ℕ
hα : |α| ≤ 1
⊢ |HPow.hPow (α := ℝ) (-1) i * α| ≤ 1
have h : |HPow.hPow (α := ℝ) (-1) i| * |α| ≤ 1
Tactic: rwa [abs_mul, abs_neg_one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
α : ℝ
i : ℕ
hα : |α| ≤ 1
h : |HPow.hPow (α := ℝ) (-1) i| * |α| ≤ 1
⊢ |HPow.hPow (α := ℝ) (-1) i * α| ≤ 1
have h₁ : 1 * |α| ≤ 1
Tactic: rwa [abs_mul, abs_neg_one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ HPow.hPow (α := ℝ) (-1) i * c i
P : ℝ[X]
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i)
    (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
have refine : ∀ (i : ℕ) (hi : i ∈ Finset.Iic n), eval (node n i) P * c i ≤ eval (node n i) (T ℝ (↑n : ℤ)) * c i
Tactic: refine Finset.sum_le_sum (fun i hi => ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ HPow.hPow (α := ℝ) (-1) i * c i
P : ℝ[X]
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
i : ℕ
hi : i ∈ Finset.Iic n
⊢ HPow.hPow (α := ℝ) (-1) i * eval (node n i) P * (HPow.hPow (α := ℝ) (-1) i * c i) ≤
    1 * (HPow.hPow (α := ℝ) (-1) i * c i)
have ha : 0 ≤ HPow.hPow (α := ℝ) (-1) i * c i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ HPow.hPow (α := ℝ) (-1) i * c i
P : ℝ[X]
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
i : ℕ
hi : i ∈ Finset.Iic n
ha : 0 ≤ HPow.hPow (α := ℝ) (-1) i * c i
⊢ HPow.hPow (α := ℝ) (-1) i * eval (node n i) P * (HPow.hPow (α := ℝ) (-1) i * c i) ≤
    1 * (HPow.hPow (α := ℝ) (-1) i * c i)
have hbc : HPow.hPow (α := ℝ) (-1) i * eval (node n i) P ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ HPow.hPow (α := ℝ) (-1) i * c i
P : ℝ[X]
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
i : ℕ
hi : i ∈ Finset.Iic n
⊢ 1 * (HPow.hPow (α := ℝ) (-1) i * c i) = eval (node n i) (T ℝ (↑n : ℤ)) * c i
have rw : 1 * (HPow.hPow (α := ℝ) (-1) i * c i) = HPow.hPow (α := ℝ) (-1) i * c i
Tactic: rw [eval_T_real_node hi, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ HPow.hPow (α := ℝ) (-1) i * c i
P : ℝ[X]
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
i : ℕ
hi : i ∈ Finset.Iic n
rw : 1 * (HPow.hPow (α := ℝ) (-1) i * c i) = HPow.hPow (α := ℝ) (-1) i * c i
⊢ 1 * (HPow.hPow (α := ℝ) (-1) i * c i) = eval (node n i) (T ℝ (↑n : ℤ)) * c i
have rw₁ : HPow.hPow (α := ℝ) (-1) i * c i = HPow.hPow (α := ℝ) (-1) i * c i
Tactic: rw [eval_T_real_node hi, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ HPow.hPow (α := ℝ) (-1) i * c i
P : ℝ[X]
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
i : ℕ
hi : i ∈ Finset.Iic n
⊢ eval (node n i) P * c i ≤ eval (node n i) (T ℝ (↑n : ℤ)) * c i
have n₁ : HPow.hPow (α := ℝ) (-1) i * eval (node n i) P * (HPow.hPow (α := ℝ) (-1) i * c i) ≤
  1 * (HPow.hPow (α := ℝ) (-1) i * c i)
Tactic: calc
    P.eval (node n i) * (c i) =
      ((-1) ^ i * P.eval (node n i)) * ((-1) ^ i * (c i)) :=
      negOnePow_mul_negOnePow_mul_cancel.symm
    _ ≤ 1 * ((-1) ^ i * (c i)) := by
      gcongr
      · exact (hcnonneg i (Finset.mem_Iic.mp hi))
      · exact (negOnePow_mul_le (hPbnd _ node_mem_Icc))
    _ = (T ℝ n).eval (node n i) * (c i) := by
      rw [eval_T_real_node hi, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ HPow.hPow (α := ℝ) (-1) i * c i
P : ℝ[X]
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
i : ℕ
hi : i ∈ Finset.Iic n
n₁ :
  HPow.hPow (α := ℝ) (-1) i * eval (node n i) P * (HPow.hPow (α := ℝ) (-1) i * c i) ≤
    1 * (HPow.hPow (α := ℝ) (-1) i * c i)
⊢ eval (node n i) P * c i ≤ eval (node n i) (T ℝ (↑n : ℤ)) * c i
have n₂ : 1 * (HPow.hPow (α := ℝ) (-1) i * c i) = eval (node n i) (T ℝ (↑n : ℤ)) * c i
Tactic: calc
    P.eval (node n i) * (c i) =
      ((-1) ^ i * P.eval (node n i)) * ((-1) ^ i * (c i)) :=
      negOnePow_mul_negOnePow_mul_cancel.symm
    _ ≤ 1 * ((-1) ^ i * (c i)) := by
      gcongr
      · exact (hcnonneg i (Finset.mem_Iic.mp hi))
      · exact (negOnePow_mul_le (hPbnd _ node_mem_Icc))
    _ = (T ℝ n).eval (node n i) * (c i) := by
      rw [eval_T_real_node hi, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
h : P = T ℝ (↑n : ℤ)
⊢ sumNodes n c P = sumNodes n c (T ℝ (↑n : ℤ))
have rw : sumNodes n c (T ℝ (↑n : ℤ)) = sumNodes n c (T ℝ (↑n : ℤ))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
⊢ sumNodes n c P = sumNodes n c (T ℝ (↑n : ℤ)) ↔ P = T ℝ (↑n : ℤ)
have refine : ∀ (h : sumNodes n c P = sumNodes n c (T ℝ (↑n : ℤ))), P = T ℝ (↑n : ℤ)
Tactic: refine ⟨fun h => ?_, by intro h; rw [h]⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (hypothesis)
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
h : sumNodes n c P = sumNodes n c (T ℝ (↑n : ℤ))
⊢ P = T ℝ (↑n : ℤ)
have h₁ : Eq (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i) (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
Tactic: rw [sumNodes, sumNodes] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
h : Eq (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i) (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
⊢ P = T ℝ (↑n : ℤ)
have degree_f_lt : P.degree < (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
Tactic: apply eq_of_degrees_lt_of_eval_finset_eq ((Finset.range (n + 1)).image (node n ·))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
h : Eq (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i) (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
degree_f_lt :
  P.degree < (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
⊢ P = T ℝ (↑n : ℤ)
have degree_g_lt : degree (T ℝ (↑n : ℤ)) <
  (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
Tactic: apply eq_of_degrees_lt_of_eval_finset_eq ((Finset.range (n + 1)).image (node n ·))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
h : Eq (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i) (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
degree_f_lt :
  P.degree < (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
degree_g_lt :
  degree (T ℝ (↑n : ℤ)) <
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
⊢ P = T ℝ (↑n : ℤ)
have eval_fg : ∀ (x : ℝ),
  Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1))) x →
    eval x P = eval x (T ℝ (↑n : ℤ))
Tactic: apply eq_of_degrees_lt_of_eval_finset_eq ((Finset.range (n + 1)).image (node n ·))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
h : Eq (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i) (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
⊢ P.degree < (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
have degree_f_lt : LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ)
  (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
Tactic: apply lt_of_le_of_lt hPdeg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
h : Eq (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i) (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
⊢ LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ)
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
have degree_f_lt : n < Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))
Tactic: rw [Nat.cast_lt, Finset.card_image_of_injOn (strictAntiOn_node n).injOn,
      Finset.card_range, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
h : Eq (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i) (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
degree_f_lt : n < Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))
⊢ LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ)
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
have degree_f_lt₁ : n < (Finset.range (n + 1)).card
Tactic: rw [Nat.cast_lt, Finset.card_image_of_injOn (strictAntiOn_node n).injOn,
      Finset.card_range, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
h : Eq (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i) (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
degree_f_lt : n < Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))
degree_f_lt₁ : n < (Finset.range (n + 1)).card
⊢ LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ)
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
have degree_f_lt₂ : n < n + 1
Tactic: rw [Nat.cast_lt, Finset.card_image_of_injOn (strictAntiOn_node n).injOn,
      Finset.card_range, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
h : Eq (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i) (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
degree_f_lt : n < Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))
degree_f_lt₁ : n < (Finset.range (n + 1)).card
degree_f_lt₂ : n < n + 1
⊢ LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ)
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
have degree_f_lt₃ : n ≤ n
Tactic: rw [Nat.cast_lt, Finset.card_image_of_injOn (strictAntiOn_node n).injOn,
      Finset.card_range, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
h : Eq (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i) (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
⊢ degree (T ℝ (↑n : ℤ)) <
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
have degree_g_lt : LT.lt (α := WithBot ℕ) (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
  (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
Tactic: rw [degree_T, Int.natAbs_natCast, Nat.cast_lt,
      Finset.card_image_of_injOn (strictAntiOn_node n).injOn,
      Finset.card_range, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
h : Eq (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i) (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
degree_g_lt :
  LT.lt (α := WithBot ℕ) (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
⊢ degree (T ℝ (↑n : ℤ)) <
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
have degree_g_lt₁ : LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ)
  (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
Tactic: rw [degree_T, Int.natAbs_natCast, Nat.cast_lt,
      Finset.card_image_of_injOn (strictAntiOn_node n).injOn,
      Finset.card_range, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
h : Eq (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i) (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
degree_g_lt :
  LT.lt (α := WithBot ℕ) (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
degree_g_lt₁ :
  LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ)
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
⊢ degree (T ℝ (↑n : ℤ)) <
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
have degree_g_lt₂ : n < Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))
Tactic: rw [degree_T, Int.natAbs_natCast, Nat.cast_lt,
      Finset.card_image_of_injOn (strictAntiOn_node n).injOn,
      Finset.card_range, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
h : Eq (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i) (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
degree_g_lt :
  LT.lt (α := WithBot ℕ) (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
degree_g_lt₁ :
  LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ)
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
degree_g_lt₂ : n < Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))
⊢ degree (T ℝ (↑n : ℤ)) <
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
have degree_g_lt₃ : n < (Finset.range (n + 1)).card
Tactic: rw [degree_T, Int.natAbs_natCast, Nat.cast_lt,
      Finset.card_image_of_injOn (strictAntiOn_node n).injOn,
      Finset.card_range, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
h : Eq (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i) (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
degree_g_lt :
  LT.lt (α := WithBot ℕ) (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
degree_g_lt₁ :
  LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ)
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
degree_g_lt₂ : n < Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))
degree_g_lt₃ : n < (Finset.range (n + 1)).card
⊢ degree (T ℝ (↑n : ℤ)) <
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
have degree_g_lt₄ : n < n + 1
Tactic: rw [degree_T, Int.natAbs_natCast, Nat.cast_lt,
      Finset.card_image_of_injOn (strictAntiOn_node n).injOn,
      Finset.card_range, Nat.lt_succ_iff]