-- Mathlib/RingTheory/Flat/Basic.lean
/-- `M` is flat if and only if `f ⊗ 𝟙 M` is injective whenever `f` is an injective linear map
in a universe that `R` fits in. -/
lemma iff_rTensor_preserves_injective_linearMapₛ [Small.{v'} R] : Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N']
      (f : N →ₗ[R] N'), Function.Injective f → Function.Injective (f.rTensor M) :=
  ⟨by introv _; apply rTensor_preserves_injective_linearMap, fun h ↦ ⟨fun P _ _ _ _ _ ↦ by
    have := Finite.small.{v'} R P
    rw [rTensor_injective_iff_subtype Subtype.val_injective (Shrink.linearEquiv.{_, v'} P R).symm]
    exact h _ Subtype.val_injective⟩⟩

Proof state:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
⊢ Flat R M →
    ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(rTensor M f)

Tactic:
introv _

Result:
R : Type u
M : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Small.{v', u} R
a✝ : Flat R M
N N' : Type v'
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N
inst✝ : Module R N'
f : N →ₗ[R] N'
⊢ Function.Injective ⇑f → Function.Injective ⇑(rTensor M f)

Proof state:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N']
    (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(rTensor M f)
P : Type u
x✝⁴ : AddCommMonoid P
x✝³ : Module R P
x✝² : Module.Finite R P
x✝¹ : Submodule R P
x✝ : x✝¹.FG
⊢ Function.Injective ⇑(rTensor M x✝¹.subtype)

Tactic:
have := Finite.small.{v'} R P

Result:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N']
    (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(rTensor M f)
P : Type u
x✝⁴ : AddCommMonoid P
x✝³ : Module R P
x✝² : Module.Finite R P
x✝¹ : Submodule R P
x✝ : x✝¹.FG
this : Small.{v', u} P
⊢ Function.Injective ⇑(rTensor M x✝¹.subtype)

Proof state:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N']
    (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(rTensor M f)
P : Type u
x✝⁴ : AddCommMonoid P
x✝³ : Module R P
x✝² : Module.Finite R P
x✝¹ : Submodule R P
x✝ : x✝¹.FG
this : Small.{v', u} P
⊢ Function.Injective ⇑(rTensor M (range (↑(Shrink.linearEquiv P R).symm ∘ₗ x✝¹.subtype)).subtype)

Tactic:
exact h _ Subtype.val_injective

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Small.{v', u} R
a✝ : Flat R M
N N' : Type v'
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N
inst✝ : Module R N'
f : N →ₗ[R] N'
⊢ Function.Injective ⇑f → Function.Injective ⇑(rTensor M f)

Tactic:
apply rTensor_preserves_injective_linearMap

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N']
    (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(rTensor M f)
P : Type u
x✝⁴ : AddCommMonoid P
x✝³ : Module R P
x✝² : Module.Finite R P
x✝¹ : Submodule R P
x✝ : x✝¹.FG
this : Small.{v', u} P
⊢ Function.Injective ⇑(rTensor M x✝¹.subtype)

Tactic:
rw [rTensor_injective_iff_subtype Subtype.val_injective (Shrink.linearEquiv.{_, v'} P R).symm]

Result:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N']
    (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(rTensor M f)
P : Type u
x✝⁴ : AddCommMonoid P
x✝³ : Module R P
x✝² : Module.Finite R P
x✝¹ : Submodule R P
x✝ : x✝¹.FG
this : Small.{v', u} P
⊢ Function.Injective ⇑(rTensor M (range (↑(Shrink.linearEquiv P R).symm ∘ₗ x✝¹.subtype)).subtype)