Theorem: TensorProduct.exists_of_fg (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
t : M ⊗[R] N
⊢ ∃ P, P.FG ∧ t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
Tactic:
let ⟨P, u, hu⟩ := Module.DirectLimit.exists_of ((rTensor_fgEquiv R M N).symm t)
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
t : M ⊗[R] N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
hu :
  (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 =
    (rTensor_fgEquiv R M N).symm t
⊢ ∃ P, P.FG ∧ t ∈ LinearMap.range (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
t : M ⊗[R] N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
hu :
  (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 =
    (rTensor_fgEquiv R M N).symm t
⊢ ∃ P, P.FG ∧ t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
Tactic:
use P.val, P.property, u
State after:
case 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
t : M ⊗[R] N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
hu :
  (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 =
    (rTensor_fgEquiv R M N).symm t
⊢ (LinearMap.rTensor N (↑P).subtype) u = t

State before:
case 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
t : M ⊗[R] N
P : Submodules_fg R M
u : ↥↑P ⊗[R] N
hu :
  (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 =
    (rTensor_fgEquiv R M N).symm t
⊢ (LinearMap.rTensor N (↑P).subtype) u = t
Tactic:
rw [← rTensor_fgEquiv_of, hu, LinearEquiv.apply_symm_apply]
State after:
no goals