-- 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.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

Tactic:
have := (Exact.split_tfae l.exact_map_mkQ_range this (Submodule.mkQ_surjective _)).out 0 1

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
this : (∃ l_1, (LinearMap.range l).mkQ ∘ₗ l_1 = LinearMap.id) ↔ ∃ l_1, l_1 ∘ₗ l = 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)
this✝ : Module.Projective R ↥(LinearMap.range l)
this : Exact ⇑(LinearMap.ker l).subtype ⇑(LinearMap.codRestrict (LinearMap.range l) l ⋯)
⊢ ∃ l', l' ∘ₗ (LinearMap.ker l).subtype = LinearMap.id

Tactic:
have := (Exact.split_tfae this
  Subtype.val_injective (fun ⟨x, y, e⟩ ↦ ⟨y, Subtype.ext e⟩)).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✝¹ : Module.Projective R ↥(LinearMap.range l)
this✝ : Exact ⇑(LinearMap.ker l).subtype ⇑(LinearMap.codRestrict (LinearMap.range l) l ⋯)
this :
  (∃ l_1, LinearMap.codRestrict (LinearMap.range l) l ⋯ ∘ₗ l_1 = LinearMap.id) ↔
    ∃ l_1, l_1 ∘ₗ (LinearMap.ker l).subtype = LinearMap.id
⊢ ∃ l', l' ∘ₗ (LinearMap.ker l).subtype = 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)
hl' : l' ∘ₗ (LinearMap.ker l).subtype = LinearMap.id
this : Module.Finite R ↥(LinearMap.ker l)
⊢ Injective ⇑(LinearMap.lTensor k (LinearMap.ker l).subtype)

Tactic:
apply_fun (LinearMap.lTensor k) 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.ker l).subtype) = LinearMap.lTensor k LinearMap.id
⊢ Injective ⇑(LinearMap.lTensor k (LinearMap.ker l).subtype)

Proof state:
case mp
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
l' : N →ₗ[R] M
hl : l' ∘ₗ l = LinearMap.id
⊢ Injective ⇑(LinearMap.lTensor k l)

Tactic:
have : l'.lTensor (ResidueField R) ∘ₗ l.lTensor (ResidueField R) = .id := by
  rw [← LinearMap.lTensor_comp, hl, LinearMap.lTensor_id]

Result:
case mp
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
l' : N →ₗ[R] M
hl : l' ∘ₗ l = LinearMap.id
this : LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k l = LinearMap.id
⊢ Injective ⇑(LinearMap.lTensor k l)

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
⊢ Injective ⇑(LinearMap.lTensor k l) → ∃ l', l' ∘ₗ l = LinearMap.id

Tactic:
intro h

Result:
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)
⊢ ∃ 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)
⊢ Exact ⇑(LinearMap.ker l).subtype ⇑(LinearMap.codRestrict (LinearMap.range l) l ⋯)

Tactic:
rw [LinearMap.exact_iff, LinearMap.ker_rangeRestrict, Submodule.range_subtype]

Result:
no goals

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)
⊢ ∃ l', l' ∘ₗ l = LinearMap.id

Tactic:
have := Module.free_of_lTensor_residueField_injective l (LinearMap.range l).mkQ
  (Submodule.mkQ_surjective _) l.exact_map_mkQ_range h

Result:
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)
⊢ ∃ l', l' ∘ₗ l = LinearMap.id