-- Mathlib/RingTheory/Flat/Basic.lean
theorem _root_.LinearMap.rTensor_injective_of_fg {f : N →ₗ[R] P}
    (h :  ∀ (N' : Submodule R N) (P' : Submodule R P),
      N'.FG → P'.FG → ∀ h : N' ≤ P'.comap f, Function.Injective ((f.restrict h).rTensor M)) :
    Function.Injective (f.rTensor M) := fun x y eq ↦ by
  have ⟨N', Nfg, sub⟩ := Submodule.exists_fg_le_subset_range_rTensor_subtype {x, y} (by simp)
  obtain ⟨x, rfl⟩ := sub (.inl rfl)
  obtain ⟨y, rfl⟩ := sub (.inr rfl)
  simp_rw [← rTensor_comp_apply, show f ∘ₗ N'.subtype = (N'.map f).subtype ∘ₗ f.submoduleMap N'
    from rfl, rTensor_comp_apply] at eq
  have ⟨P', Pfg, le, eq⟩ := (Nfg.map _).exists_rTensor_fg_inclusion_eq eq
  simp_rw [← rTensor_comp_apply] at eq
  rw [h _ _ Nfg Pfg (map_le_iff_le_comap.mp le) eq]

Proof state:
case intro
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Function.Injective ⇑(rTensor M (f.restrict h))
y : N ⊗[R] M
N' : Submodule R N
Nfg : N'.FG
x : ↥N' ⊗[R] M
eq : (rTensor M f) ((rTensor M N'.subtype) x) = (rTensor M f) y
sub : {(rTensor M N'.subtype) x, y} ⊆ ↑(range (rTensor M N'.subtype))
⊢ (rTensor M N'.subtype) x = y

Tactic:
obtain ⟨y, rfl⟩ := sub (.inr rfl)

Result:
case intro.intro
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Function.Injective ⇑(rTensor M (f.restrict h))
N' : Submodule R N
Nfg : N'.FG
x y : ↥N' ⊗[R] M
eq : (rTensor M f) ((rTensor M N'.subtype) x) = (rTensor M f) ((rTensor M N'.subtype) y)
sub : {(rTensor M N'.subtype) x, (rTensor M N'.subtype) y} ⊆ ↑(range (rTensor M N'.subtype))
⊢ (rTensor M N'.subtype) x = (rTensor M N'.subtype) y

Proof state:
case intro.intro
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Function.Injective ⇑(rTensor M (f.restrict h))
N' : Submodule R N
Nfg : N'.FG
x y : ↥N' ⊗[R] M
sub : {(rTensor M N'.subtype) x, (rTensor M N'.subtype) y} ⊆ ↑(range (rTensor M N'.subtype))
eq :
  (rTensor M (Submodule.map f N').subtype) ((rTensor M (f.submoduleMap N')) x) =
    (rTensor M (Submodule.map f N').subtype) ((rTensor M (f.submoduleMap N')) y)
⊢ (rTensor M N'.subtype) x = (rTensor M N'.subtype) y

Tactic:
have ⟨P', Pfg, le, eq⟩ := (Nfg.map _).exists_rTensor_fg_inclusion_eq eq

Result:
case intro.intro
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Function.Injective ⇑(rTensor M (f.restrict h))
N' : Submodule R N
Nfg : N'.FG
x y : ↥N' ⊗[R] M
sub : {(rTensor M N'.subtype) x, (rTensor M N'.subtype) y} ⊆ ↑(range (rTensor M N'.subtype))
eq✝ :
  (rTensor M (Submodule.map f N').subtype) ((rTensor M (f.submoduleMap N')) x) =
    (rTensor M (Submodule.map f N').subtype) ((rTensor M (f.submoduleMap N')) y)
P' : Submodule R P
Pfg : P'.FG
le : Submodule.map f N' ≤ P'
eq :
  (rTensor M (inclusion le)) ((rTensor M (f.submoduleMap N')) x) =
    (rTensor M (inclusion le)) ((rTensor M (f.submoduleMap N')) y)
⊢ (rTensor M N'.subtype) x = (rTensor M N'.subtype) y

Proof state:
case intro.intro
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Function.Injective ⇑(rTensor M (f.restrict h))
N' : Submodule R N
Nfg : N'.FG
x y : ↥N' ⊗[R] M
sub : {(rTensor M N'.subtype) x, (rTensor M N'.subtype) y} ⊆ ↑(range (rTensor M N'.subtype))
eq✝ :
  (rTensor M (Submodule.map f N').subtype) ((rTensor M (f.submoduleMap N')) x) =
    (rTensor M (Submodule.map f N').subtype) ((rTensor M (f.submoduleMap N')) y)
P' : Submodule R P
Pfg : P'.FG
le : Submodule.map f N' ≤ P'
eq : (rTensor M (inclusion le ∘ₗ f.submoduleMap N')) x = (rTensor M (inclusion le ∘ₗ f.submoduleMap N')) y
⊢ (rTensor M N'.subtype) x = (rTensor M N'.subtype) y

Tactic:
rw [h _ _ Nfg Pfg (map_le_iff_le_comap.mp le) eq]

Result:
no goals