-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
theorem exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux (X : Scheme)
    (S : X.affineOpens) (U₁ U₂ : X.Opens) {n₁ n₂ : ℕ} {y₁ : Γ(X, U₁)}
    {y₂ : Γ(X, U₂)} {f : Γ(X, U₁ ⊔ U₂)}
    {x : Γ(X, X.basicOpen f)} (h₁ : S.1 ≤ U₁) (h₂ : S.1 ≤ U₂)
    (e₁ : y₁ |_ X.basicOpen (f |_ U₁) =
      ((f |_ U₁ |_ X.basicOpen _) ^ n₁) * x |_ X.basicOpen _)
    (e₂ : y₂ |_ X.basicOpen (f |_ U₂) =
      ((f |_ U₂ |_ X.basicOpen _) ^ n₂) * x |_ X.basicOpen _) :
    ∃ n : ℕ, ∀ m, n ≤ m →
      ((f |_ U₁) ^ (m + n₂) * y₁) |_ S.1 = ((f |_ U₂) ^ (m + n₁) * y₂) |_ S.1

Proof state:
case h
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
n : ℕ
e :
  ↑⟨(fun x => (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₁) ⋯ ^ n₂ * y₁) |_ ↑S) h₁ =
    ↑⟨(fun x => (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₂) ⋯ ^ n₁ * y₂) |_ ↑S) h₂
⊢ ∀ (m : ℕ), n ≤ m → (((f |_ U₁) ⋯ ^ (m + n₂) * y₁) |_ ↑S) h₁ = (((f |_ U₂) ⋯ ^ (m + n₁) * y₂) |_ ↑S) h₂

Tactic:
intros m hm

Result:
case h
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
n : ℕ
e :
  ↑⟨(fun x => (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₁) ⋯ ^ n₂ * y₁) |_ ↑S) h₁ =
    ↑⟨(fun x => (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₂) ⋯ ^ n₁ * y₂) |_ ↑S) h₂
m : ℕ
hm : n ≤ m
⊢ (((f |_ U₁) ⋯ ^ (m + n₂) * y₁) |_ ↑S) h₁ = (((f |_ U₂) ⋯ ^ (m + n₁) * y₂) |_ ↑S) h₂

Proof state:
case h
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
n : ℕ
e :
  ↑⟨(fun x => (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₁) ⋯ ^ n₂ * y₁) |_ ↑S) h₁ =
    ↑⟨(fun x => (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₂) ⋯ ^ n₁ * y₂) |_ ↑S) h₂
m : ℕ
hm : n ≤ m
⊢ (((f |_ U₁) ⋯ ^ (m - n + n + n₂) * y₁) |_ ↑S) h₁ = (((f |_ U₂) ⋯ ^ (m - n + n + n₁) * y₂) |_ ↑S) h₂

Tactic:
simp only [TopCat.Presheaf.restrictOpenCommRingCat_apply,
  pow_add, map_pow, map_mul, mul_assoc, ← Functor.map_comp, ← op_comp, homOfLE_comp,
  Subtype.coe_mk, ← CommRingCat.comp_apply] at e ⊢

Result:
case h
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
n m : ℕ
hm : n ≤ m
e :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n₂ *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE h₁).op)) y₁) =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n₁ *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE h₂).op)) y₂)
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (m - n) *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
        ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n₂ *
          (ConcreteCategory.hom (X.presheaf.map (homOfLE h₁).op)) y₁)) =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (m - n) *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
        ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n₁ *
          (ConcreteCategory.hom (X.presheaf.map (homOfLE h₂).op)) y₂))

Proof state:
case h
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
n m : ℕ
hm : n ≤ m
e :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n₂ *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE h₁).op)) y₁) =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n₁ *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE h₂).op)) y₂)
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (m - n) *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
        ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n₂ *
          (ConcreteCategory.hom (X.presheaf.map (homOfLE h₁).op)) y₁)) =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (m - n) *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
        ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n₁ *
          (ConcreteCategory.hom (X.presheaf.map (homOfLE h₂).op)) y₂))

Tactic:
rw [e]

Result:
no goals

Proof state:
case h₇₅
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
⊢ ↑S ⊓ X.basicOpen f ≤ U₁ ⊓ X.basicOpen f

Tactic:
exact inf_le_inf h₁ le_rfl

Result:
no goals

Proof state:
case h₇₆
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
⊢ ↑S ⊓ X.basicOpen f ≤ U₂ ⊓ X.basicOpen f

Tactic:
exact inf_le_inf h₂ le_rfl

Result:
no goals