-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
theorem exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux {X : TopCat}
    (F : X.Presheaf CommRingCat) {U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens X} {n₁ n₂ : ℕ}
    {y₁ : F.obj (op U₁)} {y₂ : F.obj (op U₂)} {f : F.obj (op <| U₁ ⊔ U₂)}
    {x : F.obj (op 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₅) (h₇₆ : U₇ ≤ U₆)
    (e₁ : y₁ |_ U₅ = (f |_ U₁ |_ U₅) ^ n₁ * x |_ U₅)
    (e₂ : y₂ |_ U₆ = (f |_ U₂ |_ U₆) ^ n₂ * x |_ U₆) :
    (((f |_ U₁) ^ n₂ * y₁) |_ U₄) |_ U₇ = (((f |_ U₂) ^ n₁ * y₂) |_ U₄) |_ U₇

Proof state:
X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op 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₅
h₇₆ : U₇ ≤ U₆
e₁ : ((y₁ |_ U₅) h₅₁ |_ U₇) h₇₅ = ((((f |_ U₁) ⋯ |_ U₅) h₅₁ ^ n₁ * (x |_ U₅) h₅₃) |_ U₇) h₇₅
e₂ : ((y₂ |_ U₆) h₆₂ |_ U₇) h₇₆ = ((((f |_ U₂) ⋯ |_ U₆) h₆₂ ^ n₂ * (x |_ U₆) h₆₃) |_ U₇) h₇₆
⊢ ((((f |_ U₁) ⋯ ^ n₂ * y₁) |_ U₄) h₄₁ |_ U₇) h₇₄ = ((((f |_ U₂) ⋯ ^ n₁ * y₂) |_ U₄) h₄₂ |_ U₇) h₇₄

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

Result:
X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op 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₅
h₇₆ : U₇ ≤ U₆
e₁ :
  (ConcreteCategory.hom (F.map (homOfLE h₇₅).op)) ((ConcreteCategory.hom (F.map (homOfLE h₅₁).op)) y₁) =
    (ConcreteCategory.hom (F.map (homOfLE h₇₅).op))
      ((ConcreteCategory.hom (F.map (homOfLE h₅₁).op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f) ^ n₁ *
        (ConcreteCategory.hom (F.map (homOfLE h₅₃).op)) x)
e₂ :
  (ConcreteCategory.hom (F.map (homOfLE h₇₆).op)) ((ConcreteCategory.hom (F.map (homOfLE h₆₂).op)) y₂) =
    (ConcreteCategory.hom (F.map (homOfLE h₇₆).op))
      ((ConcreteCategory.hom (F.map (homOfLE h₆₂).op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f) ^ n₂ *
        (ConcreteCategory.hom (F.map (homOfLE h₆₃).op)) x)
⊢ (ConcreteCategory.hom (F.map (homOfLE h₇₄).op))
      ((ConcreteCategory.hom (F.map (homOfLE h₄₁).op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * y₁)) =
    (ConcreteCategory.hom (F.map (homOfLE h₇₄).op))
      ((ConcreteCategory.hom (F.map (homOfLE h₄₂).op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * y₂))

Proof state:
X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op 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₅
h₇₆ : U₇ ≤ U₆
e₁ :
  (ConcreteCategory.hom (F.map (homOfLE h₇₅).op)) ((ConcreteCategory.hom (F.map (homOfLE h₅₁).op)) y₁) =
    (ConcreteCategory.hom (F.map (homOfLE h₇₅).op))
      ((ConcreteCategory.hom (F.map (homOfLE h₅₁).op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f) ^ n₁ *
        (ConcreteCategory.hom (F.map (homOfLE h₅₃).op)) x)
e₂ :
  (ConcreteCategory.hom (F.map (homOfLE h₇₆).op)) ((ConcreteCategory.hom (F.map (homOfLE h₆₂).op)) y₂) =
    (ConcreteCategory.hom (F.map (homOfLE h₇₆).op))
      ((ConcreteCategory.hom (F.map (homOfLE h₆₂).op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f) ^ n₂ *
        (ConcreteCategory.hom (F.map (homOfLE h₆₃).op)) x)
⊢ (ConcreteCategory.hom (F.map (homOfLE h₇₄).op))
      ((ConcreteCategory.hom (F.map (homOfLE h₄₁).op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * y₁)) =
    (ConcreteCategory.hom (F.map (homOfLE h₇₄).op))
      ((ConcreteCategory.hom (F.map (homOfLE h₄₂).op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * y₂))

Tactic:
simp only [map_mul, map_pow, ← op_comp, ← F.map_comp, homOfLE_comp, ← CommRingCat.comp_apply]
  at e₁ e₂ ⊢

Result:
X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op 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₅
h₇₆ : U₇ ≤ U₆
e₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
e₂ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₂

Proof state:
X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op 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₅
h₇₆ : U₇ ≤ U₆
e₁ : (y₁ |_ U₅) h₅₁ = ((f |_ U₁) ⋯ |_ U₅) h₅₁ ^ n₁ * (x |_ U₅) h₅₃
e₂ : (y₂ |_ U₆) h₆₂ = ((f |_ U₂) ⋯ |_ U₆) h₆₂ ^ n₂ * (x |_ U₆) h₆₃
⊢ ((((f |_ U₁) ⋯ ^ n₂ * y₁) |_ U₄) h₄₁ |_ U₇) h₇₄ = ((((f |_ U₂) ⋯ ^ n₁ * y₂) |_ U₄) h₄₂ |_ U₇) h₇₄

Tactic:
apply_fun (fun x : F.obj (op U₅) ↦ x |_ U₇) at e₁

Result:
X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op 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₅
h₇₆ : U₇ ≤ U₆
e₂ : (y₂ |_ U₆) h₆₂ = ((f |_ U₂) ⋯ |_ U₆) h₆₂ ^ n₂ * (x |_ U₆) h₆₃
e₁ : ((y₁ |_ U₅) h₅₁ |_ U₇) h₇₅ = ((((f |_ U₁) ⋯ |_ U₅) h₅₁ ^ n₁ * (x |_ U₅) h₅₃) |_ U₇) h₇₅
⊢ ((((f |_ U₁) ⋯ ^ n₂ * y₁) |_ U₄) h₄₁ |_ U₇) h₇₄ = ((((f |_ U₂) ⋯ ^ n₁ * y₂) |_ U₄) h₄₂ |_ U₇) h₇₄

Proof state:
X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op 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₅
h₇₆ : U₇ ≤ U₆
e₂ : (y₂ |_ U₆) h₆₂ = ((f |_ U₂) ⋯ |_ U₆) h₆₂ ^ n₂ * (x |_ U₆) h₆₃
e₁ : ((y₁ |_ U₅) h₅₁ |_ U₇) h₇₅ = ((((f |_ U₁) ⋯ |_ U₅) h₅₁ ^ n₁ * (x |_ U₅) h₅₃) |_ U₇) h₇₅
⊢ ((((f |_ U₁) ⋯ ^ n₂ * y₁) |_ U₄) h₄₁ |_ U₇) h₇₄ = ((((f |_ U₂) ⋯ ^ n₁ * y₂) |_ U₄) h₄₂ |_ U₇) h₇₄

Tactic:
apply_fun (fun x : F.obj (op U₆) ↦ x |_ U₇) at e₂

Result:
X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op 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₅
h₇₆ : U₇ ≤ U₆
e₁ : ((y₁ |_ U₅) h₅₁ |_ U₇) h₇₅ = ((((f |_ U₁) ⋯ |_ U₅) h₅₁ ^ n₁ * (x |_ U₅) h₅₃) |_ U₇) h₇₅
e₂ : ((y₂ |_ U₆) h₆₂ |_ U₇) h₇₆ = ((((f |_ U₂) ⋯ |_ U₆) h₆₂ ^ n₂ * (x |_ U₆) h₆₃) |_ U₇) h₇₆
⊢ ((((f |_ U₁) ⋯ ^ n₂ * y₁) |_ U₄) h₄₁ |_ U₇) h₇₄ = ((((f |_ U₂) ⋯ ^ n₁ * y₂) |_ U₄) h₄₂ |_ U₇) h₇₄