awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_g_lt₄ : n < n + 1
⊢ degree (T ℝ (↑n : ℤ)) <
    (↑(Finset.card (α := ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1)))) : WithBot ℕ)
have degree_g_lt₅ : n ≤ n
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 (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 : Eq (α := ℝ) (∑ 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 : ℤ))
have 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)
Tactic: replace h := ge_of_eq 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 :
  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)
⊢ ∀ (x : ℝ),
    Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : ℕ) ↦ node n x) (Finset.range (n + 1))) x →
      eval x P = eval x (T ℝ (↑n : ℤ))
have 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)
Tactic: contrapose! 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 :
  ∃ (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)
have 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)
Tactic: obtain ⟨x, hx, hPx⟩ := 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
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)
have 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)
Tactic: obtain ⟨i, hi, hix⟩ := Finset.mem_image.mp hx
-- 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
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
⊢ 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)
have hi₁ : i ∈ Finset.Iic n
Tactic: replace hi := Finset.mem_Iic.mpr (Finset.mem_range_succ_iff.mp hi)
Cleared hypotheses: hi
-- 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
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
⊢ 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)
have 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))
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]
-- 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
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)
have refine : HPow.hPow (α := ℝ) (-1) i * eval (node n i) P ≤ HPow.hPow (α := ℝ) (-1) i * eval (node n i) (T ℝ (↑n : ℤ))
Tactic: refine mul_le_mul_of_nonneg_right ?_ (le_of_lt (hcpos i (Finset.mem_Iic.mp hi)))
-- 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
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 * eval (node n i) (T ℝ (↑n : ℤ))
have rw : HPow.hPow (α := ℝ) (-1) i * eval (node n i) P ≤ 1
Tactic: rw [eval_T_real_node hi, ← neg_pow', neg_neg, one_pow]
-- 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
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
⊢ 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))
have 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)
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)
-- 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
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))
have 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)
Tactic: refine Finset.sum_lt_sum (fun i hi => h_le hi) ⟨i, hi, lt_of_le_of_ne (h_le hi) ?_⟩
-- 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
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)
⊢ 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)
have this : 0 ≠ HPow.hPow (α := ℝ) (-1) i * c i
Tactic: have := ne_of_lt (hcpos i (Finset.mem_Iic.mp hi))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
⊢ P.degree < (↑(Finset.range (n + 1)).card : WithBot ℕ)
have rw : P.degree < (↑(n + 1) : WithBot ℕ)
Tactic: rw [Finset.card_range]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
⊢ P.degree < (↑(n + 1) : WithBot ℕ)
have grw : LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑(n + 1) : WithBot ℕ)
Tactic: grw [hP]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
⊢ LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑(n + 1) : WithBot ℕ)
have norm_cast : n < n + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (hypothesis)
Goal:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
⊢ ∑ 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
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
this : P.degree < (↑(Finset.range (n + 1)).card : WithBot ℕ)
⊢ ∑ 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
have h : Finset.Iic n = Finset.range (n + 1)
Tactic: convert! (Lagrange.coeff_eq_sum (strictAntiOn_node n).injOn this).symm using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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)
⊢ ∑ 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
have h₁ : n = (Finset.range (n + 1)).card - 1
Tactic: convert! (Lagrange.coeff_eq_sum (strictAntiOn_node n).injOn this).symm using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
⊢ sumNodes n (leadingCoeffC n) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) 2 (n - 1)
have rw : coeff (T ℝ (↑n : ℤ)) n = HPow.hPow (α := ℝ) 2 (n - 1)
Tactic: rw [sumNodes_eq_coeff (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
⊢ coeff (T ℝ (↑n : ℤ)) n = HPow.hPow (α := ℝ) 2 (n - 1)
have trans : coeff (T ℝ (↑n : ℤ)) n = leadingCoeff (T ℝ (↑n : ℤ))
Tactic: trans (T ℝ n).leadingCoeff
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
trans : coeff (T ℝ (↑n : ℤ)) n = leadingCoeff (T ℝ (↑n : ℤ))
⊢ coeff (T ℝ (↑n : ℤ)) n = HPow.hPow (α := ℝ) 2 (n - 1)
have trans₁ : leadingCoeff (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) 2 (n - 1)
Tactic: trans (T ℝ n).leadingCoeff
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (hypothesis)
Goal:
n i : ℕ
hi : i ≤ n
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * leadingCoeffC n i
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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))⁻¹
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * leadingCoeffC n i
have 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
Tactic: rwa [mul_inv, ← inv_pow, inv_neg_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * leadingCoeffC n i
have 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
Tactic: rwa [mul_inv, ← inv_pow, inv_neg_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * leadingCoeffC n i
have 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
Tactic: rwa [mul_inv, ← inv_pow, inv_neg_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
⊢ P.coeff n ≤ HPow.hPow (α := ℝ) 2 (n - 1)
have h : P.coeff n = sumNodes n (fun (i : ℕ) ↦ leadingCoeffC n i) P
Tactic: convert! sumNodes_le_sumNodes_T (fun i hi => le_of_lt <| negOnePow_mul_leadingCoeffC_pos hi) hPbnd
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
⊢ P.coeff n ≤ HPow.hPow (α := ℝ) 2 (n - 1)
have h₁ : HPow.hPow (α := ℝ) 2 (n - 1) = sumNodes n (fun (i : ℕ) ↦ leadingCoeffC n i) (T ℝ (↑n : ℤ))
Tactic: convert! sumNodes_le_sumNodes_T (fun i hi => le_of_lt <| negOnePow_mul_leadingCoeffC_pos hi) hPbnd
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
⊢ P.coeff n = sumNodes n (fun (i : ℕ) ↦ leadingCoeffC n i) P
have h : P.coeff n = P.coeff n
Tactic: rw [sumNodes_eq_coeff hPdeg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
⊢ HPow.hPow (α := ℝ) 2 (n - 1) = sumNodes n (fun (i : ℕ) ↦ leadingCoeffC n i) (T ℝ (↑n : ℤ))
have h : HPow.hPow (α := ℝ) 2 (n - 1) = HPow.hPow (α := ℝ) 2 (n - 1)
Tactic: rw [sumNodes_T_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
⊢ P.leadingCoeff ≤ HPow.hPow (α := ℝ) 2 (n - 1)
have pos : P = 0 → P.leadingCoeff ≤ HPow.hPow (α := ℝ) 2 (n - 1)
Tactic: by_cases P = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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)
⊢ P.leadingCoeff ≤ HPow.hPow (α := ℝ) 2 (n - 1)
have neg : ¬P = 0 → P.leadingCoeff ≤ HPow.hPow (α := ℝ) 2 (n - 1)
Tactic: by_cases P = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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)
have lift : ∀ (d : ℕ) (hd : (↑d : WithBot ℕ) = P.degree) (hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)),
  P.leadingCoeff ≤ HPow.hPow (α := ℝ) 2 (n - 1)
Tactic: lift P.degree to ℕ using degree_ne_bot.mpr hP with d hd
Cleared hypotheses: hPdeg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (hypothesis)
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 ℕ)
⊢ P.leadingCoeff ≤ HPow.hPow (α := ℝ) 2 (n - 1)
have hPdeg₁ : d ≤ n
Tactic: replace hPdeg : d ≤ n := (WithBot.coe_le rfl).mp hPdeg
Cleared hypotheses: hPdeg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
⊢ P.leadingCoeff ≤ HPow.hPow (α := ℝ) 2 (n - 1)
have rw : P.coeff d ≤ HPow.hPow (α := ℝ) 2 (n - 1)
Tactic: rw [leadingCoeff, natDegree_eq_of_degree_eq_some hd.symm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
⊢ P.coeff d ≤ HPow.hPow (α := ℝ) 2 (n - 1)
have h₁ : LE.le (α := ℝ) 1 2
Tactic: grw [coeff_le_of_forall_abs_le_one (le_of_eq hd.symm) hPbnd, hPdeg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
⊢ P.coeff n = HPow.hPow (α := ℝ) 2 (n - 1) ↔ P = T ℝ (↑n : ℤ)
have h : P.coeff n = sumNodes n (fun (i : ℕ) ↦ leadingCoeffC n i) P
Tactic: convert! sumNodes_eq_sumNodes_T_iff (fun i hi => negOnePow_mul_leadingCoeffC_pos hi) hPdeg hPbnd
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
⊢ P.coeff n = HPow.hPow (α := ℝ) 2 (n - 1) ↔ P = T ℝ (↑n : ℤ)
have h₁ : HPow.hPow (α := ℝ) 2 (n - 1) = sumNodes n (fun (i : ℕ) ↦ leadingCoeffC n i) (T ℝ (↑n : ℤ))
Tactic: convert! sumNodes_eq_sumNodes_T_iff (fun i hi => negOnePow_mul_leadingCoeffC_pos hi) hPdeg hPbnd
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
⊢ P.leadingCoeff = HPow.hPow (α := ℝ) 2 (n - 1) ↔ P = T ℝ (↑n : ℤ)
have refine : ∀ (hP : P.leadingCoeff = HPow.hPow (α := ℝ) 2 (n - 1)), P = T ℝ (↑n : ℤ)
Tactic: refine ⟨fun hP => ?_, fun hP => by simp [hP]⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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)
⊢ P = T ℝ (↑n : ℤ)
have apply : P.coeff n = HPow.hPow (α := ℝ) 2 (n - 1)
Tactic: apply (coeff_eq_iff_of_forall_abs_le_one hPdeg hPbnd).mp