-- Mathlib/RingTheory/Flat/Basic.lean
/-- A retract of a flat `R`-module is flat. -/
lemma of_retract [f : Flat R M] (i : N →ₗ[R] M) (r : M →ₗ[R] N) (h : r.comp i = LinearMap.id) :
    Flat R N

Proof state:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f :
  ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
⊢ ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N_1 : Submodule R P),
    Function.Injective ⇑(rTensor N N_1.subtype)

Tactic:
refine fun P _ _ Q ↦ .of_comp (f := lTensor P i) ?_

Result:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f :
  ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x✝¹ : AddCommMonoid P
x✝ : Module R P
Q : Submodule R P
⊢ Function.Injective (⇑(lTensor P i) ∘ ⇑(rTensor N Q.subtype))

Proof state:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f :
  ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x✝¹ : AddCommMonoid P
x✝ : Module R P
Q : Submodule R P
⊢ Function.Injective (⇑(lTensor P i) ∘ ⇑(rTensor N Q.subtype))

Tactic:
rw [← coe_comp, lTensor_comp_rTensor, ← rTensor_comp_lTensor, coe_comp]

Result:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f :
  ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x✝¹ : AddCommMonoid P
x✝ : Module R P
Q : Submodule R P
⊢ Function.Injective (⇑(rTensor M Q.subtype) ∘ ⇑(lTensor (↥Q) i))

Proof state:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f :
  ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x✝¹ : AddCommMonoid P
x✝ : Module R P
Q : Submodule R P
x : ↥Q ⊗[R] N
⊢ (lTensor (↥Q) r) ((lTensor (↥Q) i) x) = x

Tactic:
simp [← comp_apply, ← lTensor_comp, h]

Result:
no goals

Proof state:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f :
  ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x✝¹ : AddCommMonoid P
x✝ : Module R P
Q : Submodule R P
⊢ Function.Injective (⇑(rTensor M Q.subtype) ∘ ⇑(lTensor (↥Q) i))

Tactic:
refine (f Q).comp (Function.RightInverse.injective (g := lTensor Q r) fun x ↦ ?_)

Result:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f :
  ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x✝¹ : AddCommMonoid P
x✝ : Module R P
Q : Submodule R P
x : ↥Q ⊗[R] N
⊢ (lTensor (↥Q) r) ((lTensor (↥Q) i) x) = x

Proof state:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : Flat R M
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
⊢ Flat R N

Tactic:
rw [iff_rTensor_injectiveₛ] at *

Result:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f :
  ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
⊢ ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N_1 : Submodule R P),
    Function.Injective ⇑(rTensor N N_1.subtype)