-- Mathlib/Algebra/Colimit/TensorProduct.lean
theorem Submodule.FG.exists_rTensor_fg_inclusion_eq {N : Submodule R P} (hN : N.FG)
    {x y : N ⊗[R] M} (eq : N.subtype.rTensor M x = N.subtype.rTensor M y) :
    ∃ N', N'.FG ∧ ∃ h : N ≤ N', (N.inclusion h).rTensor M x = (N.inclusion h).rTensor M y

Proof state:
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
hN : N.FG
x y : ↥N ⊗[R] M
eq : (LinearMap.rTensor M N.subtype) x = (LinearMap.rTensor M N.subtype) y
⊢ ∃ N', N'.FG ∧ ∃ (h : N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Tactic:
lift N to {N : Submodule R P // N.FG} using hN

Result:
case intro
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq : (LinearMap.rTensor M (↑N).subtype) x = (LinearMap.rTensor M (↑N).subtype) y
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Proof state:
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
hN : N.FG
x y : ↥N ⊗[R] M
eq : (LinearMap.rTensor M N.subtype) x = (LinearMap.rTensor M N.subtype) y
⊢ ∃ N', N'.FG ∧ ∃ (h : N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Tactic:
classical
lift N to {N : Submodule R P // N.FG} using hN
apply_fun (Module.fgSystem.equiv R P).symm.toLinearMap.rTensor M at eq
apply_fun directLimitLeft _ _ at eq
simp_rw [← LinearMap.rTensor_comp_apply, ← (LinearEquiv.eq_toLinearMap_symm_comp _ _).mpr
  (Module.fgSystem.equiv_comp_of N), directLimitLeft_rTensor_of] at eq
have ⟨N', le, eq⟩ := Module.DirectLimit.exists_eq_of_of_eq eq
exact ⟨_, N'.2, le, eq⟩

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq :
  (directLimitLeft (Module.fgSystem R P) M)
      ((LinearMap.rTensor M ↑(Module.fgSystem.equiv R P).symm) ((LinearMap.rTensor M (↑N).subtype) x)) =
    (directLimitLeft (Module.fgSystem R P) M)
      ((LinearMap.rTensor M ↑(Module.fgSystem.equiv R P).symm) ((LinearMap.rTensor M (↑N).subtype) y))
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Tactic:
simp_rw [← LinearMap.rTensor_comp_apply, ← (LinearEquiv.eq_toLinearMap_symm_comp _ _).mpr
  (Module.fgSystem.equiv_comp_of N), directLimitLeft_rTensor_of] at eq

Result:
case intro
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq :
  (Module.DirectLimit.of R { N // N.FG } (fun i => ↥↑i ⊗[R] M)
        (fun i j h => LinearMap.rTensor M (Module.fgSystem R P i j h)) N)
      x =
    (Module.DirectLimit.of R { N // N.FG } (fun i => ↥↑i ⊗[R] M)
        (fun i j h => LinearMap.rTensor M (Module.fgSystem R P i j h)) N)
      y
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Proof state:
case intro
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq :
  (LinearMap.rTensor M ↑(Module.fgSystem.equiv R P).symm) ((LinearMap.rTensor M (↑N).subtype) x) =
    (LinearMap.rTensor M ↑(Module.fgSystem.equiv R P).symm) ((LinearMap.rTensor M (↑N).subtype) y)
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Tactic:
apply_fun directLimitLeft _ _ at eq

Result:
case intro
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq :
  (directLimitLeft (Module.fgSystem R P) M)
      ((LinearMap.rTensor M ↑(Module.fgSystem.equiv R P).symm) ((LinearMap.rTensor M (↑N).subtype) x)) =
    (directLimitLeft (Module.fgSystem R P) M)
      ((LinearMap.rTensor M ↑(Module.fgSystem.equiv R P).symm) ((LinearMap.rTensor M (↑N).subtype) y))
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Proof state:
case intro
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq✝ :
  (Module.DirectLimit.of R { N // N.FG } (fun i => ↥↑i ⊗[R] M)
        (fun i j h => LinearMap.rTensor M (Module.fgSystem R P i j h)) N)
      x =
    (Module.DirectLimit.of R { N // N.FG } (fun i => ↥↑i ⊗[R] M)
        (fun i j h => LinearMap.rTensor M (Module.fgSystem R P i j h)) N)
      y
N' : { N // N.FG }
le : N ≤ N'
eq : (LinearMap.rTensor M (Module.fgSystem R P N N' le)) x = (LinearMap.rTensor M (Module.fgSystem R P N N' le)) y
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Tactic:
exact ⟨_, N'.2, le, eq⟩

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq :
  (Module.DirectLimit.of R { N // N.FG } (fun i => ↥↑i ⊗[R] M)
        (fun i j h => LinearMap.rTensor M (Module.fgSystem R P i j h)) N)
      x =
    (Module.DirectLimit.of R { N // N.FG } (fun i => ↥↑i ⊗[R] M)
        (fun i j h => LinearMap.rTensor M (Module.fgSystem R P i j h)) N)
      y
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Tactic:
have ⟨N', le, eq⟩ := Module.DirectLimit.exists_eq_of_of_eq eq

Result:
case intro
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq✝ :
  (Module.DirectLimit.of R { N // N.FG } (fun i => ↥↑i ⊗[R] M)
        (fun i j h => LinearMap.rTensor M (Module.fgSystem R P i j h)) N)
      x =
    (Module.DirectLimit.of R { N // N.FG } (fun i => ↥↑i ⊗[R] M)
        (fun i j h => LinearMap.rTensor M (Module.fgSystem R P i j h)) N)
      y
N' : { N // N.FG }
le : N ≤ N'
eq : (LinearMap.rTensor M (Module.fgSystem R P N N' le)) x = (LinearMap.rTensor M (Module.fgSystem R P N N' le)) y
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Proof state:
case intro
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq : (LinearMap.rTensor M (↑N).subtype) x = (LinearMap.rTensor M (↑N).subtype) y
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Tactic:
apply_fun (Module.fgSystem.equiv R P).symm.toLinearMap.rTensor M at eq

Result:
case intro
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq :
  (LinearMap.rTensor M ↑(Module.fgSystem.equiv R P).symm) ((LinearMap.rTensor M (↑N).subtype) x) =
    (LinearMap.rTensor M ↑(Module.fgSystem.equiv R P).symm) ((LinearMap.rTensor M (↑N).subtype) y)
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y