-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I I' : { p : Ideal S // p.IsPrime }
mp :
  LE.le.{u_1} (α := { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
      (({
              toFun := fun (p : { p : Ideal S // p.IsPrime }) ↦
                Subtype.mk (p := fun (p : Ideal R) ↦ p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R))
                  (Ideal.under R (↑p : Ideal S)) ⋯,
              invFun := fun (p : { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) ↦
                Subtype.mk (p := fun (p : Ideal S) ↦ p.IsPrime)
                  (Ideal.map (F := R →+* S) (algebraMap R S) (↑p : Ideal R)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { p : Ideal S // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
          I :
        { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
      (({
              toFun := fun (p : { p : Ideal S // p.IsPrime }) ↦
                Subtype.mk (p := fun (p : Ideal R) ↦ p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R))
                  (Ideal.under R (↑p : Ideal S)) ⋯,
              invFun := fun (p : { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) ↦
                Subtype.mk (p := fun (p : Ideal S) ↦ p.IsPrime)
                  (Ideal.map (F := R →+* S) (algebraMap R S) (↑p : Ideal R)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { p : Ideal S // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
          I' :
        { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) →
    I ≤ I'
⊢ LE.le.{u_1} (α := { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
      (({
              toFun := fun (p : { p : Ideal S // p.IsPrime }) ↦
                Subtype.mk (p := fun (p : Ideal R) ↦ p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R))
                  (Ideal.under R (↑p : Ideal S)) ⋯,
              invFun := fun (p : { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) ↦
                Subtype.mk (p := fun (p : Ideal S) ↦ p.IsPrime)
                  (Ideal.map (F := R →+* S) (algebraMap R S) (↑p : Ideal R)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { p : Ideal S // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
          I :
        { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
      (({
              toFun := fun (p : { p : Ideal S // p.IsPrime }) ↦
                Subtype.mk (p := fun (p : Ideal R) ↦ p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R))
                  (Ideal.under R (↑p : Ideal S)) ⋯,
              invFun := fun (p : { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) ↦
                Subtype.mk (p := fun (p : Ideal S) ↦ p.IsPrime)
                  (Ideal.map (F := R →+* S) (algebraMap R S) (↑p : Ideal R)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { p : Ideal S // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
          I' :
        { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) ↔
    I ≤ I'
have mpr : I ≤ I' →
  LE.le.{u_1} (α := { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
    (({
            toFun := fun (p : { p : Ideal S // p.IsPrime }) ↦
              Subtype.mk (p := fun (p : Ideal R) ↦ p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R))
                (Ideal.under R (↑p : Ideal S)) sorry,
            invFun := fun (p : { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) ↦
              Subtype.mk (p := fun (p : Ideal S) ↦ p.IsPrime) (Ideal.map (F := R →+* S) (algebraMap R S) (↑p : Ideal R))
                sorry,
            left_inv := sorry, right_inv := sorry } :
          (a : { p : Ideal S // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
        I :
      { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
    (({
            toFun := fun (p : { p : Ideal S // p.IsPrime }) ↦
              Subtype.mk (p := fun (p : Ideal R) ↦ p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R))
                (Ideal.under R (↑p : Ideal S)) sorry,
            invFun := fun (p : { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) ↦
              Subtype.mk (p := fun (p : Ideal S) ↦ p.IsPrime) (Ideal.map (F := R →+* S) (algebraMap R S) (↑p : Ideal R))
                sorry,
            left_inv := sorry, right_inv := sorry } :
          (a : { p : Ideal S // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
        I' :
      { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
Tactic: constructor