no goals
R : Type u_1
S : Type ?u.113283
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (n : ℕ), T R (0 * n) = comp (T R 0) (T R n)
simp
no goals
R : Type u_1
S : Type ?u.113283
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (n : ℕ), T R (1 * n) = comp (T R 1) (T R n)
simp
R : Type u_1
S : Type ?u.113283
inst✝¹ : CommRing R
inst✝ : CommRing S
m n : ℕ
⊢ T R ((m + 2) * n) = comp (T R (m + 2)) (T R n)
R : Type u_1
S : Type ?u.113283
inst✝¹ : CommRing R
inst✝ : CommRing S
m : ℕ
⊢ ∀ (n : ℕ), T R ((m + 2) * n) = comp (T R (m + 2)) (T R n)
intro n
R : Type u_1
S : Type ?u.113283
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)
R : Type u_1
S : Type ?u.113283
inst✝¹ : CommRing R
inst✝ : CommRing S
m n : ℕ
⊢ T R ((m + 2) * n) = comp (T R (m + 2)) (T R n)
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
no goals
R : Type u_1
S : Type ?u.113283
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)
simp [this, T_mul m, ← T_mul (m + 1)]
no goals
R : Type u_1
S : Type ?u.113283
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)
convert mul_T R n (m * n) using 1 <;> ring_nf