-- Mathlib/Topology/List.lean
theorem nhds_list (as : List α) : 𝓝 as = traverse 𝓝 as

Proof state:
case cons.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
u✝ : List (Set α)
a✝¹ : α
b✝ : Set α
l₁✝ : List α
l₂✝ : List (Set α)
ht : b✝ ∈ 𝓝 a✝¹
a✝ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l₁✝ l₂✝
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
u : Set α
hut : u ⊆ b✝
hu : IsOpen u ∧ a✝¹ ∈ u
⊢ ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) (a✝¹ :: l₁✝) v ∧ sequence v ⊆ s

Tactic:
rcases ih _ Subset.rfl with ⟨v, hv, hvss⟩

Result:
case cons.intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
u✝ : List (Set α)
a✝¹ : α
b✝ : Set α
l₁✝ : List α
l₂✝ : List (Set α)
ht : b✝ ∈ 𝓝 a✝¹
a✝ : List.Forall₂ (fun b s => s ∈ 𝓝 b) l₁✝ l₂✝
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
u : Set α
hut : u ⊆ b✝
hu : IsOpen u ∧ a✝¹ ∈ u
v : List (Set α)
hv : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) l₁✝ v
hvss : sequence v ⊆ sequence l₂✝
⊢ ∃ v, List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) (a✝¹ :: l₁✝) v ∧ sequence v ⊆ s

Proof state:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
as l : List α
⊢ pure l ≤ traverse 𝓝 l

Tactic:
induction l with
| nil => exact le_rfl
| 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

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
as : List α
⊢ pure ≤ traverse 𝓝

Tactic:
intro l

Result:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
as l : List α
⊢ pure l ≤ traverse 𝓝 l

Proof state:
α : Type u_1
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
this : sequence v ∈ traverse 𝓝 l
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

Tactic:
refine List.Forall₂.flip ?_

Result:
α : Type u_1
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
this : sequence v ∈ traverse 𝓝 l
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

Proof state:
case refine_1.nil
α : Type u_1
inst✝ : TopologicalSpace α
as : List α
⊢ pure [] ≤ traverse 𝓝 []

Tactic:
exact le_rfl

Result:
no goals

Proof state:
α : Type u_1
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
this : sequence v ∈ traverse 𝓝 l
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

Tactic:
replace hv := hv.flip

Result:
α : Type u_1
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
this : sequence v ∈ traverse 𝓝 l
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