-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
theorem exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated (X : Scheme.{u}) (U : X.Opens)
    (hU : IsCompact U.1) (hU' : IsQuasiSeparated U.1) (f : Γ(X, U)) (x : Γ(X, X.basicOpen f)) :
    ∃ (n : ℕ) (y : Γ(X, U)), y |_ X.basicOpen f = (f |_ X.basicOpen f) ^ n * x

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro
X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.146054).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.146890).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
hs : ↑S ∩ ↑↑U = ⋃ i ∈ s, ↑↑i
⊢ ∃ n y,
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x

Tactic:
haveI := hs'.to_subtype

Result:
case refine_2.intro.intro.intro.intro.intro.intro
X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.146054).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.146890).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
hs : ↑S ∩ ↑↑U = ⋃ i ∈ s, ↑↑i
this : Finite ↑s
⊢ ∃ n y,
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x

Proof state:
case h.refine_1
X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
this✝ : Finite ↑s
val✝ : Fintype ↑s
hs : S ⊓ ↑U = ⨆ i, ↑↑i
hs₁ : ∀ (i : ↑s), ↑↑i ≤ S
hs₂ : ∀ (i : ↑s), ↑↑i ≤ ↑U
n : ↑s → ℕ
hn : ∀ (i : ↑s) (m : ℕ), n i ≤ m → (((f |_ S) ⋯ ^ (m + n₂) * y₁) |_ ↑↑i) ⋯ = (((f |_ ↑U) ⋯ ^ (m + n₁) * y₂) |_ ↑↑i) ⋯
this :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₂) * y₁) =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₁) * y₂)
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op))
      (↑⟨((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₂) * y₁,
              (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₁) * y₂),
            this⟩).1 =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₁ + n₂) * x)

Tactic:
rw [add_assoc, add_comm n₁]

Result:
case h.refine_1
X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
this✝ : Finite ↑s
val✝ : Fintype ↑s
hs : S ⊓ ↑U = ⨆ i, ↑↑i
hs₁ : ∀ (i : ↑s), ↑↑i ≤ S
hs₂ : ∀ (i : ↑s), ↑↑i ≤ ↑U
n : ↑s → ℕ
hn : ∀ (i : ↑s) (m : ℕ), n i ≤ m → (((f |_ S) ⋯ ^ (m + n₂) * y₁) |_ ↑↑i) ⋯ = (((f |_ ↑U) ⋯ ^ (m + n₁) * y₂) |_ ↑↑i) ⋯
this :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₂) * y₁) =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₁) * y₂)
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op))
      (↑⟨((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₂) * y₁,
              (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₁) * y₂),
            this⟩).1 =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + (n₂ + n₁)) * x)