-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
S : (↑X.affineOpens : Type u_1)
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : (↑Γ(X, U₁) : Type u_1)
y₂ : (↑Γ(X, U₂) : Type u_1)
f : (↑Γ(X, U₁ ⊔ U₂) : Type u_1)
x : (↑Γ(X, X.basicOpen f) : Type u_1)
h₁ : (↑S : X.Opens) ≤ U₁
h₂ : (↑S : X.Opens) ≤ U₂
e₁ :
  TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      CommRingCat.carrier) y₁
      (X.basicOpen
        (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) f U₁ ⋯))
      ⋯ =
    HPow.hPow (α :=
        ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
          (X.presheaf.obj
            (op
              (X.basicOpen
                (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦
                  (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) f U₁ ⋯)))))
        (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier)
          (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
            (CC := CommRingCat.carrier) f U₁ ⋯)
          (X.basicOpen
            (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
              (CC := CommRingCat.carrier) f U₁ ⋯))
          ⋯)
        n₁ *
      TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        CommRingCat.carrier) x
        (X.basicOpen
          (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
            (CC := CommRingCat.carrier) f U₁ ⋯))
        ⋯
e₂ :
  TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      CommRingCat.carrier) y₂
      (X.basicOpen
        (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) f U₂ ⋯))
      ⋯ =
    HPow.hPow (α :=
        ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
          (X.presheaf.obj
            (op
              (X.basicOpen
                (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦
                  (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) f U₂ ⋯)))))
        (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier)
          (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
            (CC := CommRingCat.carrier) f U₂ ⋯)
          (X.basicOpen
            (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
              (CC := CommRingCat.carrier) f U₂ ⋯))
          ⋯)
        n₂ *
      TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        CommRingCat.carrier) x
        (X.basicOpen
          (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
            (CC := CommRingCat.carrier) f U₂ ⋯))
        ⋯
obtain :
  ∀ (n : ℕ)
    (e :
      (↑(Subtype.mk (p := fun (x : (↑Γ(X, (↑S : X.Opens)) : Type u_1)) ↦
                Membership.mem (γ := Submonoid (↑Γ(X, (↑S : X.Opens)) : Type u_1))
                  (Submonoid.powers
                      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦
                        (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) f (↑S : X.Opens) ⋯) :
                    Submonoid (↑Γ(X, (↑S : X.Opens)) : Type u_1))
                  x)
                ((fun (x : ℕ) ↦
                    HPow.hPow (α := (↑Γ(X, (↑S : X.Opens)) : Type u_1))
                      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦
                          (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) f (↑S : X.Opens) ⋯ :
                        ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                          CommRingCat.carrier) (X.presheaf.obj (op (↑S : X.Opens))))
                      x)
                  n)
                ⋯) :
            (↑Γ(X, (↑S : X.Opens)) : Type u_1)) *
          TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
            (CC := CommRingCat.carrier)
            (HPow.hPow (α :=
                ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (X.presheaf.obj (op U₁)))
                (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦
                  (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) f U₁ ⋯)
                n₂ *
              y₁)
            (↑S : X.Opens) h₁ =
        (↑(Subtype.mk (p := fun (x : (↑Γ(X, (↑S : X.Opens)) : Type u_1)) ↦
                Membership.mem (γ := Submonoid (↑Γ(X, (↑S : X.Opens)) : Type u_1))
                  (Submonoid.powers
                      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦
                        (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) f (↑S : X.Opens) ⋯) :
                    Submonoid (↑Γ(X, (↑S : X.Opens)) : Type u_1))
                  x)
                ((fun (x : ℕ) ↦
                    HPow.hPow (α := (↑Γ(X, (↑S : X.Opens)) : Type u_1))
                      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦
                          (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) f (↑S : X.Opens) ⋯ :
                        ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                          CommRingCat.carrier) (X.presheaf.obj (op (↑S : X.Opens))))
                      x)
                  n)
                ⋯) :
            (↑Γ(X, (↑S : X.Opens)) : Type u_1)) *
          TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
            (CC := CommRingCat.carrier)
            (HPow.hPow (α :=
                ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (X.presheaf.obj (op U₂)))
                (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦
                  (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) f U₂ ⋯)
                n₁ *
              y₂)
            (↑S : X.Opens) h₂),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
              (CC := CommRingCat.carrier)
              (HPow.hPow (α :=
                  ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                    CommRingCat.carrier) (X.presheaf.obj (op U₁)))
                  (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦
                    (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) f U₁ ⋯)
                  (m + n₂) *
                y₁)
              (↑S : X.Opens) h₁ =
            TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
              (CC := CommRingCat.carrier)
              (HPow.hPow (α :=
                  ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                    CommRingCat.carrier) (X.presheaf.obj (op U₂)))
                  (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦
                    (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) f U₂ ⋯)
                  (m + n₁) *
                y₂)
              (↑S : X.Opens) h₂
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier)
            (HPow.hPow (α :=
                ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (X.presheaf.obj (op U₁)))
                (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦
                  (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) f U₁ ⋯)
                (m + n₂) *
              y₁)
            (↑S : X.Opens) h₁ =
          TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
            (CC := CommRingCat.carrier)
            (HPow.hPow (α :=
                ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (X.presheaf.obj (op U₂)))
                (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦
                  (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier) f U₂ ⋯)
                (m + n₁) *
              y₂)
            (↑S : X.Opens) h₂

Tactic:
obtain ⟨⟨_, n, rfl⟩, e⟩ :=
    (@IsLocalization.eq_iff_exists _ _ _ _ _ _
      (S.2.isLocalization_basicOpen (f |_ S.1))
        (((f |_ U₁) ^ n₂ * y₁) |_ S.1)
        (((f |_ U₂) ^ n₁ * y₂) |_ S.1)).mp <| by
    apply exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux (e₁ := e₁) (e₂ := e₂)
    · change X.basicOpen _ ≤ _
      simp only [TopCat.Presheaf.restrictOpenCommRingCat_apply, Scheme.basicOpen_res]
      exact inf_le_inf h₁ le_rfl
    · change X.basicOpen _ ≤ _
      simp only [TopCat.Presheaf.restrictOpenCommRingCat_apply, Scheme.basicOpen_res]
      exact inf_le_inf h₂ le_rfl

Premises used: Iff.mp, rfl, IsLocalization.eq_iff_exists