awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
⊢ roots (T ℝ (↑n : ℤ)) =
    Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
        (Finset.range n))
have 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))
Tactic: wlog! hn : n ≠ 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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))
⊢ roots (T ℝ (↑n : ℤ)) =
    Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
        (Finset.range n))
have 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))
Tactic: wlog! hn : n ≠ 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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))
have 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
Tactic: refine roots_eq_of_degree_eq_card (fun x hx ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ roots (T ℝ (↑n : ℤ)) =
    Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
        (Finset.range n))
have 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 : ℤ))
Tactic: refine roots_eq_of_degree_eq_card (fun x hx ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ eval x (T ℝ (↑n : ℤ)) = 0
have 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
Tactic: obtain ⟨k, hk, hx⟩ := Finset.mem_image.mp hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ eval x (T ℝ (↑n : ℤ)) = 0
have refine_1 : ∃ (k_1 : ℤ),
  (↑(↑n : ℤ) : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) =
    (HMul.hMul (α := ℝ) 2 (↑k_1 : ℝ) + 1) * π / 2
Tactic: rw [← hx, T_real_cos, cos_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ ∃ (k_1 : ℤ),
    (↑(↑n : ℤ) : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) =
      (HMul.hMul (α := ℝ) 2 (↑k_1 : ℝ) + 1) * π / 2
have h : (↑(↑n : ℤ) : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) =
  (HMul.hMul (α := ℝ) 2 (↑(↑k : ℤ) : ℝ) + 1) * π / 2
Tactic: use k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ (↑(↑n : ℤ) : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) =
    (HMul.hMul (α := ℝ) 2 (↑(↑k : ℤ) : ℝ) + 1) * π / 2
have h : (↑(↑n : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) = (↑n : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑k : ℤ) : ℝ) + 1)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ (↑(↑n : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) = (↑n : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑k : ℤ) : ℝ) + 1)
have h : n * (2 * k + 1) = n * (2 * k + 1)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ (↑(Finset.card (α := ℝ)
          (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
            (Finset.range n))) :
      WithBot ℕ) =
    degree (T ℝ (↑n : ℤ))
have refine_2 : Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
  (↑(Finset.range n) : Set ℕ)
Tactic: rw [Finset.card_image_of_injOn, Finset.card_range, degree_T, Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n k : ℕ
hk : k < n
⊢ rootMultiplicity (cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ))) (T ℝ (↑n : ℤ)) = 1
have 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 : ℝ)))
Tactic: rw [← count_roots, roots_T_real, Multiset.count_eq_one_of_mem (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
⊢ Multiset.Nodup (α := ℝ)
    (Multiset.map (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
      (Multiset.range n))
have refine : Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
  (↑(Finset.range n) : Set ℕ)
Tactic: refine (Finset.range n).nodup_map_iff_injOn.mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
⊢ Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
    (↑(Finset.range n) : Set ℕ)
have hf : Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
  (↑(Finset.range n) : Set ℕ)
Tactic: apply injOn_cos.comp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hf :
  Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
    (↑(Finset.range n) : Set ℕ)
⊢ Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
    (↑(Finset.range n) : Set ℕ)
have h : Set.MapsTo (fun (k : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (↑(Finset.range n) : Set ℕ)
  (Set.Icc 0 π)
Tactic: apply injOn_cos.comp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
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)
⊢ x = y
have hxy₁ : HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 = HAdd.hAdd (α := ℝ) (↑y : ℝ) 1
Tactic: field_simp at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
⊢ Set.MapsTo (fun (k : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
    (↑(Finset.range n) : Set ℕ) (Set.Icc 0 π)
have h : ∀ (k : ℕ) (hk : k ∈ (↑(Finset.range n) : Set ℕ)),
  (fun (k : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) k ≤ π
Tactic: refine fun k hk => Set.mem_Icc.mpr ⟨by positivity, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n k : ℕ
hk : k ∈ (↑(Finset.range n) : Set ℕ)
⊢ (fun (k : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) k ≤ π
have h : HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n k : ℕ
hk : k ∈ (↑(Finset.range n) : Set ℕ)
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have h : k + 1 ≤ n + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
⊢ roots (U ℝ (↑n : ℤ)) =
    Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
        (Finset.range n))
have 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))
Tactic: wlog! hn : n ≠ 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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))
⊢ roots (U ℝ (↑n : ℤ)) =
    Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
        (Finset.range n))
have 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))
Tactic: wlog! hn : n ≠ 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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))
have 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
Tactic: refine roots_eq_of_degree_eq_card (fun x hx ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ roots (U ℝ (↑n : ℤ)) =
    Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
        (Finset.range n))
have refine_2 : (↑(Finset.card (α := ℝ)
        (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
          (Finset.range n))) :
    WithBot ℕ) =
  degree (U ℝ (↑n : ℤ))
Tactic: refine roots_eq_of_degree_eq_card (fun x hx ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ eval x (U ℝ (↑n : ℤ)) = 0
have refine_1 : ∀ (k : ℕ) (hk : k ∈ Finset.range n) (hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = x),
  eval x (U ℝ (↑n : ℤ)) = 0
Tactic: obtain ⟨k, hk, hx⟩ := Finset.mem_image.mp hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ eval x (U ℝ (↑n : ℤ)) = 0
have refine : HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < π
Tactic: refine (mul_eq_zero_iff_right (ne_of_gt (sin_pos_of_pos_of_lt_pi (by positivity) ?_))).mp this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < π
have field_simp : HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have norm_cast : k + 1 < n + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ eval x (U ℝ (↑n : ℤ)) = 0
have refine_1 : eval x (U ℝ (↑n : ℤ)) * sin (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ eval x (U ℝ (↑n : ℤ)) * sin (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = 0
have refine_1 : ∃ (n_1 : ℤ),
  (↑n_1 : ℝ) * π =
    HAdd.hAdd (α := ℝ) (↑(↑n : ℤ) : ℝ) 1 * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [← hx, U_real_cos, sin_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ ∃ (n_1 : ℤ),
    (↑n_1 : ℝ) * π =
      HAdd.hAdd (α := ℝ) (↑(↑n : ℤ) : ℝ) 1 * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have h : (↑(HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) : ℝ) * π =
  HAdd.hAdd (α := ℝ) (↑(↑n : ℤ) : ℝ) 1 * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: use k + 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ (↑(HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) : ℝ) * π =
    HAdd.hAdd (α := ℝ) (↑(↑n : ℤ) : ℝ) 1 * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have h : (↑(HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 =
  HAdd.hAdd (α := ℝ) (↑(↑n : ℤ) : ℝ) 1 * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ (↑(HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 =
    HAdd.hAdd (α := ℝ) (↑(↑n : ℤ) : ℝ) 1 * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
have h : (k + 1) * (n + 1) = (n + 1) * (k + 1)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ (↑(Finset.card (α := ℝ)
          (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
            (Finset.range n))) :
      WithBot ℕ) =
    degree (U ℝ (↑n : ℤ))
have refine_2 : Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
  (↑(Finset.range n) : Set ℕ)
Tactic: rw [Finset.card_image_of_injOn, Finset.card_range, degree_U_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n k : ℕ
hk : k < n
⊢ rootMultiplicity (cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) (U ℝ (↑n : ℤ)) = 1
have rw : Membership.mem (γ := Multiset ℝ)
  (Finset.val
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
      (Finset.range n)))
  (cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
Tactic: rw [← count_roots, roots_U_real, Multiset.count_eq_one_of_mem (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
⊢ IsLocalMax (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
have zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
Tactic: have zero_lt : 0 < k * π / n := by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
⊢ (↑k : ℝ) * π / (↑n : ℝ) < (↑n : ℝ) * π / (↑n : ℝ)
have hc : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
hc : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ (↑k : ℝ) * π / (↑n : ℝ) < (↑n : ℝ) * π / (↑n : ℝ)
have h : 0 < π
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
⊢ IsLocalMax (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
have lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
Tactic: have lt_pi : k * π / n < π := calc
    k * π / n < n * π / n := by gcongr
    _ = π := mul_div_cancel_left₀ _ (Nat.cast_ne_zero.mpr hn)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
⊢ IsLocalMax (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
have refine_1 : ∀ (y : ℝ),
  Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y →
    LE.le (α := ℝ) ((fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) y)
      ((fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ))))
Tactic: refine eventually_nhds_iff.mpr ⟨Set.Ioo (-1) 1, ?_, isOpen_Ioo, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
refine_1 :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y →
      LE.le (α := ℝ) ((fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) y)
        ((fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ))))
⊢ IsLocalMax (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
have refine_2 : -1 < cos ((↑k : ℝ) * π / (↑n : ℝ))
Tactic: refine eventually_nhds_iff.mpr ⟨Set.Ioo (-1) 1, ?_, isOpen_Ioo, ?_, ?_⟩