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

Tactic:
intro ⟨l', hl⟩

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
⊢ Injective ⇑(LinearMap.lTensor k 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))
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

Tactic:
rw [← this]

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_1, (LinearMap.range l).mkQ ∘ₗ l_1 = 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)
H : Injective ⇑(LinearMap.lTensor k (LinearMap.ker l).subtype)
this : Subsingleton (k ⊗[R] ↥(LinearMap.ker l))
⊢ Injective ⇑l

Tactic:
rwa [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot,
  ← IsLocalRing.subsingleton_tensorProduct (R := R)]

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

Tactic:
exact Function.HasRightInverse.surjective ⟨_, DFunLike.congr_fun hl'⟩

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', l' ∘ₗ (LinearMap.ker l).subtype = LinearMap.id

Tactic:
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]

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 ⋯)
⊢ ∃ l', l' ∘ₗ (LinearMap.ker l).subtype = 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
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_1, (LinearMap.range l).mkQ ∘ₗ l_1 = LinearMap.id

Tactic:
exact Module.projective_lifting_property _ _ (Submodule.mkQ_surjective _)

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
l' : N →ₗ[R] M
hl : l' ∘ₗ l = LinearMap.id
⊢ LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k l = LinearMap.id

Tactic:
rw [← LinearMap.lTensor_comp, hl, LinearMap.lTensor_id]

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)
this : Module.Free R (N ⧸ LinearMap.range l)
⊢ ∃ l', l' ∘ₗ l = LinearMap.id

Tactic:
have : Module.Projective R (LinearMap.range l) := by
  have := (Exact.split_tfae (LinearMap.exact_subtype_mkQ (LinearMap.range l))
    Subtype.val_injective (Submodule.mkQ_surjective _)).out 0 1
  obtain ⟨l', hl'⟩ := this.mp
     (Module.projective_lifting_property _ _ (Submodule.mkQ_surjective _))
  exact Module.Projective.of_split _ _ hl'

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)
this : Module.Projective R ↥(LinearMap.range l)
⊢ ∃ l', l' ∘ₗ l = LinearMap.id