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
⊢ ⇑(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)) =
    ⇑(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

Tactic:
refine funext fun r ↦ Finsupp.induction_linear r (by simp) (by simp +contextual) fun _ _ ↦ ?_

Goal state after:
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)
x✝¹ : Fin n
x✝ : 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)))
      (Finsupp.single x✝¹ x✝) =
    (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
      (Finsupp.single x✝¹ x✝)