Leading Coefficient of Chebyshev T_N

  induction N using Nat.strong_induction_on with
  | h n IH =>
    cases n with
    | zero => omega
    | succ n' =>
      cases n' with
      | zero =>
        -- Base case: N = 1, T_1 = X has leading coeff 1 = 2^0
        norm_num [Polynomial.Chebyshev.T_one, Polynomial.leadingCoeff_X]
      | succ m =>
        -- N = m + 2 ≥ 2, use recurrence T_{n+2} = 2X·T_{n+1} - T_n
        have h_rec : Chebyshev.T ℝ (↑(m + 2) : ℤ) =
            2 * X * Chebyshev.T ℝ (↑(m + 1) : ℤ) - Chebyshev.T ℝ (↑m : ℤ) := by
          have := Polynomial.Chebyshev.T_add_two ℝ (↑m : ℤ)
          convert this using 2

        -- Apply IH to get leadingCoeff of T_{m+1}
        have IH_m1 : (Chebyshev.T ℝ ↑(m + 1)).leadingCoeff = 2 ^ m := by
          have h := IH (m + 1) (by omega : m + 1 < m + 2) (by omega : 0 < m + 1)
          simp only [Nat.add_sub_cancel] at h
          exact h

        -- Show degree(T_m) < degree(2*X*T_{m+1})
        have deg_T_m1 : (Chebyshev.T ℝ ↑(m + 1)).degree = ↑(m + 1) := by
          apply chebyshev_T_degree (m + 1)
          omega

        have deg_prod : (2 * X * Chebyshev.T ℝ ↑(m + 1)).degree = ↑(m + 2) := by
          have h_rearrange : (2 : ℝ[X]) * X * Chebyshev.T ℝ ↑(m + 1) =
              2 * (X * Chebyshev.T ℝ ↑(m + 1)) := by ring
          simp only [Polynomial.degree_mul, deg_T_m1, Polynomial.degree_X]
          have : (2 : ℝ[X]).degree = 0 := Polynomial.degree_C (show (2 : ℝ) ≠ 0 by norm_num)
          simp [this]; ring

        have deg_T_m :
            (Chebyshev.T ℝ ↑m).degree < (2 * X * Chebyshev.T ℝ ↑(m + 1)).degree := by
          rw [deg_prod]
          by_cases hm : m = 0
          · simp [hm]
          · have deg_m : (Chebyshev.T ℝ ↑m).degree = ↑m := by
              apply chebyshev_T_degree m
              omega
            rw [deg_m]
            norm_cast
            omega

        -- Apply leadingCoeff_sub_of_degree_lt
        have lc_rec : (2 * X * Chebyshev.T ℝ ↑(m + 1) - Chebyshev.T ℝ ↑m).leadingCoeff =
            (2 * X * Chebyshev.T ℝ ↑(m + 1)).leadingCoeff := by
          apply Polynomial.leadingCoeff_sub_of_degree_lt deg_T_m

        -- Calculate leadingCoeff(2*X*T_{m+1})
        have lc_prod : (2 * X * Chebyshev.T ℝ ↑(m + 1)).leadingCoeff = 2 * 2 ^ m := by
          have h_two : (2 : ℝ[X]) = C (2 : ℝ) := by rfl
          conv_lhs => rw [h_two]
          rw [Polynomial.leadingCoeff_mul, Polynomial.leadingCoeff_mul,
              Polynomial.leadingCoeff_C, Polynomial.leadingCoeff_X, IH_m1]
          ring

        -- Finish the proof
        simp only [Nat.add_sub_cancel]
        calc (Chebyshev.T ℝ ↑(m + 2)).leadingCoeff
            = (2 * X * Chebyshev.T ℝ ↑(m + 1) -
                Chebyshev.T ℝ ↑m).leadingCoeff := by rw [← h_rec]
          _ = (2 * X * Chebyshev.T ℝ ↑(m + 1)).leadingCoeff := lc_rec
          _ = 2 * 2 ^ m := lc_prod
          _ = 2 ^ (m + 1) := by ring