-- Mathlib/RingTheory/LocalRing/Module.lean
theorem IsLocalRing.split_injective_iff_lTensor_residueField_injective [IsLocalRing R]
    [Module.Finite R M] [Module.Finite R N] [Module.Free R N] (l : M →ₗ[R] N) :
    (∃ l', l' ∘ₗ l = LinearMap.id) ↔ Function.Injective (l.lTensor (ResidueField R))

Proof state:
case mpr
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Module.Free R N
l : M →ₗ[R] N
h : Injective ⇑(LinearMap.lTensor k l)
this✝ : Module.Free R (N ⧸ LinearMap.range l)
this : Module.Projective R ↥(LinearMap.range l)
⊢ ∃ l', l' ∘ₗ l = LinearMap.id

Tactic:
obtain ⟨l', hl'⟩ : ∃ l', l' ∘ₗ (LinearMap.ker l).subtype = LinearMap.id := by
  have : Function.Exact (LinearMap.ker l).subtype
      (l.codRestrict (LinearMap.range l) (LinearMap.mem_range_self l)) := by
    rw [LinearMap.exact_iff, LinearMap.ker_rangeRestrict, Submodule.range_subtype]
  have := (Exact.split_tfae this
    Subtype.val_injective (fun ⟨x, y, e⟩ ↦ ⟨y, Subtype.ext e⟩)).out 0 1
  exact this.mp (Module.projective_lifting_property _ _ (fun ⟨x, y, e⟩ ↦ ⟨y, Subtype.ext e⟩))

Result:
case mpr.intro
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Module.Free R N
l : M →ₗ[R] N
h : Injective ⇑(LinearMap.lTensor k l)
this✝ : Module.Free R (N ⧸ LinearMap.range l)
this : Module.Projective R ↥(LinearMap.range l)
l' : M →ₗ[R] ↥(LinearMap.ker l)
hl' : l' ∘ₗ (LinearMap.ker l).subtype = LinearMap.id
⊢ ∃ l', l' ∘ₗ l = LinearMap.id

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Module.Free R N
l : M →ₗ[R] N
h : Injective ⇑(LinearMap.lTensor k l)
this : Module.Free R (N ⧸ LinearMap.range l)
⊢ Module.Projective R ↥(LinearMap.range l)

Tactic:
have := (Exact.split_tfae (LinearMap.exact_subtype_mkQ (LinearMap.range l))
  Subtype.val_injective (Submodule.mkQ_surjective _)).out 0 1

Result:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Module.Free R N
l : M →ₗ[R] N
h : Injective ⇑(LinearMap.lTensor k l)
this✝ : Module.Free R (N ⧸ LinearMap.range l)
this : (∃ l_1, (LinearMap.range l).mkQ ∘ₗ l_1 = LinearMap.id) ↔ ∃ l_1, l_1 ∘ₗ (LinearMap.range l).subtype = LinearMap.id
⊢ Module.Projective R ↥(LinearMap.range l)

Proof state:
case mpr.intro
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Module.Free R N
l : M →ₗ[R] N
h : Injective ⇑(LinearMap.lTensor k l)
this✝² : Module.Free R (N ⧸ LinearMap.range l)
this✝¹ : Module.Projective R ↥(LinearMap.range l)
l' : M →ₗ[R] ↥(LinearMap.ker l)
hl' : l' ∘ₗ (LinearMap.ker l).subtype = LinearMap.id
this✝ : Module.Finite R ↥(LinearMap.ker l)
H : Injective ⇑(LinearMap.lTensor k (LinearMap.ker l).subtype)
this : Subsingleton (k ⊗[R] ↥(LinearMap.ker l))
⊢ ∃ l', l' ∘ₗ l = LinearMap.id

Tactic:
have : Function.Injective l := by
  rwa [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot,
    ← IsLocalRing.subsingleton_tensorProduct (R := R)]

Result:
case mpr.intro
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Module.Free R N
l : M →ₗ[R] N
h : Injective ⇑(LinearMap.lTensor k l)
this✝³ : Module.Free R (N ⧸ LinearMap.range l)
this✝² : Module.Projective R ↥(LinearMap.range l)
l' : M →ₗ[R] ↥(LinearMap.ker l)
hl' : l' ∘ₗ (LinearMap.ker l).subtype = LinearMap.id
this✝¹ : Module.Finite R ↥(LinearMap.ker l)
H : Injective ⇑(LinearMap.lTensor k (LinearMap.ker l).subtype)
this✝ : Subsingleton (k ⊗[R] ↥(LinearMap.ker l))
this : Injective ⇑l
⊢ ∃ l', l' ∘ₗ l = LinearMap.id

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Module.Free R N
l : M →ₗ[R] N
h : Injective ⇑(LinearMap.lTensor k l)
this✝¹ : Module.Free R (N ⧸ LinearMap.range l)
this✝ : Module.Projective R ↥(LinearMap.range l)
l' : M →ₗ[R] ↥(LinearMap.ker l)
this : Module.Finite R ↥(LinearMap.ker l)
hl' : LinearMap.lTensor k (l' ∘ₗ (LinearMap.ker l).subtype) = LinearMap.lTensor k LinearMap.id
⊢ Injective ⇑(LinearMap.lTensor k (LinearMap.ker l).subtype)

Tactic:
rw [LinearMap.lTensor_comp, LinearMap.lTensor_id] at hl'

Result:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Module.Free R N
l : M →ₗ[R] N
h : Injective ⇑(LinearMap.lTensor k l)
this✝¹ : Module.Free R (N ⧸ LinearMap.range l)
this✝ : Module.Projective R ↥(LinearMap.range l)
l' : M →ₗ[R] ↥(LinearMap.ker l)
this : Module.Finite R ↥(LinearMap.ker l)
hl' : LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k (LinearMap.ker l).subtype = LinearMap.id
⊢ Injective ⇑(LinearMap.lTensor k (LinearMap.ker l).subtype)