-- Mathlib/Topology/Gluing.lean
theorem fromOpenSubsetsGlue_isOpenMap : IsOpenMap (fromOpenSubsetsGlue U)

Proof state:
case right.left
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
⊢ IsOpen (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∩ Set.range ⇑(ConcreteCategory.hom (U i).inclusion'))

Tactic:
rw [← Set.image_preimage_eq_inter_range]

Result:
case right.left
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
⊢ IsOpen
    (⇑(ConcreteCategory.hom (U i).inclusion') ''
      (⇑(ConcreteCategory.hom (U i).inclusion') ⁻¹' (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s)))

Proof state:
case h.e'_3.h
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
e_1✝ : ↑((Opens.toTopCat (of α)).obj (U i)) = ↑((ofOpenSubsets U).U i)
⊢ ⇑(ConcreteCategory.hom (U i).inclusion') ⁻¹' (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s) =
    ⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s

Tactic:
rw [← ι_fromOpenSubsetsGlue, coe_comp, Set.preimage_comp]

Result:
case h.e'_3.h
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
e_1✝ : ↑((Opens.toTopCat (of α)).obj (U i)) = ↑((ofOpenSubsets U).U i)
⊢ ⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹'
      (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) ⁻¹' (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s)) =
    ⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s

Proof state:
case right.left
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
⊢ IsOpen
    (⇑(ConcreteCategory.hom (U i).inclusion') ''
      (⇑(ConcreteCategory.hom (U i).inclusion') ⁻¹' (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s)))

Tactic:
apply (Opens.isOpenEmbedding (X := TopCat.of α) (U i)).isOpenMap

Result:
case right.left.a
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
⊢ IsOpen (⇑(ConcreteCategory.hom (U i).inclusion') ⁻¹' (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s))

Proof state:
case intro.intro.intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
⊢ ∃ t ⊆ ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s,
    IsOpen t ∧
      (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩) ∈ t

Tactic:
use fromOpenSubsetsGlue U '' s ∩ Set.range (@Opens.inclusion' (TopCat.of α) (U i))

Result:
case h
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
⊢ ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∩ Set.range ⇑(ConcreteCategory.hom (U i).inclusion') ⊆
      ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∧
    IsOpen (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∩ Set.range ⇑(ConcreteCategory.hom (U i).inclusion')) ∧
      (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩) ∈
        ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∩ Set.range ⇑(ConcreteCategory.hom (U i).inclusion')

Proof state:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
⊢ ∀ x ∈ ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s,
    ∃ t ⊆ ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s, IsOpen t ∧ x ∈ t

Tactic:
rintro _ ⟨x, hx, rfl⟩

Result:
case intro.intro
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
x : ↑(ofOpenSubsets U).glued
hx : x ∈ s
⊢ ∃ t ⊆ ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s,
    IsOpen t ∧ (ConcreteCategory.hom (fromOpenSubsetsGlue U)) x ∈ t

Proof state:
case h
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
⊢ ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∩ Set.range ⇑(ConcreteCategory.hom (U i).inclusion') ⊆
      ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∧
    IsOpen (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∩ Set.range ⇑(ConcreteCategory.hom (U i).inclusion')) ∧
      (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩) ∈
        ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∩ Set.range ⇑(ConcreteCategory.hom (U i).inclusion')

Tactic:
use Set.inter_subset_left

Result:
case right
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
⊢ IsOpen (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∩ Set.range ⇑(ConcreteCategory.hom (U i).inclusion')) ∧
    (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩) ∈
      ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∩ Set.range ⇑(ConcreteCategory.hom (U i).inclusion')