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 : ι₁
x : M₁ i
y : M₂'
⊢ ↑(↑(toModule R ι₁ (M₂' →ₗ[R] ⨁ (i : ι₁), M₁ i ⊗[R] M₂') fun i =>
              compr₂ (mk R (M₁ i) M₂') (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i))
          (↑(lof R ι₁ M₁ i) x))
      y =
    ↑(lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)
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 : ι₁
x : M₁ i
y : M₂'
⊢ ↑(directSumLeft R M₁ M₂') (↑(lof R ι₁ M₁ i) x ⊗ₜ[R] y) = ↑(lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)
dsimp only [directSumLeft, LinearEquiv.ofLinear_apply, lift.tmul]
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 : ι₁
x : M₁ i
y : M₂'
⊢ ↑(↑(compr₂ (mk R (M₁ i) M₂') (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i)) x) y =
    ↑(lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)
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 : ι₁
x : M₁ i
y : M₂'
⊢ ↑(↑(toModule R ι₁ (M₂' →ₗ[R] ⨁ (i : ι₁), M₁ i ⊗[R] M₂') fun i =>
              compr₂ (mk R (M₁ i) M₂') (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i))
          (↑(lof R ι₁ M₁ i) x))
      y =
    ↑(lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)
rw [DirectSum.toModule_lof R i]
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 : ι₁
x : M₁ i
y : M₂'
⊢ ↑(↑(compr₂ (mk R (M₁ i) M₂') (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i)) x) y =
    ↑(lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)
rfl