awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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), l' ∘ₗ l = LinearMap.id) ↔
    Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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)
⊢ (∃ (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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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
have rw : Eq (α := k ⊗[R] M →ₗ[R] k ⊗[R] M) (LinearMap.lTensor k (l' ∘ₗ l)) LinearMap.id
Tactic: rw [← LinearMap.lTensor_comp, hl, LinearMap.lTensor_id]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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
⊢ Eq (α := k ⊗[R] M →ₗ[R] k ⊗[R] M) (LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k l) LinearMap.id
have rw₁ : Eq (α := k ⊗[R] M →ₗ[R] k ⊗[R] M) (LinearMap.lTensor k LinearMap.id) LinearMap.id
Tactic: rw [← LinearMap.lTensor_comp, hl, LinearMap.lTensor_id]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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
⊢ Eq (α := k ⊗[R] M →ₗ[R] k ⊗[R] M) (LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k l) LinearMap.id
have rw₂ : Eq (α := k ⊗[R] M →ₗ[R] k ⊗[R] M) LinearMap.id LinearMap.id
Tactic: rw [← LinearMap.lTensor_comp, hl, LinearMap.lTensor_id]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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
⊢ Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k l) : (a : k ⊗[R] M) → k ⊗[R] N)
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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)
⊢ ∃ (l' : N →ₗ[R] M), l' ∘ₗ l = LinearMap.id
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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
have 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
Tactic: have := (Exact.split_tfae (LinearMap.exact_subtype_mkQ (LinearMap.range l))
        Subtype.val_injective (Submodule.mkQ_surjective _)).out 0 1
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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
⊢ Projective.{u_1, u_3} R ↥l.range
have obtain : ∀ (l' : N →ₗ[R] ↥l.range) (hl' : l' ∘ₗ l.range.subtype = LinearMap.id), Projective.{u_1, u_3} R ↥l.range
Tactic: obtain ⟨l', hl'⟩ := this.mp
         (Module.projective_lifting_property _ _ (Submodule.mkQ_surjective _))
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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' : N →ₗ[R] M), l' ∘ₗ l = LinearMap.id
have this₁ : 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'
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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)
have rw : (LinearMap.codRestrict l.range l sorry).ker = l.ker.subtype.range
Tactic: rw [LinearMap.exact_iff, LinearMap.ker_rangeRestrict, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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
⊢ 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)
have rw₁ : l.ker = l.ker.subtype.range
Tactic: rw [LinearMap.exact_iff, LinearMap.ker_rangeRestrict, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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
⊢ 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)
have rw₂ : l.ker = l.ker
Tactic: rw [LinearMap.exact_iff, LinearMap.ker_rangeRestrict, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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), l' ∘ₗ l.ker.subtype = LinearMap.id
have 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 sorry) : (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]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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' : M →ₗ[R] ↥l.ker), l' ∘ₗ l.ker.subtype = LinearMap.id
have this₁ : (∃ (l_1 : LinearMap.{u_1, u_1, u_3, u_2} (RingHom.id R) (↥l.range) M),
    LinearMap.codRestrict l.range l sorry ∘ₗ 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
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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' : N →ₗ[R] M), l' ∘ₗ l = LinearMap.id
have mpr : ∀ (l' : M →ₗ[R] ↥l.ker) (hl' : l' ∘ₗ l.ker.subtype = 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⟩))
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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
have refine : Surjective (α := M) (β := ↥l.ker) (⇑l' : (a : M) → ↥l.ker)
Tactic: refine Module.Finite.of_surjective l' ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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
⊢ ∃ (l' : N →ₗ[R] M), l' ∘ₗ l = LinearMap.id
have this₁ : 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'⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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)
have 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)
Tactic: apply_fun (LinearMap.lTensor k) at hl'
Cleared hypotheses: hl'
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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)
⊢ 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)
have 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
Tactic: rw [LinearMap.lTensor_comp, LinearMap.lTensor_id] at hl'
Cleared hypotheses: hl'
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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
⊢ ∃ (l' : N →ₗ[R] M), l' ∘ₗ l = LinearMap.id
have H : 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'⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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
H :
  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)
⊢ Subsingleton (TensorProduct.{u_1, u_1, u_2} R k ↥l.ker)
have refine : ∀ (y : TensorProduct.{u_1, u_1, u_2} R k ↥l.ker),
  Eq (α := k ⊗[R] N)
    ((LinearMap.lTensor k l : (a : k ⊗[R] M) → k ⊗[R] N)
        ((LinearMap.lTensor k l.ker.subtype : (a : k ⊗[R] ↥l.ker) → k ⊗[R] M) y) :
      k ⊗[R] N)
    ((LinearMap.lTensor k l : (a : k ⊗[R] M) → k ⊗[R] N)
        ((LinearMap.lTensor k l.ker.subtype : (a : k ⊗[R] ↥l.ker) → k ⊗[R] M) 0) :
      k ⊗[R] N)
Tactic: refine (subsingleton_iff_forall_eq 0).mpr fun y ↦ H (h ?_)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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
H :
  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)
y : TensorProduct.{u_1, u_1, u_2} R k ↥l.ker
⊢ Eq (α := k ⊗[R] N)
    ((LinearMap.lTensor k l : (a : k ⊗[R] M) → k ⊗[R] N)
        ((LinearMap.lTensor k l.ker.subtype : (a : k ⊗[R] ↥l.ker) → k ⊗[R] M) y) :
      k ⊗[R] N)
    ((LinearMap.lTensor k l : (a : k ⊗[R] M) → k ⊗[R] N)
        ((LinearMap.lTensor k l.ker.subtype : (a : k ⊗[R] ↥l.ker) → k ⊗[R] M) 0) :
      k ⊗[R] N)
have rw : Eq (α := k ⊗[R] N)
  ((LinearMap.lTensor k l : (a : k ⊗[R] M) → k ⊗[R] N)
      ((LinearMap.lTensor k l.ker.subtype : (a : k ⊗[R] ↥l.ker) → k ⊗[R] M) y) :
    k ⊗[R] N)
  ((LinearMap.lTensor k l : (a : k ⊗[R] M) → k ⊗[R] N) 0 : k ⊗[R] N)
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]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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
H :
  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)
y : TensorProduct.{u_1, u_1, u_2} R k ↥l.ker
rw :
  Eq (α := k ⊗[R] N)
    ((LinearMap.lTensor k l : (a : k ⊗[R] M) → k ⊗[R] N)
        ((LinearMap.lTensor k l.ker.subtype : (a : k ⊗[R] ↥l.ker) → k ⊗[R] M) y) :
      k ⊗[R] N)
    ((LinearMap.lTensor k l : (a : k ⊗[R] M) → k ⊗[R] N) 0 : k ⊗[R] N)
⊢ Eq (α := k ⊗[R] N)
    ((LinearMap.lTensor k l : (a : k ⊗[R] M) → k ⊗[R] N)
        ((LinearMap.lTensor k l.ker.subtype : (a : k ⊗[R] ↥l.ker) → k ⊗[R] M) y) :
      k ⊗[R] N)
    ((LinearMap.lTensor k l : (a : k ⊗[R] M) → k ⊗[R] N)
        ((LinearMap.lTensor k l.ker.subtype : (a : k ⊗[R] ↥l.ker) → k ⊗[R] M) 0) :
      k ⊗[R] N)
have rw₁ : Eq (α := k ⊗[R] N)
  ((LinearMap.lTensor k l : (a : k ⊗[R] M) → k ⊗[R] N)
      ((LinearMap.lTensor k l.ker.subtype : (a : k ⊗[R] ↥l.ker) → k ⊗[R] M) y) :
    k ⊗[R] N)
  (0 : k ⊗[R] N)
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]