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₂'
x : M₁'
i : ι₂
y : M₂ i
⊢ ↑(Dfinsupp.mapRange.linearEquiv fun x => TensorProduct.comm R (M₂ x) M₁')
      (↑(directSumLeft R M₂ M₁') (↑(lof R ι₂ M₂ i) y ⊗ₜ[R] x)) =
    ↑(lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) 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₂'
x : M₁'
i : ι₂
y : M₂ i
⊢ ↑(directSumRight R M₁' M₂) (x ⊗ₜ[R] ↑(lof R ι₂ M₂ i) y) = ↑(lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)
dsimp only [directSumRight, LinearEquiv.trans_apply, TensorProduct.comm_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₂'
x : M₁'
i : ι₂
y : M₂ i
⊢ ↑(Dfinsupp.mapRange.linearEquiv fun x => TensorProduct.comm R (M₂ x) M₁')
      (↑(lof R ι₂ (fun i => M₂ i ⊗[R] M₁') i) (y ⊗ₜ[R] x)) =
    ↑(lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) 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₂'
x : M₁'
i : ι₂
y : M₂ i
⊢ ↑(Dfinsupp.mapRange.linearEquiv fun x => TensorProduct.comm R (M₂ x) M₁')
      (↑(directSumLeft R M₂ M₁') (↑(lof R ι₂ M₂ i) y ⊗ₜ[R] x)) =
    ↑(lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)
rw [directSumLeft_tmul_lof]
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₂'
x : M₁'
i : ι₂
y : M₂ i
⊢ ↑(Dfinsupp.mapRange.linearEquiv fun x => TensorProduct.comm R (M₂ x) M₁')
      (↑(lof R ι₂ (fun i => M₂ i ⊗[R] M₁') i) (y ⊗ₜ[R] x)) =
    ↑(lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)
exact Dfinsupp.mapRange_single (hf := fun _ => rfl)