[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ T R (n + 2) = 2 * X * T R (n + 1) - T R n
[PROOFSTEP]
rw [T]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ T R 2 = 2 * X ^ 2 - 1
[PROOFSTEP]
simp only [T, sub_left_inj, sq, mul_assoc]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h : 2 ≤ n
⊢ T R n = 2 * X * T R (n - 1) - T R (n - 2)
[PROOFSTEP]
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h : 2 ≤ 2 + n
⊢ T R (2 + n) = 2 * X * T R (2 + n - 1) - T R (2 + n - 2)
[PROOFSTEP]
rw [add_comm]
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h : 2 ≤ 2 + n
⊢ T R (n + 2) = 2 * X * T R (n + 2 - 1) - T R (n + 2 - 2)
[PROOFSTEP]
exact T_add_two R n
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ U R (n + 2) = 2 * X * U R (n + 1) - U R n
[PROOFSTEP]
rw [U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ U R 2 = 4 * X ^ 2 - 1
[PROOFSTEP]
simp only [U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 2 * X * (2 * X) - 1 = 4 * X ^ 2 - 1
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h : 2 ≤ n
⊢ U R n = 2 * X * U R (n - 1) - U R (n - 2)
[PROOFSTEP]
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h : 2 ≤ 2 + n
⊢ U R (2 + n) = 2 * X * U R (2 + n - 1) - U R (2 + n - 2)
[PROOFSTEP]
rw [add_comm]
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h : 2 ≤ 2 + n
⊢ U R (n + 2) = 2 * X * U R (n + 2 - 1) - U R (n + 2 - 2)
[PROOFSTEP]
exact U_add_two R n
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ U R (0 + 1) = X * U R 0 + T R (0 + 1)
[PROOFSTEP]
simp only [T, U, two_mul, mul_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ U R (1 + 1) = X * U R 1 + T R (1 + 1)
[PROOFSTEP]
simp only [T, U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 2 * X * (2 * X) - 1 = X * (2 * X) + (2 * X * X - 1)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ U R (n + 2 + 1) = 2 * X * (X * U R (n + 1) + T R (n + 2)) - (X * U R n + T R (n + 1))
[PROOFSTEP]
rw [U_add_two, U_eq_X_mul_U_add_T n, U_eq_X_mul_U_add_T (n + 1), U_eq_X_mul_U_add_T n]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ 2 * X * (X * U R (n + 1) + T R (n + 2)) - (X * U R n + T R (n + 1)) =
    X * (2 * X * U R (n + 1) - U R n) + (2 * X * T R (n + 2) - T R (n + 1))
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ X * (2 * X * U R (n + 1) - U R n) + (2 * X * T R (n + 2) - T R (n + 1)) = X * U R (n + 2) + T R (n + 2 + 1)
[PROOFSTEP]
simp only [U_add_two, T_add_two]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ T R (n + 1) = U R (n + 1) - X * U R n
[PROOFSTEP]
rw [U_eq_X_mul_U_add_T, add_comm (X * U R n), add_sub_cancel]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ T R (0 + 2) = X * T R (0 + 1) - (1 - X ^ 2) * U R 0
[PROOFSTEP]
simp only [T, U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 2 * X * X - 1 = X * X - (1 - X ^ 2) * 1
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ T R (1 + 2) = X * T R (1 + 1) - (1 - X ^ 2) * U R 1
[PROOFSTEP]
simp only [T, U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 2 * X * (2 * X * X - 1) - X = X * (2 * X * X - 1) - (1 - X ^ 2) * (2 * X)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ 2 * X * T R (n + 2 + 1) - T R (n + 2) =
    2 * X * (X * T R (n + 2) - (1 - X ^ 2) * U R (n + 1)) - (X * T R (n + 1) - (1 - X ^ 2) * U R n)
[PROOFSTEP]
simp only [T_eq_X_mul_T_sub_pol_U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ 2 * X * (X * T R (n + 2) - (1 - X ^ 2) * U R (n + 1)) - (X * T R (n + 1) - (1 - X ^ 2) * U R n) =
    X * (2 * X * T R (n + 2) - T R (n + 1)) - (1 - X ^ 2) * (2 * X * U R (n + 1) - U R n)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ X * (2 * X * T R (n + 2) - T R (n + 1)) - (1 - X ^ 2) * (2 * X * U R (n + 1) - U R n) =
    X * T R (n + 2 + 1) - (1 - X ^ 2) * U R (n + 2)
[PROOFSTEP]
rw [T_add_two _ (n + 1), U_add_two]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)
[PROOFSTEP]
rw [T_eq_X_mul_T_sub_pol_U, ← sub_add, sub_self, zero_add]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ map f (T R 0) = T S 0
[PROOFSTEP]
simp only [T_zero, Polynomial.map_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ map f (T R 1) = T S 1
[PROOFSTEP]
simp only [T_one, map_X]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ map f (T R (n + 2)) = T S (n + 2)
[PROOFSTEP]
simp only [T_add_two, Polynomial.map_mul, Polynomial.map_sub, map_X, Polynomial.map_add, Polynomial.map_one,
  Polynomial.map_ofNat, map_T f (n + 1), map_T f n]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ map f (U R 0) = U S 0
[PROOFSTEP]
simp only [U_zero, Polynomial.map_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ map f (U R 1) = U S 1
[PROOFSTEP]
simp [U_one, map_X, Polynomial.map_mul, Polynomial.map_add, Polynomial.map_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ map f (U R (n + 2)) = U S (n + 2)
[PROOFSTEP]
simp only [U_add_two, Polynomial.map_mul, Polynomial.map_sub, map_X, Polynomial.map_add, Polynomial.map_one,
  map_U f (n + 1), map_U f n]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ map f 2 * X * U S (n + 1) - U S n = 2 * X * U S (n + 1) - U S n
[PROOFSTEP]
norm_num
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ↑derivative (T R (0 + 1)) = (↑0 + 1) * U R 0
[PROOFSTEP]
simp only [T_one, U_zero, derivative_X, Nat.cast_zero, zero_add, mul_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ↑derivative (T R (1 + 1)) = (↑1 + 1) * U R 1
[PROOFSTEP]
simp [T_two, U_one, derivative_sub, derivative_one, derivative_mul, derivative_X_pow, add_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑derivative (T R (n + 2 + 1)) = 2 * T R (n + 2) + 2 * X * ↑derivative (T R (n + 1 + 1)) - ↑derivative (T R (n + 1))
[PROOFSTEP]
rw [T_add_two _ (n + 1), derivative_sub, derivative_mul, derivative_mul, derivative_X, derivative_ofNat]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (0 * X + 2 * 1) * T R (n + 1 + 1) + 2 * X * ↑derivative (T R (n + 1 + 1)) - ↑derivative (T R (n + 1)) =
    2 * T R (n + 2) + 2 * X * ↑derivative (T R (n + 1 + 1)) - ↑derivative (T R (n + 1))
[PROOFSTEP]
ring_nf
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ 2 * T R (n + 2) + 2 * X * ↑derivative (T R (n + 1 + 1)) - ↑derivative (T R (n + 1)) =
    2 * (U R (n + 1 + 1) - X * U R (n + 1)) + 2 * X * ((↑n + 1 + 1) * U R (n + 1)) - (↑n + 1) * U R n
[PROOFSTEP]
rw_mod_cast [T_derivative_eq_U (n + 1), T_derivative_eq_U n, T_eq_U_sub_X_mul_U _ (n + 1)]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ 2 * (U R (n + 1 + 1) - X * U R (n + 1)) + 2 * X * ((↑n + 1 + 1) * U R (n + 1)) - (↑n + 1) * U R n =
    (↑n + 1) * (2 * X * U R (n + 1) - U R n) + 2 * U R (n + 2)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (↑n + 1) * (2 * X * U R (n + 1) - U R n) + 2 * U R (n + 2) = (↑n + 1) * U R (n + 2) + 2 * U R (n + 2)
[PROOFSTEP]
rw [U_add_two]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (↑n + 1) * U R (n + 2) + 2 * U R (n + 2) = (↑n + 2 + 1) * U R (n + 2)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (↑n + 2 + 1) * U R (n + 2) = (↑(n + 2) + 1) * U R (n + 2)
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (1 - X ^ 2) * ↑derivative (T R (n + 1)) = (1 - X ^ 2) * ((↑n + 1) * U R n)
[PROOFSTEP]
rw [T_derivative_eq_U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (1 - X ^ 2) * ((↑n + 1) * U R n) = (↑n + 1) * ((1 - X ^ 2) * U R n)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (↑n + 1) * ((1 - X ^ 2) * U R n) = (↑n + 1) * (X * T R (n + 1) - (2 * X * T R (n + 1) - T R n))
[PROOFSTEP]
rw [one_sub_X_sq_mul_U_eq_pol_in_T, T_add_two]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (↑n + 1) * (X * T R (n + 1) - (2 * X * T R (n + 1) - T R n)) = (↑n + 1) * (T R n - X * T R (n + 1))
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (↑n + 1) * T R (n + 1) = X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
[PROOFSTEP]
have h :
  derivative (T R (n + 2)) =
    U R (n + 1) - X * U R n + X * derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * derivative (U R n) :=
  by
  conv_lhs => rw [T_eq_X_mul_T_sub_pol_U]
  simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow, one_mul, T_derivative_eq_U]
  rw [T_eq_U_sub_X_mul_U, C_eq_nat_cast]
  ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑derivative (T R (n + 2)) =
    U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
[PROOFSTEP]
conv_lhs => rw [T_eq_X_mul_T_sub_pol_U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
| ↑derivative (T R (n + 2))
[PROOFSTEP]
rw [T_eq_X_mul_T_sub_pol_U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
| ↑derivative (T R (n + 2))
[PROOFSTEP]
rw [T_eq_X_mul_T_sub_pol_U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
| ↑derivative (T R (n + 2))
[PROOFSTEP]
rw [T_eq_X_mul_T_sub_pol_U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑derivative (X * T R (n + 1) - (1 - X ^ 2) * U R n) =
    U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
[PROOFSTEP]
simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow, one_mul, T_derivative_eq_U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ T R (n + 1) + X * ((↑n + 1) * U R n) - ((0 - ↑C ↑2 * X ^ (2 - 1)) * U R n + (1 - X ^ 2) * ↑derivative (U R n)) =
    U R (n + 1) - X * U R n + X * ((↑n + 1) * U R n) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
[PROOFSTEP]
rw [T_eq_U_sub_X_mul_U, C_eq_nat_cast]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ U R (n + 1) - X * U R n + X * ((↑n + 1) * U R n) -
      ((0 - ↑2 * X ^ (2 - 1)) * U R n + (1 - X ^ 2) * ↑derivative (U R n)) =
    U R (n + 1) - X * U R n + X * ((↑n + 1) * U R n) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h :
  ↑derivative (T R (n + 2)) =
    U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
⊢ (↑n + 1) * T R (n + 1) = X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
[PROOFSTEP]
calc
  ((n : R[X]) + 1) * T R (n + 1) =
      ((n : R[X]) + 1 + 1) * (X * U R n + T R (n + 1)) - X * ((n + 1 : R[X]) * U R n) - (X * U R n + T R (n + 1)) :=
    by ring
  _ = derivative (T R (n + 2)) - X * derivative (T R (n + 1)) - U R (n + 1) := by
    rw [← U_eq_X_mul_U_add_T, ← T_derivative_eq_U, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_one, ←
      T_derivative_eq_U (n + 1)]
  _ =
      U R (n + 1) - X * U R n + X * derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * derivative (U R n) -
          X * derivative (T R (n + 1)) -
        U R (n + 1) :=
    by rw [h]
  _ = X * U R n - (1 - X ^ 2) * derivative (U R n) := by ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h :
  ↑derivative (T R (n + 2)) =
    U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
⊢ (↑n + 1) * T R (n + 1) = (↑n + 1 + 1) * (X * U R n + T R (n + 1)) - X * ((↑n + 1) * U R n) - (X * U R n + T R (n + 1))
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h :
  ↑derivative (T R (n + 2)) =
    U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
⊢ (↑n + 1 + 1) * (X * U R n + T R (n + 1)) - X * ((↑n + 1) * U R n) - (X * U R n + T R (n + 1)) =
    ↑derivative (T R (n + 2)) - X * ↑derivative (T R (n + 1)) - U R (n + 1)
[PROOFSTEP]
rw [← U_eq_X_mul_U_add_T, ← T_derivative_eq_U, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_one, ←
  T_derivative_eq_U (n + 1)]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h :
  ↑derivative (T R (n + 2)) =
    U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
⊢ ↑derivative (T R (n + 2)) - X * ↑derivative (T R (n + 1)) - U R (n + 1) =
    U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n) -
        X * ↑derivative (T R (n + 1)) -
      U R (n + 1)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h :
  ↑derivative (T R (n + 2)) =
    U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
⊢ U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n) -
        X * ↑derivative (T R (n + 1)) -
      U R (n + 1) =
    X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (k : ℕ), 2 * T R 0 * T R (0 + k) = T R (2 * 0 + k) + T R k
[PROOFSTEP]
simp [two_mul, add_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (k : ℕ), 2 * T R 1 * T R (1 + k) = T R (2 * 1 + k) + T R k
[PROOFSTEP]
simp [add_comm]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m : ℕ
⊢ ∀ (k : ℕ), 2 * T R (m + 2) * T R (m + 2 + k) = T R (2 * (m + 2) + k) + T R k
[PROOFSTEP]
intro k
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
⊢ 2 * T R (m + 2) * T R (m + 2 + k) = T R (2 * (m + 2) + k) + T R k
[PROOFSTEP]
suffices 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
  by
  have h_nat₁ : 2 * (m + 2) + k = 2 * m + k + 4 := by ring
  have h_nat₂ : m + 2 + k = m + k + 2 := by ring
  simpa [h_nat₁, h_nat₂] using this
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
this : 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
⊢ 2 * T R (m + 2) * T R (m + 2 + k) = T R (2 * (m + 2) + k) + T R k
[PROOFSTEP]
have h_nat₁ : 2 * (m + 2) + k = 2 * m + k + 4 := by ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
this : 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
⊢ 2 * (m + 2) + k = 2 * m + k + 4
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
this : 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
h_nat₁ : 2 * (m + 2) + k = 2 * m + k + 4
⊢ 2 * T R (m + 2) * T R (m + 2 + k) = T R (2 * (m + 2) + k) + T R k
[PROOFSTEP]
have h_nat₂ : m + 2 + k = m + k + 2 := by ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
this : 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
h_nat₁ : 2 * (m + 2) + k = 2 * m + k + 4
⊢ m + 2 + k = m + k + 2
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
this : 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
h_nat₁ : 2 * (m + 2) + k = 2 * m + k + 4
h_nat₂ : m + 2 + k = m + k + 2
⊢ 2 * T R (m + 2) * T R (m + 2 + k) = T R (2 * (m + 2) + k) + T R k
[PROOFSTEP]
simpa [h_nat₁, h_nat₂] using this
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
⊢ 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
[PROOFSTEP]
have H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1) :=
  by
  have h_nat₁ : m + 1 + (k + 1) = m + k + 2 := by ring
  have h_nat₂ : 2 * (m + 1) + (k + 1) = 2 * m + k + 3 := by ring
  simpa [h_nat₁, h_nat₂] using
    mul_T (m + 1)
      (k + 1)
        -- clean up the `T` nat indices in the inductive hypothesis applied to `m` and `k + 2`
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
⊢ 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
[PROOFSTEP]
have h_nat₁ : m + 1 + (k + 1) = m + k + 2 := by ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
⊢ m + 1 + (k + 1) = m + k + 2
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
h_nat₁ : m + 1 + (k + 1) = m + k + 2
⊢ 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
[PROOFSTEP]
have h_nat₂ : 2 * (m + 1) + (k + 1) = 2 * m + k + 3 := by ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
h_nat₁ : m + 1 + (k + 1) = m + k + 2
⊢ 2 * (m + 1) + (k + 1) = 2 * m + k + 3
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
h_nat₁ : m + 1 + (k + 1) = m + k + 2
h_nat₂ : 2 * (m + 1) + (k + 1) = 2 * m + k + 3
⊢ 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
[PROOFSTEP]
simpa [h_nat₁, h_nat₂] using
  mul_T (m + 1)
    (k + 1)
      -- clean up the `T` nat indices in the inductive hypothesis applied to `m` and `k + 2`
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
⊢ 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
[PROOFSTEP]
have H₂ : 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2) :=
  by
  have h_nat₁ : 2 * m + (k + 2) = 2 * m + k + 2 := by simp [add_assoc]
  have h_nat₂ : m + (k + 2) = m + k + 2 := by simp [add_assoc]
  simpa [h_nat₁, h_nat₂] using
    mul_T m
      (k + 2)
        -- state the `T` recurrence relation for a few useful indices
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
⊢ 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2)
[PROOFSTEP]
have h_nat₁ : 2 * m + (k + 2) = 2 * m + k + 2 := by simp [add_assoc]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
⊢ 2 * m + (k + 2) = 2 * m + k + 2
[PROOFSTEP]
simp [add_assoc]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
h_nat₁ : 2 * m + (k + 2) = 2 * m + k + 2
⊢ 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2)
[PROOFSTEP]
have h_nat₂ : m + (k + 2) = m + k + 2 := by simp [add_assoc]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
h_nat₁ : 2 * m + (k + 2) = 2 * m + k + 2
⊢ m + (k + 2) = m + k + 2
[PROOFSTEP]
simp [add_assoc]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
h_nat₁ : 2 * m + (k + 2) = 2 * m + k + 2
h_nat₂ : m + (k + 2) = m + k + 2
⊢ 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2)
[PROOFSTEP]
simpa [h_nat₁, h_nat₂] using
  mul_T m
    (k + 2)
      -- state the `T` recurrence relation for a few useful indices
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
H₂ : 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2)
⊢ 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
[PROOFSTEP]
have h₁ := T_add_two R m
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
H₂ : 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2)
h₁ : T R (m + 2) = 2 * X * T R (m + 1) - T R m
⊢ 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
[PROOFSTEP]
have h₂ : T R (2 * m + k + 4) = 2 * X * T R (2 * m + k + 3) - T R (2 * m + k + 2) := T_add_two R (2 * m + k + 2)
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
H₂ : 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2)
h₁ : T R (m + 2) = 2 * X * T R (m + 1) - T R m
h₂ : T R (2 * m + k + 4) = 2 * X * T R (2 * m + k + 3) - T R (2 * m + k + 2)
⊢ 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
[PROOFSTEP]
have h₃ := T_add_two R k
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
H₂ : 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2)
h₁ : T R (m + 2) = 2 * X * T R (m + 1) - T R m
h₂ : T R (2 * m + k + 4) = 2 * X * T R (2 * m + k + 3) - T R (2 * m + k + 2)
h₃ : T R (k + 2) = 2 * X * T R (k + 1) - T R k
⊢ 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
[PROOFSTEP]
linear_combination 2 * T R (m + k + 2) * h₁ + 2 * (X : R[X]) * H₁ - H₂ - h₂ - h₃
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (n : ℕ), T R (0 * n) = comp (T R 0) (T R n)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (n : ℕ), T R (1 * n) = comp (T R 1) (T R n)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m : ℕ
⊢ ∀ (n : ℕ), T R ((m + 2) * n) = comp (T R (m + 2)) (T R n)
[PROOFSTEP]
intro n
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m n : ℕ
⊢ T R ((m + 2) * n) = comp (T R (m + 2)) (T R n)
[PROOFSTEP]
have : 2 * T R n * T R ((m + 1) * n) = T R ((m + 2) * n) + T R (m * n) := by
  convert mul_T R n (m * n) using 1 <;> ring_nf
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m n : ℕ
⊢ 2 * T R n * T R ((m + 1) * n) = T R ((m + 2) * n) + T R (m * n)
[PROOFSTEP]
convert mul_T R n (m * n) using 1
[GOAL]
case h.e'_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m n : ℕ
⊢ 2 * T R n * T R ((m + 1) * n) = 2 * T R n * T R (n + m * n)
[PROOFSTEP]
ring_nf
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m n : ℕ
⊢ T R ((m + 2) * n) + T R (m * n) = T R (2 * n + m * n) + T R (m * n)
[PROOFSTEP]
ring_nf
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m n : ℕ
this : 2 * T R n * T R ((m + 1) * n) = T R ((m + 2) * n) + T R (m * n)
⊢ T R ((m + 2) * n) = comp (T R (m + 2)) (T R n)
[PROOFSTEP]
simp [this, T_mul m, ← T_mul (m + 1)]
