awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
inr :
  ∀
    (this :
      ∀ (n : ℕ) (hn : n ≠ 0),
        roots (T ℝ (↑n : ℤ)) =
          Finset.val
            (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
              (Finset.range n)))
    (hn : n = 0),
    roots (T ℝ (↑n : ℤ)) =
      Finset.val
        (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
          (Finset.range n))
wlog! :
  ∀ (n : ℕ) (hn : n ≠ 0),
    roots (T ℝ (↑n : ℤ)) =
      Finset.val
        (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
          (Finset.range n))
⊢ roots (T ℝ (↑n : ℤ)) =
    Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
        (Finset.range n))

Tactic:
wlog! hn : n ≠ 0
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
this :
  ∀ (n : ℕ) (hn : n ≠ 0),
    roots (T ℝ (↑n : ℤ)) =
      Finset.val
        (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
          (Finset.range n))
hn : n = 0
⊢ roots (T ℝ (↑n : ℤ)) =
    Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
        (Finset.range n))

Tactic:
simp [hn]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
⊢ roots (T ℝ (↑n : ℤ)) =
    Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
        (Finset.range n))

Tactic:
roots_eq_of_degree_eq_card (fun x hx ↦ ?_) ?_

Premises used: Polynomial.roots_eq_of_degree_eq_card
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
refine_1 :
  ∀ (x : ℝ)
    (hx :
      Membership.mem (γ := Finset ℝ)
        (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
          (Finset.range n))
        x),
    eval x (T ℝ (↑n : ℤ)) = 0
refine_2 :
  (↑(Finset.card (α := ℝ)
          (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
            (Finset.range n))) :
      WithBot ℕ) =
    degree (T ℝ (↑n : ℤ))
⊢ roots (T ℝ (↑n : ℤ)) =
    Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
        (Finset.range n))

Tactic:
refine roots_eq_of_degree_eq_card (fun x hx ↦ ?_) ?_

Premises used: Polynomial.roots_eq_of_degree_eq_card
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
refine_1 :
  ∀ (k : ℕ) (hk : k ∈ Finset.range n)
    (hx : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x), eval x (T ℝ (↑n : ℤ)) = 0
⊢ eval x (T ℝ (↑n : ℤ)) = 0

Tactic:
obtain ⟨k, hk, hx⟩ := Finset.mem_image.mp hx

Premises used: Finset.mem_image, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 :
  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
hx : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
refine_1 :
  ∃ (k_1 : ℤ),
    (↑(↑n : ℤ) : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) =
      (HMul.hMul (α := ℝ) 2 (↑k_1 : ℝ) + 1) * π / 2
⊢ eval x (T ℝ (↑n : ℤ)) = 0

Tactic:
rw [← hx, T_real_cos, cos_eq_zero_iff]

Premises used: Real.cos_eq_zero_iff, Polynomial.Chebyshev.T_real_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 :
  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
hx : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
h :
  (↑(↑n : ℤ) : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) =
    (HMul.hMul (α := ℝ) 2 (↑(↑k : ℤ) : ℝ) + 1) * π / 2
⊢ ∃ (k_1 : ℤ),
    (↑(↑n : ℤ) : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) =
      (HMul.hMul (α := ℝ) 2 (↑k_1 : ℝ) + 1) * π / 2

Tactic:
use k
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 :
  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
hx : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
h : (↑(↑n : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) = (↑n : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑k : ℤ) : ℝ) + 1)
⊢ (↑(↑n : ℤ) : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) =
    (HMul.hMul (α := ℝ) 2 (↑(↑k : ℤ) : ℝ) + 1) * π / 2

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 :
  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
hx : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
h h₁ h₂ h₃ : n * (2 * k + 1) = n * (2 * k + 1)
⊢ (↑(↑n : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) = (↑n : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑k : ℤ) : ℝ) + 1)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
refine_2 :
  Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
    (↑(Finset.range n) : Set ℕ)
⊢ (↑(Finset.card (α := ℝ)
          (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
            (Finset.range n))) :
      WithBot ℕ) =
    degree (T ℝ (↑n : ℤ))

Tactic:
rw [Finset.card_image_of_injOn, Finset.card_range, degree_T, Int.natAbs_natCast]

Premises used: Finset.card_range, Polynomial.Chebyshev.degree_T, Finset.card_image_of_injOn, Int.natAbs_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
⊢ Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
    (↑(Finset.range n) : Set ℕ)

Tactic:
(Finset.range n).nodup_map_iff_injOn.mp (roots_T_real_nodup n)

Premises used: Iff.mp, Finset.nodup_map_iff_injOn, Polynomial.Chebyshev.roots_T_real_nodup
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
⊢ Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
    (↑(Finset.range n) : Set ℕ)

Tactic:
exact (Finset.range n).nodup_map_iff_injOn.mp (roots_T_real_nodup n)

Premises used: Iff.mp, Finset.nodup_map_iff_injOn, Polynomial.Chebyshev.roots_T_real_nodup
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hk : k < n
⊢ Multiset.Nodup (α := ℝ)
    (Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
        (Finset.range n)))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hk : k < n
rw :
  Membership.mem (γ := Multiset ℝ)
    (Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
        (Finset.range n)))
    (cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
⊢ rootMultiplicity (cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ))) (T ℝ (↑n : ℤ)) = 1

Tactic:
rw [← count_roots, roots_T_real, Multiset.count_eq_one_of_mem (by simp)]

Premises used: Polynomial.count_roots, Multiset.count_eq_one_of_mem, Polynomial.Chebyshev.roots_T_real
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hk : k < n
⊢ Membership.mem (γ := Multiset ℝ)
    (Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
        (Finset.range n)))
    (cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
⊢ Multiset.Nodup (α := ℝ)
    (Multiset.map (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
      (Multiset.range n))

Tactic:
(Finset.range n).nodup_map_iff_injOn.mpr ?_

Premises used: Iff.mpr, Multiset.ofList, Multiset.range, Finset.nodup_map_iff_injOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
refine :
  Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
    (↑(Finset.range n) : Set ℕ)
⊢ Multiset.Nodup (α := ℝ)
    (Multiset.map (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
      (Multiset.range n))

Tactic:
refine (Finset.range n).nodup_map_iff_injOn.mpr ?_

Premises used: Iff.mpr, Finset.nodup_map_iff_injOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hf :
  Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
    (↑(Finset.range n) : Set ℕ)
h :
  Set.MapsTo (fun (k : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
    (↑(Finset.range n) : Set ℕ) (Set.Icc 0 π)
⊢ Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
    (↑(Finset.range n) : Set ℕ)

Tactic:
apply injOn_cos.comp

Premises used: Set.InjOn.comp, Real.injOn_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n x : ℕ
hx : x ∈ (↑(Finset.range n) : Set ℕ)
y : ℕ
hy : y ∈ (↑(Finset.range n) : Set ℕ)
hxy :
  Eq (α := ℝ) ((fun (k : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) x)
    ((fun (k : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) y)
⊢ HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 = HAdd.hAdd (α := ℝ) (↑y : ℝ) 1

Tactic:
field_simp at hxy
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n x : ℕ
hx : x ∈ (↑(Finset.range n) : Set ℕ)
y : ℕ
hy : y ∈ (↑(Finset.range n) : Set ℕ)
hxy : HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 = HAdd.hAdd (α := ℝ) (↑y : ℝ) 1
⊢ x = y

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hk : k ∈ (↑(Finset.range n) : Set ℕ)
⊢ LE.le (α := ℝ) 0 ((fun (k : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) k)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
h :
  ∀ (k : ℕ) (hk : k ∈ (↑(Finset.range n) : Set ℕ)),
    (fun (k : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) k ≤ π
⊢ Set.MapsTo (fun (k : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
    (↑(Finset.range n) : Set ℕ) (Set.Icc 0 π)

Tactic:
refine fun k hk => Set.mem_Icc.mpr ⟨by positivity, ?_⟩

Premises used: Iff.mpr, And.intro, Set.mem_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hk : k ∈ (↑(Finset.range n) : Set ℕ)
h : HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ (fun (k : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) k ≤ π

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hk : k ∈ (↑(Finset.range n) : Set ℕ)
h : k + 1 ≤ n + 1
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hk : k ∈ (↑(Finset.range n) : Set ℕ)
⊢ k + 1 ≤ n + 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
inr :
  ∀
    (this :
      ∀ (n : ℕ) (hn : n ≠ 0),
        roots (U ℝ (↑n : ℤ)) =
          Finset.val
            (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
              (Finset.range n)))
    (hn : n = 0),
    roots (U ℝ (↑n : ℤ)) =
      Finset.val
        (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
          (Finset.range n))
wlog! :
  ∀ (n : ℕ) (hn : n ≠ 0),
    roots (U ℝ (↑n : ℤ)) =
      Finset.val
        (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
          (Finset.range n))
⊢ roots (U ℝ (↑n : ℤ)) =
    Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
        (Finset.range n))

Tactic:
wlog! hn : n ≠ 0
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
this :
  ∀ (n : ℕ) (hn : n ≠ 0),
    roots (U ℝ (↑n : ℤ)) =
      Finset.val
        (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
          (Finset.range n))
hn : n = 0
⊢ roots (U ℝ (↑n : ℤ)) =
    Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
        (Finset.range n))

Tactic:
simp [hn]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
⊢ roots (U ℝ (↑n : ℤ)) =
    Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
        (Finset.range n))

Tactic:
roots_eq_of_degree_eq_card (fun x hx ↦ ?_) ?_

Premises used: Polynomial.roots_eq_of_degree_eq_card
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
refine_1 :
  ∀ (x : ℝ)
    (hx :
      Membership.mem (γ := Finset ℝ)
        (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
          (Finset.range n))
        x),
    eval x (U ℝ (↑n : ℤ)) = 0
refine_2 :
  (↑(Finset.card (α := ℝ)
          (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
            (Finset.range n))) :
      WithBot ℕ) =
    degree (U ℝ (↑n : ℤ))
⊢ roots (U ℝ (↑n : ℤ)) =
    Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
        (Finset.range n))

Tactic:
refine roots_eq_of_degree_eq_card (fun x hx ↦ ?_) ?_

Premises used: Polynomial.roots_eq_of_degree_eq_card
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
      (Finset.range n))
    x
refine_1 :
  ∀ (k : ℕ) (hk : k ∈ Finset.range n)
    (hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = x), eval x (U ℝ (↑n : ℤ)) = 0
⊢ eval x (U ℝ (↑n : ℤ)) = 0

Tactic:
obtain ⟨k, hk, hx⟩ := Finset.mem_image.mp hx

Premises used: Finset.mem_image, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
      (Finset.range n))
    x
k : ℕ
hk : k ∈ Finset.range n
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = x
this : eval x (U ℝ (↑n : ℤ)) * sin (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = 0
⊢ 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
      (Finset.range n))
    x
k : ℕ
hk : k ∈ Finset.range n
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = x
this : eval x (U ℝ (↑n : ℤ)) * sin (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = 0
refine : HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < π
⊢ eval x (U ℝ (↑n : ℤ)) = 0

Tactic:
refine (mul_eq_zero_iff_right (ne_of_gt (sin_pos_of_pos_of_lt_pi (by positivity) ?_))).mp this

Premises used: ne_of_gt, Real.sin_pos_of_pos_of_lt_pi, Iff.mp, mul_eq_zero_iff_right
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
      (Finset.range n))
    x
k : ℕ
hk : k ∈ Finset.range n
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = x
this : eval x (U ℝ (↑n : ℤ)) * sin (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = 0
field_simp : HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < π

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
      (Finset.range n))
    x
k : ℕ
hk : k ∈ Finset.range n
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = x
this : eval x (U ℝ (↑n : ℤ)) * sin (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = 0
norm_cast : k + 1 < n + 1
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
      (Finset.range n))
    x
k : ℕ
hk : k ∈ Finset.range n
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = x
this : eval x (U ℝ (↑n : ℤ)) * sin (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = 0
⊢ k + 1 < n + 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
      (Finset.range n))
    x
k : ℕ
hk : k ∈ Finset.range n
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = x
refine_1 : eval x (U ℝ (↑n : ℤ)) * sin (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = 0
⊢ eval x (U ℝ (↑n : ℤ)) = 0

Tactic:
suffices (U ℝ n).eval x * sin ((k + 1) * π / (n + 1)) = 0 by
      refine (mul_eq_zero_iff_right (ne_of_gt (sin_pos_of_pos_of_lt_pi (by positivity) ?_))).mp this
      field_simp
      norm_cast
      grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
      (Finset.range n))
    x
k : ℕ
hk : k ∈ Finset.range n
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = x
refine_1 :
  ∃ (n_1 : ℤ),
    (↑n_1 : ℝ) * π =
      HAdd.hAdd (α := ℝ) (↑(↑n : ℤ) : ℝ) 1 * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ eval x (U ℝ (↑n : ℤ)) * sin (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = 0

Tactic:
rw [← hx, U_real_cos, sin_eq_zero_iff]

Premises used: Polynomial.Chebyshev.U_real_cos, Real.sin_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
      (Finset.range n))
    x
k : ℕ
hk : k ∈ Finset.range n
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = x
h :
  (↑(HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) : ℝ) * π =
    HAdd.hAdd (α := ℝ) (↑(↑n : ℤ) : ℝ) 1 * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ ∃ (n_1 : ℤ),
    (↑n_1 : ℝ) * π =
      HAdd.hAdd (α := ℝ) (↑(↑n : ℤ) : ℝ) 1 * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
use k + 1
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
      (Finset.range n))
    x
k : ℕ
hk : k ∈ Finset.range n
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = x
h :
  (↑(HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 =
    HAdd.hAdd (α := ℝ) (↑(↑n : ℤ) : ℝ) 1 * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
⊢ (↑(HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) : ℝ) * π =
    HAdd.hAdd (α := ℝ) (↑(↑n : ℤ) : ℝ) 1 * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
      (Finset.range n))
    x
k : ℕ
hk : k ∈ Finset.range n
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = x
h : (k + 1) * (n + 1) = (n + 1) * (k + 1)
⊢ (↑(HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 =
    HAdd.hAdd (α := ℝ) (↑(↑n : ℤ) : ℝ) 1 * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
      (Finset.range n))
    x
k : ℕ
hk : k ∈ Finset.range n
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = x
⊢ (k + 1) * (n + 1) = (n + 1) * (k + 1)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
refine_2 :
  Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
    (↑(Finset.range n) : Set ℕ)
⊢ (↑(Finset.card (α := ℝ)
          (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
            (Finset.range n))) :
      WithBot ℕ) =
    degree (U ℝ (↑n : ℤ))

Tactic:
rw [Finset.card_image_of_injOn, Finset.card_range, degree_U_natCast]

Premises used: Finset.card_range, Finset.card_image_of_injOn, Polynomial.Chebyshev.degree_U_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
⊢ Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
    (↑(Finset.range n) : Set ℕ)

Tactic:
(Finset.range n).nodup_map_iff_injOn.mp (roots_U_real_nodup n)

Premises used: Iff.mp, Finset.nodup_map_iff_injOn, Polynomial.Chebyshev.roots_U_real_nodup