Forward Direction: Roots of T_N Are Chebyshev Roots

  -- Strategy: T_N has degree N and has exactly N distinct roots (the Chebyshev roots)
  -- So x must be one of them

  -- Create finset of Chebyshev roots
  let roots := Finset.image (chebyshevRoot N) (Finset.range N)

  have h_card : roots.card = N := by
    rw [Finset.card_image_of_injOn]
    · simp
    · intros k₁ hk₁ k₂ hk₂ h_eq
      simp at hk₁ hk₂
      exact chebyshevRoots_distinct N hN k₁ k₂ hk₁ hk₂ h_eq

  -- All Chebyshev roots are roots of T_N
  have h_roots : ∀ y ∈ roots, (Polynomial.Chebyshev.T ℝ N).eval y = 0 := by
    intro y hy
    simp [roots] at hy
    obtain ⟨k, hk, rfl⟩ := hy
    exact chebyshev_T_eval_chebyshevRoot N k hN hk

  -- T_N has degree N (from PolynomialProperties)
  have h_deg : (Polynomial.Chebyshev.T ℝ N).natDegree = N := by
    have deg : (Polynomial.Chebyshev.T ℝ N).degree = N := chebyshev_T_degree N hN
    rw [← Polynomial.degree_eq_iff_natDegree_eq_of_pos (by omega : 0 < N)]
    exact deg

  -- If x is not in roots, we'd have N+1 distinct roots, contradicting degree = N
  by_contra h_not_exists
  push_neg at h_not_exists

  have h_x_not_in : x ∉ roots := by
    intro h_in
    simp [roots] at h_in
    obtain ⟨k, hk, h_eq⟩ := h_in
    exact h_not_exists k hk h_eq.symm

  -- Insert x into roots to get N+1 distinct roots
  have h_insert_card : (insert x roots).card = N + 1 := by
    rw [Finset.card_insert_of_notMem h_x_not_in, h_card]

  -- But all of them are roots of T_N
  have h_all_roots : ∀ y ∈ insert x roots, (Polynomial.Chebyshev.T ℝ N).eval y = 0 := by
    intro y hy
    cases Finset.mem_insert.mp hy with
    | inl h_eq => rw [h_eq]; exact h
    | inr h_in => exact h_roots y h_in

  -- This contradicts that T_N has degree N
  have h_contradiction : N < (insert x roots).card := by
    rw [h_insert_card]
    omega

  -- T_N can't have more roots than its degree
  have h_bound : (insert x roots).card ≤ (Polynomial.Chebyshev.T ℝ N).natDegree := by
    apply Polynomial.card_le_degree_of_subset_roots
    intro y
    intro hy
    -- y ∈ (insert x roots).val, need to show y ∈ (T_N).roots
    have h_eval := h_all_roots y (Finset.mem_insert.mpr (Finset.mem_insert.mp hy))
    apply Polynomial.mem_roots'.mpr
    constructor
    · -- T_N ≠ 0 for N > 0
      intro h_zero
      have : (Polynomial.Chebyshev.T ℝ N).degree = N := chebyshev_T_degree N hN
      rw [h_zero] at this
      simp at this
    · -- T_N.IsRoot y
      rw [Polynomial.IsRoot]
      exact h_eval

  rw [h_deg] at h_bound
  omega