-- 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₂ ⋯))
        ⋯
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₂
m : ℕ
hm : n ≤ m
h :
  ∀
    (e :
      HPow.hPow (α := (↑Γ(X, (↑S : X.Opens)) : Type u_1))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                    CommRingCat.carrier) (X := X.presheaf.obj (op (U₁ ⊔ U₂)))
                    (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
                  (a : (↑(X.presheaf.obj (op (U₁ ⊔ U₂))) : Type u_1)) →
                    (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
                f :
              (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
            n *
          HMul.hMul (β := (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
            (HPow.hPow (α := (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                      CommRingCat.carrier) (X := X.presheaf.obj (op (U₁ ⊔ U₂)))
                      (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
                    (a : (↑(X.presheaf.obj (op (U₁ ⊔ U₂))) : Type u_1)) →
                      (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
                  f :
                (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
              n₂)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                    CommRingCat.carrier) (X.presheaf.map (homOfLE h₁).op) :
                  (a : (↑(X.presheaf.obj (op U₁)) : Type u_1)) → (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
                y₁ :
              (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1)) =
        HPow.hPow (α := (↑Γ(X, (↑S : X.Opens)) : Type u_1))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                    CommRingCat.carrier) (X := X.presheaf.obj (op (U₁ ⊔ U₂)))
                    (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
                  (a : (↑(X.presheaf.obj (op (U₁ ⊔ U₂))) : Type u_1)) →
                    (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
                f :
              (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
            n *
          HMul.hMul (β := (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
            (HPow.hPow (α := (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                      CommRingCat.carrier) (X := X.presheaf.obj (op (U₁ ⊔ U₂)))
                      (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
                    (a : (↑(X.presheaf.obj (op (U₁ ⊔ U₂))) : Type u_1)) →
                      (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
                  f :
                (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
              n₁)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                    CommRingCat.carrier) (X.presheaf.map (homOfLE h₂).op) :
                  (a : (↑(X.presheaf.obj (op U₂)) : Type u_1)) → (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
                y₂ :
              (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))),
    HPow.hPow (α := (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                (a : (↑(X.presheaf.obj (op (U₁ ⊔ U₂))) : Type u_1)) →
                  (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
              f :
            (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
          (m - n) *
        (HPow.hPow (α := (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                    CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                  (a : (↑(X.presheaf.obj (op (U₁ ⊔ U₂))) : Type u_1)) →
                    (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
                f :
              (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
            n *
          HMul.hMul (β := (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
            (HPow.hPow (α := (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                      CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                    (a : (↑(X.presheaf.obj (op (U₁ ⊔ U₂))) : Type u_1)) →
                      (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
                  f :
                (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
              n₂)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                    CommRingCat.carrier) (X.presheaf.map (homOfLE h₁).op) :
                  (a : (↑(X.presheaf.obj (op U₁)) : Type u_1)) → (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
                y₁ :
              (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))) =
      HPow.hPow (α := (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                (a : (↑(X.presheaf.obj (op (U₁ ⊔ U₂))) : Type u_1)) →
                  (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
              f :
            (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
          (m - n) *
        (HPow.hPow (α := (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                    CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                  (a : (↑(X.presheaf.obj (op (U₁ ⊔ U₂))) : Type u_1)) →
                    (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
                f :
              (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
            n *
          HMul.hMul (β := (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
            (HPow.hPow (α := (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                      CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                    (a : (↑(X.presheaf.obj (op (U₁ ⊔ U₂))) : Type u_1)) →
                      (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
                  f :
                (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
              n₁)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                    CommRingCat.carrier) (X.presheaf.map (homOfLE h₂).op) :
                  (a : (↑(X.presheaf.obj (op U₂)) : Type u_1)) → (↑(X.presheaf.obj (op (↑S : X.Opens))) : Type u_1))
                y₂ :
              (↑(X.presheaf.obj (op (↑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₁ ⋯)
          (m - n + n + 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 + n + n₁) *
        y₂)
      (↑S : X.Opens) h₂

Tactic:
simp only [TopCat.Presheaf.restrictOpenCommRingCat_apply,
    pow_add, map_pow, map_mul, mul_assoc, ← Functor.map_comp, ← op_comp, homOfLE_comp,
    ← CommRingCat.comp_apply] at e ⊢

Premises used: CategoryTheory.op_comp, mul_assoc, pow_add, map_pow, map_mul, TopCat.Presheaf.restrictOpenCommRingCat_apply, CategoryTheory.homOfLE_comp, CommRingCat.comp_apply, CategoryTheory.Functor.map_comp