-- Mathlib/Topology/Gluing.lean
theorem range_fromOpenSubsetsGlue : Set.range (fromOpenSubsetsGlue U) = ⋃ i, (U i : Set α)

Proof state:
case h.mp.intro
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x : ↑(ofOpenSubsets U).glued
⊢ (ConcreteCategory.hom (fromOpenSubsetsGlue U)) x ∈ ⋃ i, ↑(U i)

Tactic:
obtain ⟨i, ⟨x, hx'⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x

Result:
case h.mp.intro.intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
⊢ (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩) ∈ ⋃ i, ↑(U i)

Proof state:
case h.mp
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
⊢ x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) → x✝ ∈ ⋃ i, ↑(U i)

Tactic:
rintro ⟨x, rfl⟩

Result:
case h.mp.intro
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x : ↑(ofOpenSubsets U).glued
⊢ (ConcreteCategory.hom (fromOpenSubsetsGlue U)) x ∈ ⋃ i, ↑(U i)

Proof state:
case h.mpr.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x : ↑(of α)
i : J
hx : x ∈ (fun i => ↑(U i)) i
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Tactic:
exact ⟨(ofOpenSubsets U).toGlueData.ι i ⟨x, hx⟩, ι_fromOpenSubsetsGlue_apply _ _ _⟩

Result:
no goals

Proof state:
case h.mpr.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
i : J
hx : x✝ ∈ (fun i => ↑(U i)) i
⊢ x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Tactic:
rename_i x

Result:
case h.mpr.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x : ↑(of α)
i : J
hx : x ∈ (fun i => ↑(U i)) i
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Proof state:
case h.mp.intro.intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
⊢ (U i).inclusion' ⟨x, hx'⟩ ∈ ⋃ i, ↑(U i)

Tactic:
exact Set.subset_iUnion _ i hx'

Result:
no goals

Proof state:
case h.mp.intro.intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
⊢ (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩) ∈ ⋃ i, ↑(U i)

Tactic:
rw [ι_fromOpenSubsetsGlue_apply]

Result:
case h.mp.intro.intro.intro.mk
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
⊢ (U i).inclusion' ⟨x, hx'⟩ ∈ ⋃ i, ↑(U i)

Proof state:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
⊢ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) = ⋃ i, ↑(U i)

Tactic:
ext

Result:
case h
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
⊢ x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) ↔ x✝ ∈ ⋃ i, ↑(U i)

Proof state:
case h.mpr
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
⊢ x✝ ∈ ⋃ i, ↑(U i) → x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Tactic:
rintro ⟨_, ⟨i, rfl⟩, hx⟩

Result:
case h.mpr.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
i : J
hx : x✝ ∈ (fun i => ↑(U i)) i
⊢ x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Proof state:
case h
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
⊢ x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) ↔ x✝ ∈ ⋃ i, ↑(U i)

Tactic:
constructor

Result:
case h.mp
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
⊢ x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) → x✝ ∈ ⋃ i, ↑(U i)

case h.mpr
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
⊢ x✝ ∈ ⋃ i, ↑(U i) → x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))