-- 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₁ :
  (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (F.map (homOfLE ⋯).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 ⋯))) :
              (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 ⋯).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 ⋯).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 ⋯))) :
              (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 ⋯).op) :
            (a : (↑(F.obj (op U₃)) : Type u_1)) → (↑(F.obj (op U₇)) : Type u_1))
          x :
        (↑(F.obj (op U₇)) : Type u_1))
rw :
  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 ⋯))) :
              (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₂ *
      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 ⋯))) :
                (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 ⋯).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 ⋯))) :
              (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 ⋯).op) :
            (a : (↑(F.obj (op U₂)) : Type u_1)) → (↑(F.obj (op U₇)) : Type u_1))
          y₂ :
        (↑(F.obj (op U₇)) : Type u_1))
rw₁ :
  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 ⋯))) :
              (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₂ *
      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 ⋯))) :
                (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 ⋯).op) :
              (a : (↑(F.obj (op U₃)) : Type u_1)) → (↑(F.obj (op U₇)) : Type u_1))
            x :
          (↑(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 ⋯))) :
              (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₁ *
      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 ⋯))) :
                (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 ⋯).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 ⋯))) :
              (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 ⋯).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 ⋯))) :
              (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 ⋯).op) :
            (a : (↑(F.obj (op U₂)) : Type u_1)) → (↑(F.obj (op U₇)) : Type u_1))
          y₂ :
        (↑(F.obj (op U₇)) : Type u_1))
have rw₂ : 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₁ *
    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)) =
  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₁ *
    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))
Tactic: rw [e₁, e₂, mul_left_comm]