no goals
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i₁ : ι₁
m₁ : M₁ i₁
i₂ : ι₂
m₂ : M₂ i₂
⊢ ↑(TensorProduct.directSum R M₁ M₂) (↑(lof R ι₁ M₁ i₁) m₁ ⊗ₜ[R] ↑(lof R ι₂ M₂ i₂) m₂) =
    ↑(lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)
simp [TensorProduct.directSum]