-- Mathlib/AlgebraicGeometry/Gluing.lean
theorem fromGlued_open_map : IsOpenMap 𝒰.fromGlued.base

Proof state:
X : Scheme
𝒰 : X.OpenCover
⊢ IsOpenMap ⇑(ConcreteCategory.hom (fromGlued 𝒰).base)

Tactic:
intro U hU

Result:
X : Scheme
𝒰 : X.OpenCover
U : Set ↑↑(gluedCover 𝒰).glued.toPresheafedSpace
hU : IsOpen U
⊢ IsOpen (⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U)

Proof state:
case right.right
X : Scheme
𝒰 : X.OpenCover
U : Set ↑↑(gluedCover 𝒰).glued.toPresheafedSpace
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑(ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) ⁻¹' U)
x : ↑↑X.toPresheafedSpace
hx : x ∈ ⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U
⊢ x ∈ ⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U ∩ Set.range ⇑(ConcreteCategory.hom (𝒰.map (𝒰.f x)).base)

Tactic:
exact ⟨hx, 𝒰.covers x⟩

Result:
no goals

Proof state:
X : Scheme
𝒰 : X.OpenCover
U : Set ↑↑(gluedCover 𝒰).glued.toPresheafedSpace
hU : IsOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ ⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U
⊢ ∃ t ⊆ ⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U, IsOpen t ∧ x ∈ t

Tactic:
rw [𝒰.gluedCover.isOpen_iff] at hU

Result:
X : Scheme
𝒰 : X.OpenCover
U : Set ↑↑(gluedCover 𝒰).glued.toPresheafedSpace
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑(ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) ⁻¹' U)
x : ↑↑X.toPresheafedSpace
hx : x ∈ ⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U
⊢ ∃ t ⊆ ⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U, IsOpen t ∧ x ∈ t

Proof state:
X : Scheme
𝒰 : X.OpenCover
U : Set ↑↑(gluedCover 𝒰).glued.toPresheafedSpace
hU : IsOpen U
⊢ IsOpen (⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U)

Tactic:
rw [isOpen_iff_forall_mem_open]

Result:
X : Scheme
𝒰 : X.OpenCover
U : Set ↑↑(gluedCover 𝒰).glued.toPresheafedSpace
hU : IsOpen U
⊢ ∀ x ∈ ⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U,
    ∃ t ⊆ ⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U, IsOpen t ∧ x ∈ t

Proof state:
case h
X : Scheme
𝒰 : X.OpenCover
U : Set ↑↑(gluedCover 𝒰).glued.toPresheafedSpace
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑(ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) ⁻¹' U)
x : ↑↑X.toPresheafedSpace
hx : x ∈ ⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U
⊢ ⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U ∩ Set.range ⇑(ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) ⊆
      ⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U ∧
    IsOpen (⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U ∩ Set.range ⇑(ConcreteCategory.hom (𝒰.map (𝒰.f x)).base)) ∧
      x ∈ ⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U ∩ Set.range ⇑(ConcreteCategory.hom (𝒰.map (𝒰.f x)).base)

Tactic:
use Set.inter_subset_left

Result:
case right
X : Scheme
𝒰 : X.OpenCover
U : Set ↑↑(gluedCover 𝒰).glued.toPresheafedSpace
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑(ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) ⁻¹' U)
x : ↑↑X.toPresheafedSpace
hx : x ∈ ⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U
⊢ IsOpen (⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U ∩ Set.range ⇑(ConcreteCategory.hom (𝒰.map (𝒰.f x)).base)) ∧
    x ∈ ⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U ∩ Set.range ⇑(ConcreteCategory.hom (𝒰.map (𝒰.f x)).base)

Proof state:
case right.left
X : Scheme
𝒰 : X.OpenCover
U : Set ↑↑(gluedCover 𝒰).glued.toPresheafedSpace
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑(ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) ⁻¹' U)
x : ↑↑X.toPresheafedSpace
hx : x ∈ ⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U
⊢ IsOpen (⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U ∩ Set.range ⇑(ConcreteCategory.hom (𝒰.map (𝒰.f x)).base))

Tactic:
rw [← Set.image_preimage_eq_inter_range]

Result:
case right.left
X : Scheme
𝒰 : X.OpenCover
U : Set ↑↑(gluedCover 𝒰).glued.toPresheafedSpace
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑(ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) ⁻¹' U)
x : ↑↑X.toPresheafedSpace
hx : x ∈ ⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U
⊢ IsOpen
    (⇑(ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) ''
      (⇑(ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) ⁻¹' (⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U)))