-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
this : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : Ne (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S) : S ⧸ P) (0 : S ⧸ P)
h₂ :
  Ne.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    (((equivQuotientMapOfIsMaximal p Sₚ P :
            RingEquiv.{u_2, u_4} (S ⧸ P)
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
          (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S)) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    (0 : HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
rw :
  Eq (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) : (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        (mk' Sₚ x s) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    (((equivQuotientMapOfIsMaximal p Sₚ P :
            RingEquiv.{u_2, u_4} (S ⧸ P)
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
          (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        (HMul.hMul (α := S ⧸ P) (β := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x : S ⧸ P)
          (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
rw₁ :
  HMul.hMul (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) (β :=
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          (mk' Sₚ x s) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      (((equivQuotientMapOfIsMaximal p Sₚ P :
              RingEquiv.{u_2, u_4} (S ⧸ P)
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
            (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S)) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) =
    HMul.hMul (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) (β :=
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      (((equivQuotientMapOfIsMaximal p Sₚ P :
              RingEquiv.{u_2, u_4} (S ⧸ P)
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
            (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          (HMul.hMul (α := S ⧸ P) (β := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x : S ⧸ P)
            (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      (((equivQuotientMapOfIsMaximal p Sₚ P :
              RingEquiv.{u_2, u_4} (S ⧸ P)
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
            (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S)) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
rw₂ :
  HMul.hMul (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) (β :=
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          (mk' Sₚ x s) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      (((equivQuotientMapOfIsMaximal p Sₚ P :
              RingEquiv.{u_2, u_4} (S ⧸ P)
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
            (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S)) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) =
    HMul.hMul (β := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      (HMul.hMul (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) (β :=
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
        (((equivQuotientMapOfIsMaximal p Sₚ P :
                RingEquiv.{u_2, u_4} (S ⧸ P)
                  (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
              (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
            ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x) :
          HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
        (((equivQuotientMapOfIsMaximal p Sₚ P :
                RingEquiv.{u_2, u_4} (S ⧸ P)
                  (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
              (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
            ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ :
          HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
      (((equivQuotientMapOfIsMaximal p Sₚ P :
              RingEquiv.{u_2, u_4} (S ⧸ P)
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
            (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S)) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
rw₃ :
  HMul.hMul (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) (β :=
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          (mk' Sₚ x s) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      (((equivQuotientMapOfIsMaximal p Sₚ P :
              RingEquiv.{u_2, u_4} (S ⧸ P)
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
            (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S)) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) =
    HMul.hMul (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      (((equivQuotientMapOfIsMaximal p Sₚ P :
              RingEquiv.{u_2, u_4} (S ⧸ P)
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
            (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      (HMul.hMul (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) (β :=
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
        (((equivQuotientMapOfIsMaximal p Sₚ P :
                RingEquiv.{u_2, u_4} (S ⧸ P)
                  (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
              (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
            ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ :
          HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
        (((equivQuotientMapOfIsMaximal p Sₚ P :
                RingEquiv.{u_2, u_4} (S ⧸ P)
                  (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
              (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
            ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S)) :
          HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
rw₄ :
  HMul.hMul (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) (β :=
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          (mk' Sₚ x s) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      (((equivQuotientMapOfIsMaximal p Sₚ P :
              RingEquiv.{u_2, u_4} (S ⧸ P)
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
            (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S)) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) =
    HMul.hMul (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) (β :=
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      (((equivQuotientMapOfIsMaximal p Sₚ P :
              RingEquiv.{u_2, u_4} (S ⧸ P)
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
            (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      (((equivQuotientMapOfIsMaximal p Sₚ P :
              RingEquiv.{u_2, u_4} (S ⧸ P)
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
            (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          (HMul.hMul (α := S ⧸ P) (β := S ⧸ P) (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
            ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S) : S ⧸ P)) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
⊢ ((RingEquiv.symm (equivQuotientMapOfIsMaximal p Sₚ P) :
          RingEquiv.{u_4, u_2} (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
            (S ⧸ P)) :
        (a : Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P) → S ⧸ P)
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
          (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        (mk' Sₚ x s)) =
    HMul.hMul (α := S ⧸ P) (β := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x : S ⧸ P)
      (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
have rw₅ : HMul.hMul (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) (β :=
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) : (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        (mk' Sₚ x s) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    (((equivQuotientMapOfIsMaximal p Sₚ P :
            RingEquiv.{u_2, u_4} (S ⧸ P)
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
          (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S)) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) =
  HMul.hMul (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) (β :=
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    (((equivQuotientMapOfIsMaximal p Sₚ P :
            RingEquiv.{u_2, u_4} (S ⧸ P)
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
          (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    (((equivQuotientMapOfIsMaximal p Sₚ P :
            RingEquiv.{u_2, u_4} (S ⧸ P)
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
          (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        1 :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
Tactic: rw [RingEquiv.symm_apply_eq, ← mul_left_inj' h₂, map_mul, mul_assoc, ← map_mul,
    inv_mul_cancel₀ h₁, map_one, mul_one, equivQuotientMapOfIsMaximal_apply_mk,
    ← map_mul, mk'_spec, Quotient.mk_algebraMap, equivQuotientMapOfIsMaximal_apply_mk,
    Quotient.mk_algebraMap]