awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
u : List (Set α)
a : α
b : Set α
l₁ : List α
l₂ : List (Set α)
ht : b ∈ 𝓝 a
h : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l₁ l₂
ih :
  ∀ (s : Set (List α)) (hus : sequence l₂ ⊆ s),
    ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l₁ v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (b :: l₂) ⊆ s
cons :
  ∀ (u : Set α) (hut : u ⊆ b) (hu : IsOpen[inst] u ∧ a ∈ u),
    ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) (a :: l₁) v ∧ sequence v ⊆ s
⊢ ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) (a :: l₁) v ∧ sequence v ⊆ s

Tactic:
rcases mem_nhds_iff.1 ht with ⟨u, hut, hu⟩

Premises used: mem_nhds_iff, Iff.mp
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
u_1 : List (Set α)
a : α
b : Set α
l₁ : List α
l₂ : List (Set α)
ht : b ∈ 𝓝 a
h : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l₁ l₂
ih :
  ∀ (s : Set (List α)) (hus : sequence l₂ ⊆ s),
    ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l₁ v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (b :: l₂) ⊆ s
u : Set α
hut : u ⊆ b
hu : IsOpen[inst] u ∧ a ∈ u
cons :
  ∀ (v : List (Set α)) (hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l₁ v)
    (hvss : sequence v ⊆ sequence l₂),
    ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) (a :: l₁) v ∧ sequence v ⊆ s
⊢ ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) (a :: l₁) v ∧ sequence v ⊆ s

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

Premises used: Set.Subset.rfl
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
u_1 : List (Set α)
a : α
b : Set α
l₁ : List α
l₂ : List (Set α)
ht : b ∈ 𝓝 a
h : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l₁ l₂
ih :
  ∀ (s : Set (List α)) (hus : sequence l₂ ⊆ s),
    ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l₁ v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (b :: l₂) ⊆ s
u : Set α
hut : u ⊆ b
hu : IsOpen[inst] u ∧ a ∈ u
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l₁ v
hvss : sequence v ⊆ sequence l₂
⊢ ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) (a :: l₁) v ∧ sequence v ⊆ s

Tactic:
⟨u::v, List.Forall₂.cons hu hv,
            Subset.trans (Set.seq_mono (Set.image_mono hut) hvss) hus⟩

Premises used: List.Forall₂.cons, Set.Subset.trans, Set.image_mono, List.cons, And.intro, Exists.intro, Set.seq_mono
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
u_1 : List (Set α)
a : α
b : Set α
l₁ : List α
l₂ : List (Set α)
ht : b ∈ 𝓝 a
h : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l₁ l₂
ih :
  ∀ (s : Set (List α)) (hus : sequence l₂ ⊆ s),
    ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l₁ v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (b :: l₂) ⊆ s
u : Set α
hut : u ⊆ b
hu : IsOpen[inst] u ∧ a ∈ u
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l₁ v
hvss : sequence v ⊆ sequence l₂
⊢ ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) (a :: l₁) v ∧ sequence v ⊆ s

Tactic:
exact
          ⟨u::v, List.Forall₂.cons hu hv,
            Subset.trans (Set.seq_mono (Set.image_mono hut) hvss) hus⟩
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
nil :
  ∀ (s : Set (List α)) (hus : sequence [] ⊆ s),
    ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) [] v ∧ sequence v ⊆ s
cons :
  ∀ {a : α} {b : Set α} {l₁ : List α} {l₂ : List (Set α)} (ht : b ∈ 𝓝 a),
    List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l₁ l₂ →
      ∀
        (ih :
          ∀ (s : Set (List α)) (hus : sequence l₂ ⊆ s),
            ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l₁ v ∧ sequence v ⊆ s)
        (s : Set (List α)) (hus : sequence (b :: l₂) ⊆ s),
        ∃ (v : List (Set α)),
          List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) (a :: l₁) v ∧ sequence v ⊆ s
⊢ ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v ∧ sequence v ⊆ s

Tactic:
induction hu generalizing s with
      | nil =>
        exists []
        simp only [List.forall₂_nil_left_iff]
        exact ⟨trivial, hus⟩
      | cons 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_mono hut) hvss) hus⟩

Premises used: List.forall₂_nil_left_iff
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
⊢ ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v ∧ sequence v ⊆ s

Tactic:
have : ∃ v : List (Set α), l.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) v ∧ sequence v ⊆ s := by
      induction hu generalizing s with
      | nil =>
        exists []
        simp only [List.forall₂_nil_left_iff]
        exact ⟨trivial, hus⟩
      | cons 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_mono hut) hvss) hus⟩
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
this : ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v ∧ sequence v ⊆ s
refine_2 :
  ∀ (v : List (Set α)) (hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v)
    (hvs : sequence v ⊆ s), ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y

Tactic:
rcases this with ⟨v, hv, hvs⟩
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
⊢ sequence v ∈ traverse 𝓝 l

Tactic:
have : sequence v ∈ traverse 𝓝 l :=
      mem_traverse _ _ <| hv.imp fun a s ⟨hs, ha⟩ => IsOpen.mem_nhds hs ha
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this : sequence v ∈ traverse 𝓝 l
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y

Tactic:
mem_of_superset this fun u hu ↦ ?_

Premises used: Filter.Eventually, Filter.mem_of_superset
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this : sequence v ∈ traverse 𝓝 l
refine_2 :
  ∀ (u : List α) (hu : u ∈ sequence v),
    Membership.mem (γ := Set (List α)) {x : List α | (fun (y : List α) ↦ s ∈ traverse 𝓝 y) x} u
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y

Tactic:
refine mem_of_superset this fun u hu ↦ ?_

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this : sequence v ∈ traverse 𝓝 l
u : List α
hu : u ∈ sequence v
⊢ List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v

Tactic:
have hu := (List.mem_traverse _ _).1 hu
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this : sequence v ∈ traverse 𝓝 l
u : List α
hu_2 : u ∈ sequence v
hu : List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v
⊢ List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) u v

Tactic:
List.Forall₂.flip ?_

Premises used: List.Forall₂.flip
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this : sequence v ∈ traverse 𝓝 l
u : List α
hu_2 : u ∈ sequence v
hu : List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v
refine : List.Forall₂ (flip fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) v u
⊢ List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) u v

Tactic:
refine List.Forall₂.flip ?_

Premises used: List.Forall₂.flip
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this : sequence v ∈ traverse 𝓝 l
u : List α
hu_2 : u ∈ sequence v
hu : List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v
⊢ List.Forall₂ (fun (s : Set α) (a : α) ↦ IsOpen[inst] s ∧ a ∈ s) v l

Tactic:
replace hv := hv.flip
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hvs : sequence v ⊆ s
this : sequence v ∈ traverse 𝓝 l
u : List α
hu_2 : u ∈ sequence v
hu : List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v
hv : List.Forall₂ (fun (s : Set α) (a : α) ↦ IsOpen[inst] s ∧ a ∈ s) v l
simp :
  ∀ (hv : (∀ a ∈ v, IsOpen[inst] a) ∧ List.Forall₂ Membership.mem v l),
    (∀ a ∈ v, IsOpen[inst] a) ∧ List.Forall₂ Membership.mem v u
⊢ List.Forall₂ (flip fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) v u

Tactic:
simp only [List.forall₂_and_left, Function.flip_def] at hv ⊢

Premises used: Function.flip_def, List.forall₂_and_left
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hvs : sequence v ⊆ s
this : sequence v ∈ traverse 𝓝 l
u : List α
hu_2 : u ∈ sequence v
hu : List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v
hv : (∀ a ∈ v, IsOpen[inst] a) ∧ List.Forall₂ Membership.mem v l
⊢ (∀ a ∈ v, IsOpen[inst] a) ∧ List.Forall₂ Membership.mem v u

Tactic:
⟨hv.1, hu.flip⟩

Premises used: List.Forall₂.flip, And.left, And.intro
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hvs : sequence v ⊆ s
this : sequence v ∈ traverse 𝓝 l
u : List α
hu_2 : u ∈ sequence v
hu : List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v
hv : (∀ a ∈ v, IsOpen[inst] a) ∧ List.Forall₂ Membership.mem v l
⊢ (∀ a ∈ v, IsOpen[inst] a) ∧ List.Forall₂ Membership.mem v u

Tactic:
exact ⟨hv.1, hu.flip⟩
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this : sequence v ∈ traverse 𝓝 l
u : List α
hu_2 : u ∈ sequence v
hu : List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v
⊢ List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) u v

Tactic:
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, Function.flip_def] at hv ⊢
      exact ⟨hv.1, hu.flip⟩
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this_1 : sequence v ∈ traverse 𝓝 l
u : List α
hu_2 : u ∈ sequence v
hu : List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v
this : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) u v
refine_2 : Membership.mem (γ := Set (List α)) {x : List α | (fun (y : List α) ↦ sequence v ∈ traverse 𝓝 y) x} u
⊢ Membership.mem (γ := Set (List α)) {x : List α | (fun (y : List α) ↦ s ∈ traverse 𝓝 y) x} u

Tactic:
grw [← hvs]
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this_1 : sequence v ∈ traverse 𝓝 l
u : List α
hu_2 : u ∈ sequence v
hu : List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v
this : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) u v
⊢ Membership.mem (γ := Set (List α)) {x : List α | (fun (y : List α) ↦ sequence v ∈ traverse 𝓝 y) x} u

Tactic:
mem_traverse _ _ (this.imp fun a s ⟨hs, ha⟩ => IsOpen.mem_nhds hs ha)

Premises used: Set.Mem, setOf, List.Forall₂.imp, Filter.mem_traverse, sequence
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this_1 : sequence v ∈ traverse 𝓝 l
u : List α
hu_2 : u ∈ sequence v
hu : List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v
this : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) u v
⊢ Membership.mem (γ := Set (List α)) {x : List α | (fun (y : List α) ↦ sequence v ∈ traverse 𝓝 y) x} u

Tactic:
exact mem_traverse _ _ (this.imp fun a s ⟨hs, ha⟩ => IsOpen.mem_nhds hs ha)

Premises used: List.Forall₂.imp, Filter.mem_traverse
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
rw : Eq.{u_1 + 1} (α := Filter (List α)) (traverse 𝓝 []) (pure [])
rw₁ rw₂ : Eq.{u_1 + 1} (α := Filter (List α)) (pure []) (pure [])
⊢ Eq.{u_1 + 1} (α := Filter (List α)) (𝓝 []) (pure [])

Tactic:
rw [nhds_list, List.traverse_nil _]

Premises used: List.traverse_nil, nhds_list
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
l : List α
rw : traverse 𝓝 (a :: l) = List.cons <$> 𝓝 a <*> 𝓝 l
rw₁ : (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) <$> 𝓝 a <*> traverse 𝓝 l = List.cons <$> 𝓝 a <*> 𝓝 l
rw₂ rw₃ : (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) <$> 𝓝 a <*> 𝓝 l = List.cons <$> 𝓝 a <*> 𝓝 l
⊢ 𝓝 (a :: l) = List.cons <$> 𝓝 a <*> 𝓝 l

Tactic:
rw [nhds_list, List.traverse_cons _, ← nhds_list]

Premises used: List.traverse_cons, nhds_list
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
l : List α
rw : Filter.seq (Filter.map (fun (a : α) (b : List α) ↦ (a, b).1 :: (a, b).2) (𝓝 a)) (𝓝 l) ≤ cons <$> 𝓝 a <*> 𝓝 l
⊢ Tendsto (fun (p : α × List α) ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: l))

Tactic:
rw [nhds_cons, Tendsto, Filter.map_prod]

Premises used: nhds_cons, Filter.map_prod, Filter.Tendsto
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
l : List α
⊢ Filter.seq (Filter.map (fun (a : α) (b : List α) ↦ (a, b).1 :: (a, b).2) (𝓝 a)) (𝓝 l) ≤ cons <$> 𝓝 a <*> 𝓝 l

Tactic:
le_rfl

Premises used: le_rfl, Set.Mem, setOf
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
l : List α
⊢ Filter.seq (Filter.map (fun (a : α) (b : List α) ↦ (a, b).1 :: (a, b).2) (𝓝 a)) (𝓝 l) ≤ cons <$> 𝓝 a <*> 𝓝 l

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Topology.List
Goal:
β : Type u_2
inst : TopologicalSpace β
α : Type u_3
f : α → β
g : α → List β
a : Filter α
b : β
l : List β
hf : Tendsto f a (𝓝 b)
hg : Tendsto g a (𝓝 l)
⊢ Tendsto (fun (a : α) ↦ f a :: g a) a (𝓝 (b :: l))

Tactic:
List.tendsto_cons.comp (Tendsto.prodMk hf hg)

Premises used: Filter.Tendsto.prodMk, Filter.Tendsto.comp, List.tendsto_cons
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
simp : cons <$> 𝓝 a <*> 𝓝 l = (fun (p : α × List α) ↦ p.1 :: p.2) <$> (Prod.mk <$> 𝓝 a <*> 𝓝 l)
⊢ 𝓝 (a :: l) = Filter.map (fun (p : α × List α) ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)

Tactic:
simp only [nhds_cons, Filter.prod_eq, (Filter.map_def _ _).symm,
      (Filter.seq_eq_filter_seq _ _).symm]

Premises used: Filter.prod_eq, nhds_cons, Filter.seq_eq_filter_seq, Filter.map_def, Eq.symm
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
⊢ cons <$> 𝓝 a <*> 𝓝 l = (fun (p : α × List α) ↦ p.1 :: p.2) <$> (Prod.mk <$> 𝓝 a <*> 𝓝 l)

Tactic:
simp [-Filter.map_def, Function.comp_def, functor_norm]

Premises used: Function.comp_def, Filter.map_def
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
⊢ 𝓝 (a :: l) = Filter.map (fun (p : α × List α) ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)

Tactic:
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, Function.comp_def, functor_norm]
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun (p : α × List α) ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)
rw :
  Tendsto (f ∘ fun (p : α × List α) ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) b ↔
    Tendsto (fun (p : α × List α) ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b
⊢ Tendsto f (𝓝 (a :: l)) b ↔ Tendsto (fun (p : α × List α) ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b

Tactic:
rw [this, Filter.tendsto_map'_iff]

Premises used: Filter.tendsto_map'_iff
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun (p : α × List α) ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto (f ∘ fun (p : α × List α) ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) b ↔
    Tendsto (fun (p : α × List α) ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b

Tactic:
rfl
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceList] fun (x : α × List α) ↦ x.1 :: x.2

Tactic:
continuous_iff_continuousAt.mpr fun ⟨_x, _y⟩ => continuousAt_fst.cons continuousAt_snd

Premises used: Iff.mpr, ContinuousAt, _private.0.List.continuous_cons.match_1, Prod.fst, List.cons, Filter.Tendsto.cons, Prod.snd, continuousAt_snd, continuousAt_fst, continuous_iff_continuousAt
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
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 : α × List α) ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
rwa rwa₁ rwa₂ rwa₃ : Tendsto f (pure []) (r [])
⊢ Tendsto f (𝓝 []) (r [])

Tactic:
rwa [nhds_nil]

Premises used: nhds_nil
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
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 : α × List α) ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
a : α
l : List α
rw : Tendsto (fun (p : α × List α) ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
⊢ Tendsto f (𝓝 (a :: l)) (r (a :: l))

Tactic:
rw [tendsto_cons_iff]

Premises used: List.tendsto_cons_iff
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
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 : α × List α) ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
a : α
l : List α
⊢ Tendsto (fun (p : α × List α) ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))

Tactic:
h_cons l a (@tendsto_nhds _ _ _ h_nil h_cons l)
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
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 : α × List α) ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
a : α
l : List α
⊢ Tendsto (fun (p : α × List α) ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))

Tactic:
exact h_cons l a (@tendsto_nhds _ _ _ h_nil h_cons l)
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : DiscreteTopology α
rw : ∀ (x : List α), 𝓝 x = pure x
⊢ DiscreteTopology.{u_1} (List α)

Tactic:
rw [discreteTopology_iff_nhds]

Premises used: discreteTopology_iff_nhds
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : DiscreteTopology α
l : List α
nil : Eq.{u_1 + 1} (α := Filter (List α)) (𝓝 []) (pure [])
cons : ∀ (head : α) (tail : List α), 𝓝 tail = pure tail → 𝓝 (head :: tail) = pure (head :: tail)
⊢ 𝓝 l = pure l

Tactic:
induction l
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : DiscreteTopology α
⊢ Eq.{u_1 + 1} (α := Filter (List α)) (𝓝 []) (pure [])

Tactic:
simp [*, nhds_cons]

Premises used: nhds_cons
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : DiscreteTopology α
head : α
tail : List α
tail_ih : 𝓝 tail = pure tail
⊢ 𝓝 (head :: tail) = pure (head :: tail)

Tactic:
simp [*, nhds_cons]

Premises used: nhds_cons
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
simp : ∀ (l : List α), Tendsto length (𝓝 l) (pure l.length)
⊢ ∀ (l : List α), ContinuousAt length l

Tactic:
simp only [ContinuousAt, nhds_discrete]

Premises used: ContinuousAt, nhds_discrete
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ ∀ (l : List α), Tendsto length (𝓝 l) (pure l.length)

Tactic:
tendsto_nhds ?_ ?_

Premises used: List.tendsto_nhds
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
refine_1 : Tendsto.{u_1, 0} (α := List α) length (pure []) (pure (length.{u_1} (α := α) []))
refine_2 :
  ∀ (l : List α) (a : α),
    Tendsto length (𝓝 l) (pure l.length) →
      Tendsto (fun (p : α × List α) ↦ (p.1 :: p.2).length) (𝓝 a ×ˢ 𝓝 l) (pure (a :: l).length)
⊢ ∀ (l : List α), Tendsto length (𝓝 l) (pure l.length)

Tactic:
refine tendsto_nhds ?_ ?_

Premises used: List.tendsto_nhds
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Tendsto.{u_1, 0} (α := List α) length (pure []) (pure (length.{u_1} (α := α) []))

Tactic:
tendsto_pure_pure _ _

Premises used: Filter.tendsto_pure_pure