no goals
R : Type u_1
S : Type ?u.100205
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (k : ℕ), 2 * T R 0 * T R (0 + k) = T R (2 * 0 + k) + T R k
simp [two_mul, add_mul]
no goals
R : Type u_1
S : Type ?u.100205
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (k : ℕ), 2 * T R 1 * T R (1 + k) = T R (2 * 1 + k) + T R k
simp [add_comm]
R : Type u_1
S : Type ?u.100205
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
R : Type u_1
S : Type ?u.100205
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
intro k
R : Type u_1
S : Type ?u.100205
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
R : Type u_1
S : Type ?u.100205
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
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
R : Type u_1
S : Type ?u.100205
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
R : Type u_1
S : Type ?u.100205
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
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)
R : Type u_1
S : Type ?u.100205
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
R : Type u_1
S : Type ?u.100205
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
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)
R : Type u_1
S : Type ?u.100205
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
R : Type u_1
S : Type ?u.100205
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
have h₁ := T_add_two R m
R : Type u_1
S : Type ?u.100205
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
R : Type u_1
S : Type ?u.100205
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
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)
R : Type u_1
S : Type ?u.100205
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
R : Type u_1
S : Type ?u.100205
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
have h₃ := T_add_two R k
no goals
R : Type u_1
S : Type ?u.100205
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
linear_combination 2 * T R (m + k + 2) * h₁ + 2 * (X : R[X]) * H₁ - H₂ - h₂ - h₃
R : Type u_1
S : Type ?u.100205
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
R : Type u_1
S : Type ?u.100205
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
have h_nat₁ : 2 * (m + 2) + k = 2 * m + k + 4 := by ring
R : Type u_1
S : Type ?u.100205
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
R : Type u_1
S : Type ?u.100205
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
have h_nat₂ : m + 2 + k = m + k + 2 := by ring
no goals
R : Type u_1
S : Type ?u.100205
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
simpa [h_nat₁, h_nat₂] using this
no goals
R : Type u_1
S : Type ?u.100205
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
ring
no goals
R : Type u_1
S : Type ?u.100205
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
ring
R : Type u_1
S : Type ?u.100205
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)
R : Type u_1
S : Type ?u.100205
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)
have h_nat₁ : m + 1 + (k + 1) = m + k + 2 := by ring
R : Type u_1
S : Type ?u.100205
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)
R : Type u_1
S : Type ?u.100205
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)
have h_nat₂ : 2 * (m + 1) + (k + 1) = 2 * m + k + 3 := by ring
no goals
R : Type u_1
S : Type ?u.100205
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)
simpa [h_nat₁, h_nat₂] using mul_T (m + 1) (k + 1)
no goals
R : Type u_1
S : Type ?u.100205
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
⊢ m + 1 + (k + 1) = m + k + 2
ring
no goals
R : Type u_1
S : Type ?u.100205
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
ring
R : Type u_1
S : Type ?u.100205
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)
R : Type u_1
S : Type ?u.100205
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)
have h_nat₁ : 2 * m + (k + 2) = 2 * m + k + 2 := by simp [add_assoc]
R : Type u_1
S : Type ?u.100205
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)
R : Type u_1
S : Type ?u.100205
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)
have h_nat₂ : m + (k + 2) = m + k + 2 := by simp [add_assoc]
no goals
R : Type u_1
S : Type ?u.100205
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)
simpa [h_nat₁, h_nat₂] using mul_T m (k + 2)
no goals
R : Type u_1
S : Type ?u.100205
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
simp [add_assoc]
no goals
R : Type u_1
S : Type ?u.100205
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
simp [add_assoc]