awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
hn : n ≠ 0
x : ℕ
hx : x ≤ n
inr : 0 ≤ π / (↑n : ℝ)
⊢ (↑x : ℝ) * (π / (↑n : ℝ)) ≤ (↑n : ℝ) * (π / (↑n : ℝ))

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n i j : ℕ
hj : j ≤ n
hij : i < j
⊢ i ≤ n

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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)
inr : ∀ (hn : n ≠ 0), 0 < HPow.hPow (α := ℝ) (-1) i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)
⊢ 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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
i : ℕ
hi : i ≤ 0
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * ∏ j ∈ (Finset.range (HAdd.hAdd (α := ℕ) 0 1)).erase i, (node 0 i - node 0 j)

Tactic:
simp [Nat.le_zero.mp hi]

Premises used: Nat.le_zero, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
⊢ 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))
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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 * ∏ x ∈ Finset.range i, (node n i - node n x)

Tactic:
rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range] at h₁

Premises used: Finset.prod_mul_distrib, Finset.card_range, Finset.prod_const
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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)
⊢ 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)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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))
⊢ (Finset.range (n + 1)).erase i = Finset.range i ∪ Finset.Ioc i n

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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))
⊢ (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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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 (Finset.range i) (Finset.Ioc i n)

Tactic:
grind [Finset.disjoint_iff_ne]

Premises used: Finset.disjoint_iff_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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 (Finset.range i) (Finset.Ioc i n)

Tactic:
have disjoint : Disjoint (Finset.range i) (Finset.Ioc i n) := by grind [Finset.disjoint_iff_ne]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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)
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)
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)

Tactic:
rw [union, Finset.prod_union disjoint, ← mul_assoc]

Premises used: mul_assoc, Finset.prod_union
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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 * ∏ x ∈ Finset.range i, (node n i - node n x)) *
      ∏ x ∈ Finset.Ioc i n, (node n i - node n x)

Tactic:
mul_pos h₁ h₂

Premises used: mul_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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 * ∏ x ∈ Finset.range i, (node n i - node n x)) *
      ∏ x ∈ Finset.Ioc i n, (node n i - node n x)

Tactic:
exact mul_pos h₁ h₂

Premises used: mul_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
α : ℝ
i : ℕ
hα : |α| ≤ 1
h : |HPow.hPow (α := ℝ) (-1) i * α| ≤ 1
⊢ HPow.hPow (α := ℝ) (-1) i * α ≤ 1

Tactic:
apply le_of_abs_le

Premises used: le_of_abs_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
α : ℝ
i : ℕ
hα : |α| ≤ 1
h : |HPow.hPow (α := ℝ) (-1) i| * |α| ≤ 1
h₁ : 1 * |α| ≤ 1
h₂ h₃ h₄ h₅ : |α| ≤ 1
⊢ |HPow.hPow (α := ℝ) (-1) i * α| ≤ 1

Tactic:
rwa [abs_mul, abs_neg_one_pow, one_mul]

Premises used: abs_neg_one_pow, abs_mul, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
α β : ℝ
i : ℕ
⊢ HPow.hPow (α := ℝ) (-1) i * α * (HPow.hPow (α := ℝ) (-1) i * β) =
    HPow.hPow (α := ℝ) (-1) i * HPow.hPow (α := ℝ) (-1) i * α * β

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
α β : ℝ
i : ℕ
⊢ HPow.hPow (α := ℝ) (-1) i * HPow.hPow (α := ℝ) (-1) i * α * β = α * β

Tactic:
simp [← mul_pow]

Premises used: mul_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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)

Tactic:
Finset.sum_le_sum (fun i hi => ?_)

Premises used: Finset.sum_le_sum
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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
refine : ∀ (i : ℕ) (hi : i ∈ Finset.Iic n), eval (node n i) P * c i ≤ eval (node n i) (T ℝ (↑n : ℤ)) * c i
⊢ 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)

Tactic:
refine Finset.sum_le_sum (fun i hi => ?_)

Premises used: Finset.sum_le_sum
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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 = HPow.hPow (α := ℝ) (-1) i * eval (node n i) P * (HPow.hPow (α := ℝ) (-1) i * c i)

Tactic:
negOnePow_mul_negOnePow_mul_cancel.symm

Premises used: _private.0.Polynomial.Chebyshev.negOnePow_mul_negOnePow_mul_cancel, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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
hbc : HPow.hPow (α := ℝ) (-1) i * eval (node n i) P ≤ 1
⊢ HPow.hPow (α := ℝ) (-1) i * eval (node n i) P * (HPow.hPow (α := ℝ) (-1) i * c i) ≤
    1 * (HPow.hPow (α := ℝ) (-1) i * c i)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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
⊢ 0 ≤ HPow.hPow (α := ℝ) (-1) i * c i

Tactic:
(hcnonneg i (Finset.mem_Iic.mp hi))

Premises used: Finset.mem_Iic, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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
⊢ 0 ≤ HPow.hPow (α := ℝ) (-1) i * c i

Tactic:
exact (hcnonneg i (Finset.mem_Iic.mp hi))

Premises used: Finset.mem_Iic, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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 ≤ 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 : ℕ → ℝ
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 ≤ 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 : ℕ → ℝ
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
rw₁ rw₂ : 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

Tactic:
rw [eval_T_real_node hi, one_mul]

Premises used: Polynomial.Chebyshev.eval_T_real_node, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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)
n₂ : 1 * (HPow.hPow (α := ℝ) (-1) i * c i) = eval (node n i) (T ℝ (↑n : ℤ)) * c i
⊢ eval (node n i) P * 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]

Premises used: Polynomial.eval, Real, HMul.hMul, Polynomial.Chebyshev.T, Polynomial.Chebyshev.node, Nat.cast, HPow.hPow, _private.0.Polynomial.Chebyshev.negOnePow_mul_negOnePow_mul_cancel, OfNat.ofNat, Eq.symm, Neg.neg
-- 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
h : P = T ℝ (↑n : ℤ)
rw rw₁ : sumNodes n c (T ℝ (↑n : ℤ)) = sumNodes n c (T ℝ (↑n : ℤ))
⊢ sumNodes n c P = sumNodes n c (T ℝ (↑n : ℤ))

Tactic:
rw [h]
-- 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
refine : ∀ (h : sumNodes n c P = sumNodes n c (T ℝ (↑n : ℤ))), P = T ℝ (↑n : ℤ)
⊢ sumNodes n c P = sumNodes n c (T ℝ (↑n : ℤ)) ↔ P = T ℝ (↑n : ℤ)

Tactic:
refine ⟨fun h => ?_, by intro h; rw [h]⟩
-- 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
h : sumNodes n c P = sumNodes n c (T ℝ (↑n : ℤ))
⊢ 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

Premises used: Polynomial.Chebyshev.sumNodes
-- 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
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 ℕ)
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 : ℤ))
⊢ P = T ℝ (↑n : ℤ)

Tactic:
apply eq_of_degrees_lt_of_eval_finset_eq ((Finset.range (n + 1)).image (node n ·))

Premises used: Polynomial.Chebyshev.node, Finset.range, HAdd.hAdd, Polynomial.eq_of_degrees_lt_of_eval_finset_eq, OfNat.ofNat, Finset.image
-- 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
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 :
  LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ)
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
⊢ P.degree < (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)

Tactic:
apply lt_of_le_of_lt hPdeg

Premises used: lt_of_le_of_lt
-- 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
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
degree_f_lt₃ degree_f_lt₄ : n ≤ n
⊢ LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ)
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)

Tactic:
rw [Nat.cast_lt, Finset.card_image_of_injOn (strictAntiOn_node n).injOn,
      Finset.card_range, Nat.lt_succ_iff]

Premises used: Finset.card_range, Polynomial.Chebyshev.strictAntiOn_node, StrictAntiOn.injOn, Nat.lt_succ_iff, Finset.card_image_of_injOn, Nat.cast_lt
-- 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
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_g_lt₄ : n < n + 1
degree_g_lt₅ degree_g_lt₆ : n ≤ n
⊢ degree (T ℝ (↑n : ℤ)) <
    (↑(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]

Premises used: Finset.card_range, Polynomial.Chebyshev.degree_T, Polynomial.Chebyshev.strictAntiOn_node, StrictAntiOn.injOn, Nat.lt_succ_iff, Finset.card_image_of_injOn, Int.natAbs_natCast, Nat.cast_lt
-- 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
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)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
    (∑ i ∈ Finset.Iic n, eval (node n i) P * c i)

Tactic:
replace h := ge_of_eq h
-- 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
h :
  LE.le (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
    (∑ i ∈ Finset.Iic n, eval (node n i) P * c i)
eval_fg :
  ∀
    (h :
      ∃ (x : ℝ),
        Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1))) x ∧
          eval x P ≠ eval x (T ℝ (↑n : ℤ))),
    LT.lt (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i)
      (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)
⊢ ∀ (x : ℝ),
    Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1))) x →
      eval x P = eval x (T ℝ (↑n : ℤ))

Tactic:
contrapose! h
-- 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
h :
  ∃ (x : ℝ),
    Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1))) x ∧
      eval x P ≠ eval x (T ℝ (↑n : ℤ))
eval_fg :
  ∀ (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 : ℤ))),
    LT.lt (α := ℝ) (∑ 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 (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i)
    (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)

Tactic:
obtain ⟨x, hx, hPx⟩ := h
-- 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 : ℤ))
eval_fg :
  ∀ (i : ℕ) (hi : i ∈ Finset.range (n + 1)) (hix : node n i = x),
    LT.lt (α := ℝ) (∑ 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 (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i)
    (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)

Tactic:
obtain ⟨i, hi, hix⟩ := Finset.mem_image.mp hx

Premises used: Finset.mem_image, 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 : ℕ
hi : i ∈ Finset.range (n + 1)
hix : node n i = x
⊢ i ∈ Finset.Iic n

Tactic:
replace hi := Finset.mem_Iic.mpr (Finset.mem_range_succ_iff.mp hi)
-- 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
this :
  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))
⊢ LT.lt (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i)
    (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)

Tactic:
simpa [negOnePow_mul_negOnePow_mul_cancel]

Premises used: _private.0.Polynomial.Chebyshev.negOnePow_mul_negOnePow_mul_cancel
-- 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
eval_fg :
  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))
⊢ LT.lt (α := ℝ) (∑ i ∈ Finset.Iic n, eval (node n i) P * c i)
    (∑ i ∈ Finset.Iic n, eval (node n i) (T ℝ (↑n : ℤ)) * c i)

Tactic:
suffices ∑ i ≤ n, ((-1) ^ i * P.eval (node n i)) * ((-1) ^ i * c i) <
      ∑ i ≤ n, ((-1) ^ i * (T ℝ n).eval (node n i)) * ((-1) ^ i * c i) by
    simpa [negOnePow_mul_negOnePow_mul_cancel]