awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ))))
refine_2 : -1 < cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ IsLocalMax (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
have refine_3 : cos ((↑k : ℝ) * π / (↑n : ℝ)) < 1
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 : ℝ) < π
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) x
⊢ eval x (T ℝ (↑n : ℤ)) ≤ eval (cos ((↑k : ℝ) * π / (↑n : ℝ))) (T ℝ (↑n : ℤ))
have refine_1 : eval x (T ℝ (↑n : ℤ)) ≤ 1
Tactic: rw [(eval_T_real_eq_one_iff hn _).mpr ⟨k, le_of_lt hk₁, hk₂, rfl⟩]
-- 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 : ℝ) < π
⊢ -1 < cos ((↑k : ℝ) * π / (↑n : ℝ))
have refine_2 : cos π < cos ((↑k : ℝ) * π / (↑n : ℝ))
Tactic: rw [← cos_pi]
-- 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 : ℝ) < π
⊢ cos ((↑k : ℝ) * π / (↑n : ℝ)) < 1
have refine_3 : cos ((↑k : ℝ) * π / (↑n : ℝ)) < cos 0
Tactic: rw [← cos_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
⊢ IsLocalMin (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
have k_pos : 0 < k
Tactic: have k_pos : 0 < k := hk₂.pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
⊢ IsLocalMin (β := ℝ) (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₁ : k < n
hk₂ : Odd k
k_pos : 0 < 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₁ : k < n
hk₂ : Odd k
k_pos : 0 < 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₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
⊢ IsLocalMin (β := ℝ) (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₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
⊢ IsLocalMin (β := ℝ) (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 : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ))))
      ((fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) y)
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₁ : k < n
hk₂ : Odd k
k_pos : 0 < 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 : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ))))
        ((fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) y)
⊢ IsLocalMin (β := ℝ) (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, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < 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 : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ))))
        ((fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) y)
refine_2 : -1 < cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ IsLocalMin (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
have refine_3 : cos ((↑k : ℝ) * π / (↑n : ℝ)) < 1
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₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) x
⊢ eval (cos ((↑k : ℝ) * π / (↑n : ℝ))) (T ℝ (↑n : ℤ)) ≤ eval x (T ℝ (↑n : ℤ))
have refine_1 : -1 ≤ eval x (T ℝ (↑n : ℤ))
Tactic: rw [(eval_T_real_eq_neg_one_iff hn _).mpr ⟨k, le_of_lt hk₁, hk₂, rfl⟩]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
⊢ -1 < cos ((↑k : ℝ) * π / (↑n : ℝ))
have refine_2 : cos π < cos ((↑k : ℝ) * π / (↑n : ℝ))
Tactic: rw [← cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
⊢ cos ((↑k : ℝ) * π / (↑n : ℝ)) < 1
have refine_3 : cos ((↑k : ℝ) * π / (↑n : ℝ)) < cos 0
Tactic: rw [← cos_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
⊢ IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
have inl : Even k → IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
Tactic: cases k.even_or_odd
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
inl : Even k → IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
⊢ IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
have inr : Odd k → IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
Tactic: cases k.even_or_odd
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
⊢ IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) x ↔ ∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mp : IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) x → ∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
mp :
  IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) x → ∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) x ↔ ∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mpr : (∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))) → IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) x
⊢ ∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have hx₁ : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) x) 0
Tactic: replace hx := hx.deriv_eq_zero
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) x) 0
⊢ ∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have hx₁ : eval x (U ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) = 0
Tactic: rw [Polynomial.deriv, T_derivative_eq_U, eval_mul, Int.cast_natCast, eval_natCast,
      mul_eq_zero_iff_left (by aesop)] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : eval x (U ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) = 0
⊢ ∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have hx₁ : x ∈ roots (U ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
Tactic: replace hx : x ∈ (U ℝ (n - 1)).roots :=
      (mem_roots (degree_ne_bot.mp (ne_of_eq_of_ne (by grind [degree_U_natCast])
        (WithBot.natCast_ne_bot (n - 1))))).mpr hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : x ∈ roots (U ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
⊢ ∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have hx₁ : Membership.mem (γ := Finset ℝ)
  (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
    (Finset.range (n - 1)))
  x
Tactic: rw [show (n - 1 : ℤ) = (n - 1 : ℕ) by grind, roots_U_real, Finset.mem_val] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x
⊢ ∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mp : ∀ (k : ℕ) (hk₁ : k ∈ Finset.range (n - 1))
  (hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = x),
  ∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
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 : 2 ≤ n
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = x
⊢ ∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mp : x = cos ((↑(k + 1) : ℝ) * π / (↑n : ℝ))
Tactic: refine ⟨k + 1, Finset.mem_Ioo.mpr ⟨k.zero_lt_succ, by grind⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = x
⊢ x = cos ((↑(k + 1) : ℝ) * π / (↑n : ℝ))
have mp : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = cos ((↑(k + 1) : ℝ) * π / (↑n : ℝ))
Tactic: rw [← hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = x
⊢ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = cos ((↑(k + 1) : ℝ) * π / (↑n : ℝ))
have mp : HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 = (↑(k + 1) : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = x
mp : HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 = (↑(k + 1) : ℝ)
⊢ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = cos ((↑(k + 1) : ℝ) * π / (↑n : ℝ))
have mp₁ : HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1 = (↑n : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = x
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 = (↑(k + 1) : ℝ)
have mp : k + 1 = k + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = x
⊢ HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1 = (↑n : ℝ)
have mp : n - 1 + 1 = n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
k : ℕ
hk : k ∈ Finset.Ioo 0 n
hx : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) x
have mpr : IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n k : ℕ
hn : n ≠ 0
hk : k ≤ n
⊢ IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
have inl : Even k → IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
Tactic: cases k.even_or_odd
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n k : ℕ
hn : n ≠ 0
hk : k ≤ n
inl : Even k → IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
⊢ IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
have inr : Odd k → IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
Tactic: cases k.even_or_odd
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
⊢ IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x ↔
    ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mp : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x → ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
mp :
  IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x →
    ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x ↔
    ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mpr : (∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))) →
  IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
⊢ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mp : |eval x (T ℝ (↑n : ℤ))| = 1
Tactic: apply (abs_eval_T_real_eq_one_iff hn x).mp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
⊢ |eval x (T ℝ (↑n : ℤ))| = 1
have mp : 1 ≤ |eval x (T ℝ (↑n : ℤ))|
Tactic: apply eq_of_le_of_ge (abs_eval_T_real_le_one n (by grind))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ (↑n : ℤ))|
have mp : ∀ (h : IsMinOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x), 1 ≤ |eval x (T ℝ (↑n : ℤ))|
Tactic: refine h.elim (fun h => ?_) (fun h => ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
mp : ∀ (h : IsMinOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x), 1 ≤ |eval x (T ℝ (↑n : ℤ))|
⊢ 1 ≤ |eval x (T ℝ (↑n : ℤ))|
have mp₁ : ∀ (h : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x), 1 ≤ |eval x (T ℝ (↑n : ℤ))|
Tactic: refine h.elim (fun h => ?_) (fun h => ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMinOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ (↑n : ℤ))|
have mp : eval x (T ℝ (↑n : ℤ)) ≤ -1
Tactic: refine le_abs.mpr (.inr (le_neg_of_le_neg ?_))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMinOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
⊢ eval x (T ℝ (↑n : ℤ)) ≤ -1
have this : eval x (T ℝ (↑n : ℤ)) ≤ eval (cos (1 * π / (↑n : ℝ))) (T ℝ (↑n : ℤ))
Tactic: have := isMinOn_iff.mp h (cos (1 * π / n)) (by grind [abs_cos_le_one])
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ (↑n : ℤ))|
have mp : 1 ≤ eval x (T ℝ (↑n : ℤ))
Tactic: refine le_abs.mpr (.inl ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
⊢ 1 ≤ eval x (T ℝ (↑n : ℤ))
have this : eval (cos (0 * π / (↑n : ℝ))) (T ℝ (↑n : ℤ)) ≤ eval x (T ℝ (↑n : ℤ))
Tactic: have := isMaxOn_iff.mp h (cos (0 * π / n)) (by simp)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
k : ℕ
hk : k ≤ n
hx : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
have mpr : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
x : ℝ
hroot : IsRoot (T ℝ (↑n : ℤ)) x
hnz : x ≠ 0
⊢ Irrational x
have hroot₁ : Membership.mem (γ := Finset ℝ)
  (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
    (Finset.range n))
  x
Tactic: rw [← mem_roots (T_ne_zero ℝ n), roots_T_real, Finset.mem_val] at hroot
Cleared hypotheses: hroot, 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
hnz : x ≠ 0
⊢ Irrational x
have obtain : ∀ (k : ℕ) (hk₁ : k ∈ Finset.range n)
  (hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x), Irrational x
Tactic: obtain ⟨k, hk₁, hk₂⟩ := Finset.mem_image.mp hroot
-- 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
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
⊢ Irrational x
have hn : n ≠ 0
Tactic: have hn : n ≠ 0 := 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
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 x
have rw : Irrational (cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
Tactic: rw [← hk₂]