-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.sum {s : Set (Set α)} (hs : IsTopologicalBasis s) {t : Set (Set β)}
    (ht : IsTopologicalBasis t) :
    IsTopologicalBasis ((fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t)

Proof state:
case h_nhds.inl
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen u
⊢ ∃ v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t, Sum.inl x ∈ v ∧ v ⊆ u

Tactic:
obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ s, x ∈ v ∧ v ⊆ Sum.inl ⁻¹' u :=
  hs.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).1

Result:
case h_nhds.inl.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen u
v : Set α
vs : v ∈ s
xv : x ∈ v
vu : v ⊆ Sum.inl ⁻¹' u
⊢ ∃ v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t, Sum.inl x ∈ v ∧ v ⊆ u

Proof state:
case h_nhds.inr.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen u
v : Set β
vs : v ∈ t
xv : x ∈ v
vu : v ⊆ Sum.inr ⁻¹' u
⊢ ∃ v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t, Sum.inr x ∈ v ∧ v ⊆ u

Tactic:
exact ⟨Sum.inr '' v, mem_union_right _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
  image_subset_iff.2 vu⟩

Result:
no goals

Proof state:
case h_open
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ ∀ u ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t, IsOpen u

Tactic:
rintro u (⟨w, hw, rfl⟩ | ⟨w, hw, rfl⟩)

Result:
case h_open.inl.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
w : Set α
hw : w ∈ s
⊢ IsOpen ((fun u => Sum.inl '' u) w)

case h_open.inr.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
w : Set β
hw : w ∈ t
⊢ IsOpen ((fun u => Sum.inr '' u) w)

Proof state:
case h_nhds.inr
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen u
⊢ ∃ v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t, Sum.inr x ∈ v ∧ v ⊆ u

Tactic:
obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ t, x ∈ v ∧ v ⊆ Sum.inr ⁻¹' u :=
  ht.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).2

Result:
case h_nhds.inr.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen u
v : Set β
vs : v ∈ t
xv : x ∈ v
vu : v ⊆ Sum.inr ⁻¹' u
⊢ ∃ v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t, Sum.inr x ∈ v ∧ v ⊆ u

Proof state:
case h_open.inl.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
w : Set α
hw : w ∈ s
⊢ IsOpen ((fun u => Sum.inl '' u) w)

Tactic:
exact IsOpenEmbedding.inl.isOpenMap w (hs.isOpen hw)

Result:
no goals

Proof state:
case h_open.inr.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
w : Set β
hw : w ∈ t
⊢ IsOpen ((fun u => Sum.inr '' u) w)

Tactic:
exact IsOpenEmbedding.inr.isOpenMap w (ht.isOpen hw)

Result:
no goals

Proof state:
case h_nhds.inl.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen u
v : Set α
vs : v ∈ s
xv : x ∈ v
vu : v ⊆ Sum.inl ⁻¹' u
⊢ ∃ v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t, Sum.inl x ∈ v ∧ v ⊆ u

Tactic:
exact ⟨Sum.inl '' v, mem_union_left _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
  image_subset_iff.2 vu⟩

Result:
no goals

Proof state:
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ IsTopologicalBasis ((fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t)

Tactic:
apply isTopologicalBasis_of_isOpen_of_nhds

Result:
case h_open
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ ∀ u ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t, IsOpen u

case h_nhds
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ ∀ (a : α ⊕ β) (u : Set (α ⊕ β)),
    a ∈ u → IsOpen u → ∃ v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t, a ∈ v ∧ v ⊆ u

Proof state:
case h_nhds
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ ∀ (a : α ⊕ β) (u : Set (α ⊕ β)),
    a ∈ u → IsOpen u → ∃ v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t, a ∈ v ∧ v ⊆ u

Tactic:
rintro (x | x) u hxu u_open

Result:
case h_nhds.inl
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen u
⊢ ∃ v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t, Sum.inl x ∈ v ∧ v ⊆ u

case h_nhds.inr
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen u
⊢ ∃ v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t, Sum.inr x ∈ v ∧ v ⊆ u