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

Tactic:
constructor

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

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

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 : (∃ 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)

Tactic:
obtain ⟨l', hl'⟩ := this.mp
   (Module.projective_lifting_property _ _ (Submodule.mkQ_surjective _))

Result:
case 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 : (∃ l_1, (LinearMap.range l).mkQ ∘ₗ l_1 = LinearMap.id) ↔ ∃ l_1, l_1 ∘ₗ (LinearMap.range l).subtype = LinearMap.id
l' : N →ₗ[R] ↥(LinearMap.range l)
hl' : l' ∘ₗ (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)
⊢ ∃ l', l' ∘ₗ l = LinearMap.id

Tactic:
have H : Function.Injective ((LinearMap.ker l).subtype.lTensor k) := by
  apply_fun (LinearMap.lTensor k) at hl'
  rw [LinearMap.lTensor_comp, LinearMap.lTensor_id] at hl'
  exact Function.HasLeftInverse.injective ⟨l'.lTensor k, 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)
H : Injective ⇑(LinearMap.lTensor k (LinearMap.ker l).subtype)
⊢ ∃ l', l' ∘ₗ l = LinearMap.id

Proof state:
case 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 : (∃ l_1, (LinearMap.range l).mkQ ∘ₗ l_1 = LinearMap.id) ↔ ∃ l_1, l_1 ∘ₗ (LinearMap.range l).subtype = LinearMap.id
l' : N →ₗ[R] ↥(LinearMap.range l)
hl' : l' ∘ₗ (LinearMap.range l).subtype = LinearMap.id
⊢ Module.Projective R ↥(LinearMap.range l)

Tactic:
exact Module.Projective.of_split _ _ hl'

Result:
no goals

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

Tactic:
exact Function.HasLeftInverse.injective ⟨_, LinearMap.congr_fun this⟩

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
⊢ Module.Finite R ↥(LinearMap.ker l)

Tactic:
refine Module.Finite.of_surjective l' ?_

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
⊢ Surjective ⇑l'