awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
this : Irrational (cos ((↑(Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))) : ℝ) * π))
⊢ Irrational (cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
have h : (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ) =
  (↑(Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))) : ℝ) * π
Tactic: convert! this using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
this : Irrational (cos ((↑(Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))) : ℝ) * π))
⊢ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ) =
    (↑(Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))) : ℝ) * π
have h : (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ) =
  (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
⊢ Irrational x
have suffices : Irrational (cos ((↑(Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))) : ℝ) * π))
Tactic: suffices Irrational (cos ((Rat.divInt (2 * k + 1) (2 * n)) * π)) by
    rw [← hk₂]; convert! this using 2; push_cast; field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
⊢ Irrational (cos ((↑(Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))) : ℝ) * π))
have hr : 3 < (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den
Tactic: apply irrational_cos_rat_mul_pi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
⊢ 3 < (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den
have hr : ∀ (hnz : (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den ≤ 3), x = 0
Tactic: contrapose! hnz
Cleared hypotheses: hnz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
hnz : (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den ≤ 3
⊢ (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den = 2 * n / (2 * n).gcd (2 * k + 1)
have rw : (if HMul.hMul (α := ℤ) 2 (↑n : ℤ) = 0 then 1
  else
    (HMul.hMul (α := ℤ) 2 (↑n : ℤ)).natAbs / (HMul.hMul (α := ℤ) 2 (↑n : ℤ)).gcd (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1)) =
  2 * n / (2 * n).gcd (2 * k + 1)
Tactic: rw [Rat.den_divInt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
hnz : (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den ≤ 3
⊢ (if HMul.hMul (α := ℤ) 2 (↑n : ℤ) = 0 then 1
    else
      (HMul.hMul (α := ℤ) 2 (↑n : ℤ)).natAbs /
        (HMul.hMul (α := ℤ) 2 (↑n : ℤ)).gcd (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1)) =
    2 * n / (2 * n).gcd (2 * k + 1)
have norm_cast : (if 2 * n = 0 then 1 else 2 * n / (2 * n).gcd (2 * k + 1)) = 2 * n / (2 * n).gcd (2 * k + 1)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
hnz : (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den ≤ 3
⊢ 2 * n / (2 * n).gcd (2 * k + 1) = 2 * (n / n.gcd (2 * k + 1))
have rw : 2 * n / n.gcd (2 * k + 1) = 2 * (n / n.gcd (2 * k + 1))
Tactic: rw [Nat.Coprime.gcd_mul_left_cancel n (by simp),
      Nat.mul_div_assoc _ (Nat.gcd_dvd_left ..)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
hnz : (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den ≤ 3
rw : 2 * n / n.gcd (2 * k + 1) = 2 * (n / n.gcd (2 * k + 1))
⊢ 2 * n / (2 * n).gcd (2 * k + 1) = 2 * (n / n.gcd (2 * k + 1))
have rw₁ : 2 * (n / n.gcd (2 * k + 1)) = 2 * (n / n.gcd (2 * k + 1))
Tactic: rw [Nat.Coprime.gcd_mul_left_cancel n (by simp),
      Nat.mul_div_assoc _ (Nat.gcd_dvd_left ..)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
hnz : (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den ≤ 3
⊢ x = 0
have this : (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den = 2 * (n / n.gcd (2 * k + 1))
Tactic: have : (Rat.divInt (2 * k + 1) (2 * n)).den = 2 * (n / n.gcd (2 * k + 1)) := calc
    _ = 2 * n / (2 * n).gcd (2 * k + 1) := by rw [Rat.den_divInt]; norm_cast; simp [hn]
    _ = _ := by rw [Nat.Coprime.gcd_mul_left_cancel n (by simp),
      Nat.mul_div_assoc _ (Nat.gcd_dvd_left ..)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
hnz : (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den ≤ 3
this :
  (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den = 2 * (n / n.gcd (2 * k + 1))
⊢ x = 0
have hn₁ : 2 * k + 1 = n
Tactic: have hn : 2 * k + 1 = n := Nat.eq_of_dvd_of_lt_two_mul (by simp) (Nat.gcd_eq_left_iff_dvd.mp <|
    Nat.eq_of_dvd_of_div_eq_one (Nat.gcd_dvd_left ..) (by grind [Rat.den_pos])) (by grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn_1 : n ≠ 0
hnz : (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den ≤ 3
this :
  (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den = 2 * (n / n.gcd (2 * k + 1))
hn : 2 * k + 1 = n
⊢ x = 0
have hr : ∀
  (hroot :
    Membership.mem (γ := Finset ℝ)
      (Finset.image (fun (k : ℕ) ↦ cos ((↑(2 * k + 1) : ℝ) * π / (↑(2 * n) : ℝ))) (Finset.range n)) x)
  (hk₂ : cos ((↑(2 * k + 1) : ℝ) * π / (↑(2 * n) : ℝ)) = x) (hnz : (NNRat.divNat (2 * k + 1) (2 * n)).den ≤ 3)
  (this : (NNRat.divNat (2 * k + 1) (2 * n)).den = 2 * (n / n.gcd (2 * k + 1))), cos ((↑n : ℝ) * π / (↑(2 * n) : ℝ)) = 0
Tactic: rw_mod_cast [← hk₂, hn]
Cleared hypotheses: hroot, hk₂, hnz, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
x : ℝ
k : ℕ
hk₁ : k ∈ Finset.range n
hn_1 : ¬n = 0
hn : 2 * k + 1 = n
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((↑(2 * k + 1) : ℝ) * π / (↑(2 * n) : ℝ))) (Finset.range n)) x
hk₂ : cos ((↑(2 * k + 1) : ℝ) * π / (↑(2 * n) : ℝ)) = x
hnz : (NNRat.divNat (2 * k + 1) (2 * n)).den ≤ 3
this : (NNRat.divNat (2 * k + 1) (2 * n)).den = 2 * (n / n.gcd (2 * k + 1))
⊢ cos ((↑n : ℝ) * π / (↑(2 * n) : ℝ)) = 0
have h : (↑n : ℝ) * π / (↑(2 * n) : ℝ) = π / 2
Tactic: convert! cos_pi_div_two using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
x : ℝ
k : ℕ
hk₁ : k ∈ Finset.range n
hn_1 : ¬n = 0
hn : 2 * k + 1 = n
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((↑(2 * k + 1) : ℝ) * π / (↑(2 * n) : ℝ))) (Finset.range n)) x
hk₂ : cos ((↑(2 * k + 1) : ℝ) * π / (↑(2 * n) : ℝ)) = x
hnz : (NNRat.divNat (2 * k + 1) (2 * n)).den ≤ 3
this : (NNRat.divNat (2 * k + 1) (2 * n)).den = 2 * (n / n.gcd (2 * k + 1))
⊢ (↑n : ℝ) * π / (↑(2 * n) : ℝ) = π / 2
have h : (↑n : ℝ) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ) = π / 2
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
⊢ |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))
have inr : ∀
  (this :
    ∀ (n : ℤ) (k : ℕ) {x : ℝ} (hx : |x| ≤ 1) (hn : 0 ≤ n),
      |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n)))
  (hn : ¬0 ≤ n),
  |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))
Tactic: wlog hn : 0 ≤ n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
inr :
  ∀
    (this :
      ∀ (n : ℤ) (k : ℕ) {x : ℝ} (hx : |x| ≤ 1) (hn : 0 ≤ n),
        |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| ≤
          eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n)))
    (hn : ¬0 ≤ n),
    |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))
⊢ |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))
have wlog : ∀ (n : ℤ) (k : ℕ) {x : ℝ} (hx : |x| ≤ 1) (hn : 0 ≤ n),
  |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))
Tactic: wlog hn : 0 ≤ n
Cleared hypotheses: n, k, x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
this :
  ∀ (n : ℤ) (k : ℕ) {x : ℝ} (hx : |x| ≤ 1) (hn : 0 ≤ n),
    |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))
hn : ¬0 ≤ n
⊢ |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))
have h : |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| = |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (-n)))|
Tactic: convert! this (-n) k hx (by grind) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
this :
  ∀ (n : ℤ) (k : ℕ) {x : ℝ} (hx : |x| ≤ 1) (hn : 0 ≤ n),
    |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))
hn : ¬0 ≤ n
h :
  |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| = |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (-n)))|
⊢ |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))
have h₁ : eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n)) = eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (-n)))
Tactic: convert! this (-n) k hx (by grind) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
this :
  ∀ (n : ℤ) (k : ℕ) {x : ℝ} (hx : |x| ≤ 1) (hn : 0 ≤ n),
    |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))
hn : ¬0 ≤ n
⊢ |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| = |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (-n)))|
have h : |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| = |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))|
Tactic: rw [T_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
this :
  ∀ (n : ℤ) (k : ℕ) {x : ℝ} (hx : |x| ≤ 1) (hn : 0 ≤ n),
    |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))
hn : ¬0 ≤ n
⊢ eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n)) = eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (-n)))
have h : eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n)) = eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))
Tactic: rw [T_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
hn : 0 ≤ n
⊢ |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))
have lift : ∀ (n : ℕ),
  |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))| ≤
    eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
Tactic: lift n to ℕ using hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
⊢ |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))| ≤
    eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
have this : Membership.mem (γ := Submodule ℕ ℝ[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)))
  ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
Tactic: have := T_iterate_derivative_mem_span_T (R := ℝ) n k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this :
  Membership.mem (γ := Submodule ℕ ℝ[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)))
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
⊢ |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))| ≤
    eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
have obtain : ∀ (f : ℝ[X] →₀ ℕ) (hfsupp : (↑f.support : Set ℝ[X]) ⊆ (fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k))
  (hfderiv :
    Eq (α := ℝ[X]) (f.sum fun (mi : ℝ[X]) (r : ℕ) ↦ r • mi) ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))),
  |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))| ≤
    eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
Tactic: obtain ⟨f, hfsupp, hfderiv⟩ := Submodule.mem_span_set.mp this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this :
  Membership.mem (γ := Submodule ℕ ℝ[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)))
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
f : ℝ[X] →₀ ℕ
hfsupp : (↑f.support : Set ℝ[X]) ⊆ (fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)
hfderiv : Eq (α := ℝ[X]) (f.sum fun (mi : ℝ[X]) (r : ℕ) ↦ r • mi) ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
⊢ Eq (α := ℝ[X]) (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) p)
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
have rw : Eq (α := ℝ[X]) (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) p)
  (f.sum fun (mi : ℝ[X]) (r : ℕ) ↦ r • mi)
Tactic: rw [← hfderiv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this :
  Membership.mem (γ := Submodule ℕ ℝ[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)))
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
f : ℝ[X] →₀ ℕ
hfsupp : (↑f.support : Set ℝ[X]) ⊆ (fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)
hfderiv : Eq (α := ℝ[X]) (f.sum fun (mi : ℝ[X]) (r : ℕ) ↦ r • mi) ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
⊢ |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))| ≤
    eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
have hfderiv₁ : Eq (α := ℝ[X]) (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) p)
  ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
Tactic: replace hfderiv : ∑ p ∈ f.support, f p • p = derivative^[k] (T ℝ n) := by rw [← hfderiv]; rfl
Cleared hypotheses: hfderiv
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this :
  Membership.mem (γ := Submodule ℕ ℝ[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)))
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
f : ℝ[X] →₀ ℕ
hfsupp : (↑f.support : Set ℝ[X]) ⊆ (fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)
hfderiv :
  Eq (α := ℝ[X]) (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) p)
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
y : ℝ
⊢ ∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) (eval y p) =
    eval y ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
have rw : Eq (α := ℝ) (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) (eval y p))
  (∑ i ∈ f.support, eval y (HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) i : ℕ) i))
Tactic: rw [← hfderiv, Polynomial.eval_finsetSum]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this :
  Membership.mem (γ := Submodule ℕ ℝ[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)))
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
f : ℝ[X] →₀ ℕ
hfsupp : (↑f.support : Set ℝ[X]) ⊆ (fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)
hfderiv :
  Eq (α := ℝ[X]) (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) p)
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
⊢ |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))| ≤
    eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
have hf : ∀ (y : ℝ),
  ∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) (eval y p) =
    eval y ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
Tactic: have hf (y : ℝ) :
      ∑ p ∈ f.support, f p • p.eval y = (derivative^[k] (T ℝ n)).eval y := by
    rw [← hfderiv, Polynomial.eval_finsetSum]
    simp_rw [Polynomial.eval_smul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this :
  Membership.mem (γ := Submodule ℕ ℝ[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)))
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
f : ℝ[X] →₀ ℕ
hfsupp : (↑f.support : Set ℝ[X]) ⊆ (fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)
hfderiv :
  Eq (α := ℝ[X]) (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) p)
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
hf :
  ∀ (y : ℝ),
    ∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) (eval y p) =
      eval y ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
⊢ |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))| ≤
    eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
have rw : LE.le (α := ℝ) |∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) (eval x p)|
  (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) (eval 1 p))
Tactic: rw [← hf x, ← hf 1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this :
  Membership.mem (γ := Submodule ℕ ℝ[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)))
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
f : ℝ[X] →₀ ℕ
hfsupp : (↑f.support : Set ℝ[X]) ⊆ (fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)
hfderiv :
  Eq (α := ℝ[X]) (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) p)
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
hf :
  ∀ (y : ℝ),
    ∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) (eval y p) =
      eval y ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
⊢ LE.le (α := ℝ) |∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) (eval x p)|
    (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) (eval 1 p))
have grw : LE.le (α := ℝ) (∑ i ∈ f.support, |HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) i : ℕ) (eval x i)|)
  (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) (eval 1 p))
Tactic: grw [Finset.abs_sum_le_sum_abs]