-- 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:
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)
y : k ⊗[R] ↥(LinearMap.ker l)
⊢ (LinearMap.lTensor k l) ((LinearMap.lTensor k (LinearMap.ker l).subtype) y) =
    (LinearMap.lTensor k l) ((LinearMap.lTensor k (LinearMap.ker l).subtype) 0)

Tactic:
rw [map_zero, map_zero, ← LinearMap.comp_apply, ← LinearMap.lTensor_comp,
  l.exact_subtype_ker_map.linearMap_comp_eq_zero, LinearMap.lTensor_zero,
  LinearMap.zero_apply]

Result:
no goals

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

Tactic:
have : Subsingleton (k ⊗[R] LinearMap.ker l) := by
  refine (subsingleton_iff_forall_eq 0).mpr fun y ↦ H (h ?_)
  rw [map_zero, map_zero, ← LinearMap.comp_apply, ← LinearMap.lTensor_comp,
    l.exact_subtype_ker_map.linearMap_comp_eq_zero, LinearMap.lTensor_zero,
    LinearMap.zero_apply]

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

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

Tactic:
have : Module.Finite R (LinearMap.ker l) := by
  refine Module.Finite.of_surjective l' ?_
  exact Function.HasRightInverse.surjective ⟨_, DFunLike.congr_fun hl'⟩

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)
⊢ ∃ 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 ⋯)
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

Tactic:
exact this.mp (Module.projective_lifting_property _ _ (fun ⟨x, y, e⟩ ↦ ⟨y, Subtype.ext e⟩))

Result:
no goals

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)
H : Injective ⇑(LinearMap.lTensor k (LinearMap.ker l).subtype)
⊢ Subsingleton (k ⊗[R] ↥(LinearMap.ker l))

Tactic:
refine (subsingleton_iff_forall_eq 0).mpr fun y ↦ H (h ?_)

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)
hl' : l' ∘ₗ (LinearMap.ker l).subtype = LinearMap.id
this : Module.Finite R ↥(LinearMap.ker l)
H : Injective ⇑(LinearMap.lTensor k (LinearMap.ker l).subtype)
y : k ⊗[R] ↥(LinearMap.ker l)
⊢ (LinearMap.lTensor k l) ((LinearMap.lTensor k (LinearMap.ker l).subtype) y) =
    (LinearMap.lTensor k l) ((LinearMap.lTensor k (LinearMap.ker l).subtype) 0)

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

Tactic:
exact Function.HasLeftInverse.injective ⟨l'.lTensor k, DFunLike.congr_fun hl'⟩

Result:
no goals