[GOAL]
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₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) ≃ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd
[PROOFSTEP]
refine LinearEquiv.ofLinear (R := R) (R₂ := R) ?toFun ?invFun ?left ?right
[GOAL]
case toFun
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₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd
[PROOFSTEP]
refine lift ?_
[GOAL]
case toFun
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₁ i₁) →ₗ[R] (⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd
[PROOFSTEP]
refine DirectSum.toModule R _ _ fun i₁ => ?_
[GOAL]
case toFun
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₁ i₁ →ₗ[R] (⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd
[PROOFSTEP]
refine @LinearMap.flip R _ R _ R _ R _ _ _ _ _ _ _ _ _ _ _ _ _ _ ?_
[GOAL]
case toFun
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₁ : ι₁
⊢ (⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd
[PROOFSTEP]
refine DirectSum.toModule R _ _ fun i₂ => LinearMap.flip <| ?_
[GOAL]
case toFun
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₁ : ι₁
i₂ : ι₂
⊢ M₁ i₁ →ₗ[R] M₂ i₂ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd
[PROOFSTEP]
refine curry ?_
[GOAL]
case toFun
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₁ : ι₁
i₂ : ι₂
⊢ M₁ i₁ ⊗[R] M₂ i₂ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd
[PROOFSTEP]
exact DirectSum.lof R (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂)
[GOAL]
case invFun
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₁ i.fst ⊗[R] M₂ i.snd) →ₗ[R] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂
[PROOFSTEP]
refine DirectSum.toModule R _ _ fun i => ?_
[GOAL]
case invFun
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₁ i.fst ⊗[R] M₂ i.snd →ₗ[R] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂
[PROOFSTEP]
exact map (DirectSum.lof R _ M₁ i.1) (DirectSum.lof R _ M₂ i.2)
[GOAL]
case left
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₂'
⊢ comp
      (lift
        (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
          LinearMap.flip
            (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
              LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))
      (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
        map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd)) =
    LinearMap.id
[PROOFSTEP]
refine DirectSum.linearMap_ext R fun ⟨i₁, i₂⟩ => ?_
[GOAL]
case left
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✝ : ι₁ × ι₂
i₁ : ι₁
i₂ : ι₂
⊢ comp
      (comp
        (lift
          (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
            LinearMap.flip
              (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
                LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))
        (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
          map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd)))
      (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂)) =
    comp LinearMap.id (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))
[PROOFSTEP]
refine TensorProduct.ext ?_
[GOAL]
case left
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✝ : ι₁ × ι₂
i₁ : ι₁
i₂ : ι₂
⊢ compr₂ (mk R (M₁ (i₁, i₂).fst) (M₂ (i₁, i₂).snd))
      (comp
        (comp
          (lift
            (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
              LinearMap.flip
                (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
                  LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))
          (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
            map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd)))
        (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))) =
    compr₂ (mk R (M₁ (i₁, i₂).fst) (M₂ (i₁, i₂).snd))
      (comp LinearMap.id (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂)))
[PROOFSTEP]
refine
  LinearMap.ext₂ fun m₁ m₂ =>
    ?_
      -- porting note: seems much nicer than the `repeat` lean 3 proof.
[GOAL]
case left
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✝ : ι₁ × ι₂
i₁ : ι₁
i₂ : ι₂
m₁ : M₁ (i₁, i₂).fst
m₂ : M₂ (i₁, i₂).snd
⊢ ↑(↑(compr₂ (mk R (M₁ (i₁, i₂).fst) (M₂ (i₁, i₂).snd))
              (comp
                (comp
                  (lift
                    (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
                      LinearMap.flip
                        (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
                          LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))
                  (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
                    map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd)))
                (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))
          m₁)
      m₂ =
    ↑(↑(compr₂ (mk R (M₁ (i₁, i₂).fst) (M₂ (i₁, i₂).snd))
              (comp LinearMap.id (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))
          m₁)
      m₂
[PROOFSTEP]
simp only [compr₂_apply, comp_apply, id_apply, mk_apply, DirectSum.toModule_lof, map_tmul, lift.tmul, flip_apply,
  curry_apply]
[GOAL]
case right
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₂'
⊢ comp
      (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
        map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd))
      (lift
        (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
          LinearMap.flip
            (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
              LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂)))))) =
    LinearMap.id
[PROOFSTEP]
refine TensorProduct.ext ?_
[GOAL]
case right
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₂'
⊢ compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂))
      (comp
        (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
          map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd))
        (lift
          (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
            LinearMap.flip
              (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
                LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))) =
    compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂)) LinearMap.id
[PROOFSTEP]
refine @DirectSum.linearMap_ext R _ _ _ _ _ _ _ _ (_) _ _ fun i₁ => ?_
[GOAL]
case right
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₁ : ι₁
⊢ comp
      (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂))
        (comp
          (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
            map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd))
          (lift
            (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
              LinearMap.flip
                (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
                  LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))))
      (lof R ι₁ (fun i => M₁ i) i₁) =
    comp (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂)) LinearMap.id) (lof R ι₁ (fun i => M₁ i) i₁)
[PROOFSTEP]
refine @LinearMap.ext _ _ _ _ _ _ _ _ (_) (_) _ _ _ fun x₁ => ?_
[GOAL]
case right
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₁
⊢ ↑(comp
          (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂))
            (comp
              (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
                map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd))
              (lift
                (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
                  LinearMap.flip
                    (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
                      LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))))
          (lof R ι₁ (fun i => M₁ i) i₁))
      x₁ =
    ↑(comp (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂)) LinearMap.id) (lof R ι₁ (fun i => M₁ i) i₁)) x₁
[PROOFSTEP]
refine @DirectSum.linearMap_ext R _ _ _ _ _ _ _ _ (_) _ _ fun i₂ => ?_
[GOAL]
case right
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₁
i₂ : ι₂
⊢ comp
      (↑(comp
            (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂))
              (comp
                (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
                  map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd))
                (lift
                  (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
                    LinearMap.flip
                      (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
                        LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))))
            (lof R ι₁ (fun i => M₁ i) i₁))
        x₁)
      (lof R ι₂ (fun i => M₂ i) i₂) =
    comp
      (↑(comp (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂)) LinearMap.id) (lof R ι₁ (fun i => M₁ i) i₁)) x₁)
      (lof R ι₂ (fun i => M₂ i) i₂)
[PROOFSTEP]
refine
  LinearMap.ext fun x₂ =>
    ?_
      -- porting note: seems much nicer than the `repeat` lean 3 proof.
[GOAL]
case right
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₁
i₂ : ι₂
x₂ : M₂ i₂
⊢ ↑(comp
          (↑(comp
                (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂))
                  (comp
                    (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
                      map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd))
                    (lift
                      (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
                        LinearMap.flip
                          (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
                            LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))))
                (lof R ι₁ (fun i => M₁ i) i₁))
            x₁)
          (lof R ι₂ (fun i => M₂ i) i₂))
      x₂ =
    ↑(comp
          (↑(comp (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂)) LinearMap.id) (lof R ι₁ (fun i => M₁ i) i₁))
            x₁)
          (lof R ι₂ (fun i => M₂ i) i₂))
      x₂
[PROOFSTEP]
simp only [compr₂_apply, comp_apply, id_apply, mk_apply, DirectSum.toModule_lof, map_tmul, lift.tmul, flip_apply,
  curry_apply]
  /- was:
  
      refine'
        LinearEquiv.ofLinear
          (lift <|
            DirectSum.toModule R _ _ fun i₁ => LinearMap.flip <| DirectSum.toModule R _ _ fun i₂ =>
                  LinearMap.flip <| curry <|
                    DirectSum.lof R (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂))
          (DirectSum.toModule R _ _ fun i => map (DirectSum.lof R _ _ _) (DirectSum.lof R _ _ _)) _
          _ <;>
      [ext ⟨i₁, i₂⟩ x₁ x₂ : 4, ext i₁ i₂ x₁ x₂ : 5]
    repeat'
      first
        |rw [compr₂_apply]|rw [comp_apply]|rw [id_apply]|rw [mk_apply]|rw [DirectSum.toModule_lof]
        |rw [map_tmul]|rw [lift.tmul]|rw [flip_apply]|rw [curry_apply]
    -/
  
  /- alternative with explicit types:
    refine'
        LinearEquiv.ofLinear
          (lift <|
            DirectSum.toModule
              (R := R) (M := M₁) (N := (⨁ i₂, M₂ i₂) →ₗ[R] ⨁ i : ι₁ × ι₂, M₁ i.1 ⊗[R] M₂ i.2)
              (φ := fun i₁ => LinearMap.flip <|
                DirectSum.toModule (R := R) (M := M₂) (N := ⨁ i : ι₁ × ι₂, M₁ i.1 ⊗[R] M₂ i.2)
                (φ := fun i₂ => LinearMap.flip <| curry <|
                    DirectSum.lof R (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂))))
          (DirectSum.toModule
            (R := R)
            (M := fun i : ι₁ × ι₂ => M₁ i.1 ⊗[R] M₂ i.2)
            (N := (⨁ i₁, M₁ i₁) ⊗[R] ⨁ i₂, M₂ i₂)
            (φ := fun i : ι₁ × ι₂ => map (DirectSum.lof R _ M₁ i.1) (DirectSum.lof R _ M₂ i.2))) _
          _ <;>
      [ext ⟨i₁, i₂⟩ x₁ x₂ : 4, ext i₁ i₂ x₁ x₂ : 5]
    repeat'
      first
        |rw [compr₂_apply]|rw [comp_apply]|rw [id_apply]|rw [mk_apply]|rw [DirectSum.toModule_lof]
        |rw [map_tmul]|rw [lift.tmul]|rw [flip_apply]|rw [curry_apply]
  -/
[GOAL]
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
m₂ : M₂'
⊢ ↑(↑(compr₂ (mk R (M₁ i) M₂')
              (comp
                (comp
                  (lift
                    (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)))
                  (toModule R ι₁ ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂') fun i => rTensor M₂' (lof R ι₁ M₁ i)))
                (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i)))
          m₁)
      m₂ =
    ↑(↑(compr₂ (mk R (M₁ i) M₂') (comp LinearMap.id (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i))) m₁) m₂
[PROOFSTEP]
dsimp only [comp_apply, compr₂_apply, id_apply, mk_apply]
[GOAL]
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
m₂ : M₂'
⊢ ↑(lift
          (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)))
      (↑(toModule R ι₁ ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂') fun i => rTensor M₂' (lof R ι₁ M₁ i))
        (↑(lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (m₁ ⊗ₜ[R] m₂))) =
    ↑(lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (m₁ ⊗ₜ[R] m₂)
[PROOFSTEP]
simp_rw [DirectSum.toModule_lof, rTensor_tmul, lift.tmul, DirectSum.toModule_lof, compr₂_apply, mk_apply]
[GOAL]
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
m₂ : M₂'
⊢ ↑(↑(comp
              (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) M₂')
                (comp (toModule R ι₁ ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂') fun i => rTensor M₂' (lof R ι₁ M₁ i))
                  (lift
                    (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 ι₁ (fun i => M₁ i) i))
          m₁)
      m₂ =
    ↑(↑(comp (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) M₂') LinearMap.id) (lof R ι₁ (fun i => M₁ i) i)) m₁) m₂
[PROOFSTEP]
dsimp only [comp_apply, compr₂_apply, id_apply, mk_apply]
[GOAL]
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
m₂ : M₂'
⊢ ↑(toModule R ι₁ ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂') fun i => rTensor M₂' (lof R ι₁ M₁ i))
      (↑(lift
            (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 ι₁ (fun i => M₁ i) i) m₁ ⊗ₜ[R] m₂)) =
    ↑(lof R ι₁ (fun i => M₁ i) i) m₁ ⊗ₜ[R] m₂
[PROOFSTEP]
simp_rw [lift.tmul, DirectSum.toModule_lof, compr₂_apply, mk_apply, DirectSum.toModule_lof, rTensor_tmul]
[GOAL]
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₂)
[PROOFSTEP]
simp [TensorProduct.directSum]
[GOAL]
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)
[PROOFSTEP]
dsimp only [directSumLeft, LinearEquiv.ofLinear_apply, lift.tmul]
[GOAL]
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)
[PROOFSTEP]
rw [DirectSum.toModule_lof R i]
[GOAL]
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)
[PROOFSTEP]
rfl
[GOAL]
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₂'
⊢ ↑(LinearEquiv.symm (directSumLeft R M₁ M₂')) (↑(lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)) =
    ↑(lof R ι₁ M₁ i) x ⊗ₜ[R] y
[PROOFSTEP]
rw [LinearEquiv.symm_apply_eq, directSumLeft_tmul_lof]
[GOAL]
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)
[PROOFSTEP]
dsimp only [directSumRight, LinearEquiv.trans_apply, TensorProduct.comm_tmul]
[GOAL]
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)
[PROOFSTEP]
rw [directSumLeft_tmul_lof]
[GOAL]
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)
[PROOFSTEP]
exact DFinsupp.mapRange_single (hf := fun _ => rfl)
[GOAL]
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
⊢ ↑(LinearEquiv.symm (directSumRight R M₁' M₂)) (↑(lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)) =
    x ⊗ₜ[R] ↑(lof R ι₂ M₂ i) y
[PROOFSTEP]
rw [LinearEquiv.symm_apply_eq, directSumRight_tmul_lof]
