-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens (↑X : Type u)
n₁ n₂ : ℕ
y₁ : (↑(F.obj (op U₁)) : Type u_1)
y₂ : (↑(F.obj (op U₂)) : Type u_1)
f : (↑(F.obj (op (U₁ ⊔ U₂))) : Type u_1)
x : (↑(F.obj (op U₃)) : Type u_1)
h₄₁ : U₄ ≤ U₁
h₄₂ : U₄ ≤ U₂
h₅₁ : U₅ ≤ U₁
h₅₃ : U₅ ≤ U₃
h₆₂ : U₆ ≤ U₂
h₆₃ : U₆ ≤ U₃
h₇₄ : U₇ ≤ U₄
h₇₅ : U₇ ≤ U₅
h₇₆ : U₇ ≤ U₆
e₁ :
  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) y₁ U₅ h₅₁)
      U₇ 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)
            (F.obj (op 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₁ ⋯)
            U₅ h₅₁)
          n₁ *
        TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) x U₅ h₅₃)
      U₇ h₇₅
e₂ :
  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) y₂ U₆ h₆₂)
      U₇ 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)
            (F.obj (op 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₂ ⋯)
            U₆ h₆₂)
          n₂ *
        TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) x U₆ h₆₃)
      U₇ h₇₆
dsimp :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
      (F.obj (op U₇)))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (F.map (homOfLE h₇₄).op) :
          (a : (↑(F.obj (op U₄)) : Type u_1)) → (↑(F.obj (op U₇)) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (F.map (homOfLE h₄₁).op) :
              (a : (↑(F.obj (op U₁)) : Type u_1)) → (↑(F.obj (op U₄)) : Type u_1))
            (HPow.hPow (α :=
                ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (F.obj (op U₁)))
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
                        (CC := CommRingCat.carrier) (X := F.obj (op (U₁ ⊔ U₂))) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
                      (a : (↑(F.obj (op (U₁ ⊔ U₂))) : Type u_1)) → (↑(F.obj (op U₁)) : Type u_1))
                    f :
                  (↑(F.obj (op U₁)) : Type u_1))
                n₂ *
              y₁) :
          (↑(F.obj (op U₄)) : Type u_1)) :
      (↑(F.obj (op U₇)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (F.map (homOfLE h₇₄).op) :
          (a : (↑(F.obj (op U₄)) : Type u_1)) → (↑(F.obj (op U₇)) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (F.map (homOfLE h₄₂).op) :
              (a : (↑(F.obj (op U₂)) : Type u_1)) → (↑(F.obj (op U₄)) : Type u_1))
            (HPow.hPow (α :=
                ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (F.obj (op U₂)))
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
                        (CC := CommRingCat.carrier) (X := F.obj (op (U₁ ⊔ U₂))) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
                      (a : (↑(F.obj (op (U₁ ⊔ U₂))) : Type u_1)) → (↑(F.obj (op U₂)) : Type u_1))
                    f :
                  (↑(F.obj (op U₂)) : Type u_1))
                n₁ *
              y₂) :
          (↑(F.obj (op U₄)) : Type u_1)) :
      (↑(F.obj (op U₇)) : Type u_1))
⊢ 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)
        (HPow.hPow (α :=
            ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (F.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₁)
        U₄ h₄₁)
      U₇ h₇₄ =
    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)
        (HPow.hPow (α :=
            ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (F.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₂)
        U₄ h₄₂)
      U₇ h₇₄

Tactic:
dsimp only [TopCat.Presheaf.restrictOpenCommRingCat_apply] at e₁ e₂ ⊢

Premises used: TopCat.Presheaf.restrictOpenCommRingCat_apply