-- Mathlib/AlgebraicGeometry/Cover/Open.lean
/-- If two global sections agree after restriction to each member of an open cover, then
they agree globally. -/
lemma OpenCover.ext_elem {X : Scheme.{u}} {U : X.Opens} (f g : Γ(X, U)) (𝒰 : X.OpenCover)
    (h : ∀ i : 𝒰.J, (𝒰.map i).app U f = (𝒰.map i).app U g) : f = g

Proof state:
case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
x : ↑↑X.toPresheafedSpace
h :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op ≫ (IsOpenImmersion.ΓIso (𝒰.map (𝒰.f x)) U).inv)) f =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op ≫ (IsOpenImmersion.ΓIso (𝒰.map (𝒰.f x)) U).inv)) g
⊢ (ConcreteCategory.hom (X.sheaf.val.map (homOfLE ⋯).op)) f = (ConcreteCategory.hom (X.sheaf.val.map (homOfLE ⋯).op)) g

Tactic:
exact (IsOpenImmersion.ΓIso (𝒰.map (𝒰.f x)) U).commRingCatIsoToRingEquiv.symm.injective h

Result:
no goals

Proof state:
case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) g
⊢ ∀ (i : ↑↑X.toPresheafedSpace),
    (ConcreteCategory.hom (X.sheaf.val.map (homOfLE ⋯).op)) f =
      (ConcreteCategory.hom (X.sheaf.val.map (homOfLE ⋯).op)) g

Tactic:
intro x

Result:
case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) g
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom (X.sheaf.val.map (homOfLE ⋯).op)) f = (ConcreteCategory.hom (X.sheaf.val.map (homOfLE ⋯).op)) g

Proof state:
case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) g
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom (X.sheaf.val.map (homOfLE ⋯).op)) f = (ConcreteCategory.hom (X.sheaf.val.map (homOfLE ⋯).op)) g

Tactic:
replace h := h (𝒰.f x)

Result:
case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
x : ↑↑X.toPresheafedSpace
h : (ConcreteCategory.hom (Hom.app (𝒰.map (𝒰.f x)) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.map (𝒰.f x)) U)) g
⊢ (ConcreteCategory.hom (X.sheaf.val.map (homOfLE ⋯).op)) f = (ConcreteCategory.hom (X.sheaf.val.map (homOfLE ⋯).op)) g

Proof state:
case hcover
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) g
⊢ U ≤ ⨆ i, Hom.opensRange (𝒰.map (𝒰.f i)) ⊓ U

Tactic:
intro x hx

Result:
case hcover
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) g
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ x ∈ ↑(⨆ i, Hom.opensRange (𝒰.map (𝒰.f i)) ⊓ U)

Proof state:
case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
x : ↑↑X.toPresheafedSpace
h : (ConcreteCategory.hom (Hom.app (𝒰.map (𝒰.f x)) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.map (𝒰.f x)) U)) g
⊢ (ConcreteCategory.hom (X.sheaf.val.map (homOfLE ⋯).op)) f = (ConcreteCategory.hom (X.sheaf.val.map (homOfLE ⋯).op)) g

Tactic:
rw [← IsOpenImmersion.map_ΓIso_inv] at h

Result:
case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
x : ↑↑X.toPresheafedSpace
h :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op ≫ (IsOpenImmersion.ΓIso (𝒰.map (𝒰.f x)) U).inv)) f =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op ≫ (IsOpenImmersion.ΓIso (𝒰.map (𝒰.f x)) U).inv)) g
⊢ (ConcreteCategory.hom (X.sheaf.val.map (homOfLE ⋯).op)) f = (ConcreteCategory.hom (X.sheaf.val.map (homOfLE ⋯).op)) g

Proof state:
case hcover
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) g
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ x ∈ ↑(⨆ i, Hom.opensRange (𝒰.map (𝒰.f i)) ⊓ U)

Tactic:
simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_inf, Hom.coe_opensRange, Opens.coe_mk,
  Set.mem_iUnion, Set.mem_inter_iff, Set.mem_range, SetLike.mem_coe, exists_and_right]

Result:
case hcover
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) g
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ (∃ x_1 y, (ConcreteCategory.hom (𝒰.map (𝒰.f x_1)).base) y = x) ∧ x ∈ U

Proof state:
case hcover
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) g
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ (∃ x_1 y, (ConcreteCategory.hom (𝒰.map (𝒰.f x_1)).base) y = x) ∧ x ∈ U

Tactic:
refine ⟨?_, hx⟩

Result:
case hcover
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) g
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ ∃ x_1 y, (ConcreteCategory.hom (𝒰.map (𝒰.f x_1)).base) y = x

Proof state:
case hcover
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) g
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ ∃ x_1 y, (ConcreteCategory.hom (𝒰.map (𝒰.f x_1)).base) y = x

Tactic:
simpa using ⟨_, 𝒰.covers x⟩

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) g
⊢ f = g

Tactic:
fapply TopCat.Sheaf.eq_of_locally_eq' X.sheaf
  (fun i ↦ (𝒰.map (𝒰.f i)).opensRange ⊓ U) _ (fun _ ↦ homOfLE inf_le_right)

Result:
case hcover
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) g
⊢ U ≤ ⨆ i, Hom.opensRange (𝒰.map (𝒰.f i)) ⊓ U

case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) g
⊢ ∀ (i : ↑↑X.toPresheafedSpace),
    (ConcreteCategory.hom (X.sheaf.val.map (homOfLE ⋯).op)) f =
      (ConcreteCategory.hom (X.sheaf.val.map (homOfLE ⋯).op)) g