-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
h₂ : ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P
h :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) (mk' Sₚ x s))
h₃ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      mk' Sₚ ((↑s : S) * x) s)
h₄ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (β := Sₚ)
      (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ))
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ))
h₅ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) ((↑s : S) * (x * s')) : Sₚ)
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ))
h₆ :
  Membership.mem.{u_4, u_4} (α := Sₚ) (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    ((algebraMap S Sₚ : (a : S) → Sₚ) ((↑s : S) * (x * s') - x) : Sₚ)
h₇ :
  Membership.mem (γ := Ideal S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) ((↑s : S) * (x * s') - x)
h₈ : (↑s : S) * (x * s') - x ∈ P
h₉ :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) ((↑s : S) * (x * s')) : S ⧸ P)
    ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x : S ⧸ P)
h₁₀ :
  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) (x * s') : S ⧸ P) =
    (Ideal.Quotient.mk P : (a : S) → S ⧸ P) x
h₁₁ :
  HMul.hMul (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : 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 ⧸ P)) =
    (Ideal.Quotient.mk P : (a : S) → S ⧸ P) x
h₁₂ :
  HMul.hMul (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : 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)) =
    (Ideal.Quotient.mk P : (a : S) → S ⧸ P) x
h₁₃ :
  HMul.hMul (β := 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))
      ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S) : S ⧸ P) =
    (Ideal.Quotient.mk P : (a : S) → S ⧸ P) x
h₁₄ h₁₅ :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x : S ⧸ P)
    ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x : S ⧸ P)
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
      (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s)))

Tactic:
rw [mul_sub, mul_mk'_eq_mk'_of_mul, mk'_mul_cancel_left, ← map_mul, ← map_sub, ← mem_comap,
    comap_map_eq_self_of_isMaximal _ IsPrime.ne_top', ← Ideal.Quotient.eq, map_mul, map_mul, hs,
    mul_comm, inv_mul_cancel_right₀ (Quotient.eq_zero_iff_mem.not.mpr h₁)]

Premises used: Iff.mpr, map_sub, mul_sub, IsLocalization.mk'_mul_cancel_left, Iff.not, Ideal.Quotient.eq_zero_iff_mem, Ideal.Quotient.eq, map_mul, Ideal.comap_map_eq_self_of_isMaximal, mul_comm, IsLocalization.mul_mk'_eq_mk'_of_mul, Ideal.IsPrime.ne_top', Ideal.mem_comap, inv_mul_cancel_right₀