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
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)
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)
⊢ 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 ∘ₗ LinearMap.lTensor k l.ker.subtype : (a : k ⊗[R] ↥l.ker) → k ⊗[R] N) 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]
-- 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)
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)
rw₂ :
  Eq (α := k ⊗[R] N)
    ((LinearMap.lTensor k l ∘ₗ LinearMap.lTensor k l.ker.subtype : (a : k ⊗[R] ↥l.ker) → k ⊗[R] N) y : 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 ∘ₗ l.ker.subtype) : (a : k ⊗[R] ↥l.ker) → k ⊗[R] N) 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]
-- 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)
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)
rw₂ :
  Eq (α := k ⊗[R] N)
    ((LinearMap.lTensor k l ∘ₗ LinearMap.lTensor k l.ker.subtype : (a : k ⊗[R] ↥l.ker) → k ⊗[R] N) y : k ⊗[R] N)
    (0 : k ⊗[R] N)
rw₃ :
  Eq (α := k ⊗[R] N) ((LinearMap.lTensor k (l ∘ₗ l.ker.subtype) : (a : k ⊗[R] ↥l.ker) → k ⊗[R] N) y : 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 0 : (a : k ⊗[R] ↥l.ker) → k ⊗[R] N) 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]
-- 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)
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)
rw₂ :
  Eq (α := k ⊗[R] N)
    ((LinearMap.lTensor k l ∘ₗ LinearMap.lTensor k l.ker.subtype : (a : k ⊗[R] ↥l.ker) → k ⊗[R] N) y : k ⊗[R] N)
    (0 : k ⊗[R] N)
rw₃ :
  Eq (α := k ⊗[R] N) ((LinearMap.lTensor k (l ∘ₗ l.ker.subtype) : (a : k ⊗[R] ↥l.ker) → k ⊗[R] N) y : k ⊗[R] N)
    (0 : k ⊗[R] N)
rw₄ : Eq (α := k ⊗[R] N) ((LinearMap.lTensor k 0 : (a : k ⊗[R] ↥l.ker) → k ⊗[R] N) y : 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) ((0 : (a : k ⊗[R] ↥l.ker) → k ⊗[R] N) 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]
-- 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)
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)
rw₂ :
  Eq (α := k ⊗[R] N)
    ((LinearMap.lTensor k l ∘ₗ LinearMap.lTensor k l.ker.subtype : (a : k ⊗[R] ↥l.ker) → k ⊗[R] N) y : k ⊗[R] N)
    (0 : k ⊗[R] N)
rw₃ :
  Eq (α := k ⊗[R] N) ((LinearMap.lTensor k (l ∘ₗ l.ker.subtype) : (a : k ⊗[R] ↥l.ker) → k ⊗[R] N) y : k ⊗[R] N)
    (0 : k ⊗[R] N)
rw₄ : Eq (α := k ⊗[R] N) ((LinearMap.lTensor k 0 : (a : k ⊗[R] ↥l.ker) → k ⊗[R] N) y : k ⊗[R] N) (0 : k ⊗[R] N)
rw₅ : Eq (α := k ⊗[R] N) ((0 : (a : k ⊗[R] ↥l.ker) → k ⊗[R] N) y : 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) 0 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]
-- 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
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)
⊢ ∃ (l' : N →ₗ[R] M), l' ∘ₗ l = LinearMap.id
have this₁ : Subsingleton (TensorProduct.{u_1, u_1, u_2} R k ↥l.ker)
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]
-- 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_3 : 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)
this : Subsingleton (TensorProduct.{u_1, u_1, u_2} R k ↥l.ker)
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
have rwa : l.ker = ⊥
Tactic: rwa [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot,
        ← IsLocalRing.subsingleton_tensorProduct (R := R)]
-- 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_3 : 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)
this : Subsingleton (TensorProduct.{u_1, u_1, u_2} R k ↥l.ker)
rwa : l.ker = ⊥
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
have rwa₁ : Subsingleton.{u_2 + 1} ↥l.ker
Tactic: rwa [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot,
        ← IsLocalRing.subsingleton_tensorProduct (R := R)]
-- 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_3 : 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)
this : Subsingleton (TensorProduct.{u_1, u_1, u_2} R k ↥l.ker)
⊢ ∃ (l' : N →ₗ[R] M), l' ∘ₗ l = LinearMap.id
have this₁ : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
Tactic: have : Function.Injective l := by
      rwa [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot,
        ← IsLocalRing.subsingleton_tensorProduct (R := R)]
-- 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_3 : 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)
this_4 : Subsingleton (TensorProduct.{u_1, u_1, u_2} R k ↥l.ker)
this : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
⊢ ∃ (l' : N →ₗ[R] M), l' ∘ₗ l = LinearMap.id
have this₁ : (∃ (l_1 : N ⧸ l.range →ₗ[R] N), l.range.mkQ ∘ₗ l_1 = LinearMap.id) ↔ ∃ (l_1 : N →ₗ[R] M), l_1 ∘ₗ l = LinearMap.id
Tactic: have := (Exact.split_tfae l.exact_map_mkQ_range this (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_2 : Projective.{u_1, u_3} R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
this_3 : 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)
this_4 : Subsingleton (TensorProduct.{u_1, u_1, u_2} R k ↥l.ker)
this_5 : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
this : (∃ (l_1 : N ⧸ l.range →ₗ[R] N), l.range.mkQ ∘ₗ l_1 = LinearMap.id) ↔ ∃ (l_1 : N →ₗ[R] M), l_1 ∘ₗ l = LinearMap.id
⊢ ∃ (l' : N →ₗ[R] M), l' ∘ₗ l = LinearMap.id
have mpr : ∃ (l_1 : N ⧸ l.range →ₗ[R] N), l.range.mkQ ∘ₗ l_1 = LinearMap.id
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
this : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I) := @Quotient.field
⊢ Nonempty (Basis (Fin n) R M)
have have : ∀ (b' : (P : MaximalSpectrum R) → Basis (Fin n) (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M)), Nonempty (Basis (Fin n) R M)
Tactic: have b' (P) := Module.finBasisOfFinrankEq _ _ (rk P)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
this : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I) := @Quotient.field
b' : (P : MaximalSpectrum R) → Basis (Fin n) (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M)
⊢ Nonempty (Basis (Fin n) R M)
have choose : ∀ (b : (i : Fin n) → M)
  (hb :
    ∀ (i : Fin n),
      Eq (α := (i : MaximalSpectrum R) → (R ⧸ i.asIdeal) ⊗[R] M)
        ((LinearMap.pi (φ := fun (i : MaximalSpectrum R) ↦ (R ⧸ i.asIdeal) ⊗[R] M) fun (i : MaximalSpectrum R) ↦
                (TensorProduct.mk R (R ⧸ i.asIdeal) M : (a : R ⧸ i.asIdeal) → M →ₗ[R] (R ⧸ i.asIdeal) ⊗[R] M) 1 :
              (a : M) → (i : MaximalSpectrum R) → (R ⧸ i.asIdeal) ⊗[R] M)
            (b i) :
          (i : MaximalSpectrum R) → (R ⧸ i.asIdeal) ⊗[R] M)
        fun (x : MaximalSpectrum R) ↦ ((b' x : (a : Fin n) → (R ⧸ x.asIdeal) ⊗[R] M) i : (R ⧸ x.asIdeal) ⊗[R] M)),
  Nonempty (Basis (Fin n) R M)
Tactic: choose b hb using fun i ↦ pi_tensorProductMk_quotient_surjective M _
    (fun _ _ ne ↦ isCoprime_of_isMaximal (MaximalSpectrum.ext_iff.ne.mp ne)) (b' · i)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
this : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I) := @Quotient.field
b' : (P : MaximalSpectrum R) → Basis (Fin n) (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M)
b : (i : Fin n) → M
hb :
  ∀ (i : Fin n),
    Eq (α := (i : MaximalSpectrum R) → (R ⧸ i.asIdeal) ⊗[R] M)
      ((LinearMap.pi (φ := fun (i : MaximalSpectrum R) ↦ (R ⧸ i.asIdeal) ⊗[R] M) fun (i : MaximalSpectrum R) ↦
              (TensorProduct.mk R (R ⧸ i.asIdeal) M : (a : R ⧸ i.asIdeal) → M →ₗ[R] (R ⧸ i.asIdeal) ⊗[R] M) 1 :
            (a : M) → (i : MaximalSpectrum R) → (R ⧸ i.asIdeal) ⊗[R] M)
          (b i) :
        (i : MaximalSpectrum R) → (R ⧸ i.asIdeal) ⊗[R] M)
      fun (x : MaximalSpectrum R) ↦ ((b' x : (a : Fin n) → (R ⧸ x.asIdeal) ⊗[R] M) i : (R ⧸ x.asIdeal) ⊗[R] M)
⊢ Nonempty (Basis (Fin n) R M)
have refine : ∀ (P : Ideal R) (x : P.IsMaximal),
  Function.Bijective (α := Fin n →₀ Localization (M := R) P.primeCompl) (β := Localization (M := R) P.primeCompl ⊗[R] M)
    (⇑((IsLocalizedModule.map P.primeCompl
                ((fun (P : Ideal R) (x : P.IsMaximal) ↦
                    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (M := R) P.primeCompl)) :
                      (Fin n →₀ R) →ₗ[R] Fin n →₀ Localization (M := R) P.primeCompl))
                  P x)
                ((fun (P : Ideal R) (x : P.IsMaximal) ↦
                    ((TensorProduct.mk R (Localization (M := R) P.primeCompl) M :
                          (a : Localization P.primeCompl) → M →ₗ[R] Localization P.primeCompl ⊗[R] M)
                        1 :
                      M →ₗ[R] Localization (M := R) P.primeCompl ⊗[R] M))
                  P x) :
              (a : (Fin n →₀ R) →ₗ[R] M) → (Fin n →₀ Localization P.primeCompl) →ₗ[R] Localization P.primeCompl ⊗[R] M)
            (Finsupp.linearCombination R b) :
          (Fin n →₀ Localization (M := R) P.primeCompl) →ₗ[R] Localization (M := R) P.primeCompl ⊗[R] M) :
      (a : Fin n →₀ Localization P.primeCompl) → Localization P.primeCompl ⊗[R] M)
Tactic: refine ⟨⟨.symm <| .ofBijective (Finsupp.linearCombination R b) <| bijective_of_isLocalized_maximal
    _ (fun P _ ↦ Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization P.primeCompl)))
    _ (fun P _ ↦ TensorProduct.mk R (Localization P.primeCompl) M 1) _ fun P _ ↦ ?_⟩⟩