-- 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_1 : P.IsMaximal
h :
  Function.Bijective (α := Fin n →₀ IsLocalRing.ResidueField (Localization (M := R) P.primeCompl)) (β :=
    IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[Localization (M := R) P.primeCompl]
      (Localization (M := R) P.primeCompl ⊗[R] M))
    (⇑(Finsupp.linearCombination (IsLocalRing.ResidueField (Localization (M := R) P.primeCompl))
          (Function.comp (β := Localization (M := R) P.primeCompl ⊗[R] M)
            (⇑((TensorProduct.mk (Localization (M := R) P.primeCompl)
                      (IsLocalRing.ResidueField (Localization (M := R) P.primeCompl))
                      (Localization (M := R) P.primeCompl ⊗[R] M) :
                    (a : IsLocalRing.ResidueField (Localization P.primeCompl)) →
                      Localization P.primeCompl ⊗[R] M →ₗ[Localization P.primeCompl]
                        IsLocalRing.ResidueField (Localization P.primeCompl) ⊗[Localization P.primeCompl]
                          (Localization P.primeCompl ⊗[R] M))
                  1) :
              (a : Localization P.primeCompl ⊗[R] M) →
                IsLocalRing.ResidueField (Localization P.primeCompl) ⊗[Localization P.primeCompl]
                  (Localization P.primeCompl ⊗[R] M))
            ((⇑((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_1) :
                (a : M) → Localization P.primeCompl ⊗[R] M) ∘
              b))) :
      (a : Fin n →₀ IsLocalRing.ResidueField (Localization P.primeCompl)) →
        IsLocalRing.ResidueField (Localization P.primeCompl) ⊗[Localization P.primeCompl]
          (Localization P.primeCompl ⊗[R] M))
⊢ 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_1) :
              (a : M) → Localization P.primeCompl ⊗[R] M) ∘
            b)) :
      (a : Fin n →₀ Localization P.primeCompl) → Localization P.primeCompl ⊗[R] M)

Tactic:
apply IsLocalRing.linearCombination_bijective_of_flat

Premises used: Module.IsLocalRing.linearCombination_bijective_of_flat