Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: 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.sheaf.obj.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.sheaf.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₁ + n₂) * x)

pp: case h.refine_2
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.sheaf.obj.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⟩).2 =
    (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₁ + n₂) * x)

Tactic:
· -- This unfolds `X.sheaf`
      change (X.presheaf.map _) _ = (X.presheaf.map _) _
      rw [add_assoc, add_comm n₁]
      simp only [pow_add, map_pow, map_mul, hy₁, ← CommRingCat.comp_apply, ← mul_assoc,
        ← Functor.map_comp, ← op_comp, homOfLE_comp]

Goal state after:
case h.refine_2
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.sheaf.obj.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⟩).2 =
    (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₁ + n₂) * x)