-- 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
r : Fin n →₀ IsLocalRing.ResidueField (Localization (M := R) P.primeCompl)
⊢ ∀ (f g : Fin n →₀ IsLocalRing.ResidueField (Localization (M := R) P.primeCompl)),
    Eq (α := IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R ⧸ P] ((R ⧸ P) ⊗[R] M))
        (Function.comp (β := IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R] M)
            (⇑(AddEquiv.toEquiv
                  (LinearEquiv.toAddEquiv
                    (LinearEquiv.symm
                        (AlgebraTensorModule.cancelBaseChange R (R ⧸ P) P.ResidueField
                          (IsLocalRing.ResidueField (Localization (M := R) P.primeCompl)) M) :
                      IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R] M ≃ₗ[P.ResidueField]
                        IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R ⧸ P] ((R ⧸ P) ⊗[R] M)))) :
              (a : IsLocalRing.ResidueField (Localization P.primeCompl) ⊗[R] M) →
                IsLocalRing.ResidueField (Localization P.primeCompl) ⊗[R ⧸ P] ((R ⧸ P) ⊗[R] M))
            (Function.comp (β :=
              IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[Localization (M := R) P.primeCompl]
                (Localization (M := R) P.primeCompl ⊗[R] M))
              (⇑(AddEquiv.toEquiv
                    (LinearEquiv.toAddEquiv
                      (AlgebraTensorModule.cancelBaseChange R (Localization (M := R) P.primeCompl) P.ResidueField
                          (IsLocalRing.ResidueField (Localization (M := R) P.primeCompl)) M :
                        IsLocalRing.ResidueField
                              (Localization (M := R) P.primeCompl) ⊗[Localization (M := R) P.primeCompl]
                            (Localization (M := R) P.primeCompl ⊗[R] M) ≃ₗ[P.ResidueField]
                          IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R] M))) :
                (a :
                    IsLocalRing.ResidueField (Localization P.primeCompl) ⊗[Localization P.primeCompl]
                      (Localization P.primeCompl ⊗[R] M)) →
                  IsLocalRing.ResidueField (Localization 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) :
                          (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)))
            f :
          IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R ⧸ P] ((R ⧸ P) ⊗[R] M))
        ((LinearEquiv.symm
                (LinearEquiv.lTensor P.ResidueField
                    (Basis.repr (b' { asIdeal := P, isMaximal := h : MaximalSpectrum R })) ≪≫ₗ
                  finsuppScalarRight (R ⧸ { asIdeal := P, isMaximal := h : MaximalSpectrum R }.asIdeal)
                    (R ⧸ { asIdeal := P, isMaximal := h : MaximalSpectrum R }.asIdeal) P.ResidueField (Fin n)) :
              (a : Fin n →₀ P.ResidueField) →
                P.ResidueField ⊗[R ⧸ { asIdeal := P, isMaximal := h }.asIdeal]
                  ((R ⧸ { asIdeal := P, isMaximal := h }.asIdeal) ⊗[R] M))
            f :
          P.ResidueField ⊗[R ⧸ { asIdeal := P, isMaximal := h : MaximalSpectrum R }.asIdeal]
            ((R ⧸ { asIdeal := P, isMaximal := h : MaximalSpectrum R }.asIdeal) ⊗[R] M)) →
      Eq (α := IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R ⧸ P] ((R ⧸ P) ⊗[R] M))
          (Function.comp (β := IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R] M)
              (⇑(AddEquiv.toEquiv
                    (LinearEquiv.toAddEquiv
                      (LinearEquiv.symm
                          (AlgebraTensorModule.cancelBaseChange R (R ⧸ P) P.ResidueField
                            (IsLocalRing.ResidueField (Localization (M := R) P.primeCompl)) M) :
                        IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R] M ≃ₗ[P.ResidueField]
                          IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R ⧸ P] ((R ⧸ P) ⊗[R] M)))) :
                (a : IsLocalRing.ResidueField (Localization P.primeCompl) ⊗[R] M) →
                  IsLocalRing.ResidueField (Localization P.primeCompl) ⊗[R ⧸ P] ((R ⧸ P) ⊗[R] M))
              (Function.comp (β :=
                IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[Localization (M := R) P.primeCompl]
                  (Localization (M := R) P.primeCompl ⊗[R] M))
                (⇑(AddEquiv.toEquiv
                      (LinearEquiv.toAddEquiv
                        (AlgebraTensorModule.cancelBaseChange R (Localization (M := R) P.primeCompl) P.ResidueField
                            (IsLocalRing.ResidueField (Localization (M := R) P.primeCompl)) M :
                          IsLocalRing.ResidueField
                                (Localization (M := R) P.primeCompl) ⊗[Localization (M := R) P.primeCompl]
                              (Localization (M := R) P.primeCompl ⊗[R] M) ≃ₗ[P.ResidueField]
                            IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R] M))) :
                  (a :
                      IsLocalRing.ResidueField (Localization P.primeCompl) ⊗[Localization P.primeCompl]
                        (Localization P.primeCompl ⊗[R] M)) →
                    IsLocalRing.ResidueField (Localization 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) :
                            (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)))
              g :
            IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R ⧸ P] ((R ⧸ P) ⊗[R] M))
          ((LinearEquiv.symm
                  (LinearEquiv.lTensor P.ResidueField
                      (Basis.repr (b' { asIdeal := P, isMaximal := h : MaximalSpectrum R })) ≪≫ₗ
                    finsuppScalarRight (R ⧸ { asIdeal := P, isMaximal := h : MaximalSpectrum R }.asIdeal)
                      (R ⧸ { asIdeal := P, isMaximal := h : MaximalSpectrum R }.asIdeal) P.ResidueField (Fin n)) :
                (a : Fin n →₀ P.ResidueField) →
                  P.ResidueField ⊗[R ⧸ { asIdeal := P, isMaximal := h }.asIdeal]
                    ((R ⧸ { asIdeal := P, isMaximal := h }.asIdeal) ⊗[R] M))
              g :
            P.ResidueField ⊗[R ⧸ { asIdeal := P, isMaximal := h : MaximalSpectrum R }.asIdeal]
              ((R ⧸ { asIdeal := P, isMaximal := h : MaximalSpectrum R }.asIdeal) ⊗[R] M)) →
        Eq (α := IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R ⧸ P] ((R ⧸ P) ⊗[R] M))
          (Function.comp (β := IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R] M)
              (⇑(AddEquiv.toEquiv
                    (LinearEquiv.toAddEquiv
                      (LinearEquiv.symm
                          (AlgebraTensorModule.cancelBaseChange R (R ⧸ P) P.ResidueField
                            (IsLocalRing.ResidueField (Localization (M := R) P.primeCompl)) M) :
                        IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R] M ≃ₗ[P.ResidueField]
                          IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R ⧸ P] ((R ⧸ P) ⊗[R] M)))) :
                (a : IsLocalRing.ResidueField (Localization P.primeCompl) ⊗[R] M) →
                  IsLocalRing.ResidueField (Localization P.primeCompl) ⊗[R ⧸ P] ((R ⧸ P) ⊗[R] M))
              (Function.comp (β :=
                IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[Localization (M := R) P.primeCompl]
                  (Localization (M := R) P.primeCompl ⊗[R] M))
                (⇑(AddEquiv.toEquiv
                      (LinearEquiv.toAddEquiv
                        (AlgebraTensorModule.cancelBaseChange R (Localization (M := R) P.primeCompl) P.ResidueField
                            (IsLocalRing.ResidueField (Localization (M := R) P.primeCompl)) M :
                          IsLocalRing.ResidueField
                                (Localization (M := R) P.primeCompl) ⊗[Localization (M := R) P.primeCompl]
                              (Localization (M := R) P.primeCompl ⊗[R] M) ≃ₗ[P.ResidueField]
                            IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R] M))) :
                  (a :
                      IsLocalRing.ResidueField (Localization P.primeCompl) ⊗[Localization P.primeCompl]
                        (Localization P.primeCompl ⊗[R] M)) →
                    IsLocalRing.ResidueField (Localization 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) :
                            (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)))
              (f + g) :
            IsLocalRing.ResidueField (Localization (M := R) P.primeCompl) ⊗[R ⧸ P] ((R ⧸ P) ⊗[R] M))
          ((LinearEquiv.symm
                  (LinearEquiv.lTensor P.ResidueField
                      (Basis.repr (b' { asIdeal := P, isMaximal := h : MaximalSpectrum R })) ≪≫ₗ
                    finsuppScalarRight (R ⧸ { asIdeal := P, isMaximal := h : MaximalSpectrum R }.asIdeal)
                      (R ⧸ { asIdeal := P, isMaximal := h : MaximalSpectrum R }.asIdeal) P.ResidueField (Fin n)) :
                (a : Fin n →₀ P.ResidueField) →
                  P.ResidueField ⊗[R ⧸ { asIdeal := P, isMaximal := h }.asIdeal]
                    ((R ⧸ { asIdeal := P, isMaximal := h }.asIdeal) ⊗[R] M))
              (f + g) :
            P.ResidueField ⊗[R ⧸ { asIdeal := P, isMaximal := h : MaximalSpectrum R }.asIdeal]
              ((R ⧸ { asIdeal := P, isMaximal := h : MaximalSpectrum R }.asIdeal) ⊗[R] M))

Tactic:
simp +contextual