-- Mathlib/RingTheory/Flat/Basic.lean
theorem rTensor_preserves_injective_linearMap [Flat R M] (f : N →ₗ[R] P)
    (hf : Function.Injective f) : Function.Injective (f.rTensor M)

Proof state:
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✝
inst✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Function.Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : N.FG
Pfg : P.FG
le : N ≤ comap f P
⊢ Function.Injective ⇑(rTensor M (f.restrict le))

Tactic:
rw [← Finite.iff_fg] at Nfg Pfg

Result:
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✝
inst✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Function.Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : Module.Finite R ↥N
Pfg : Module.Finite R ↥P
le : N ≤ comap f P
⊢ Function.Injective ⇑(rTensor M (f.restrict le))

Proof state:
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
inst✝ : Flat R M
f : N →ₗ[R] P
hf : Function.Injective ⇑f
⊢ Function.Injective ⇑(rTensor M f)

Tactic:
refine rTensor_injective_of_fg fun N P Nfg Pfg le ↦ ?_

Result:
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✝
inst✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Function.Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : N.FG
Pfg : P.FG
le : N ≤ comap f P
⊢ Function.Injective ⇑(rTensor M (f.restrict le))

Proof state:
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✝
inst✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Function.Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : Module.Finite R ↥N
Pfg : Module.Finite R ↥P
le : N ≤ comap f P
this✝ : Small.{u, u_2} ↥P
se : ↥P ≃ₗ[R] Shrink.{u, u_2} ↥P := (Shrink.linearEquiv (↥P) R).symm
this : Module.Finite R (Shrink.{u, u_2} ↥P)
⊢ Function.Injective ⇑(rTensor M (range (↑se ∘ₗ f.restrict le)).subtype)

Tactic:
exact (flat_iff R M).mp ‹_› _ (Finite.iff_fg.mp inferInstance)

Result:
no goals

Proof state:
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✝
inst✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Function.Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : Module.Finite R ↥N
Pfg : Module.Finite R ↥P
le : N ≤ comap f P
this : Small.{max u ?u.28196, u_2} ↥P
⊢ Function.Injective ⇑(rTensor M (f.restrict le))

Tactic:
let se := (Shrink.linearEquiv.{_, u} P R).symm

Result:
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✝
inst✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Function.Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : Module.Finite R ↥N
Pfg : Module.Finite R ↥P
le : N ≤ comap f P
this : Small.{u, u_2} ↥P
se : ↥P ≃ₗ[R] Shrink.{u, u_2} ↥P := (Shrink.linearEquiv (↥P) R).symm
⊢ Function.Injective ⇑(rTensor M (f.restrict le))

Proof state:
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✝
inst✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Function.Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : Module.Finite R ↥N
Pfg : Module.Finite R ↥P
le : N ≤ comap f P
this : Small.{u, u_2} ↥P
se : ↥P ≃ₗ[R] Shrink.{u, u_2} ↥P := (Shrink.linearEquiv (↥P) R).symm
⊢ Function.Injective ⇑(rTensor M (f.restrict le))

Tactic:
have := Module.Finite.equiv se

Result:
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✝
inst✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Function.Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : Module.Finite R ↥N
Pfg : Module.Finite R ↥P
le : N ≤ comap f P
this✝ : Small.{u, u_2} ↥P
se : ↥P ≃ₗ[R] Shrink.{u, u_2} ↥P := (Shrink.linearEquiv (↥P) R).symm
this : Module.Finite R (Shrink.{u, u_2} ↥P)
⊢ Function.Injective ⇑(rTensor M (f.restrict le))

Proof state:
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✝
inst✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Function.Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : Module.Finite R ↥N
Pfg : Module.Finite R ↥P
le : N ≤ comap f P
⊢ Function.Injective ⇑(rTensor M (f.restrict le))

Tactic:
have := Finite.small R P

Result:
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✝
inst✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Function.Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : Module.Finite R ↥N
Pfg : Module.Finite R ↥P
le : N ≤ comap f P
this : Small.{max u ?u.28196, u_2} ↥P
⊢ Function.Injective ⇑(rTensor M (f.restrict le))