case refine'_1
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
⊢ ∀ (u : Set (α × β)), u ∈ image2 (fun x x_1 => x ×ˢ x_1) B₁ B₂ → IsOpen u

case refine'_2
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
⊢ ∀ (a : α × β) (u : Set (α × β)), a ∈ u → IsOpen u → ∃ v, v ∈ image2 (fun x x_1 => x ×ˢ x_1) B₁ B₂ ∧ a ∈ v ∧ v ⊆ u
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
⊢ IsTopologicalBasis (image2 (fun x x_1 => x ×ˢ x_1) B₁ B₂)
refine' isTopologicalBasis_of_open_of_nhds _ _
case refine'_1.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
u₁ : Set α
u₂ : Set β
hu₁ : u₁ ∈ B₁
hu₂ : u₂ ∈ B₂
⊢ IsOpen ((fun x x_1 => x ×ˢ x_1) u₁ u₂)
case refine'_1
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
⊢ ∀ (u : Set (α × β)), u ∈ image2 (fun x x_1 => x ×ˢ x_1) B₁ B₂ → IsOpen u
rintro _ ⟨u₁, u₂, hu₁, hu₂, rfl⟩
no goals
case refine'_1.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
u₁ : Set α
u₂ : Set β
hu₁ : u₁ ∈ B₁
hu₂ : u₂ ∈ B₂
⊢ IsOpen ((fun x x_1 => x ×ˢ x_1) u₁ u₂)
exact (h₁.isOpen hu₁).prod (h₂.isOpen hu₂)
case refine'_2.mk
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : α
b : β
u : Set (α × β)
hu : (a, b) ∈ u
uo : IsOpen u
⊢ ∃ v, v ∈ image2 (fun x x_1 => x ×ˢ x_1) B₁ B₂ ∧ (a, b) ∈ v ∧ v ⊆ u
case refine'_2
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
⊢ ∀ (a : α × β) (u : Set (α × β)), a ∈ u → IsOpen u → ∃ v, v ∈ image2 (fun x x_1 => x ×ˢ x_1) B₁ B₂ ∧ a ∈ v ∧ v ⊆ u
rintro ⟨a, b⟩ u hu uo
case refine'_2.mk.intro.mk.intro.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : α
b : β
u : Set (α × β)
hu✝ : (a, b) ∈ u
uo : IsOpen u
s : Set α
t : Set β
hu : (s, t).fst ×ˢ (s, t).snd ⊆ u
hs : (s, t).fst ∈ B₁
ha : a ∈ (s, t).fst
ht : (s, t).snd ∈ B₂
hb : b ∈ (s, t).snd
⊢ ∃ v, v ∈ image2 (fun x x_1 => x ×ˢ x_1) B₁ B₂ ∧ (a, b) ∈ v ∧ v ⊆ u
case refine'_2.mk
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : α
b : β
u : Set (α × β)
hu : (a, b) ∈ u
uo : IsOpen u
⊢ ∃ v, v ∈ image2 (fun x x_1 => x ×ˢ x_1) B₁ B₂ ∧ (a, b) ∈ v ∧ v ⊆ u
rcases(h₁.nhds_hasBasis.prod_nhds h₂.nhds_hasBasis).mem_iff.1 (IsOpen.mem_nhds uo hu) with
  ⟨⟨s, t⟩, ⟨⟨hs, ha⟩, ht, hb⟩, hu⟩
no goals
case refine'_2.mk.intro.mk.intro.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : α
b : β
u : Set (α × β)
hu✝ : (a, b) ∈ u
uo : IsOpen u
s : Set α
t : Set β
hu : (s, t).fst ×ˢ (s, t).snd ⊆ u
hs : (s, t).fst ∈ B₁
ha : a ∈ (s, t).fst
ht : (s, t).snd ∈ B₂
hb : b ∈ (s, t).snd
⊢ ∃ v, v ∈ image2 (fun x x_1 => x ×ˢ x_1) B₁ B₂ ∧ (a, b) ∈ v ∧ v ⊆ u
exact ⟨s ×ˢ t, mem_image2_of_mem hs ht, ⟨ha, hb⟩, hu⟩