-- 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
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
hp : p ≠ ⊥
Q Q' : (↑(p.primesOver S) : Type u_2)
⊢ LE.le.{u_4} (α := (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4))
      (({
              toFun := fun (P : (↑(p.primesOver S) : Type u_2)) ↦
                Subtype.mk (p := fun (x : Ideal Sₚ) ↦
                  Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) x)
                  (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) ⋯,
              invFun := fun (Q : (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)) ↦
                Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x)
                  (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (↑Q : Ideal Sₚ)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
          Q :
        (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4))
      (({
              toFun := fun (P : (↑(p.primesOver S) : Type u_2)) ↦
                Subtype.mk (p := fun (x : Ideal Sₚ) ↦
                  Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) x)
                  (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) ⋯,
              invFun := fun (Q : (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)) ↦
                Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x)
                  (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (↑Q : Ideal Sₚ)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
          Q' :
        (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)) ↔
    Q ≤ Q'
have refine : ∀
  (h :
    LE.le.{u_4} (α := (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4))
      (({
              toFun := fun (P : (↑(p.primesOver S) : Type u_2)) ↦
                Subtype.mk (p := fun (x : Ideal Sₚ) ↦
                  Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) x)
                  (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) sorry,
              invFun := fun (Q : (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)) ↦
                Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x)
                  (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (↑Q : Ideal Sₚ)) sorry,
              left_inv := sorry, right_inv := sorry } :
            (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
          Q :
        (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4))
      (({
              toFun := fun (P : (↑(p.primesOver S) : Type u_2)) ↦
                Subtype.mk (p := fun (x : Ideal Sₚ) ↦
                  Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) x)
                  (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) sorry,
              invFun := fun (Q : (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)) ↦
                Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x)
                  (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (↑Q : Ideal Sₚ)) sorry,
              left_inv := sorry, right_inv := sorry } :
            (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
          Q' :
        (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4))),
  Q ≤ Q'
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ map_mono h⟩