-- 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₁ :
  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))
            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))
        (HMul.hMul (β :=
          ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
            (F.obj (op U₅)))
          (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) (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) (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)) :
              (↑(F.obj (op U₅)) : Type u_1))
            n₁)
          ((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))
              x :
            (↑(F.obj (op U₅)) : Type u_1))) :
      (↑(F.obj (op U₇)) : Type u_1))
e₂ :
  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))
            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))
        (HMul.hMul (β :=
          ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
            (F.obj (op U₆)))
          (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) (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) (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)) :
              (↑(F.obj (op U₆)) : Type u_1))
            n₂)
          ((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))
              x :
            (↑(F.obj (op U₆)) : Type u_1))) :
      (↑(F.obj (op U₇)) : Type u_1))
⊢ 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))
have simp : ∀
  (e₁ :
    (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (F.map (homOfLE sorry).op) :
          (a : (↑(F.obj (op U₁)) : Type u_1)) → (↑(F.obj (op U₇)) : Type u_1))
        y₁ =
      HMul.hMul (β := (↑(F.obj (op U₇)) : Type u_1))
        (HPow.hPow (α := (↑(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) (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₁)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (F.map (homOfLE sorry).op) :
              (a : (↑(F.obj (op U₃)) : Type u_1)) → (↑(F.obj (op U₇)) : Type u_1))
            x :
          (↑(F.obj (op U₇)) : Type u_1)))
  (e₂ :
    (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (F.map (homOfLE sorry).op) :
          (a : (↑(F.obj (op U₂)) : Type u_1)) → (↑(F.obj (op U₇)) : Type u_1))
        y₂ =
      HMul.hMul (β := (↑(F.obj (op U₇)) : Type u_1))
        (HPow.hPow (α := (↑(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) (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₂)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (F.map (homOfLE sorry).op) :
              (a : (↑(F.obj (op U₃)) : Type u_1)) → (↑(F.obj (op U₇)) : Type u_1))
            x :
          (↑(F.obj (op U₇)) : Type u_1))),
  HMul.hMul (β := (↑(F.obj (op U₇)) : Type u_1))
      (HPow.hPow (α := (↑(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) (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₂)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (F.map (homOfLE sorry).op) :
            (a : (↑(F.obj (op U₁)) : Type u_1)) → (↑(F.obj (op U₇)) : Type u_1))
          y₁ :
        (↑(F.obj (op U₇)) : Type u_1)) =
    HMul.hMul (β := (↑(F.obj (op U₇)) : Type u_1))
      (HPow.hPow (α := (↑(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) (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₁)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (F.map (homOfLE sorry).op) :
            (a : (↑(F.obj (op U₂)) : Type u_1)) → (↑(F.obj (op U₇)) : Type u_1))
          y₂ :
        (↑(F.obj (op U₇)) : Type u_1))
Tactic: simp only [map_mul, map_pow, ← op_comp, ← F.map_comp, homOfLE_comp, ← CommRingCat.comp_apply]
    at e₁ e₂ ⊢
Cleared hypotheses: e₁, e₂