awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
mp :
  (∃ (l' : N →ₗ[R] M), l' ∘ₗ l = LinearMap.id) →
    Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
mpr :
  Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N) →
    ∃ (l' : N →ₗ[R] M), l' ∘ₗ l = LinearMap.id
⊢ (∃ (l' : N →ₗ[R] M), l' ∘ₗ l = LinearMap.id) ↔
    Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)

Tactic:
constructor
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
l' : N →ₗ[R] M
hl : l' ∘ₗ l = LinearMap.id
rw : Eq (α := k ⊗[R] M →ₗ[R] k ⊗[R] M) (LinearMap.lTensor k (l' ∘ₗ l)) LinearMap.id
rw₁ : Eq (α := k ⊗[R] M →ₗ[R] k ⊗[R] M) (LinearMap.lTensor k LinearMap.id) LinearMap.id
rw₂ rw₃ : Eq (α := k ⊗[R] M →ₗ[R] k ⊗[R] M) LinearMap.id LinearMap.id
⊢ Eq (α := k ⊗[R] M →ₗ[R] k ⊗[R] M) (LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k l) LinearMap.id

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

Premises used: LinearMap.lTensor_id, LinearMap.lTensor_comp
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
l' : N →ₗ[R] M
hl : l' ∘ₗ l = LinearMap.id
⊢ Eq (α := k ⊗[R] M →ₗ[R] k ⊗[R] M) (LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k l) LinearMap.id

Tactic:
have : l'.lTensor (ResidueField R) ∘ₗ l.lTensor (ResidueField R) = .id := by
      rw [← LinearMap.lTensor_comp, hl, LinearMap.lTensor_id]
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
l' : N →ₗ[R] M
hl : l' ∘ₗ l = LinearMap.id
this : Eq (α := k ⊗[R] M →ₗ[R] k ⊗[R] M) (LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k l) LinearMap.id
⊢ Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)

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

Premises used: Function.HasLeftInverse.injective, LinearMap.congr_fun, Exists.intro
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
l' : N →ₗ[R] M
hl : l' ∘ₗ l = LinearMap.id
this : Eq (α := k ⊗[R] M →ₗ[R] k ⊗[R] M) (LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k l) LinearMap.id
⊢ Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)

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

Premises used: Function.HasLeftInverse.injective, LinearMap.congr_fun, Exists.intro
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
⊢ Free.{u_1, u_3} R (N ⧸ l.range)

Tactic:
have := Module.free_of_lTensor_residueField_injective l (LinearMap.range l).mkQ
      (Submodule.mkQ_surjective _) l.exact_map_mkQ_range h
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this : Free.{u_1, u_3} R (N ⧸ l.range)
⊢ (∃ (l_1 : N ⧸ l.range →ₗ[R] N), l.range.mkQ ∘ₗ l_1 = LinearMap.id) ↔
    ∃ (l_1 : N →ₗ[R] ↥l.range), l_1 ∘ₗ l.range.subtype = LinearMap.id

Tactic:
have := (Exact.split_tfae (LinearMap.exact_subtype_mkQ (LinearMap.range l))
        Subtype.val_injective (Submodule.mkQ_surjective _)).out 0 1
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this :
  (∃ (l_1 : N ⧸ l.range →ₗ[R] N), l.range.mkQ ∘ₗ l_1 = LinearMap.id) ↔
    ∃ (l_1 : N →ₗ[R] ↥l.range), l_1 ∘ₗ l.range.subtype = LinearMap.id
obtain : ∀ (l' : N →ₗ[R] ↥l.range) (hl' : l' ∘ₗ l.range.subtype = LinearMap.id), Projective.{u_1, u_3} R ↥l.range
⊢ Projective.{u_1, u_3} R ↥l.range

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

Premises used: Iff.mp, Module.projective_lifting_property, Submodule.mkQ_surjective
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this :
  (∃ (l_1 : N ⧸ l.range →ₗ[R] N), l.range.mkQ ∘ₗ l_1 = LinearMap.id) ↔
    ∃ (l_1 : N →ₗ[R] ↥l.range), l_1 ∘ₗ l.range.subtype = LinearMap.id
l' : N →ₗ[R] ↥l.range
hl' : l' ∘ₗ l.range.subtype = LinearMap.id
⊢ Projective.{u_1, u_3} R ↥l.range

Tactic:
Module.Projective.of_split _ _ hl'

Premises used: Module.Projective.of_split
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this :
  (∃ (l_1 : N ⧸ l.range →ₗ[R] N), l.range.mkQ ∘ₗ l_1 = LinearMap.id) ↔
    ∃ (l_1 : N →ₗ[R] ↥l.range), l_1 ∘ₗ l.range.subtype = LinearMap.id
l' : N →ₗ[R] ↥l.range
hl' : l' ∘ₗ l.range.subtype = LinearMap.id
⊢ Projective.{u_1, u_3} R ↥l.range

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

Premises used: Module.Projective.of_split
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this : Free.{u_1, u_3} R (N ⧸ l.range)
⊢ Projective.{u_1, u_3} R ↥l.range

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'
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this : Projective.{u_1, u_3} R ↥l.range
rw : (LinearMap.codRestrict l.range l ⋯).ker = l.ker.subtype.range
rw₁ : l.ker = l.ker.subtype.range
rw₂ rw₃ : l.ker = l.ker
⊢ Exact.{u_2, u_2, u_3} (M := ↥l.ker) (N := M) (P := ↥l.range) (⇑l.ker.subtype : (a : ↥l.ker) → M)
    (⇑(LinearMap.codRestrict l.range l ⋯) : (a : M) → ↥l.range)

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

Premises used: LinearMap.ker_rangeRestrict, LinearMap.exact_iff, Submodule.range_subtype
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this : Projective.{u_1, u_3} R ↥l.range
⊢ Exact.{u_2, u_2, u_3} (M := ↥l.ker) (N := M) (P := ↥l.range) (⇑l.ker.subtype : (a : ↥l.ker) → M)
    (⇑(LinearMap.codRestrict l.range l ⋯) : (a : M) → ↥l.range)

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]
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this_2 : Projective.{u_1, u_3} R ↥l.range
this :
  Exact.{u_2, u_2, u_3} (M := ↥l.ker) (N := M) (P := ↥l.range) (⇑l.ker.subtype : (a : ↥l.ker) → M)
    (⇑(LinearMap.codRestrict l.range l ⋯) : (a : M) → ↥l.range)
⊢ (∃ (l_1 : LinearMap.{u_1, u_1, u_3, u_2} (RingHom.id R) (↥l.range) M),
      LinearMap.codRestrict l.range l ⋯ ∘ₗ l_1 = LinearMap.id) ↔
    ∃ (l_1 : M →ₗ[R] ↥l.ker), l_1 ∘ₗ l.ker.subtype = LinearMap.id

Tactic:
have := (Exact.split_tfae this
        Subtype.val_injective (fun ⟨x, y, e⟩ ↦ ⟨y, Subtype.ext e⟩)).out 0 1
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this_2 : Projective.{u_1, u_3} R ↥l.range
this_3 :
  Exact.{u_2, u_2, u_3} (M := ↥l.ker) (N := M) (P := ↥l.range) (⇑l.ker.subtype : (a : ↥l.ker) → M)
    (⇑(LinearMap.codRestrict l.range l ⋯) : (a : M) → ↥l.range)
this :
  (∃ (l_1 : LinearMap.{u_1, u_1, u_3, u_2} (RingHom.id R) (↥l.range) M),
      LinearMap.codRestrict l.range l ⋯ ∘ₗ l_1 = LinearMap.id) ↔
    ∃ (l_1 : M →ₗ[R] ↥l.ker), l_1 ∘ₗ l.ker.subtype = LinearMap.id
⊢ ∃ (l' : M →ₗ[R] ↥l.ker), l' ∘ₗ l.ker.subtype = LinearMap.id

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

Premises used: _private.0.IsLocalRing.split_injective_iff_lTensor_residueField_injective.match_2, Exists, LinearMap.range, LinearMap.mem_range_self, Exists.intro, Iff.mp, Module.projective_lifting_property, LinearMap.codRestrict, Eq, DFunLike.coe, Subtype.ext
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this_2 : Projective.{u_1, u_3} R ↥l.range
this_3 :
  Exact.{u_2, u_2, u_3} (M := ↥l.ker) (N := M) (P := ↥l.range) (⇑l.ker.subtype : (a : ↥l.ker) → M)
    (⇑(LinearMap.codRestrict l.range l ⋯) : (a : M) → ↥l.range)
this :
  (∃ (l_1 : LinearMap.{u_1, u_1, u_3, u_2} (RingHom.id R) (↥l.range) M),
      LinearMap.codRestrict l.range l ⋯ ∘ₗ l_1 = LinearMap.id) ↔
    ∃ (l_1 : M →ₗ[R] ↥l.ker), l_1 ∘ₗ l.ker.subtype = LinearMap.id
⊢ ∃ (l' : M →ₗ[R] ↥l.ker), l' ∘ₗ l.ker.subtype = LinearMap.id

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

Premises used: _private.0.IsLocalRing.split_injective_iff_lTensor_residueField_injective.match_2, Exists, LinearMap.range, LinearMap.mem_range_self, Exists.intro, Iff.mp, Module.projective_lifting_property, LinearMap.codRestrict, Eq, DFunLike.coe, Subtype.ext
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this : Projective.{u_1, u_3} R ↥l.range
mpr : ∀ (l' : M →ₗ[R] ↥l.ker) (hl' : l' ∘ₗ l.ker.subtype = LinearMap.id), ∃ (l' : N →ₗ[R] M), l' ∘ₗ l = LinearMap.id
⊢ ∃ (l' : N →ₗ[R] M), 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⟩))

Premises used: LinearMap.id, LinearMap.ker, Submodule.subtype
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this : Projective.{u_1, u_3} R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
⊢ Module.Finite.{u_1, u_2} R ↥l.ker

Tactic:
Module.Finite.of_surjective l' ?_

Premises used: Module.Finite.of_surjective
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this : Projective.{u_1, u_3} R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
refine : Surjective (α := M) (β := ↥l.ker) (⇑l' : (a : M) → ↥l.ker)
⊢ Module.Finite.{u_1, u_2} R ↥l.ker

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

Premises used: Module.Finite.of_surjective
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this : Projective.{u_1, u_3} R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
⊢ Surjective (α := M) (β := ↥l.ker) (⇑l' : (a : M) → ↥l.ker)

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

Premises used: DFunLike.congr_fun, Function.HasRightInverse.surjective, Exists.intro
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this : Projective.{u_1, u_3} R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
⊢ Surjective (α := M) (β := ↥l.ker) (⇑l' : (a : M) → ↥l.ker)

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

Premises used: DFunLike.congr_fun, Function.HasRightInverse.surjective, Exists.intro
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this : Projective.{u_1, u_3} R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
⊢ Module.Finite.{u_1, u_2} R ↥l.ker

Tactic:
have : Module.Finite R (LinearMap.ker l) := by
      refine Module.Finite.of_surjective l' ?_
      exact Function.HasRightInverse.surjective ⟨_, DFunLike.congr_fun hl'⟩
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this_2 : Projective.{u_1, u_3} R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
this : Module.Finite.{u_1, u_2} R ↥l.ker
⊢ Eq (α := TensorProduct.{u_1, u_1, u_2} R k ↥l.ker →ₗ[R] TensorProduct.{u_1, u_1, u_2} R k ↥l.ker)
    (LinearMap.lTensor k (l' ∘ₗ l.ker.subtype)) (LinearMap.lTensor k LinearMap.id)

Tactic:
apply_fun (LinearMap.lTensor k) at hl'
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this_2 : Projective.{u_1, u_3} R ↥l.range
l' : M →ₗ[R] ↥l.ker
this : Module.Finite.{u_1, u_2} R ↥l.ker
hl' :
  Eq (α := TensorProduct.{u_1, u_1, u_2} R k ↥l.ker →ₗ[R] TensorProduct.{u_1, u_1, u_2} R k ↥l.ker)
    (LinearMap.lTensor k (l' ∘ₗ l.ker.subtype)) (LinearMap.lTensor k LinearMap.id)
⊢ Eq (α := TensorProduct.{u_1, u_1, u_2} R k ↥l.ker →ₗ[R] TensorProduct.{u_1, u_1, u_2} R k ↥l.ker)
    (LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k l.ker.subtype) LinearMap.id

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

Premises used: LinearMap.lTensor_id, LinearMap.lTensor_comp
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this_2 : Projective.{u_1, u_3} R ↥l.range
l' : M →ₗ[R] ↥l.ker
this : Module.Finite.{u_1, u_2} R ↥l.ker
hl' :
  Eq (α := TensorProduct.{u_1, u_1, u_2} R k ↥l.ker →ₗ[R] TensorProduct.{u_1, u_1, u_2} R k ↥l.ker)
    (LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k l.ker.subtype) LinearMap.id
⊢ Function.Injective (α := TensorProduct.{u_1, u_1, u_2} R k ↥l.ker) (β := k ⊗[R] M)
    (⇑(LinearMap.lTensor k l.ker.subtype) : (a : k ⊗[R] ↥l.ker) → k ⊗[R] M)

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

Premises used: DFunLike.congr_fun, Function.HasLeftInverse.injective, LinearMap.lTensor, IsLocalRing.ResidueField, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this_2 : Projective.{u_1, u_3} R ↥l.range
l' : M →ₗ[R] ↥l.ker
this : Module.Finite.{u_1, u_2} R ↥l.ker
hl' :
  Eq (α := TensorProduct.{u_1, u_1, u_2} R k ↥l.ker →ₗ[R] TensorProduct.{u_1, u_1, u_2} R k ↥l.ker)
    (LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k l.ker.subtype) LinearMap.id
⊢ Function.Injective (α := TensorProduct.{u_1, u_1, u_2} R k ↥l.ker) (β := k ⊗[R] M)
    (⇑(LinearMap.lTensor k l.ker.subtype) : (a : k ⊗[R] ↥l.ker) → k ⊗[R] M)

Tactic:
exact Function.HasLeftInverse.injective ⟨l'.lTensor k, DFunLike.congr_fun hl'⟩
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsLocalRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
inst_8 : Free R N
l : M →ₗ[R] N
h : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
this_1 : Free.{u_1, u_3} R (N ⧸ l.range)
this_2 : Projective.{u_1, u_3} R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
this : Module.Finite.{u_1, u_2} R ↥l.ker
⊢ Function.Injective (α := TensorProduct.{u_1, u_1, u_2} R k ↥l.ker) (β := k ⊗[R] M)
    (⇑(LinearMap.lTensor k l.ker.subtype) : (a : k ⊗[R] ↥l.ker) → k ⊗[R] M)

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'⟩