Theorem: rTensor_fgEquiv_of (DividedPowers/ForMathlib/DirectLimit.lean)

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
⊢ (rTensor_fgEquiv R M N)
      ((Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
          (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) P)
        u) =
    (LinearMap.rTensor N (↑P).subtype) u
Tactic:
suffices (rTensor_fgEquiv R M N).toLinearMap.comp
    (Module.DirectLimit.of R (Submodules_fg R M) (fun P ↦ P.val ⊗[R] N)
      (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) P)
    = LinearMap.rTensor N (Submodule.subtype P.val) by
  exact DFunLike.congr_fun this u
State after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
⊢ ↑(rTensor_fgEquiv R M N) ∘ₗ
      Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) P =
    LinearMap.rTensor N (↑P).subtype

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
⊢ ↑(rTensor_fgEquiv R M N) ∘ₗ
      Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) P =
    LinearMap.rTensor N (↑P).subtype
Tactic:
ext p n
State after:
case a.h.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ ((AlgebraTensorModule.curry
          (↑(rTensor_fgEquiv R M N) ∘ₗ
            Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
              (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) P))
        p)
      n =
    ((AlgebraTensorModule.curry (LinearMap.rTensor N (↑P).subtype)) p) n

State before:
case a.h.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ ((AlgebraTensorModule.curry
          (↑(rTensor_fgEquiv R M N) ∘ₗ
            Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
              (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) P))
        p)
      n =
    ((AlgebraTensorModule.curry (LinearMap.rTensor N (↑P).subtype)) p) n
Tactic:
simp only [rTensor_fgEquiv, AlgebraTensorModule.curry_apply, curry_apply,
  LinearMap.coe_restrictScalars, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
  LinearEquiv.trans_apply, directLimitLeft_symm_of_tmul, LinearEquiv.rTensor_tmul,
  LinearMap.rTensor_tmul, Submodule.coeSubtype]
State after:
case a.h.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (Submodules_fg_equiv R M)
        ((Module.DirectLimit.of R (Submodules_fg R M) (fun i => ↥↑i)
            (fun P Q hPQ => Submodules_fg_inclusion R M P Q hPQ) P)
          p) ⊗ₜ[R]
      n =
    ↑p ⊗ₜ[R] n

State before:
case a.h.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (Submodules_fg_equiv R M)
        ((Module.DirectLimit.of R (Submodules_fg R M) (fun i => ↥↑i)
            (fun P Q hPQ => Submodules_fg_inclusion R M P Q hPQ) P)
          p) ⊗ₜ[R]
      n =
    ↑p ⊗ₜ[R] n
Tactic:
congr
State after:
case a.h.h.e_m
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (Submodules_fg_equiv R M)
      ((Module.DirectLimit.of R (Submodules_fg R M) (fun i => ↥↑i) (fun P Q hPQ => Submodules_fg_inclusion R M P Q hPQ)
          P)
        p) =
    ↑p

State before:
case a.h.h.e_m
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (Submodules_fg_equiv R M)
      ((Module.DirectLimit.of R (Submodules_fg R M) (fun i => ↥↑i) (fun P Q hPQ => Submodules_fg_inclusion R M P Q hPQ)
          P)
        p) =
    ↑p
Tactic:
simp only [Submodules_fg_equiv, LinearEquiv.ofBijective_apply]
State after:
case a.h.h.e_m
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (Submodules_fg_map R M)
      ((Module.DirectLimit.of R (Submodules_fg R M) (fun i => ↥↑i) (fun P Q hPQ => Submodules_fg_inclusion R M P Q hPQ)
          P)
        p) =
    ↑p

State before:
case a.h.h.e_m
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (Submodules_fg_map R M)
      ((Module.DirectLimit.of R (Submodules_fg R M) (fun i => ↥↑i) (fun P Q hPQ => Submodules_fg_inclusion R M P Q hPQ)
          P)
        p) =
    ↑p
Tactic:
simp only [Submodules_fg_map]
State after:
case a.h.h.e_m
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (Module.DirectLimit.lift R (Submodules_fg R M) (fun P => ↥↑P) (Submodules_fg_inclusion R M) (fun P => (↑P).subtype) ⋯)
      ((Module.DirectLimit.of R (Submodules_fg R M) (fun i => ↥↑i) (fun P Q hPQ => Submodules_fg_inclusion R M P Q hPQ)
          P)
        p) =
    ↑p

State before:
case a.h.h.e_m
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (Module.DirectLimit.lift R (Submodules_fg R M) (fun P => ↥↑P) (Submodules_fg_inclusion R M) (fun P => (↑P).subtype) ⋯)
      ((Module.DirectLimit.of R (Submodules_fg R M) (fun i => ↥↑i) (fun P Q hPQ => Submodules_fg_inclusion R M P Q hPQ)
          P)
        p) =
    ↑p
Tactic:
simp only [Module.DirectLimit.lift_of]
State after:
case a.h.h.e_m
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (↑P).subtype p = ↑p

State before:
case a.h.h.e_m
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ (↑P).subtype p = ↑p
Tactic:
simp only [Submodule.coeSubtype]
State after:
no goals

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
this :
  ↑(rTensor_fgEquiv R M N) ∘ₗ
      Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) P =
    LinearMap.rTensor N (↑P).subtype
⊢ (rTensor_fgEquiv R M N)
      ((Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
          (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) P)
        u) =
    (LinearMap.rTensor N (↑P).subtype) u
Tactic:
exact DFunLike.congr_fun this u
State after:
no goals