case refine'_1
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
⊢ pure ≤ traverse 𝓝

case refine'_2
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
⊢ ∀ (a : List α) (s : Set (List α)),
    s ∈ traverse 𝓝 a → ∃ t, t ∈ traverse 𝓝 a ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
⊢ 𝓝 as = traverse 𝓝 as
refine' nhds_mkOfNhds _ _ _ _
case refine'_1
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as l : List α
⊢ pure l ≤ traverse 𝓝 l
case refine'_1
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
⊢ pure ≤ traverse 𝓝
intro l
case refine'_1.nil
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
⊢ pure [] ≤ traverse 𝓝 []

case refine'_1.cons
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
head✝ : α
tail✝ : List α
tail_ih✝ : pure tail✝ ≤ traverse 𝓝 tail✝
⊢ pure (head✝ :: tail✝) ≤ traverse 𝓝 (head✝ :: tail✝)
case refine'_1
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as l : List α
⊢ pure l ≤ traverse 𝓝 l
induction l
case refine'_1.cons
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
head✝ : α
tail✝ : List α
tail_ih✝ : pure tail✝ ≤ traverse 𝓝 tail✝
⊢ pure (head✝ :: tail✝) ≤ traverse 𝓝 (head✝ :: tail✝)
case refine'_1.nil
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
⊢ pure [] ≤ traverse 𝓝 []

case refine'_1.cons
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
head✝ : α
tail✝ : List α
tail_ih✝ : pure tail✝ ≤ traverse 𝓝 tail✝
⊢ pure (head✝ :: tail✝) ≤ traverse 𝓝 (head✝ :: tail✝)
case nil => exact le_rfl
no goals
case refine'_1.cons
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
head✝ : α
tail✝ : List α
tail_ih✝ : pure tail✝ ≤ traverse 𝓝 tail✝
⊢ pure (head✝ :: tail✝) ≤ traverse 𝓝 (head✝ :: tail✝)
case cons a l ih =>
  suffices List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l by
    simpa only [functor_norm] using this
  exact Filter.seq_mono (Filter.map_mono <| pure_le_nhds a) ih
no goals
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
⊢ pure [] ≤ traverse 𝓝 []
exact le_rfl
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
a : α
l : List α
ih : pure l ≤ traverse 𝓝 l
⊢ (Seq.seq (List.cons <$> pure a) fun x => pure l) ≤ Seq.seq (List.cons <$> 𝓝 a) fun x => traverse 𝓝 l
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
a : α
l : List α
ih : pure l ≤ traverse 𝓝 l
⊢ pure (a :: l) ≤ traverse 𝓝 (a :: l)
suffices List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l by
  simpa only [functor_norm] using this
no goals
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
a : α
l : List α
ih : pure l ≤ traverse 𝓝 l
⊢ (Seq.seq (List.cons <$> pure a) fun x => pure l) ≤ Seq.seq (List.cons <$> 𝓝 a) fun x => traverse 𝓝 l
exact Filter.seq_mono (Filter.map_mono <| pure_le_nhds a) ih
no goals
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
a : α
l : List α
ih : pure l ≤ traverse 𝓝 l
this : (Seq.seq (List.cons <$> pure a) fun x => pure l) ≤ Seq.seq (List.cons <$> 𝓝 a) fun x => traverse 𝓝 l
⊢ pure (a :: l) ≤ traverse 𝓝 (a :: l)
simpa only [functor_norm] using this
case refine'_2
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as l : List α
s : Set (List α)
hs : s ∈ traverse 𝓝 l
⊢ ∃ t, t ∈ traverse 𝓝 l ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
case refine'_2
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
⊢ ∀ (a : List α) (s : Set (List α)),
    s ∈ traverse 𝓝 a → ∃ t, t ∈ traverse 𝓝 a ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
intro l s hs
case refine'_2.intro.intro
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as l : List α
s : Set (List α)
hs : s ∈ traverse 𝓝 l
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
⊢ ∃ t, t ∈ traverse 𝓝 l ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
case refine'_2
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as l : List α
s : Set (List α)
hs : s ∈ traverse 𝓝 l
⊢ ∃ t, t ∈ traverse 𝓝 l ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
rcases(mem_traverse_iff _ _).1 hs with ⟨u, hu, hus⟩
case refine'_2.intro.intro
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
⊢ ∃ t, t ∈ traverse 𝓝 l ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
case refine'_2.intro.intro
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as l : List α
s : Set (List α)
hs : s ∈ traverse 𝓝 l
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
⊢ ∃ t, t ∈ traverse 𝓝 l ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
clear as hs
case this
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
⊢ ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v ∧ sequence v ⊆ s

case refine'_2.intro.intro
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
this : ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v ∧ sequence v ⊆ s
⊢ ∃ t, t ∈ traverse 𝓝 l ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
case refine'_2.intro.intro
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
⊢ ∃ t, t ∈ traverse 𝓝 l ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
have : ∃ v : List (Set α), l.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) v ∧ sequence v ⊆ s
case this.nil
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
⊢ ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) [] v ∧ sequence v ⊆ s

case this.cons
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
u : List (Set α)
a✝² : α
b✝ : Set α
l₁✝ : List α
l₂✝ : List (Set α)
a✝¹ : b✝ ∈ 𝓝 a✝²
a✝ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l₁✝ l₂✝
a_ih✝ : ∀ (s : Set (List α)), sequence l₂✝ ⊆ s → ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l₁✝ v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (b✝ :: l₂✝) ⊆ s
⊢ ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) (a✝² :: l₁✝) v ∧ sequence v ⊆ s

case refine'_2.intro.intro
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
this : ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v ∧ sequence v ⊆ s
⊢ ∃ t, t ∈ traverse 𝓝 l ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
case this
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
⊢ ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v ∧ sequence v ⊆ s

case refine'_2.intro.intro
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
this : ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v ∧ sequence v ⊆ s
⊢ ∃ t, t ∈ traverse 𝓝 l ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
induction hu generalizing s
case this.cons
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
u : List (Set α)
a✝² : α
b✝ : Set α
l₁✝ : List α
l₂✝ : List (Set α)
a✝¹ : b✝ ∈ 𝓝 a✝²
a✝ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l₁✝ l₂✝
a_ih✝ : ∀ (s : Set (List α)), sequence l₂✝ ⊆ s → ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l₁✝ v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (b✝ :: l₂✝) ⊆ s
⊢ ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) (a✝² :: l₁✝) v ∧ sequence v ⊆ s

case refine'_2.intro.intro
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
this : ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v ∧ sequence v ⊆ s
⊢ ∃ t, t ∈ traverse 𝓝 l ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
case this.nil
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
⊢ ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) [] v ∧ sequence v ⊆ s

case this.cons
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
u : List (Set α)
a✝² : α
b✝ : Set α
l₁✝ : List α
l₂✝ : List (Set α)
a✝¹ : b✝ ∈ 𝓝 a✝²
a✝ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l₁✝ l₂✝
a_ih✝ : ∀ (s : Set (List α)), sequence l₂✝ ⊆ s → ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l₁✝ v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (b✝ :: l₂✝) ⊆ s
⊢ ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) (a✝² :: l₁✝) v ∧ sequence v ⊆ s

case refine'_2.intro.intro
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
this : ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v ∧ sequence v ⊆ s
⊢ ∃ t, t ∈ traverse 𝓝 l ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
case nil _hs  =>
  exists []
  simp only [List.forall₂_nil_left_iff, exists_eq_left]
  exact ⟨trivial, hus⟩
case refine'_2.intro.intro
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
this : ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v ∧ sequence v ⊆ s
⊢ ∃ t, t ∈ traverse 𝓝 l ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
case this.cons
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
u : List (Set α)
a✝² : α
b✝ : Set α
l₁✝ : List α
l₂✝ : List (Set α)
a✝¹ : b✝ ∈ 𝓝 a✝²
a✝ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l₁✝ l₂✝
a_ih✝ : ∀ (s : Set (List α)), sequence l₂✝ ⊆ s → ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l₁✝ v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (b✝ :: l₂✝) ⊆ s
⊢ ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) (a✝² :: l₁✝) v ∧ sequence v ⊆ s

case refine'_2.intro.intro
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
this : ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v ∧ sequence v ⊆ s
⊢ ∃ t, t ∈ traverse 𝓝 l ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
case cons a s as ss hts h ht _ ih =>
  rcases mem_nhds_iff.1 ht with ⟨u, hut, hu⟩
  rcases ih _ Subset.rfl with ⟨v, hv, hvss⟩
  exact
    ⟨u::v, List.Forall₂.cons hu hv,
      Subset.trans (Set.seq_mono (Set.image_subset _ hut) hvss) hus⟩
case refine'_2.intro.intro.intro.intro
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
⊢ ∃ t, t ∈ traverse 𝓝 l ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
case refine'_2.intro.intro
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
this : ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v ∧ sequence v ⊆ s
⊢ ∃ t, t ∈ traverse 𝓝 l ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
rcases this with ⟨v, hv, hvs⟩
case refine'_2.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
⊢ List.Forall₂ (fun b c => id c ∈ 𝓝 b) l v

case refine'_2.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
⊢ ∀ (a' : List α), a' ∈ sequence v → s ∈ traverse 𝓝 a'
case refine'_2.intro.intro.intro.intro
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
⊢ ∃ t, t ∈ traverse 𝓝 l ∧ t ⊆ s ∧ ∀ (a' : List α), a' ∈ t → s ∈ traverse 𝓝 a'
refine' ⟨sequence v, mem_traverse _ _ _, hvs, _⟩
α : Type u_1
β : Type ?u.219
inst✝ : TopologicalSpace α
_hs : TopologicalSpace β
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
⊢ List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) [] [] ∧ sequence [] ⊆ s
α : Type u_1
β : Type ?u.219
inst✝ : TopologicalSpace α
_hs : TopologicalSpace β
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
⊢ ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) [] v ∧ sequence v ⊆ s
exists []
α : Type u_1
β : Type ?u.219
inst✝ : TopologicalSpace α
_hs : TopologicalSpace β
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
⊢ True ∧ sequence [] ⊆ s
α : Type u_1
β : Type ?u.219
inst✝ : TopologicalSpace α
_hs : TopologicalSpace β
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
⊢ List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) [] [] ∧ sequence [] ⊆ s
simp only [List.forall₂_nil_left_iff, exists_eq_left]
no goals
α : Type u_1
β : Type ?u.219
inst✝ : TopologicalSpace α
_hs : TopologicalSpace β
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
⊢ True ∧ sequence [] ⊆ s
exact ⟨trivial, hus⟩
case intro.intro
α : Type u_1
β : Type ?u.219
a : TopologicalSpace α
s✝ : TopologicalSpace β
l : List α
u✝ : List (Set α)
as : α
ss : Set α
hts : List α
h : List (Set α)
ht : ss ∈ 𝓝 as
a✝ : List.Forall₂ (fun b s => s ∈ 𝓝 b) hts h
ih : ∀ (s : Set (List α)), sequence h ⊆ s → ∃ v, List.Forall₂ (fun a_1 s => IsOpen s ∧ a_1 ∈ s) hts v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (ss :: h) ⊆ s
u : Set α
hut : u ⊆ ss
hu : IsOpen u ∧ as ∈ u
⊢ ∃ v, List.Forall₂ (fun a_1 s => IsOpen s ∧ a_1 ∈ s) (as :: hts) v ∧ sequence v ⊆ s
α : Type u_1
β : Type ?u.219
a : TopologicalSpace α
s✝ : TopologicalSpace β
l : List α
u : List (Set α)
as : α
ss : Set α
hts : List α
h : List (Set α)
ht : ss ∈ 𝓝 as
a✝ : List.Forall₂ (fun b s => s ∈ 𝓝 b) hts h
ih : ∀ (s : Set (List α)), sequence h ⊆ s → ∃ v, List.Forall₂ (fun a_1 s => IsOpen s ∧ a_1 ∈ s) hts v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (ss :: h) ⊆ s
⊢ ∃ v, List.Forall₂ (fun a_1 s => IsOpen s ∧ a_1 ∈ s) (as :: hts) v ∧ sequence v ⊆ s
rcases mem_nhds_iff.1 ht with ⟨u, hut, hu⟩
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.219
a : TopologicalSpace α
s✝ : TopologicalSpace β
l : List α
u✝ : List (Set α)
as : α
ss : Set α
hts : List α
h : List (Set α)
ht : ss ∈ 𝓝 as
a✝ : List.Forall₂ (fun b s => s ∈ 𝓝 b) hts h
ih : ∀ (s : Set (List α)), sequence h ⊆ s → ∃ v, List.Forall₂ (fun a_1 s => IsOpen s ∧ a_1 ∈ s) hts v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (ss :: h) ⊆ s
u : Set α
hut : u ⊆ ss
hu : IsOpen u ∧ as ∈ u
v : List (Set α)
hv : List.Forall₂ (fun a_1 s => IsOpen s ∧ a_1 ∈ s) hts v
hvss : sequence v ⊆ sequence h
⊢ ∃ v, List.Forall₂ (fun a_1 s => IsOpen s ∧ a_1 ∈ s) (as :: hts) v ∧ sequence v ⊆ s
case intro.intro
α : Type u_1
β : Type ?u.219
a : TopologicalSpace α
s✝ : TopologicalSpace β
l : List α
u✝ : List (Set α)
as : α
ss : Set α
hts : List α
h : List (Set α)
ht : ss ∈ 𝓝 as
a✝ : List.Forall₂ (fun b s => s ∈ 𝓝 b) hts h
ih : ∀ (s : Set (List α)), sequence h ⊆ s → ∃ v, List.Forall₂ (fun a_1 s => IsOpen s ∧ a_1 ∈ s) hts v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (ss :: h) ⊆ s
u : Set α
hut : u ⊆ ss
hu : IsOpen u ∧ as ∈ u
⊢ ∃ v, List.Forall₂ (fun a_1 s => IsOpen s ∧ a_1 ∈ s) (as :: hts) v ∧ sequence v ⊆ s
rcases ih _ Subset.rfl with ⟨v, hv, hvss⟩
no goals
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.219
a : TopologicalSpace α
s✝ : TopologicalSpace β
l : List α
u✝ : List (Set α)
as : α
ss : Set α
hts : List α
h : List (Set α)
ht : ss ∈ 𝓝 as
a✝ : List.Forall₂ (fun b s => s ∈ 𝓝 b) hts h
ih : ∀ (s : Set (List α)), sequence h ⊆ s → ∃ v, List.Forall₂ (fun a_1 s => IsOpen s ∧ a_1 ∈ s) hts v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (ss :: h) ⊆ s
u : Set α
hut : u ⊆ ss
hu : IsOpen u ∧ as ∈ u
v : List (Set α)
hv : List.Forall₂ (fun a_1 s => IsOpen s ∧ a_1 ∈ s) hts v
hvss : sequence v ⊆ sequence h
⊢ ∃ v, List.Forall₂ (fun a_1 s => IsOpen s ∧ a_1 ∈ s) (as :: hts) v ∧ sequence v ⊆ s
exact
  ⟨u::v, List.Forall₂.cons hu hv,
    Subset.trans (Set.seq_mono (Set.image_subset _ hut) hvss) hus⟩
no goals
case refine'_2.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
⊢ List.Forall₂ (fun b c => id c ∈ 𝓝 b) l v
exact hv.imp fun a s ⟨hs, ha⟩ => IsOpen.mem_nhds hs ha
case refine'_2.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
u : List α
hu : u ∈ sequence v
⊢ s ∈ traverse 𝓝 u
case refine'_2.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
⊢ ∀ (a' : List α), a' ∈ sequence v → s ∈ traverse 𝓝 a'
intro u hu
case refine'_2.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a => b ∈ id a) u v
⊢ s ∈ traverse 𝓝 u
case refine'_2.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
u : List α
hu : u ∈ sequence v
⊢ s ∈ traverse 𝓝 u
have hu := (List.mem_traverse _ _).1 hu
case refine'_2.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a => b ∈ id a) u v
this : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) u v
⊢ s ∈ traverse 𝓝 u
case refine'_2.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a => b ∈ id a) u v
⊢ s ∈ traverse 𝓝 u
have : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) u v := by
  refine' List.Forall₂.flip _
  replace hv := hv.flip
  simp only [List.forall₂_and_left, flip] at hv⊢
  exact ⟨hv.1, hu.flip⟩
case refine'_2.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a => b ∈ id a) u v
this : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) u v
⊢ sequence v ∈ traverse 𝓝 u
case refine'_2.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a => b ∈ id a) u v
this : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) u v
⊢ s ∈ traverse 𝓝 u
refine' mem_of_superset _ hvs
no goals
case refine'_2.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a => b ∈ id a) u v
this : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) u v
⊢ sequence v ∈ traverse 𝓝 u
exact mem_traverse _ _ (this.imp fun a s ⟨hs, ha⟩ => IsOpen.mem_nhds hs ha)
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a => b ∈ id a) u v
⊢ List.Forall₂ (flip fun a s => IsOpen s ∧ a ∈ s) v u
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a => b ∈ id a) u v
⊢ List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) u v
refine' List.Forall₂.flip _
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hvs : sequence v ⊆ s
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a => b ∈ id a) u v
hv : List.Forall₂ (fun s a => IsOpen s ∧ a ∈ s) v l
⊢ List.Forall₂ (flip fun a s => IsOpen s ∧ a ∈ s) v u
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a => b ∈ id a) u v
⊢ List.Forall₂ (flip fun a s => IsOpen s ∧ a ∈ s) v u
replace hv := hv.flip
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hvs : sequence v ⊆ s
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a => b ∈ id a) u v
hv : (∀ (a : Set α), a ∈ v → IsOpen a) ∧ List.Forall₂ (fun a b => b ∈ a) v l
⊢ (∀ (a : Set α), a ∈ v → IsOpen a) ∧ List.Forall₂ (fun a b => b ∈ a) v u
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hvs : sequence v ⊆ s
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a => b ∈ id a) u v
hv : List.Forall₂ (fun s a => IsOpen s ∧ a ∈ s) v l
⊢ List.Forall₂ (flip fun a s => IsOpen s ∧ a ∈ s) v u
simp only [List.forall₂_and_left, flip] at hv⊢
no goals
α : Type u_1
β : Type ?u.219
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hvs : sequence v ⊆ s
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a => b ∈ id a) u v
hv : (∀ (a : Set α), a ∈ v → IsOpen a) ∧ List.Forall₂ (fun a b => b ∈ a) v l
⊢ (∀ (a : Set α), a ∈ v → IsOpen a) ∧ List.Forall₂ (fun a b => b ∈ a) v u
exact ⟨hv.1, hu.flip⟩