no goals
R : Type u_1
S : Type ?u.44951
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ↑derivative (T R (0 + 1)) = (↑0 + 1) * U R 0
simp only [T_one, U_zero, derivative_X, Nat.cast_zero, zero_add, mul_one]
no goals
R : Type u_1
S : Type ?u.44951
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ↑derivative (T R (1 + 1)) = (↑1 + 1) * U R 1
simp [T_two, U_one, derivative_sub, derivative_one, derivative_mul, derivative_X_pow, add_mul]
R : Type u_1
S : Type ?u.44951
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))
R : Type u_1
S : Type ?u.44951
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))
rw [T_add_two _ (n + 1), derivative_sub, derivative_mul, derivative_mul, derivative_X,
  derivative_ofNat]
no goals
R : Type u_1
S : Type ?u.44951
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))
ring_nf
no goals
R : Type u_1
S : Type ?u.44951
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
rw_mod_cast [T_derivative_eq_U (n + 1), T_derivative_eq_U n, T_eq_U_sub_X_mul_U _ (n + 1)]
no goals
R : Type u_1
S : Type ?u.44951
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)
ring
no goals
R : Type u_1
S : Type ?u.44951
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)
rw [U_add_two]
no goals
R : Type u_1
S : Type ?u.44951
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)
ring
no goals
R : Type u_1
S : Type ?u.44951
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (↑n + 2 + 1) * U R (n + 2) = (↑(n + 2) + 1) * U R (n + 2)
norm_cast