awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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
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)
⊢ (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:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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 2 * n = 0 then 1 else 2 * n / (2 * n).gcd (2 * k + 1)) = 2 * n / (2 * n).gcd (2 * k + 1)

Tactic:
simp [hn]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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
⊢ Nat.Coprime 2 (2 * k + 1)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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))
rw₁ 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))

Tactic:
rw [Nat.Coprime.gcd_mul_left_cancel n (by simp),
      Nat.mul_div_assoc _ (Nat.gcd_dvd_left ..)]

Premises used: Nat.gcd_dvd_left, Nat.Coprime.gcd_mul_left_cancel, Nat.mul_div_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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 / 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 ..)]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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))
⊢ 2 * k + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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))
⊢ n / n.gcd (2 * k + 1) = 1

Tactic:
grind [Rat.den_pos]

Premises used: Rat.den_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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))
⊢ 2 * k + 1 < 2 * n

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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))
⊢ 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)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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
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
⊢ x = 0

Tactic:
rw_mod_cast [← hk₂, hn]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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 (π / 2) = 0

Tactic:
cos_pi_div_two

Premises used: Real.cos_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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))
h : (↑n : ℝ) * π / (↑(2 * n) : ℝ) = π / 2
⊢ cos ((↑n : ℝ) * π / (↑(2 * n) : ℝ)) = 0

Tactic:
convert! cos_pi_div_two using 2

Premises used: Real.cos_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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))
h : (↑n : ℝ) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ) = π / 2
⊢ (↑n : ℝ) * π / (↑(2 * n) : ℝ) = π / 2

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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 : ℝ) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ) = π / 2

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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))
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))
⊢ |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))

Tactic:
wlog hn : 0 ≤ n
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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
⊢ 0 ≤ -n

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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)))|
h₁ : eval 1 ((⇑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))

Tactic:
convert! this (-n) k hx (by grind) using 1

Premises used: Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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 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 x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (-n)))|

Tactic:
rw [T_neg]

Premises used: Polynomial.Chebyshev.T_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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 h₁ : eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n)) = eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n))
⊢ eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ n)) = eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (-n)))

Tactic:
rw [T_neg]

Premises used: Polynomial.Chebyshev.T_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
hn : 0 ≤ n
⊢ 0 ≤ n

Tactic:
hn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
hn : 0 ≤ n
lift :
  ∀ (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))

Tactic:
lift n to ℕ using hn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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 : ℤ)))
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 : ℤ)))
⊢ |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

Premises used: Submodule.mem_span_set, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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 : ℤ)))
rw :
  Eq (α := ℝ[X]) (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) p)
    (f.sum fun (mi : ℝ[X]) (r : ℕ) ↦ r • mi)
⊢ Eq (α := ℝ[X]) (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) p)
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))

Tactic:
rw [← hfderiv]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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)
    (f.sum fun (mi : ℝ[X]) (r : ℕ) ↦ r • mi)

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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 : ℤ)))

Tactic:
replace hfderiv : ∑ p ∈ f.support, f p • p = derivative^[k] (T ℝ n) := by rw [← hfderiv]; rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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 : ℝ
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))
⊢ ∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) (eval y p) =
    eval y ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))

Tactic:
rw [← hfderiv, Polynomial.eval_finsetSum]

Premises used: Polynomial.eval_finsetSum
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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 : ℝ
⊢ 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:
simp_rw [Polynomial.eval_smul]

Premises used: Polynomial.eval_smul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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 : ℤ)))

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]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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 : ℤ)))
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))
⊢ |eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))| ≤
    eval 1 ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))

Tactic:
rw [← hf x, ← hf 1]

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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 : ℤ)))
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))
⊢ 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:
grw [Finset.abs_sum_le_sum_abs]

Premises used: Finset.abs_sum_le_sum_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
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 (α := ℝ) (∑ 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:
Finset.sum_le_sum (fun i hi => ?_)

Premises used: Finset.sum_le_sum