[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
⊢ 𝓝 as = traverse 𝓝 as
[PROOFSTEP]
refine' nhds_mkOfNhds _ _ _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
⊢ pure ≤ traverse 𝓝
[PROOFSTEP]
intro l
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as l : List α
⊢ pure l ≤ traverse 𝓝 l
[PROOFSTEP]
induction l
[GOAL]
case refine'_1.nil
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
⊢ pure [] ≤ traverse 𝓝 []
case refine'_1.cons
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
head✝ : α
tail✝ : List α
tail_ih✝ : pure tail✝ ≤ traverse 𝓝 tail✝
⊢ pure (head✝ :: tail✝) ≤ traverse 𝓝 (head✝ :: tail✝)
[PROOFSTEP]
case nil => exact le_rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
⊢ pure [] ≤ traverse 𝓝 []
[PROOFSTEP]
case nil => exact le_rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
⊢ pure [] ≤ traverse 𝓝 []
[PROOFSTEP]
exact le_rfl
[GOAL]
case refine'_1.cons
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
head✝ : α
tail✝ : List α
tail_ih✝ : pure tail✝ ≤ traverse 𝓝 tail✝
⊢ pure (head✝ :: tail✝) ≤ traverse 𝓝 (head✝ :: tail✝)
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
a : α
l : List α
ih : pure l ≤ traverse 𝓝 l
⊢ pure (a :: l) ≤ traverse 𝓝 (a :: l)
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
as : List α
a : α
l : List α
ih : pure l ≤ traverse 𝓝 l
⊢ pure (a :: l) ≤ traverse 𝓝 (a :: l)
[PROOFSTEP]
suffices List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l by simpa only [functor_norm] using this
[GOAL]
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simpa only [functor_norm] using this
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact Filter.seq_mono (Filter.map_mono <| pure_le_nhds a) ih
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
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'
[PROOFSTEP]
intro l s hs
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
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'
[PROOFSTEP]
rcases(mem_traverse_iff _ _).1 hs with ⟨u, hu, hus⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
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'
[PROOFSTEP]
clear as hs
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
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'
[PROOFSTEP]
have : ∃ v : List (Set α), l.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) v ∧ sequence v ⊆ s
[GOAL]
case this
α : Type u_1
β : Type u_2
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_2
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'
[PROOFSTEP]
induction hu generalizing s
[GOAL]
case this.nil
α : Type u_1
β : Type u_2
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_2
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_2
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'
[PROOFSTEP]
case nil _hs =>
  exists []
  simp only [List.forall₂_nil_left_iff, exists_eq_left]
  exact
    ⟨trivial, hus⟩
      -- porting note -- renamed reordered variables based on previous types
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
case nil _hs =>
  exists []
  simp only [List.forall₂_nil_left_iff, exists_eq_left]
  exact
    ⟨trivial, hus⟩
      -- porting note -- renamed reordered variables based on previous types
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exists []
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [List.forall₂_nil_left_iff, exists_eq_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
_hs : TopologicalSpace β
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
⊢ True ∧ sequence [] ⊆ s
[PROOFSTEP]
exact
  ⟨trivial, hus⟩
    -- porting note -- renamed reordered variables based on previous types
[GOAL]
case this.cons
α : Type u_1
β : Type u_2
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_2
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'
[PROOFSTEP]
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⟩
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
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⟩
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rcases mem_nhds_iff.1 ht with ⟨u, hut, hu⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rcases ih _ Subset.rfl with ⟨v, hv, hvss⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact ⟨u :: v, List.Forall₂.cons hu hv, Subset.trans (Set.seq_mono (Set.image_subset _ hut) hvss) hus⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
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'
[PROOFSTEP]
rcases this with ⟨v, hv, hvs⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
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'
[PROOFSTEP]
refine' ⟨sequence v, mem_traverse _ _ _, hvs, _⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact hv.imp fun a s ⟨hs, ha⟩ => IsOpen.mem_nhds hs ha
[GOAL]
case refine'_2.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
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'
[PROOFSTEP]
intro u hu
[GOAL]
case refine'_2.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have hu := (List.mem_traverse _ _).1 hu
[GOAL]
case refine'_2.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
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⟩
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
refine' List.Forall₂.flip _
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
replace hv := hv.flip
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [List.forall₂_and_left, flip] at hv ⊢
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact ⟨hv.1, hu.flip⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
refine' mem_of_superset _ hvs
[GOAL]
case refine'_2.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact mem_traverse _ _ (this.imp fun a s ⟨hs, ha⟩ => IsOpen.mem_nhds hs ha)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ 𝓝 [] = pure []
[PROOFSTEP]
rw [nhds_list, List.traverse_nil _]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
l : List α
⊢ 𝓝 (a :: l) = Seq.seq (List.cons <$> 𝓝 a) fun x => 𝓝 l
[PROOFSTEP]
rw [nhds_list, List.traverse_cons _, ← nhds_list]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
l : List α
⊢ Tendsto (fun p => p.fst :: p.snd) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: l))
[PROOFSTEP]
rw [nhds_cons, Tendsto, Filter.map_prod]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
l : List α
⊢ Filter.seq (Filter.map (fun a b => (a, b).fst :: (a, b).snd) (𝓝 a)) (𝓝 l) ≤ Seq.seq (cons <$> 𝓝 a) fun x => 𝓝 l
[PROOFSTEP]
exact le_rfl
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
⊢ Tendsto f (𝓝 (a :: l)) b ↔ Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) b
[PROOFSTEP]
have : 𝓝 (a :: l) = (𝓝 a ×ˢ 𝓝 l).map fun p : α × List α => p.1 :: p.2 :=
  by
  simp only [nhds_cons, Filter.prod_eq, (Filter.map_def _ _).symm, (Filter.seq_eq_filter_seq _ _).symm]
  simp [-Filter.map_def, (· ∘ ·), functor_norm]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
⊢ 𝓝 (a :: l) = Filter.map (fun p => p.fst :: p.snd) (𝓝 a ×ˢ 𝓝 l)
[PROOFSTEP]
simp only [nhds_cons, Filter.prod_eq, (Filter.map_def _ _).symm, (Filter.seq_eq_filter_seq _ _).symm]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
⊢ (Seq.seq (cons <$> 𝓝 a) fun x => 𝓝 l) = (fun p => p.fst :: p.snd) <$> Seq.seq (Prod.mk <$> 𝓝 a) fun x => 𝓝 l
[PROOFSTEP]
simp [-Filter.map_def, (· ∘ ·), functor_norm]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun p => p.fst :: p.snd) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto f (𝓝 (a :: l)) b ↔ Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) b
[PROOFSTEP]
rw [this, Filter.tendsto_map'_iff]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun p => p.fst :: p.snd) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto (f ∘ fun p => p.fst :: p.snd) (𝓝 a ×ˢ 𝓝 l) b ↔ Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_3
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
⊢ Tendsto f (𝓝 []) (r [])
[PROOFSTEP]
rwa [nhds_nil]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_3
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
a : α
l : List α
⊢ Tendsto f (𝓝 (a :: l)) (r (a :: l))
[PROOFSTEP]
rw [tendsto_cons_iff]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_3
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
a : α
l : List α
⊢ Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
[PROOFSTEP]
exact h_cons l a (@tendsto_nhds _ _ _ h_nil h_cons l)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ ∀ (l : List α), ContinuousAt length l
[PROOFSTEP]
simp only [ContinuousAt, nhds_discrete]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ ∀ (l : List α), Tendsto length (𝓝 l) (pure (length l))
[PROOFSTEP]
refine' tendsto_nhds _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ Tendsto length (pure []) (pure (length []))
[PROOFSTEP]
exact tendsto_pure_pure _ _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ ∀ (l : List α) (a : α),
    Tendsto length (𝓝 l) (pure (length l)) →
      Tendsto (fun p => length (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) (pure (length (a :: l)))
[PROOFSTEP]
intro l a ih
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure (length l))
⊢ Tendsto (fun p => length (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) (pure (length (a :: l)))
[PROOFSTEP]
dsimp only [List.length]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure (length l))
⊢ Tendsto (fun p => length p.snd + 1) (𝓝 a ×ˢ 𝓝 l) (pure (length l + 1))
[PROOFSTEP]
refine' Tendsto.comp (tendsto_pure_pure (fun x => x + 1) _) _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure (length l))
⊢ Tendsto (fun p => Nat.add (length p.snd) 0) (𝓝 a ×ˢ 𝓝 l) (pure (length l))
[PROOFSTEP]
refine' Tendsto.comp ih tendsto_snd
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
n : ℕ
⊢ Tendsto (fun p => insertNth (n + 1) p.fst p.snd) (𝓝 a ×ˢ 𝓝 []) (𝓝 (insertNth (n + 1) a []))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
n : ℕ
a' : α
l : List α
⊢ Tendsto (fun p => insertNth (n + 1) p.fst p.snd) (𝓝 a ×ˢ 𝓝 (a' :: l)) (𝓝 (insertNth (n + 1) a (a' :: l)))
[PROOFSTEP]
have : 𝓝 a ×ˢ 𝓝 (a' :: l) = (𝓝 a ×ˢ (𝓝 a' ×ˢ 𝓝 l)).map fun p : α × α × List α => (p.1, p.2.1 :: p.2.2) :=
  by
  simp only [nhds_cons, Filter.prod_eq, ← Filter.map_def, ← Filter.seq_eq_filter_seq]
  simp [-Filter.map_def, (· ∘ ·), functor_norm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
n : ℕ
a' : α
l : List α
⊢ 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p => (p.fst, p.snd.fst :: p.snd.snd)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
[PROOFSTEP]
simp only [nhds_cons, Filter.prod_eq, ← Filter.map_def, ← Filter.seq_eq_filter_seq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
n : ℕ
a' : α
l : List α
⊢ (Seq.seq (Prod.mk <$> 𝓝 a) fun x => Seq.seq (cons <$> 𝓝 a') fun x => 𝓝 l) =
    (fun p => (p.fst, p.snd.fst :: p.snd.snd)) <$>
      Seq.seq (Prod.mk <$> 𝓝 a) fun x => Seq.seq (Prod.mk <$> 𝓝 a') fun x => 𝓝 l
[PROOFSTEP]
simp [-Filter.map_def, (· ∘ ·), functor_norm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
n : ℕ
a' : α
l : List α
this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p => (p.fst, p.snd.fst :: p.snd.snd)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
⊢ Tendsto (fun p => insertNth (n + 1) p.fst p.snd) (𝓝 a ×ˢ 𝓝 (a' :: l)) (𝓝 (insertNth (n + 1) a (a' :: l)))
[PROOFSTEP]
rw [this, tendsto_map'_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
n : ℕ
a' : α
l : List α
this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p => (p.fst, p.snd.fst :: p.snd.snd)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
⊢ Tendsto ((fun p => insertNth (n + 1) p.fst p.snd) ∘ fun p => (p.fst, p.snd.fst :: p.snd.snd)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
    (𝓝 (insertNth (n + 1) a (a' :: l)))
[PROOFSTEP]
exact
  (tendsto_fst.comp tendsto_snd).cons
    ((@tendsto_insertNth' _ n l).comp <| tendsto_fst.prod_mk <| tendsto_snd.comp tendsto_snd)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
x✝ : α × List α
a : α
l : List α
⊢ ContinuousAt (fun p => insertNth n p.fst p.snd) (a, l)
[PROOFSTEP]
rw [ContinuousAt, nhds_prod_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
x✝ : α × List α
a : α
l : List α
⊢ Tendsto (fun p => insertNth n p.fst p.snd) (𝓝 a ×ˢ 𝓝 l) (𝓝 (insertNth n (a, l).fst (a, l).snd))
[PROOFSTEP]
exact tendsto_insertNth'
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x✝ : ℕ
⊢ Tendsto (fun l => removeNth l x✝) (𝓝 []) (𝓝 (removeNth [] x✝))
[PROOFSTEP]
rw [nhds_nil]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x✝ : ℕ
⊢ Tendsto (fun l => removeNth l x✝) (pure []) (𝓝 (removeNth [] x✝))
[PROOFSTEP]
exact tendsto_pure_nhds _ _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
l : List α
⊢ Tendsto (fun l => removeNth l 0) (𝓝 (a :: l)) (𝓝 (removeNth (a :: l) 0))
[PROOFSTEP]
rw [tendsto_cons_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
l : List α
⊢ Tendsto (fun p => removeNth (p.fst :: p.snd) 0) (𝓝 a ×ˢ 𝓝 l) (𝓝 (removeNth (a :: l) 0))
[PROOFSTEP]
exact tendsto_snd
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
a : α
l : List α
⊢ Tendsto (fun l => removeNth l (n + 1)) (𝓝 (a :: l)) (𝓝 (removeNth (a :: l) (n + 1)))
[PROOFSTEP]
rw [tendsto_cons_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
a : α
l : List α
⊢ Tendsto (fun p => removeNth (p.fst :: p.snd) (n + 1)) (𝓝 a ×ˢ 𝓝 l) (𝓝 (removeNth (a :: l) (n + 1)))
[PROOFSTEP]
dsimp [removeNth]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
a : α
l : List α
⊢ Tendsto (fun p => p.fst :: removeNth p.snd n) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: removeNth l n))
[PROOFSTEP]
exact tendsto_fst.cons ((@tendsto_removeNth n l).comp tendsto_snd)
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
l : List α
⊢ Tendsto prod (𝓝 l) (𝓝 (prod l))
[PROOFSTEP]
induction' l with x l ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
⊢ Tendsto prod (𝓝 []) (𝓝 (prod []))
[PROOFSTEP]
simp (config := { contextual := true }) [nhds_nil, mem_of_mem_nhds, tendsto_pure_left]
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 (prod l))
⊢ Tendsto prod (𝓝 (x :: l)) (𝓝 (prod (x :: l)))
[PROOFSTEP]
simp_rw [tendsto_cons_iff, prod_cons]
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 (prod l))
⊢ Tendsto (fun p => p.fst * prod p.snd) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * prod l))
[PROOFSTEP]
have := continuous_iff_continuousAt.mp continuous_mul (x, l.prod)
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 (prod l))
this : ContinuousAt (fun p => p.fst * p.snd) (x, prod l)
⊢ Tendsto (fun p => p.fst * prod p.snd) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * prod l))
[PROOFSTEP]
rw [ContinuousAt, nhds_prod_eq] at this
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 (prod l))
this : Tendsto (fun p => p.fst * p.snd) (𝓝 x ×ˢ 𝓝 (prod l)) (𝓝 ((x, prod l).fst * (x, prod l).snd))
⊢ Tendsto (fun p => p.fst * prod p.snd) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * prod l))
[PROOFSTEP]
exact this.comp (tendsto_id.prod_map ih)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
⊢ TopologicalSpace (Vector α n)
[PROOFSTEP]
unfold Vector
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
⊢ TopologicalSpace { l // List.length l = n }
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
a : α
l : Vector α n
⊢ Tendsto (fun p => p.fst ::ᵥ p.snd) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a ::ᵥ l))
[PROOFSTEP]
rw [tendsto_subtype_rng, cons_val]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
a : α
l : Vector α n
⊢ Tendsto (fun x => ↑(x.fst ::ᵥ x.snd)) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: ↑l))
[PROOFSTEP]
exact tendsto_fst.cons (Tendsto.comp continuousAt_subtype_val tendsto_snd)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : List.length l = n
⊢ Tendsto (fun p => insertNth p.fst i p.snd) (𝓝 a ×ˢ 𝓝 { val := l, property := hl })
    (𝓝 (insertNth a i { val := l, property := hl }))
[PROOFSTEP]
rw [insertNth, tendsto_subtype_rng]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : List.length l = n
⊢ Tendsto (fun x => ↑(insertNth x.fst i x.snd)) (𝓝 a ×ˢ 𝓝 { val := l, property := hl })
    (𝓝
      ↑{ val := List.insertNth (↑i) a ↑{ val := l, property := hl },
          property := (_ : List.length (List.insertNth (↑i) a ↑{ val := l, property := hl }) = n + 1) })
[PROOFSTEP]
simp [insertNth_val]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : List.length l = n
⊢ Tendsto (fun x => List.insertNth (↑i) x.fst ↑x.snd) (𝓝 a ×ˢ 𝓝 { val := l, property := hl })
    (𝓝 (List.insertNth (↑i) a l))
[PROOFSTEP]
exact List.tendsto_insertNth tendsto_fst (Tendsto.comp continuousAt_subtype_val tendsto_snd : _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
x✝ : α × Vector α n
a : α
l : Vector α n
⊢ ContinuousAt (fun p => insertNth p.fst i p.snd) (a, l)
[PROOFSTEP]
rw [ContinuousAt, nhds_prod_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
x✝ : α × Vector α n
a : α
l : Vector α n
⊢ Tendsto (fun p => insertNth p.fst i p.snd) (𝓝 a ×ˢ 𝓝 l) (𝓝 (insertNth (a, l).fst i (a, l).snd))
[PROOFSTEP]
exact tendsto_insertNth
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
l : List α
hl : List.length l = n + 1
⊢ ContinuousAt (removeNth i) { val := l, property := hl }
[PROOFSTEP]
rw [ContinuousAt, removeNth, tendsto_subtype_rng]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
l : List α
hl : List.length l = n + 1
⊢ Tendsto (fun x => ↑(removeNth i x)) (𝓝 { val := l, property := hl })
    (𝓝
      ↑(match { val := l, property := hl } with
        | { val := l, property := p } =>
          { val := List.removeNth l ↑i, property := (_ : List.length (List.removeNth l ↑i) = n + 1 - 1) }))
[PROOFSTEP]
simp only [Vector.removeNth_val]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
l : List α
hl : List.length l = n + 1
⊢ Tendsto (fun x => List.removeNth ↑x ↑i) (𝓝 { val := l, property := hl }) (𝓝 (List.removeNth l ↑i))
[PROOFSTEP]
exact Tendsto.comp List.tendsto_removeNth continuousAt_subtype_val