awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n : ℕ
hn : n ≠ 0
rw :
  HAdd.hAdd (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑n : ℤ))) ∂measureT)
        (∫ (x : ℝ), eval x (T ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) (↑n : ℤ))) ∂measureT) /
      2 =
    π / 2
rw₁ : HAdd.hAdd (α := ℝ) 0 (∫ (x : ℝ), eval x (T ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) (↑n : ℤ))) ∂measureT) / 2 = π / 2
rw₂ : HAdd.hAdd (α := ℝ) 0 (∫ (x : ℝ), eval x (T ℝ 0) ∂measureT) / 2 = π / 2
⊢ ∫ (x : ℝ), eval x (T ℝ (↑n : ℤ)) * eval x (T ℝ (↑n : ℤ)) ∂measureT = π / 2
have rw₃ : (0 + π) / 2 = π / 2
Tactic: rw [integral_eval_T_real_mul_eval_T_real_measureT,
    integral_eval_T_real_measureT_of_ne_zero (by grind), sub_self,
    integral_eval_T_real_measureT_zero, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n : ℕ
hn : n ≠ 0
rw :
  HAdd.hAdd (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑n : ℤ))) ∂measureT)
        (∫ (x : ℝ), eval x (T ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) (↑n : ℤ))) ∂measureT) /
      2 =
    π / 2
rw₁ : HAdd.hAdd (α := ℝ) 0 (∫ (x : ℝ), eval x (T ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) (↑n : ℤ))) ∂measureT) / 2 = π / 2
rw₂ : HAdd.hAdd (α := ℝ) 0 (∫ (x : ℝ), eval x (T ℝ 0) ∂measureT) / 2 = π / 2
rw₃ : (0 + π) / 2 = π / 2
⊢ ∫ (x : ℝ), eval x (T ℝ (↑n : ℤ)) * eval x (T ℝ (↑n : ℤ)) ∂measureT = π / 2
have rw₄ : π / 2 = π / 2
Tactic: rw [integral_eval_T_real_mul_eval_T_real_measureT,
    integral_eval_T_real_measureT_of_ne_zero (by grind), sub_self,
    integral_eval_T_real_measureT_zero, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
⊢ Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) (eval x (T ℝ n))
have rw : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) (eval (cos (arccos x)) (T ℝ n))
Tactic: rw [← cos_arccos (x := x) (by grind) (by grind)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
x : ℝ
hx : 1 ≤ x
⊢ 1 ≤ eval x (T ℝ n)
have rw : 1 ≤ eval (cosh (arcosh x)) (T ℝ n)
Tactic: rw [← cosh_arcosh hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
⊢ 1 < eval x (T ℝ n)
have this : arcosh x ≠ 0
Tactic: have : arcosh x ≠ 0 := by grind [cosh_arcosh, cosh_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
⊢ 1 < eval x (T ℝ n)
have rw : Ne (α := ℝ) (↑n : ℝ) 0 ∧ arcosh x ≠ 0
Tactic: rw [← cosh_arcosh (le_of_lt hx), T_real_cosh, one_lt_cosh, mul_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
⊢ Ne (α := ℝ) (↑n : ℝ) 0
have norm_cast : ¬n = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
x : ℝ
hx : x ≤ -1
⊢ 1 ≤ (↑(↑n.negOnePow : ℤ) : ℝ) * eval x (T ℝ n)
have rw : 1 ≤ (↑(↑n.negOnePow : ℤ) : ℝ) * ((↑(↑n.negOnePow : ℤ) : ℝ) * eval (-x) (T ℝ n))
Tactic: rw [← neg_neg x, T_eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
x : ℝ
hx : x ≤ -1
⊢ 1 ≤ (↑(↑n.negOnePow : ℤ) : ℝ) * ((↑(↑n.negOnePow : ℤ) : ℝ) * eval (-x) (T ℝ n))
have h : (↑(↑n.negOnePow : ℤ) : ℝ) * ((↑(↑n.negOnePow : ℤ) : ℝ) * eval (-x) (T ℝ n)) = eval (-x) (T ℝ n)
Tactic: convert! one_le_eval_T_real n (le_neg_of_le_neg hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
x : ℝ
hx : x ≤ -1
⊢ (↑(↑n.negOnePow : ℤ) : ℝ) * ((↑(↑n.negOnePow : ℤ) : ℝ) * eval (-x) (T ℝ n)) = eval (-x) (T ℝ n)
have h : HMul.hMul (α := ℝ) (-1) (-1) ^ n * eval (-x) (T ℝ n) = eval (-x) (T ℝ n)
Tactic: rw [Int.cast_negOnePow, ← mul_assoc, ← mul_zpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
⊢ 1 < (↑(↑n.negOnePow : ℤ) : ℝ) * eval x (T ℝ n)
have rw : 1 < (↑(↑n.negOnePow : ℤ) : ℝ) * ((↑(↑n.negOnePow : ℤ) : ℝ) * eval (-x) (T ℝ n))
Tactic: rw [← neg_neg x, T_eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
⊢ 1 < (↑(↑n.negOnePow : ℤ) : ℝ) * ((↑(↑n.negOnePow : ℤ) : ℝ) * eval (-x) (T ℝ n))
have h : (↑(↑n.negOnePow : ℤ) : ℝ) * ((↑(↑n.negOnePow : ℤ) : ℝ) * eval (-x) (T ℝ n)) = eval (-x) (T ℝ n)
Tactic: convert! one_lt_eval_T_real hn (lt_neg_of_lt_neg hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
⊢ (↑(↑n.negOnePow : ℤ) : ℝ) * ((↑(↑n.negOnePow : ℤ) : ℝ) * eval (-x) (T ℝ n)) = eval (-x) (T ℝ n)
have h : HMul.hMul (α := ℝ) (-1) (-1) ^ n * eval (-x) (T ℝ n) = eval (-x) (T ℝ n)
Tactic: rw [Int.cast_negOnePow, ← mul_assoc, ← mul_zpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
x : ℝ
hx : 1 ≤ |x|
⊢ 1 ≤ |eval x (T ℝ n)|
have inr : ∀ (this : ∀ (n : ℤ) {x : ℝ} (hx : 1 ≤ |x|) (h : 0 ≤ x), 1 ≤ |eval x (T ℝ n)|) (h : x < 0), 1 ≤ |eval x (T ℝ n)|
Tactic: wlog! h : 0 ≤ x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
x : ℝ
hx : 1 ≤ |x|
inr : ∀ (this : ∀ (n : ℤ) {x : ℝ} (hx : 1 ≤ |x|) (h : 0 ≤ x), 1 ≤ |eval x (T ℝ n)|) (h : x < 0), 1 ≤ |eval x (T ℝ n)|
⊢ 1 ≤ |eval x (T ℝ n)|
have wlog! : ∀ (n : ℤ) {x : ℝ} (hx : 1 ≤ |x|) (h : 0 ≤ x), 1 ≤ |eval x (T ℝ n)|
Tactic: wlog! h : 0 ≤ x
Cleared hypotheses: n, x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < |x|
⊢ 1 < |eval x (T ℝ n)|
have inr : ∀ (this : ∀ {n : ℤ} (hn : n ≠ 0) {x : ℝ} (hx : 1 < |x|) (h : 0 ≤ x), 1 < |eval x (T ℝ n)|) (h : x < 0),
  1 < |eval x (T ℝ n)|
Tactic: wlog! h : 0 ≤ x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < |x|
inr :
  ∀ (this : ∀ {n : ℤ} (hn : n ≠ 0) {x : ℝ} (hx : 1 < |x|) (h : 0 ≤ x), 1 < |eval x (T ℝ n)|) (h : x < 0),
    1 < |eval x (T ℝ n)|
⊢ 1 < |eval x (T ℝ n)|
have wlog! : ∀ {n : ℤ} (hn : n ≠ 0) {x : ℝ} (hx : 1 < |x|) (h : 0 ≤ x), 1 < |eval x (T ℝ n)|
Tactic: wlog! h : 0 ≤ x
Cleared hypotheses: n, hn, x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ |eval x (T ℝ (↑n : ℤ))| = 1 ↔ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mp : |eval x (T ℝ (↑n : ℤ))| = 1 → ∃ 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 : ℝ
mp : |eval x (T ℝ (↑n : ℤ))| = 1 → ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ |eval x (T ℝ (↑n : ℤ))| = 1 ↔ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mpr : (∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))) → |eval x (T ℝ (↑n : ℤ))| = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : |eval x (T ℝ (↑n : ℤ))| = 1
⊢ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have hx : |x| ≤ 1
Tactic: have hx := (abs_eval_T_real_le_one_iff (Nat.cast_ne_zero.mpr hn) x).mpr (le_of_eq hTx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : |eval x (T ℝ (↑n : ℤ))| = 1
hx : |x| ≤ 1
⊢ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have hTx₁ : ∃ (k : ℤ), (↑k : ℝ) * π = (↑n : ℝ) * arccos x
Tactic: rw [← cos_arccos (neg_le_of_abs_le hx) (le_of_max_le_left hx), T_real_cos,
      Int.cast_natCast, abs_cos_eq_one_iff] at hTx
Cleared hypotheses: hTx, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : ∃ (k : ℤ), (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hx : |x| ≤ 1
⊢ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mp : ∀ (k : ℤ) (hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x), ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
Tactic: obtain ⟨k, hk⟩ := hTx
Cleared hypotheses: hTx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℤ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
⊢ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
Tactic: have hk' : k = n * (arccos x / π) := by simpa [field]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℤ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
⊢ 0 ≤ k
have rw : 0 ≤ (↑n : ℝ) * (arccos x / π)
Tactic: rw [← Int.cast_nonneg_iff (R := ℝ), hk']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℤ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
⊢ 0 ≤ (↑n : ℝ) * (arccos x / π)
have positivity : 0 ≤ arccos x → 0 ≤ (↑n : ℝ) * (arccos x / π)
Tactic: positivity [arccos_nonneg x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℤ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
⊢ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mp : ∀ (k : ℕ) (hk : (↑(↑k : ℤ) : ℝ) * π = (↑n : ℝ) * arccos x) (hk' : (↑(↑k : ℤ) : ℝ) = (↑n : ℝ) * (arccos x / π)),
  ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
Tactic: lift k to ℕ using (by rw [← Int.cast_nonneg_iff (R := ℝ), hk']; positivity [arccos_nonneg x])
Cleared hypotheses: k, hk, hk'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑(↑k : ℤ) : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑(↑k : ℤ) : ℝ) = (↑n : ℝ) * (arccos x / π)
⊢ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have hk₁ : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
Tactic: simp only [Int.cast_natCast] at hk hk'
Cleared hypotheses: hk, hk'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑(↑k : ℤ) : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑(↑k : ℤ) : ℝ) = (↑n : ℝ) * (arccos x / π)
hk₁ : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
⊢ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have hk'₁ : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
Tactic: simp only [Int.cast_natCast] at hk hk'
Cleared hypotheses: hk, hk'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
⊢ LE.le (α := ℝ) (↑k : ℝ) (↑n : ℝ)
have rw : (↑n : ℝ) * (arccos x / π) ≤ HMul.hMul (α := ℝ) (↑n : ℝ) 1
Tactic: rw [← mul_one (n : ℝ), hk']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
⊢ (↑n : ℝ) * (arccos x / π) ≤ HMul.hMul (α := ℝ) (↑n : ℝ) 1
have hbc : arccos x / π ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
⊢ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have hkn : LE.le (α := ℝ) (↑k : ℝ) (↑n : ℝ)
Tactic: have hkn : (k : ℝ) ≤ n := by
      rw [← mul_one (n : ℝ), hk']
      gcongr
      exact div_le_one_of_le₀ (arccos_le_pi x) (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
hkn : LE.le (α := ℝ) (↑k : ℝ) (↑n : ℝ)
⊢ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mp : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
Tactic: refine ⟨k, by simpa using hkn, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
hkn : LE.le (α := ℝ) (↑k : ℝ) (↑n : ℝ)
⊢ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have h : x = cos ((↑n : ℝ) * arccos x / (↑n : ℝ))
Tactic: convert! congr(cos ($hk.symm / n))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
hkn : LE.le (α := ℝ) (↑k : ℝ) (↑n : ℝ)
⊢ x = cos ((↑n : ℝ) * arccos x / (↑n : ℝ))
have h : x = cos (arccos x)
Tactic: rw [mul_div_cancel_left₀ _ (by simpa), cos_arccos (by grind) (by grind)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
hkn : LE.le (α := ℝ) (↑k : ℝ) (↑n : ℝ)
h : x = cos (arccos x)
⊢ x = cos ((↑n : ℝ) * arccos x / (↑n : ℝ))
have h₁ : x = x
Tactic: rw [mul_div_cancel_left₀ _ (by simpa), cos_arccos (by grind) (by grind)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ≤ n
⊢ |eval (cos ((↑k : ℝ) * π / (↑n : ℝ))) (T ℝ (↑n : ℤ))| = 1
have mpr : ∃ (k_1 : ℤ), (↑k_1 : ℝ) * π = (↑(↑n : ℤ) : ℝ) * ((↑k : ℝ) * π / (↑n : ℝ))
Tactic: rw [T_real_cos, abs_cos_eq_one_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
k n : ℕ
hn : n ≠ 0
⊢ eval (cos ((↑k : ℝ) * π / (↑n : ℝ))) (T ℝ (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑k : ℤ)) : ℤ) : ℝ)
have rw : cos ((↑(↑n : ℤ) : ℝ) * ((↑k : ℝ) * π / (↑n : ℝ))) = HPow.hPow (α := ℝ) (β := ℤ) (-1) (↑k : ℤ)
Tactic: rw [T_real_cos, Int.cast_negOnePow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
k n : ℕ
hn : n ≠ 0
⊢ cos ((↑(↑n : ℤ) : ℝ) * ((↑k : ℝ) * π / (↑n : ℝ))) = HPow.hPow (α := ℝ) (β := ℤ) (-1) (↑k : ℤ)
have h : (↑(↑n : ℤ) : ℝ) * ((↑k : ℝ) * π / (↑n : ℝ)) = (↑(↑k : ℤ) : ℝ) * π
Tactic: convert! Real.cos_int_mul_pi k using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ eval x (T ℝ (↑n : ℤ)) = 1 ↔ ∃ k ≤ n, Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mp : eval x (T ℝ (↑n : ℤ)) = 1 → ∃ k ≤ n, Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
mp : eval x (T ℝ (↑n : ℤ)) = 1 → ∃ k ≤ n, Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ eval x (T ℝ (↑n : ℤ)) = 1 ↔ ∃ k ≤ n, Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mpr : (∃ k ≤ n, Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))) → eval x (T ℝ (↑n : ℤ)) = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = 1
⊢ ∃ k ≤ n, Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mp : ∀ (k : ℕ) (hk₁ : k ≤ n) (hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))), ∃ k ≤ n, Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
Tactic: obtain ⟨k, hk₁, hk₂⟩ := (abs_eval_T_real_eq_one_iff hn x).mp
      ((abs_eq_abs.mpr (.inl hx)).trans abs_one)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = 1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ ∃ k ≤ n, Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have h : k ≤ n ∧ Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
Tactic: use k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = 1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ k ≤ n ∧ Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have h : Even k
Tactic: refine ⟨hk₁, ?_, hk₂⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = 1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ Even k
have hx₁ : HPow.hPow (α := ℝ) (-1) k = 1
Tactic: rw [hk₂, eval_T_real_cos_int_mul_pi_div hn, Int.cast_negOnePow_natCast] at hx
Cleared hypotheses: hx, hk₁, hk₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Even k
hx : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ eval x (T ℝ (↑n : ℤ)) = 1
have mpr : Eq (α := ℝ) (↑(↑1 : ℤ) : ℝ) 1
Tactic: rw [hx, eval_T_real_cos_int_mul_pi_div hn, Int.negOnePow_even k ((Int.even_coe_nat k).mpr hk₂)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Even k
hx : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ Eq (α := ℝ) (↑(↑1 : ℤ) : ℝ) 1
have mpr : Eq (α := ℤ) 1 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ eval x (T ℝ (↑n : ℤ)) = -1 ↔ ∃ k ≤ n, Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mp : eval x (T ℝ (↑n : ℤ)) = -1 → ∃ k ≤ n, Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
mp : eval x (T ℝ (↑n : ℤ)) = -1 → ∃ k ≤ n, Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ eval x (T ℝ (↑n : ℤ)) = -1 ↔ ∃ k ≤ n, Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mpr : (∃ k ≤ n, Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))) → eval x (T ℝ (↑n : ℤ)) = -1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = -1
⊢ ∃ k ≤ n, Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have mp : ∀ (k : ℕ) (hk₁ : k ≤ n) (hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))), ∃ k ≤ n, Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
Tactic: obtain ⟨k, hk₁, hk₂⟩ := (abs_eval_T_real_eq_one_iff hn x).mp
      ((abs_eq_abs.mpr (.inl hx)).trans ((abs_neg 1).trans abs_one))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = -1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ ∃ k ≤ n, Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have h : k ≤ n ∧ Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
Tactic: use k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = -1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ k ≤ n ∧ Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
have h : Odd k
Tactic: refine ⟨hk₁, ?_, hk₂⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = -1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ Odd k
have hx₁ : HPow.hPow (α := ℝ) (-1) k = -1
Tactic: rw [hk₂, eval_T_real_cos_int_mul_pi_div hn, Int.cast_negOnePow_natCast] at hx
Cleared hypotheses: hx, hk₁, hk₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Odd k
hx : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ eval x (T ℝ (↑n : ℤ)) = -1
have mpr : Eq (α := ℝ) (↑(↑(-1) : ℤ) : ℝ) (-1)
Tactic: rw [hx, eval_T_real_cos_int_mul_pi_div hn, Int.negOnePow_odd k ((Int.odd_coe_nat k).mpr hk₂)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Odd k
hx : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ Eq (α := ℝ) (↑(↑(-1) : ℤ) : ℝ) (-1)
have mpr : -1 = Int.negSucc 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
⊢ Multiset.Nodup (α := ℝ)
    (Multiset.map (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Multiset.range n))
have inr : ∀
  (this :
    ∀ (n : ℕ) (hn : n ≠ 0),
      Multiset.Nodup (α := ℝ)
        (Multiset.map (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
          (Multiset.range n)))
  (hn : n = 0),
  Multiset.Nodup (α := ℝ)
    (Multiset.map (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Multiset.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),
        Multiset.Nodup (α := ℝ)
          (Multiset.map (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
            (Multiset.range n)))
    (hn : n = 0),
    Multiset.Nodup (α := ℝ)
      (Multiset.map (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
        (Multiset.range n))
⊢ Multiset.Nodup (α := ℝ)
    (Multiset.map (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Multiset.range n))
have wlog! : ∀ (n : ℕ) (hn : n ≠ 0),
  Multiset.Nodup (α := ℝ)
    (Multiset.map (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Multiset.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
⊢ Multiset.Nodup (α := ℝ)
    (Multiset.map (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Multiset.range n))
have refine : Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
  (↑(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 : ℕ
hn : n ≠ 0
⊢ Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
    (↑(Finset.range n) : Set ℕ)
have refine : ∀ (k : ℕ) (hk : k ∈ (↑(Finset.range n) : Set ℕ)),
  (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ) ≤ π
Tactic: refine injOn_cos.comp (by aesop) fun k hk => Set.mem_Icc.mpr ⟨by positivity, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ∈ (↑(Finset.range n) : Set ℕ)
⊢ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ) ≤ π
have field_simp : HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ∈ (↑(Finset.range n) : Set ℕ)
⊢ HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ)
have norm_cast : 2 * k + 1 ≤ 2 * n
Tactic: norm_cast