-- Mathlib/RingTheory/Flat/Basic.lean
/-- `M` is flat if and only if `f ⊗ 𝟙 M` is injective whenever `f` is an injective linear map.
  See `Module.Flat.iff_rTensor_preserves_injective_linearMap` to specialize the universe of
  `N, N', N''` to `Type (max u v)`. -/
lemma iff_rTensor_preserves_injective_linearMap' [Small.{v'} R] : Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [AddCommGroup N] [AddCommGroup 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 ↦
    iff_rTensor_preserves_injective_linearMapₛ.mpr fun P N _ _ _ _ ↦ by
      letI := Module.addCommMonoidToAddCommGroup R (M := P)
      letI := Module.addCommMonoidToAddCommGroup R (M := N)
      apply h⟩

Proof state:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
⊢ Flat R M →
    ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup 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✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Small.{v', u} R
a✝ : Flat R M
N N' : Type v'
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup 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✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
    (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(rTensor M f)
P N : Type v'
x✝³ : AddCommMonoid P
x✝² : AddCommMonoid N
x✝¹ : Module R P
x✝ : Module R N
this : AddCommGroup P := addCommMonoidToAddCommGroup R
⊢ ∀ (f : P →ₗ[R] N), Function.Injective ⇑f → Function.Injective ⇑(rTensor M f)

Tactic:
letI := Module.addCommMonoidToAddCommGroup R (M := N)

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

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

Tactic:
letI := Module.addCommMonoidToAddCommGroup R (M := P)

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

Proof state:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Small.{v', u} R
a✝ : Flat R M
N N' : Type v'
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup 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✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
    (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(rTensor M f)
P N : Type v'
x✝³ : AddCommMonoid P
x✝² : AddCommMonoid N
x✝¹ : Module R P
x✝ : Module R N
this✝ : AddCommGroup P := addCommMonoidToAddCommGroup R
this : AddCommGroup N := addCommMonoidToAddCommGroup R
⊢ ∀ (f : P →ₗ[R] N), Function.Injective ⇑f → Function.Injective ⇑(rTensor M f)

Tactic:
apply h

Result:
no goals