-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ_1 : Type u_5
inst_9 : CommSemiring Sₚ_1
inst_10 : Algebra S_1 Sₚ_1
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ_1
inst_12 : Algebra Rₚ_1 Sₚ_1
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
Sₚ : Type u_9
inst_19 : CommRing S
inst_20 : Algebra R S
inst_21 : CommRing Sₚ
inst_22 : Algebra S Sₚ
inst_23 : Algebra R Sₚ
inst_24 : Algebra Rₚ Sₚ
inst_25 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_26 : IsScalarTower R S Sₚ
inst_27 : IsScalarTower R Rₚ Sₚ
h :
  Eq.{u_9 + 1} (α := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))
    (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p))
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S : (a : R) → S) α = (↑s : S)
β γ : R
hγ : γ ∈ p
hβ : α * β = 1 + γ
h₁ :
  HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
      (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ) (mk' Sₚ x s)) =
    (algebraMap S Sₚ : (a : S) → Sₚ) (γ • x)
h₂ :
  HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ) -
      HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) (mk' Sₚ x s) =
    (algebraMap S Sₚ : (a : S) → Sₚ) (γ • x)
h₃ :
  HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ) -
      mk' Sₚ ((↑s : S) * x) s =
    (algebraMap S Sₚ : (a : S) → Sₚ) (γ • x)
h₄ :
  HSub.hSub (β := Sₚ)
      (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ))
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ) =
    (algebraMap S Sₚ : (a : S) → Sₚ) (γ • x)
h₅ :
  HSub.hSub (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) ((↑s : S) * β • x) : Sₚ)
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ) =
    (algebraMap S Sₚ : (a : S) → Sₚ) (γ • x)
h₆ :
  HSub.hSub (α := Sₚ) (β := Sₚ)
      ((algebraMap S Sₚ : (a : S) → Sₚ) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) α : S) (β • x)) : Sₚ)
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ) =
    (algebraMap S Sₚ : (a : S) → Sₚ) (γ • x)
h₇ :
  HSub.hSub (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (α • β • x) : Sₚ)
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ) =
    (algebraMap S Sₚ : (a : S) → Sₚ) (γ • x)
⊢ HMul.hMul (β := Sₚ) (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ) (mk' Sₚ x s))
      ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) =
    (algebraMap S Sₚ : (a : S) → Sₚ) (γ • x)
have h₈ : HSub.hSub (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) ((α * β) • x) : Sₚ)
    ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ) =
  (algebraMap S Sₚ : (a : S) → Sₚ) (γ • x)
Tactic: rw [mul_comm, mul_sub, IsLocalization.mul_mk'_eq_mk'_of_mul,
      IsLocalization.mk'_mul_cancel_left, ← map_mul, ← e, ← Algebra.smul_def, smul_smul,
      hβ, ← map_sub, add_smul, one_smul, add_comm x, add_sub_cancel_right]