-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) p
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule.{u_1, u_2} p.asIdeal.primeCompl (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
Mₚ'' : Type (max u_1 u_2) :=
  Mₚ ⧸ HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
rw :
  Submodule.localized' (Localization (M := R) p.asIdeal.primeCompl) p.asIdeal.primeCompl
      (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M) (HSMul.hSMul (β := Submodule R M) I ⊤) =
    HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
rw₁ :
  HSMul.hSMul (α := Submodule (Localization (M := R) p.asIdeal.primeCompl) (Localization (M := R) p.asIdeal.primeCompl))
      (β := Submodule (Localization (M := R) p.asIdeal.primeCompl) (LocalizedModule p.asIdeal.primeCompl M))
      (Submodule.localized' (Localization (M := R) p.asIdeal.primeCompl) p.asIdeal.primeCompl
        (Algebra.linearMap R (Localization (M := R) p.asIdeal.primeCompl)) I)
      (Submodule.localized' (Localization (M := R) p.asIdeal.primeCompl) p.asIdeal.primeCompl
        (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M) ⊤) =
    HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
rw₂ :
  HSMul.hSMul (α := Submodule (Localization (M := R) p.asIdeal.primeCompl) (Localization (M := R) p.asIdeal.primeCompl))
      (β := Submodule (Localization (M := R) p.asIdeal.primeCompl) (LocalizedModule p.asIdeal.primeCompl M))
      (Ideal.map (F := R →+* Localization (M := R) p.asIdeal.primeCompl)
        (algebraMap R (Localization (M := R) p.asIdeal.primeCompl)) I)
      (Submodule.localized' (Localization (M := R) p.asIdeal.primeCompl) p.asIdeal.primeCompl
        (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M) ⊤) =
    HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
rw₃ rw₄ :
  HSMul.hSMul (α := Submodule (Localization (M := R) p.asIdeal.primeCompl) (Localization (M := R) p.asIdeal.primeCompl))
      (β := Submodule (Localization (M := R) p.asIdeal.primeCompl) (LocalizedModule p.asIdeal.primeCompl M))
      (Ideal.map (F := R →+* Localization (M := R) p.asIdeal.primeCompl)
        (algebraMap R (Localization (M := R) p.asIdeal.primeCompl)) I)
      ⊤ =
    HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
⊢ Submodule.localized p.asIdeal.primeCompl (HSMul.hSMul (β := Submodule R M) I ⊤) =
    HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤

Tactic:
rw [Submodule.localized,
        Submodule.localized'_smul, Ideal.localized'_eq_map, Submodule.localized'_top]

Premises used: Submodule.localized'_top, Ideal.localized'_eq_map, Submodule.localized, Submodule.localized'_smul