-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Rₚ : Type u_8
inst_2 : CommRing Rₚ
inst_3 : Algebra R Rₚ
inst_4 : IsLocalization.AtPrime Rₚ p
inst_5 : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
h₁ : Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R) : R ⧸ p) (0 : R ⧸ p)
h₂ :
  Ne.{u_8 + 1} (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    (((equivQuotMaximalIdeal p Rₚ :
            RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
          (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
        ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R)) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    (0 : HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
rw :
  Eq (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) (mk' Rₚ x s) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ))
    (((equivQuotMaximalIdeal p Rₚ :
            RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
          (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
        (HMul.hMul (α := R ⧸ p) (β := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) x : R ⧸ p)
          (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R))⁻¹ : R ⧸ p)) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
rw₁ :
  HMul.hMul (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (β :=
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) (mk' Rₚ x s) :
        HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ))
      (((equivQuotMaximalIdeal p Rₚ :
              RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
            (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
          ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R)) :
        HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) =
    HMul.hMul (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (β :=
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      (((equivQuotMaximalIdeal p Rₚ :
              RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
            (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
          (HMul.hMul (α := R ⧸ p) (β := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) x : R ⧸ p)
            (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R))⁻¹ : R ⧸ p)) :
        HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      (((equivQuotMaximalIdeal p Rₚ :
              RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
            (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
          ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R)) :
        HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
rw₂ :
  HMul.hMul (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (β :=
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) (mk' Rₚ x s) :
        HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ))
      (((equivQuotMaximalIdeal p Rₚ :
              RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
            (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
          ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R)) :
        HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) =
    HMul.hMul (β := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      (HMul.hMul (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (β :=
        HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
        (((equivQuotMaximalIdeal p Rₚ :
                RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
              (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
            ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) x) :
          HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
        (((equivQuotMaximalIdeal p Rₚ :
                RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
              (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
            ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R))⁻¹ :
          HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
      (((equivQuotMaximalIdeal p Rₚ :
              RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
            (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
          ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R)) :
        HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
⊢ ((RingEquiv.symm (equivQuotMaximalIdeal p Rₚ) :
          RingEquiv.{u_8, u_7} (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (R ⧸ p)) :
        (a : Rₚ ⧸ maximalIdeal Rₚ) → R ⧸ p)
      ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) (mk' Rₚ x s)) =
    HMul.hMul (α := R ⧸ p) (β := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) x : R ⧸ p)
      (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R))⁻¹ : R ⧸ p)
have rw₃ : HMul.hMul (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (β :=
    HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) (mk' Rₚ x s) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ))
    (((equivQuotMaximalIdeal p Rₚ :
            RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
          (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
        ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R)) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) =
  HMul.hMul (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    (((equivQuotMaximalIdeal p Rₚ :
            RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
          (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
        ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) x) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    (HMul.hMul (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (β :=
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      (((equivQuotMaximalIdeal p Rₚ :
              RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
            (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
          ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R))⁻¹ :
        HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      (((equivQuotMaximalIdeal p Rₚ :
              RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
            (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
          ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R)) :
        HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
Tactic: rw [RingEquiv.symm_apply_eq, ← mul_left_inj' h₂, map_mul, mul_assoc, ← map_mul,
    inv_mul_cancel₀ h₁, map_one, mul_one, equivQuotMaximalIdeal_apply_mk, ← map_mul,
    mk'_spec, Ideal.Quotient.mk_algebraMap, equivQuotMaximalIdeal_apply_mk,
    Ideal.Quotient.mk_algebraMap]