Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : 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 : Fin n → M
hb : ∀ (i : Fin n), (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ i.asIdeal) M) 1) (b i) = fun x ↦ (b' x) i
P : Ideal R
x✝ : P.IsMaximal
r : Fin n →₀ IsLocalRing.ResidueField (Localization P.primeCompl)
⊢ ∀ (f g : Fin n →₀ IsLocalRing.ResidueField (Localization P.primeCompl)),
    (⇑(AlgebraTensorModule.cancelBaseChange R (R ⧸ P) P.ResidueField
                      (IsLocalRing.ResidueField (Localization P.primeCompl)) M).symm.toAddEquiv.toEquiv ∘
            ⇑(AlgebraTensorModule.cancelBaseChange R (Localization P.primeCompl) P.ResidueField
                      (IsLocalRing.ResidueField (Localization P.primeCompl)) M).toAddEquiv.toEquiv ∘
              ⇑(Finsupp.linearCombination (IsLocalRing.ResidueField (Localization P.primeCompl))
                  (⇑((TensorProduct.mk (Localization P.primeCompl)
                          (IsLocalRing.ResidueField (Localization P.primeCompl)) (Localization P.primeCompl ⊗[R] M))
                        1) ∘
                    ⇑((TensorProduct.mk R (Localization P.primeCompl) M) 1) ∘ b)))
          f =
        (LinearEquiv.lTensor P.ResidueField (b' { asIdeal := P, isMaximal := x✝ }).repr ≪≫ₗ
              finsuppScalarRight (R ⧸ { asIdeal := P, isMaximal := x✝ }.asIdeal)
                (R ⧸ { asIdeal := P, isMaximal := x✝ }.asIdeal) P.ResidueField (Fin n)).symm
          f →
      (⇑(AlgebraTensorModule.cancelBaseChange R (R ⧸ P) P.ResidueField
                        (IsLocalRing.ResidueField (Localization P.primeCompl)) M).symm.toAddEquiv.toEquiv ∘
              ⇑(AlgebraTensorModule.cancelBaseChange R (Localization P.primeCompl) P.ResidueField
                        (IsLocalRing.ResidueField (Localization P.primeCompl)) M).toAddEquiv.toEquiv ∘
                ⇑(Finsupp.linearCombination (IsLocalRing.ResidueField (Localization P.primeCompl))
                    (⇑((TensorProduct.mk (Localization P.primeCompl)
                            (IsLocalRing.ResidueField (Localization P.primeCompl)) (Localization P.primeCompl ⊗[R] M))
                          1) ∘
                      ⇑((TensorProduct.mk R (Localization P.primeCompl) M) 1) ∘ b)))
            g =
          (LinearEquiv.lTensor P.ResidueField (b' { asIdeal := P, isMaximal := x✝ }).repr ≪≫ₗ
                finsuppScalarRight (R ⧸ { asIdeal := P, isMaximal := x✝ }.asIdeal)
                  (R ⧸ { asIdeal := P, isMaximal := x✝ }.asIdeal) P.ResidueField (Fin n)).symm
            g →
        (⇑(AlgebraTensorModule.cancelBaseChange R (R ⧸ P) P.ResidueField
                        (IsLocalRing.ResidueField (Localization P.primeCompl)) M).symm.toAddEquiv.toEquiv ∘
              ⇑(AlgebraTensorModule.cancelBaseChange R (Localization P.primeCompl) P.ResidueField
                        (IsLocalRing.ResidueField (Localization P.primeCompl)) M).toAddEquiv.toEquiv ∘
                ⇑(Finsupp.linearCombination (IsLocalRing.ResidueField (Localization P.primeCompl))
                    (⇑((TensorProduct.mk (Localization P.primeCompl)
                            (IsLocalRing.ResidueField (Localization P.primeCompl)) (Localization P.primeCompl ⊗[R] M))
                          1) ∘
                      ⇑((TensorProduct.mk R (Localization P.primeCompl) M) 1) ∘ b)))
            (f + g) =
          (LinearEquiv.lTensor P.ResidueField (b' { asIdeal := P, isMaximal := x✝ }).repr ≪≫ₗ
                finsuppScalarRight (R ⧸ { asIdeal := P, isMaximal := x✝ }.asIdeal)
                  (R ⧸ { asIdeal := P, isMaximal := x✝ }.asIdeal) P.ResidueField (Fin n)).symm
            (f + g)

Tactic:
by simp +contextual

Goal state after: