-- Module: Mathlib.RingTheory.Localization.Ideal
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'
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)) ⋯,
              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) })
⊢ 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'

Tactic:
constructor