awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (hypothesis)
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.coeff n = HPow.hPow (α := ℝ) 2 (n - 1)
have hPdeg'₁ : P.degree = (↑n : WithBot ℕ)
Tactic: replace hPdeg' : P.degree = n := eq_of_le_of_ge hPdeg hPdeg'
Cleared hypotheses: hPdeg'
-- 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)
hPdeg' : P.degree = (↑n : WithBot ℕ)
⊢ P.coeff n = HPow.hPow (α := ℝ) 2 (n - 1)
have rwa : ∀ (hP : P.coeff P.natDegree = HPow.hPow (α := ℝ) 2 (n - 1)) (hPdeg' : P.degree = (↑n : WithBot ℕ)),
  P.coeff n = HPow.hPow (α := ℝ) 2 (n - 1)
Tactic: rwa [leadingCoeff, natDegree_eq_of_degree_eq_some hPdeg'] at hP
Cleared hypotheses: hP, hPdeg'
-- 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)
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)
⊢ P.coeff n = HPow.hPow (α := ℝ) 2 (n - 1)
have rwa₁ : ∀ (hP : P.coeff n = HPow.hPow (α := ℝ) 2 (n - 1)) (hPdeg' : P.degree = (↑n : WithBot ℕ)),
  P.coeff n = HPow.hPow (α := ℝ) 2 (n - 1)
Tactic: rwa [leadingCoeff, natDegree_eq_of_degree_eq_some hPdeg'] at hP
Cleared hypotheses: hP, hPdeg'
-- 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.coeff n = HPow.hPow (α := ℝ) 2 (n - 1)
have suffices : (↑n : WithBot ℕ) ≤ P.degree
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
-- 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)
⊢ (↑n : WithBot ℕ) ≤ P.degree
have lift : P.degree ≠ ⊥
Tactic: lift P.degree to ℕ with d hd
-- 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)
lift : P.degree ≠ ⊥
⊢ (↑n : WithBot ℕ) ≤ P.degree
have lift₁ : ∀ (d : ℕ) (hd : (↑d : WithBot ℕ) = P.degree) (hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)),
  (↑n : WithBot ℕ) ≤ (↑d : WithBot ℕ)
Tactic: lift P.degree to ℕ with d hd
Cleared hypotheses: hPdeg
-- 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.degree ≠ ⊥
have contrapose! : ∀ (hP : P.degree = ⊥), P.leadingCoeff ≠ HPow.hPow (α := ℝ) 2 (n - 1)
Tactic: contrapose! hP
Cleared hypotheses: 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.degree = ⊥
⊢ P.leadingCoeff ≠ HPow.hPow (α := ℝ) 2 (n - 1)
have rw : 0 ≠ HPow.hPow (α := ℝ) 2 (n - 1)
Tactic: rw [degree_eq_bot.mp hP, leadingCoeff_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (hypothesis)
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hP : P.leadingCoeff = HPow.hPow (α := ℝ) 2 (n - 1)
d : ℕ
hd : (↑d : WithBot ℕ) = P.degree
hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)
⊢ (↑n : WithBot ℕ) ≤ (↑d : WithBot ℕ)
have hP₁ : HPow.hPow (α := ℝ) 2 (n - 1) ≤ P.leadingCoeff
Tactic: replace hP := ge_of_eq hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
d : ℕ
hd : (↑d : WithBot ℕ) = P.degree
hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)
hP : HPow.hPow (α := ℝ) 2 (n - 1) ≤ P.leadingCoeff
⊢ (↑n : WithBot ℕ) ≤ (↑d : WithBot ℕ)
have contrapose! : ∀ (hP : (↑d : WithBot ℕ) < (↑n : WithBot ℕ)), P.leadingCoeff < HPow.hPow (α := ℝ) 2 (n - 1)
Tactic: contrapose! hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (hypothesis)
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
d : ℕ
hd : (↑d : WithBot ℕ) = P.degree
hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)
hP : (↑d : WithBot ℕ) < (↑n : WithBot ℕ)
⊢ P.leadingCoeff < HPow.hPow (α := ℝ) 2 (n - 1)
have this : d - 1 < n - 1
Tactic: have : d - 1 < n - 1 := by grind [Nat.cast_withBot, WithBot.coe_le_coe, WithBot.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
d : ℕ
hd : (↑d : WithBot ℕ) = P.degree
hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)
hP : (↑d : WithBot ℕ) < (↑n : WithBot ℕ)
this : d - 1 < n - 1
⊢ HPow.hPow (α := ℝ) 2 (d - 1) < HPow.hPow (α := ℝ) 2 (n - 1)
have h : LT.lt (α := ℝ) 1 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
d : ℕ
hd : (↑d : WithBot ℕ) = P.degree
hPdeg : (↑d : WithBot ℕ) ≤ (↑n : WithBot ℕ)
hP : (↑d : WithBot ℕ) < (↑n : WithBot ℕ)
this : d - 1 < n - 1
⊢ P.leadingCoeff < HPow.hPow (α := ℝ) 2 (n - 1)
have calc : HPow.hPow (α := ℝ) 2 (d - 1) < HPow.hPow (α := ℝ) 2 (n - 1)
Tactic: calc P.leadingCoeff ≤ 2 ^ (d - 1) := leadingCoeff_le_of_forall_abs_le_one (le_of_eq hd.symm) hPbnd
  _ < 2 ^ (n - 1) := by gcongr; norm_num
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k : ℕ
hk : k ≤ n
x : ℝ
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 k : ℕ
hk : k ≤ n
x : ℝ
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 k : ℕ
hk : k ≤ n
x : ℝ
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 k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
⊢ ∑ x_1 ∈ Finset.Iic n,
      eval (node n x_1) P *
        (HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase x_1, (node n x_1 - node n j))⁻¹ *
          ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase x_1), ∏ a ∈ t, (x - node n a)) =
    eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P)
have h₁ : P.degree < (↑(Finset.range (n + 1)).card : WithBot ℕ)
Tactic: have h₁ : P.degree < (Finset.range (n + 1)).card := by
    rw [Finset.card_range]; grw [hP]; norm_cast; simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
h₁ : P.degree < (↑(Finset.range (n + 1)).card : WithBot ℕ)
⊢ ∑ x_1 ∈ Finset.Iic n,
      eval (node n x_1) P *
        (HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase x_1, (node n x_1 - node n j))⁻¹ *
          ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase x_1), ∏ a ∈ t, (x - node n a)) =
    eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P)
have h : ∑ x_1 ∈ Finset.Iic n,
    eval (node n x_1) P *
      (HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase x_1, (node n x_1 - node n j))⁻¹ *
        ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase x_1), ∏ a ∈ t, (x - node n a)) =
  HMul.hMul (α := ℝ) (↑k.factorial : ℝ)
    (∑ i ∈ Finset.range (n + 1),
      (eval (node n i) P / ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)) *
        ∑ t ∈ Finset.powersetCard ((Finset.range (n + 1)).card - (k + 1)) ((Finset.range (n + 1)).erase i),
          ∏ a ∈ t, (x - node n a))
Tactic: convert!
    (Lagrange.eval_iterate_derivative_eq_sum (strictAntiOn_node n).injOn h₁
        (show k < _ by simp [hk]) x).symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ (↑n : WithBot ℕ)
h₁ : P.degree < (↑(Finset.range (n + 1)).card : WithBot ℕ)
⊢ ∑ x_1 ∈ Finset.Iic n,
      eval (node n x_1) P *
        (HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase x_1, (node n x_1 - node n j))⁻¹ *
          ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase x_1), ∏ a ∈ t, (x - node n a)) =
    HMul.hMul (α := ℝ) (↑k.factorial : ℝ)
      (∑ i ∈ Finset.range (n + 1),
        (eval (node n i) P / ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)) *
          ∑ t ∈ Finset.powersetCard ((Finset.range (n + 1)).card - (k + 1)) ((Finset.range (n + 1)).erase i),
            ∏ a ∈ t, (x - node n a))
have h : Eq (α := ℝ)
  (∑ x_1 ∈ Finset.Iic n,
    eval (node n x_1) P *
      (HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase x_1, (node n x_1 - node n j))⁻¹ *
        ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase x_1), ∏ a ∈ t, (x - node n a)))
  (∑ i ∈ Finset.range (n + 1),
    (↑k.factorial : ℝ) *
      ((eval (node n i) P / ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)) *
        ∑ t ∈ Finset.powersetCard ((Finset.range (n + 1)).card - (k + 1)) ((Finset.range (n + 1)).erase i),
          ∏ a ∈ t, (x - node n a)))
Tactic: rw [Finset.mul_sum]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ HPow.hPow (α := ℝ) (-1) i * iterateDerivativeC n k x i
have rw : 0 ≤
  HPow.hPow (α := ℝ) (-1) i *
      HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
    ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)
Tactic: rw [iterateDerivativeC, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤
    HPow.hPow (α := ℝ) (-1) i *
        HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)
have refine_1 : 0 ≤
  HPow.hPow (α := ℝ) (-1) i *
    HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
Tactic: refine mul_nonneg ?_ (Finset.sum_nonneg' ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
refine_1 :
  0 ≤
    HPow.hPow (α := ℝ) (-1) i *
      HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
⊢ 0 ≤
    HPow.hPow (α := ℝ) (-1) i *
        HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)
have refine_2 : ∀ (i : Finset ℕ), LE.le (α := ℝ) 0 (∏ a ∈ i, (x - node n a))
Tactic: refine mul_nonneg ?_ (Finset.sum_nonneg' ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤
    HPow.hPow (α := ℝ) (-1) i *
      HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
have refine_1 : 0 ≤ (↑k.factorial : ℝ) * (HPow.hPow (α := ℝ) (-1) i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)
Tactic: rw [← mul_assoc, mul_comm (a := (-1) ^ i), mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 < HPow.hPow (α := ℝ) (-1) i * iterateDerivativeC n k x i
have rw : 0 <
  HPow.hPow (α := ℝ) (-1) i *
      HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
    ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)
Tactic: rw [iterateDerivativeC, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 <
    HPow.hPow (α := ℝ) (-1) i *
        HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)
have refine_1 : 0 <
  HPow.hPow (α := ℝ) (-1) i *
    HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
Tactic: refine mul_pos ?_ (Finset.sum_pos' ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
refine_1 :
  0 <
    HPow.hPow (α := ℝ) (-1) i *
      HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
⊢ 0 <
    HPow.hPow (α := ℝ) (-1) i *
        HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)
have refine_2 : ∀ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), LE.le (α := ℝ) 0 (∏ a ∈ i_1, (x - node n a))
Tactic: refine mul_pos ?_ (Finset.sum_pos' ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
refine_1 :
  0 <
    HPow.hPow (α := ℝ) (-1) i *
      HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
refine_2 :
  ∀ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), LE.le (α := ℝ) 0 (∏ a ∈ i_1, (x - node n a))
⊢ 0 <
    HPow.hPow (α := ℝ) (-1) i *
        HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)
have refine_3 : ∃ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), LT.lt (α := ℝ) 0 (∏ a ∈ i_1, (x - node n a))
Tactic: refine mul_pos ?_ (Finset.sum_pos' ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 <
    HPow.hPow (α := ℝ) (-1) i *
      HMul.hMul (α := ℝ) (↑k.factorial : ℝ) (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
have refine_1 : 0 < (↑k.factorial : ℝ) * (HPow.hPow (α := ℝ) (-1) i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)
Tactic: rw [← mul_assoc, mul_comm (a := (-1) ^ i), mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s
have by_cases : 1 ≤ i ∧ i ≤ n - k → ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s
Tactic: by_cases 1 ≤ i ∧ i ≤ n - k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
by_cases : 1 ≤ i ∧ i ≤ n - k → ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s
⊢ ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s
have by_cases₁ : ¬(1 ≤ i ∧ i ≤ n - k) → ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s
Tactic: by_cases 1 ≤ i ∧ i ≤ n - k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (hypothesis)
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∃ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), LT.lt (α := ℝ) 0 (∏ a ∈ i_1, (x - node n a))
have this : ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s
Tactic: have : ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s := by
      by_cases 1 ≤ i ∧ i ≤ n - k
      case neg => exact ⟨Finset.Icc 1 (n - k), by grind, by grind [Nat.card_Icc], by simp⟩
      case pos => exact ⟨(Finset.Icc 1 (n - k + 1)).erase i, by grind, by grind [Nat.card_Icc],
        by simp⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
this : ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s
⊢ ∃ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), LT.lt (α := ℝ) 0 (∏ a ∈ i_1, (x - node n a))
have refine_3 : ∀ (s : Finset ℕ) (hs : s ⊆ (Finset.range (n + 1)).erase i) (hscard : s.card = n - k) (hsn : 0 ∉ s),
  ∃ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), LT.lt (α := ℝ) 0 (∏ a ∈ i_1, (x - node n a))
Tactic: obtain ⟨s, hs, hscard, hsn⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
⊢ ∃ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), LT.lt (α := ℝ) 0 (∏ a ∈ i_1, (x - node n a))
have refine_3 : ∀ (a : ℕ) (ha : a ∈ s), 0 < x - node n a
Tactic: refine ⟨s, by simp [hs, hscard], Finset.prod_pos (fun a ha => ?_)⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
a : ℕ
ha : a ∈ s
⊢ node n a < 1
have rw : node n a < node n 0
Tactic: rw [← node_eq_one (n := n)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
have pos : ∀ (hk : n < k),
  eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
Tactic: by_cases! hk : n < k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
pos :
  ∀ (hk : n < k),
    eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
have neg : ∀ (hk : k ≤ n),
  eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
Tactic: by_cases! hk : n < k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hk : n < k
⊢ P.degree < (↑k : WithBot ℕ)
have grw : LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑k : WithBot ℕ)
Tactic: grw [hPdeg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hk : n < k
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
have pos : eval x 0 ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
Tactic: rw [iterate_derivative_eq_zero_of_degree_lt (by grw [hPdeg]; simpa),
      iterate_derivative_eq_zero_of_degree_lt (by simp [hk])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hk : n < k
pos : eval x 0 ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
have pos₁ : eval x 0 ≤ eval x 0
Tactic: rw [iterate_derivative_eq_zero_of_degree_lt (by grw [hPdeg]; simpa),
      iterate_derivative_eq_zero_of_degree_lt (by simp [hk])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hk : k ≤ n
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
have h : eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) = sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) P
Tactic: convert!
    sumNodes_le_sumNodes_T (fun i hi => negOnePow_mul_iterateDerivativeC_nonneg hi hx) hPbnd using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hk : k ≤ n
h : eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) = sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) P
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
have h₁ : eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ))) =
  sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) (T ℝ (↑n : ℤ))
Tactic: convert!
    sumNodes_le_sumNodes_T (fun i hi => negOnePow_mul_iterateDerivativeC_nonneg hi hx) hPbnd using 1