-- Mathlib/AlgebraicGeometry/Gluing.lean
theorem fromGlued_open_map : IsOpenMap 𝒰.fromGlued.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 (𝒰.map (𝒰.f x)).base) ''
      (⇑(ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) ⁻¹' (⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U)))

Tactic:
apply (show IsOpenImmersion (𝒰.map (𝒰.f x)) from inferInstance).base_open.isOpenMap

Result:
case right.left.a
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 (fromGlued 𝒰).base) '' U))

Proof state:
case h.e'_3.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
e_1✝ : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace = ↑↑((gluedCover 𝒰).U (𝒰.f x)).toPresheafedSpace
⊢ ⇑(ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) ⁻¹' (⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U) =
    ⇑(ConcreteCategory.hom ((gluedCover 𝒰).ι (𝒰.f x)).base) ⁻¹' U

Tactic:
simp only [← ι_fromGlued, gluedCover_U, comp_coeBase, TopCat.hom_comp, ContinuousMap.coe_comp,
  Set.preimage_comp]

Result:
case h.e'_3.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
e_1✝ : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace = ↑↑((gluedCover 𝒰).U (𝒰.f x)).toPresheafedSpace
⊢ ⇑(TopCat.Hom.hom ((gluedCover 𝒰).ι (𝒰.f x)).base) ⁻¹'
      (⇑(TopCat.Hom.hom (fromGlued 𝒰).base) ⁻¹' ((fun a => (ConcreteCategory.hom (fromGlued 𝒰).base) a) '' U)) =
    ⇑(ConcreteCategory.hom ((gluedCover 𝒰).ι (𝒰.f x)).base) ⁻¹' U

Proof state:
case h.e'_3.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
e_1✝ : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace = ↑↑((gluedCover 𝒰).U (𝒰.f x)).toPresheafedSpace
⊢ ⇑(TopCat.Hom.hom ((gluedCover 𝒰).ι (𝒰.f x)).base) ⁻¹'
      (⇑(TopCat.Hom.hom (fromGlued 𝒰).base) ⁻¹' ((fun a => (ConcreteCategory.hom (fromGlued 𝒰).base) a) '' U)) =
    ⇑(ConcreteCategory.hom ((gluedCover 𝒰).ι (𝒰.f x)).base) ⁻¹' U

Tactic:
congr! 1

Result:
case h.e'_3.h.h.e'_4
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
e_1✝ : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace = ↑↑((gluedCover 𝒰).U (𝒰.f x)).toPresheafedSpace
⊢ ⇑(TopCat.Hom.hom (fromGlued 𝒰).base) ⁻¹' ((fun a => (ConcreteCategory.hom (fromGlued 𝒰).base) a) '' U) = U

Proof state:
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

Tactic:
use 𝒰.fromGlued.base '' U ∩ Set.range (𝒰.map (𝒰.f x)).base

Result:
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)

Proof state:
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

Tactic:
intro x hx

Result:
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

Proof state:
case right.left.a
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 (fromGlued 𝒰).base) '' U))

Tactic:
convert hU (𝒰.f x) using 1

Result:
case h.e'_3.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
e_1✝ : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace = ↑↑((gluedCover 𝒰).U (𝒰.f x)).toPresheafedSpace
⊢ ⇑(ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) ⁻¹' (⇑(ConcreteCategory.hom (fromGlued 𝒰).base) '' U) =
    ⇑(ConcreteCategory.hom ((gluedCover 𝒰).ι (𝒰.f x)).base) ⁻¹' U

Proof state:
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)

Tactic:
constructor

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 (fromGlued 𝒰).base) '' U ∩ Set.range ⇑(ConcreteCategory.hom (𝒰.map (𝒰.f x)).base))

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)

Proof state:
case h.e'_3.h.h.e'_4
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
e_1✝ : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace = ↑↑((gluedCover 𝒰).U (𝒰.f x)).toPresheafedSpace
⊢ ⇑(TopCat.Hom.hom (fromGlued 𝒰).base) ⁻¹' ((fun a => (ConcreteCategory.hom (fromGlued 𝒰).base) a) '' U) = U

Tactic:
exact Set.preimage_image_eq _ 𝒰.fromGlued_injective

Result:
no goals