no goals
R : Type u_1
S : Type ?u.12813
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ U R (0 + 1) = X * U R 0 + T R (0 + 1)
simp only [T, U, two_mul, mul_one]
R : Type u_1
S : Type ?u.12813
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 2 * X * (2 * X) - 1 = X * (2 * X) + (2 * X * X - 1)
R : Type u_1
S : Type ?u.12813
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ U R (1 + 1) = X * U R 1 + T R (1 + 1)
simp only [T, U]
no goals
R : Type u_1
S : Type ?u.12813
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 2 * X * (2 * X) - 1 = X * (2 * X) + (2 * X * X - 1)
ring
no goals
R : Type u_1
S : Type ?u.12813
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))
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]
no goals
R : Type u_1
S : Type ?u.12813
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))
ring
no goals
R : Type u_1
S : Type ?u.12813
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)
simp only [U_add_two, T_add_two]