case intro
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
⊢ IsOpen s ↔ ∀ (f : (a : ι) → π a), f ∈ s → ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ Set.pi univ u ⊆ s
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
⊢ IsOpen s ↔ ∀ (f : (a : ι) → π a), f ∈ s → ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ Set.pi univ u ⊆ s
cases nonempty_fintype ι
case intro
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
⊢ (∀ (a : (a : ι) → π a), a ∈ s → 𝓝 a ≤ 𝓟 s) ↔
    ∀ (f : (a : ι) → π a), f ∈ s → ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ Set.pi univ u ⊆ s
case intro
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
⊢ IsOpen s ↔ ∀ (f : (a : ι) → π a), f ∈ s → ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ Set.pi univ u ⊆ s
rw [isOpen_iff_nhds]
case intro
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
⊢ (∀ (a : (a : ι) → π a), a ∈ s → ∃ I t, (∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1) ∧ Set.pi (↑I) t ⊆ s) ↔
    ∀ (f : (a : ι) → π a), f ∈ s → ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ Set.pi univ u ⊆ s
case intro
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
⊢ (∀ (a : (a : ι) → π a), a ∈ s → 𝓝 a ≤ 𝓟 s) ↔
    ∀ (f : (a : ι) → π a), f ∈ s → ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ Set.pi univ u ⊆ s
simp_rw [le_principal_iff, nhds_pi, Filter.mem_pi', mem_nhds_iff]
case intro.refine_1
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
⊢ (∃ I t, (∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1) ∧ Set.pi (↑I) t ⊆ s) →
    ∃ u, (∀ (a_2 : ι), IsOpen (u a_2) ∧ a a_2 ∈ u a_2) ∧ Set.pi univ u ⊆ s

case intro.refine_2
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
⊢ (∃ u, (∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi univ u ⊆ s) →
    ∃ I t, (∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1) ∧ Set.pi (↑I) t ⊆ s
case intro
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
⊢ (∀ (a : (a : ι) → π a), a ∈ s → ∃ I t, (∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1) ∧ Set.pi (↑I) t ⊆ s) ↔
    ∀ (f : (a : ι) → π a), f ∈ s → ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ Set.pi univ u ⊆ s
refine ball_congr fun a _ => ⟨?_, ?_⟩
case intro.refine_1.intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1
h2 : Set.pi (↑I) t ⊆ s
⊢ ∃ u, (∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi univ u ⊆ s
case intro.refine_1
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
⊢ (∃ I t, (∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1) ∧ Set.pi (↑I) t ⊆ s) →
    ∃ u, (∀ (a_2 : ι), IsOpen (u a_2) ∧ a a_2 ∈ u a_2) ∧ Set.pi univ u ⊆ s
rintro ⟨I, t, ⟨h1, h2⟩⟩
case intro.refine_1.intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1
h2 : Set.pi (↑I) t ⊆ s
⊢ (Set.pi univ fun i => t i) ⊆ Set.pi (↑I) t
case intro.refine_1.intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1
h2 : Set.pi (↑I) t ⊆ s
⊢ ∃ u, (∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi univ u ⊆ s
refine
  ⟨fun i => (h1 i).choose,
    ⟨fun i => (h1 i).choose_spec.2,
      (Set.pi_mono fun i _ => (h1 i).choose_spec.1).trans (Subset.trans ?_ h2)⟩⟩
case intro.refine_1.intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1
h2 : Set.pi (↑I) t ⊆ s
⊢ ((Set.pi ↑I fun i => t i) ∩ Set.pi (↑Iᶜ) fun i => t i) ⊆ Set.pi (↑I) t
case intro.refine_1.intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1
h2 : Set.pi (↑I) t ⊆ s
⊢ (Set.pi univ fun i => t i) ⊆ Set.pi (↑I) t
rw [← Set.pi_inter_compl (I : Set ι)]
no goals
case intro.refine_1.intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1
h2 : Set.pi (↑I) t ⊆ s
⊢ ((Set.pi ↑I fun i => t i) ∩ Set.pi (↑Iᶜ) fun i => t i) ⊆ Set.pi (↑I) t
exact inter_subset_left _ _
no goals
case intro.refine_2
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
⊢ (∃ u, (∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi univ u ⊆ s) →
    ∃ I t, (∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1) ∧ Set.pi (↑I) t ⊆ s
exact fun ⟨u, ⟨h1, _⟩⟩ =>
  ⟨Finset.univ, u, ⟨fun i => ⟨u i, ⟨rfl.subset, h1 i⟩⟩, by rwa [Finset.coe_univ]⟩⟩
no goals
α : Type u
β : Type v
γ : Type ?u.254008
δ : Type ?u.254011
ε : Type ?u.254014
ζ : Type ?u.254017
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.254028
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝¹ : a ∈ s
x✝ : ∃ u, (∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi univ u ⊆ s
u : (a : ι) → Set (π a)
h1 : ∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1
right✝ : Set.pi univ u ⊆ s
⊢ Set.pi (↑Finset.univ) u ⊆ s
rwa [Finset.coe_univ]