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

Tactic:
(subsingleton_iff_forall_eq 0).mpr fun y ↦ H (h ?_)

Premises used: Iff.mpr, subsingleton_iff_forall_eq, OfNat.ofNat
-- 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
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)
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)
⊢ Subsingleton (TensorProduct.{u_1, u_1, u_2} R k ↥l.ker)

Tactic:
refine (subsingleton_iff_forall_eq 0).mpr fun y ↦ H (h ?_)

Premises used: Iff.mpr, subsingleton_iff_forall_eq, OfNat.ofNat
-- 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
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)
rw₆ rw₇ : Eq (α := k ⊗[R] N) 0 0
⊢ 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:
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]

Premises used: LinearMap.zero_apply, LinearMap.comp_apply, map_zero, LinearMap.lTensor_zero, Function.Exact.linearMap_comp_eq_zero, LinearMap.exact_subtype_ker_map, 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
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)

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]
-- 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_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 = ⊥
rwa₁ : Subsingleton.{u_2 + 1} ↥l.ker
rwa₂ rwa₃ rwa₄ rwa₅ : 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)

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

Premises used: Submodule.subsingleton_iff_eq_bot, LinearMap.ker_eq_bot, IsLocalRing.subsingleton_tensorProduct
-- 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_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)

Tactic:
have : Function.Injective l := by
      rwa [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot,
        ← IsLocalRing.subsingleton_tensorProduct (R := R)]
-- 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_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_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
-- 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_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
mpr : ∃ (l_1 : N ⧸ l.range →ₗ[R] N), l.range.mkQ ∘ₗ l_1 = LinearMap.id
⊢ ∃ (l' : N →ₗ[R] M), l' ∘ₗ l = LinearMap.id

Tactic:
rw [← this]
-- 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_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_1 : N ⧸ l.range →ₗ[R] N), l.range.mkQ ∘ₗ l_1 = LinearMap.id

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

Premises used: 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_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_1 : N ⧸ l.range →ₗ[R] N), l.range.mkQ ∘ₗ l_1 = LinearMap.id

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

Premises used: Module.projective_lifting_property, Submodule.mkQ_surjective
-- Module: Mathlib.RingTheory.LocalRing.Module
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
have :
  ∀ (b' : (P : MaximalSpectrum R) → Basis (Fin n) (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M)),
    Nonempty (Basis (Fin n) R M)
⊢ Nonempty (Basis (Fin n) R M)

Tactic:
have b' (P) := Module.finBasisOfFinrankEq _ _ (rk P)
-- Module: Mathlib.RingTheory.LocalRing.Module
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)
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)
⊢ 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)

Premises used: MaximalSpectrum.asIdeal, Ideal.pi_tensorProductMk_quotient_surjective, Iff.ne, Iff.mp, MaximalSpectrum.ext_iff, DFunLike.coe, Ideal.isCoprime_of_isMaximal
-- Module: Mathlib.RingTheory.LocalRing.Module
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)

Tactic:
⟨⟨.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 _ ↦ ?_⟩⟩

Premises used: Module.Basis.ofRepr, LinearEquiv.symm, Nonempty.intro, bijective_of_isLocalized_maximal, Finsupp.mapRange.linearMap, Finsupp.linearCombination, LinearEquiv.ofBijective
-- Module: Mathlib.RingTheory.LocalRing.Module
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)
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)
⊢ Nonempty (Basis (Fin n) 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 _ ↦ ?_⟩⟩
-- Module: Mathlib.RingTheory.LocalRing.Module
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)
P : Ideal R
h : P.IsMaximal
rw :
  Function.Bijective (α := Fin n →₀ Localization (M := R) P.primeCompl) (β := Localization (M := R) P.primeCompl ⊗[R] M)
    (⇑(Finsupp.linearCombination (Localization (M := R) P.primeCompl)
          ((⇑((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 h) :
              (a : M) → Localization P.primeCompl ⊗[R] M) ∘
            b)) :
      (a : Fin n →₀ Localization P.primeCompl) → Localization P.primeCompl ⊗[R] M)
⊢ 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 h)
                ((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 h) :
              (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:
rw [IsLocalizedModule.map_linearCombination, LinearMap.coe_restrictScalars]

Premises used: LinearMap.coe_restrictScalars, IsLocalizedModule.map_linearCombination