-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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₇₆
⊢ 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₇₄
have 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 sorry))) :
                    (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 sorry))) :
                    (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))
Tactic: dsimp only [TopCat.Presheaf.restrictOpenCommRingCat_apply] at e₁ e₂ ⊢