awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : Realizer.{u_1, u_5} f
G : (i : α) → Realizer.{u_2, u_6} (m i)
x x_1 : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)
x_2 : β
simp :
  ∀ (x_3 : α)
    (x_4 :
      x_3 ∈
        F.F.f
          (F.F.inf (x.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))
            (x_1.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))))
    (h :
      x_2 ∈
        (G x_3).F.f
          ((G x_3).F.inf (x.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) x_3 ⋯)
            (x_1.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) x_3 ⋯))),
    ∃ (i : α) (i_1 : i ∈ F.F.f (x_1.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))),
      x_2 ∈ (G i).F.f (x_1.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) i i_1)
⊢ Membership.mem (γ := Set β)
      (match (motive := (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ) → Set β)
          match (motive :=
            (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ) → (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)) x with
          | ⟨a, f_1⟩ =>
            match (motive :=
              (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ) → (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)) x_1 with
            | ⟨b, f'⟩ =>
              Sigma.mk (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) (F.F.inf a b)
                fun (i : α) (h : i ∈ F.F.f (F.F.inf a b)) ↦ (G i).F.inf (f_1 i ⋯) (f' i ⋯) with
        | ⟨s, f_1⟩ => ⋃ (i : α), ⋃ (h : i ∈ F.F.f s), (G i).F.f (f_1 i h) :
        Set β)
      x_2 →
    Membership.mem (γ := Set β)
      (match (motive := (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ) → Set β) x_1 with
        | ⟨s, f_1⟩ => ⋃ (i : α), ⋃ (h : i ∈ F.F.f s), (G i).F.f (f_1 i h) :
        Set β)
      x_2

Tactic:
simp only [mem_iUnion, forall_exists_index]

Premises used: Set.mem_iUnion, forall_exists_index
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : Realizer.{u_1, u_5} f
G : (i : α) → Realizer.{u_2, u_6} (m i)
x x_1 : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)
x_2 : β
⊢ ∀ (x_3 : α)
    (x_4 :
      x_3 ∈
        F.F.f
          (F.F.inf (x.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))
            (x_1.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))))
    (h :
      x_2 ∈
        (G x_3).F.f
          ((G x_3).F.inf (x.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) x_3 ⋯)
            (x_1.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) x_3 ⋯))),
    ∃ (i : α) (i_1 : i ∈ F.F.f (x_1.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))),
      x_2 ∈ (G i).F.f (x_1.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) i i_1)

Tactic:
fun i h₁ h₂ ↦ ⟨i, F.F.inf_le_right _ _ h₁, (G i).F.inf_le_right _ _ h₂⟩

Premises used: Iff.mpr, CFilter.inf, Iff.of_eq, Membership.mem, Sigma.fst, Filter.Realizer.F, Exists.intro, Eq.refl, CFilter.inf_le_left, Sigma.snd, CFilter.inf_le_right, CFilter.f
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : Realizer.{u_1, u_5} f
G : (i : α) → Realizer.{u_2, u_6} (m i)
x x_1 : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)
x_2 : β
⊢ ∀ (x_3 : α)
    (x_4 :
      x_3 ∈
        F.F.f
          (F.F.inf (x.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))
            (x_1.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))))
    (h :
      x_2 ∈
        (G x_3).F.f
          ((G x_3).F.inf (x.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) x_3 ⋯)
            (x_1.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) x_3 ⋯))),
    ∃ (i : α) (i_1 : i ∈ F.F.f (x_1.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))),
      x_2 ∈ (G i).F.f (x_1.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) i i_1)

Tactic:
exact fun i h₁ h₂ ↦ ⟨i, F.F.inf_le_right _ _ h₁, (G i).F.inf_le_right _ _ h₂⟩
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → Filter β
G : (i : α) → Realizer.{u_2, u_6} (m i)
x : Set β
σ_1 : Type u_5
F : CFilter.{u_1, u_5} (Set α) σ_1
⊢ Membership.mem (γ := Set (Set β))
      {a : Set β |
        ∃ (a_1 : σ_1) (b : (i : α) → i ∈ F.f a_1 → (G i).σ), ∀ (i : α) (i_1 : i ∈ F.f a_1), (G i).F.f (b i i_1) ⊆ a}
      x ↔
    ∃
      t ∈
        { sets := {a : Set α | ∃ (b : σ_1), F.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ :
          Filter α },
      ∀ x_1 ∈ t, x ∈ m x_1

Tactic:
⟨fun ⟨s, f, h⟩ ↦
          ⟨F s, ⟨s, Subset.refl _⟩, fun i H ↦ (G i).mem_sets.2 ⟨f i H, fun _ h' ↦ h i H h'⟩⟩,
          fun ⟨_, ⟨s, h⟩, f⟩ ↦
          let ⟨f', h'⟩ := Classical.axiom_of_choice fun i : F s ↦ (G i).mem_sets.1 (f i (h i.2))
          ⟨s, fun i h ↦ f' ⟨i, h⟩, fun _ H _ m ↦ h' ⟨_, H⟩ m⟩⟩

Premises used: Iff.mpr, Set.Subset.refl, _private.0.Filter.Realizer.bind.match_6, CFilter.toFilter._proof_1, CFilter.toFilter._proof_3, setOf, CFilter.toFilter._proof_2, Membership.mem, Exists, Filter.mk, HasSubset.Subset, _private.0.Filter.Realizer.bind.match_7, Filter.Realizer.mem_sets, Classical.axiom_of_choice, Subtype.mk, And, And.intro, Iff.intro, Exists.intro, Iff.mp, _private.0.Filter.Realizer.bind.match_8, Subtype.val, Subtype.property, CFilter.f
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → Filter β
G : (i : α) → Realizer.{u_2, u_6} (m i)
x : Set β
σ_1 : Type u_5
F : CFilter.{u_1, u_5} (Set α) σ_1
⊢ Membership.mem (γ := Set (Set β))
      {a : Set β |
        ∃ (a_1 : σ_1) (b : (i : α) → i ∈ F.f a_1 → (G i).σ), ∀ (i : α) (i_1 : i ∈ F.f a_1), (G i).F.f (b i i_1) ⊆ a}
      x ↔
    ∃
      t ∈
        { sets := {a : Set α | ∃ (b : σ_1), F.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ :
          Filter α },
      ∀ x_1 ∈ t, x ∈ m x_1

Tactic:
exact
        ⟨fun ⟨s, f, h⟩ ↦
          ⟨F s, ⟨s, Subset.refl _⟩, fun i H ↦ (G i).mem_sets.2 ⟨f i H, fun _ h' ↦ h i H h'⟩⟩,
          fun ⟨_, ⟨s, h⟩, f⟩ ↦
          let ⟨f', h'⟩ := Classical.axiom_of_choice fun i : F s ↦ (G i).mem_sets.1 (f i (h i.2))
          ⟨s, fun i h ↦ f' ⟨i, h⟩, fun _ H _ m ↦ h' ⟨_, H⟩ m⟩⟩
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : α → Filter β
F : (i : α) → Realizer.{u_2, u_5} (f i)
⊢ ∀ (x : Set β), x ∈ (bind ⊤ f).sets ↔ Membership.mem (γ := Set (Set β)) (sets (⨆ (i : α), f i)) x

Tactic:
simp [Filter.bind, iSup_sets_eq]

Premises used: Filter.bind, Filter.iSup_sets_eq
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
f g : Filter α
F : Realizer.{u_1, u_5} f
G : Realizer.{u_1, u_6} g
⊢ f ≤ g ↔ ∀ (b : G.σ), ∃ (a : F.σ), F.F.f a ≤ G.F.f b

Tactic:
⟨fun H t ↦ F.mem_sets.1 (H (G.mem_sets.2 ⟨t, Subset.refl _⟩)), fun H _ h ↦
    F.mem_sets.2 <|
      let ⟨s, h₁⟩ := G.mem_sets.1 h
      let ⟨t, h₂⟩ := H s
      ⟨t, Subset.trans h₂ h₁⟩⟩

Premises used: Iff.mpr, Set.Subset.refl, Set.Subset.trans, Exists, HasSubset.Subset, _private.0.Filter.Realizer.le_iff.match_1, Filter.Realizer.mem_sets, Filter.Realizer.F, Iff.intro, Exists.intro, Iff.mp, _private.0.Filter.Realizer.le_iff.match_2, CFilter.f
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
f : α → β
l₁ : Filter α
l₂ : Filter β
L₁ : Realizer.{u_1, u_5} l₁
L₂ : Realizer.{u_2, u_6} l₂
⊢ Tendsto f l₁ l₂ ↔ ∀ (b : L₂.σ), ∃ (a : L₁.σ), ∀ x ∈ L₁.F.f a, f x ∈ L₂.F.f b

Tactic:
(le_iff (L₁.map f) L₂).trans <| forall_congr' fun _ ↦ exists_congr fun _ ↦ image_subset_iff

Premises used: exists_congr, Filter.Tendsto, Filter.Realizer.le_iff, forall_congr', Iff.trans, Filter.Realizer.map, Set.image_subset_iff
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
f : Filter α
F : Realizer.{u_1, u_5} f
rw :
  (∃ (x : F.σ), ¬(F.F.f x).Nonempty) ↔
    ∀ (b : σ.{u_1, 0} (α := α) Realizer.bot), ∃ (a : F.σ), F.F.f a ≤ CFilter.f (Realizer.F Realizer.bot) b
⊢ f ≠ ⊥ ↔ ∀ (a : F.σ), (F.F.f a).Nonempty

Tactic:
rw [not_iff_comm, ← le_bot_iff, F.le_iff Realizer.bot, not_forall]

Premises used: le_bot_iff, Filter.Realizer.bot, Filter.Realizer.le_iff, Classical.not_forall, not_iff_comm
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
f : Filter α
F : Realizer.{u_1, u_5} f
simp :
  (∃ (x : F.σ), F.F.f x = ∅) ↔
    ∀ (b : σ.{u_1, 0} (α := α) Realizer.bot), ∃ (a : F.σ), F.F.f a ≤ CFilter.f (Realizer.F Realizer.bot) b
⊢ (∃ (x : F.σ), ¬(F.F.f x).Nonempty) ↔
    ∀ (b : σ.{u_1, 0} (α := α) Realizer.bot), ∃ (a : F.σ), F.F.f a ≤ CFilter.f (Realizer.F Realizer.bot) b

Tactic:
simp only [Set.not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
f : Filter α
F : Realizer.{u_1, u_5} f
⊢ (∃ (x : F.σ), F.F.f x = ∅) ↔
    ∀ (b : σ.{u_1, 0} (α := α) Realizer.bot), ∃ (a : F.σ), F.F.f a ≤ CFilter.f (Realizer.F Realizer.bot) b

Tactic:
⟨fun ⟨x, e⟩ _ ↦ ⟨x, le_of_eq e⟩, fun h ↦
    let ⟨x, h⟩ := h ()
    ⟨x, le_bot_iff.1 h⟩⟩

Premises used: le_bot_iff, Unit.unit, Filter.Realizer.bot, Exists, _private.0.Filter.Realizer.ne_bot_iff.match_2, LE.le, Filter.Realizer.F, Iff.intro, Exists.intro, Iff.mp, EmptyCollection.emptyCollection, le_of_eq, Eq, _private.0.Filter.Realizer.ne_bot_iff.match_1, CFilter.f
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
f : Filter α
F : Realizer.{u_1, u_5} f
⊢ (∃ (x : F.σ), F.F.f x = ∅) ↔
    ∀ (b : σ.{u_1, 0} (α := α) Realizer.bot), ∃ (a : F.σ), F.F.f a ≤ CFilter.f (Realizer.F Realizer.bot) b

Tactic:
exact ⟨fun ⟨x, e⟩ _ ↦ ⟨x, le_of_eq e⟩, fun h ↦
    let ⟨x, h⟩ := h ()
    ⟨x, le_bot_iff.1 h⟩⟩
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
σ : Type u_3
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
a : σ
⊢ { f := f, top := T, top_mem := h₁, inter := I, inter_mem := h₂, inter_sub := h₃ : Ctop α σ }.f a = f a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
x : α
⊢ x ∈ f ((E.symm : (a : τ) → σ) ((E : (a : σ) → τ) (T x) : τ))

Tactic:
simpa using h₁ x
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
a b : τ
x : α
h : x ∈ f ((E.symm : (a : τ) → σ) a) ∩ f ((E.symm : (a : τ) → σ) b)
⊢ x ∈ f ((E.symm : (a : τ) → σ) ((E : (a : σ) → τ) (I ((E.symm : (a : τ) → σ) a) ((E.symm : (a : τ) → σ) b) x h) : τ))

Tactic:
simpa using h₂ (E.symm a) (E.symm b) x h

Premises used: Equiv.symm, DFunLike.coe
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
a b : τ
x : α
h : x ∈ f ((E.symm : (a : τ) → σ) a) ∩ f ((E.symm : (a : τ) → σ) b)
⊢ f ((E.symm : (a : τ) → σ) ((E : (a : σ) → τ) (I ((E.symm : (a : τ) → σ) a) ((E.symm : (a : τ) → σ) b) x h) : τ)) ⊆
    f ((E.symm : (a : τ) → σ) a) ∩ f ((E.symm : (a : τ) → σ) b)

Tactic:
simpa using h₃ (E.symm a) (E.symm b) x h

Premises used: Equiv.symm, DFunLike.coe
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
σ : Type u_3
τ : Type u_4
E : σ ≃ τ
F : Ctop α σ
a : τ
mk :
  ∀ (f : σ → Set α) (top : α → σ) (top_mem : ∀ (x : α), x ∈ f (top x)) (inter : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ)
    (inter_mem : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (inter a b x h))
    (inter_sub : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (inter a b x h) ⊆ f a ∩ f b),
    (ofEquiv E
            { f := f, top := top, top_mem := top_mem, inter := inter, inter_mem := inter_mem, inter_sub := inter_sub :
              Ctop α σ }).f
        a =
      { f := f, top := top, top_mem := top_mem, inter := inter, inter_mem := inter_mem, inter_sub := inter_sub :
            Ctop α σ }.f
        ((E.symm : (a : τ) → σ) a)
⊢ (ofEquiv E F).f a = F.f ((E.symm : (a : τ) → σ) a)

Tactic:
cases F
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
σ : Type u_3
τ : Type u_4
E : σ ≃ τ
a : τ
f : σ → Set α
top : α → σ
top_mem : ∀ (x : α), x ∈ f (top x)
inter : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
inter_mem : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (inter a b x h)
inter_sub : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (inter a b x h) ⊆ f a ∩ f b
⊢ (ofEquiv E
          { f := f, top := top, top_mem := top_mem, inter := inter, inter_mem := inter_mem, inter_sub := inter_sub :
            Ctop α σ }).f
      a =
    { f := f, top := top, top_mem := top_mem, inter := inter, inter_mem := inter_mem, inter_sub := inter_sub :
          Ctop α σ }.f
      ((E.symm : (a : τ) → σ) a)

Tactic:
rfl
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
σ : Type u_3
F : Ctop α σ
⊢ TopologicalSpace.IsTopologicalBasis (range F.f)

Tactic:
letI := F.toTopsp
  ⟨fun _u ⟨a, e₁⟩ _v ⟨b, e₂⟩ ↦
    e₁ ▸ e₂ ▸ fun x h ↦ ⟨_, ⟨_, rfl⟩, F.inter_mem a b x h, F.inter_sub a b x h⟩,
    eq_univ_iff_forall.2 fun x ↦ ⟨_, ⟨_, rfl⟩, F.top_mem x⟩, rfl⟩

Premises used: Iff.mpr, Ctop.inter_mem, Set.eq_univ_iff_forall, _private.0.Ctop.toTopsp_isTopologicalBasis.match_1, Ctop.top_mem, Eq.rec, Ctop.f, And.intro, Exists.intro, Ctop.inter, rfl, Ctop.top, TopologicalSpace.IsTopologicalBasis.mk, Ctop.inter_sub
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
σ : Type u_3
F : Ctop α σ
s : Set α
a : α
⊢ s ∈ 𝓝 a ↔ ∃ (b : σ), a ∈ F.f b ∧ F.f b ⊆ s

Tactic:
(@TopologicalSpace.IsTopologicalBasis.mem_nhds_iff _ F.toTopsp _ _ _
        F.toTopsp_isTopologicalBasis).trans <|
    ⟨fun ⟨_, ⟨x, rfl⟩, h⟩ ↦ ⟨x, h⟩, fun ⟨x, h⟩ ↦ ⟨_, ⟨x, rfl⟩, h⟩⟩

Premises used: Membership.mem, Exists, _private.0.Ctop.mem_nhds_toTopsp.match_2, HasSubset.Subset, Ctop.f, And, And.intro, Iff.intro, Exists.intro, Ctop.toTopsp_isTopologicalBasis, Iff.trans, Set.range, _private.0.Ctop.mem_nhds_toTopsp.match_1, TopologicalSpace.IsTopologicalBasis.mem_nhds_iff, rfl
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
T : TopologicalSpace α
F : Realizer.{u_5, u_1} α
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)

Tactic:
have := toTopsp_isTopologicalBasis F.F
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
T : TopologicalSpace α
F : Realizer.{u_5, u_1} α
this : TopologicalSpace.IsTopologicalBasis (range F.F.f)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : TopologicalSpace.IsTopologicalBasis (range F.F.f)), TopologicalSpace.IsTopologicalBasis (range F.F.f)
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)

Tactic:
rwa [F.eq] at this

Premises used: Ctop.Realizer.eq
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
T : TopologicalSpace α
F : Realizer.{u_5, u_1} α
s : Set α
a : α
⊢ s ∈ 𝓝 a ↔ ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s

Tactic:
have := @mem_nhds_toTopsp _ _ F.F s a
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
T : TopologicalSpace α
F : Realizer.{u_5, u_1} α
s : Set α
a : α
this : s ∈ 𝓝 a ↔ ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : s ∈ 𝓝 a ↔ ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s), s ∈ 𝓝 a ↔ ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s
⊢ s ∈ 𝓝 a ↔ ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s

Tactic:
rwa [F.eq] at this

Premises used: Ctop.Realizer.eq
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
s : Set α
⊢ IsOpen[inst] s ↔ ∀ a ∈ s, ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s

Tactic:
isOpen_iff_mem_nhds.trans <| forall₂_congr fun _a _h ↦ F.mem_nhds

Premises used: Ctop.Realizer.mem_nhds, forall₂_congr, Iff.trans, isOpen_iff_mem_nhds
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
s : Set α
a : α
haveI :
  ∀ (this : (a : Prop) → Decidable a),
    (a ∉ s → ∃ (b : F.σ), a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔
      (∀ (b : F.σ), a ∈ F.F.f b → ∃ (z : α), z ∈ F.F.f b ∩ s) → a ∈ s
⊢ (a ∉ s → ∃ (b : F.σ), a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔
    (∀ (b : F.σ), a ∈ F.F.f b → ∃ (z : α), z ∈ F.F.f b ∩ s) → a ∈ s

Tactic:
haveI := Classical.propDecidable
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
s : Set α
a : α
this : (a : Prop) → Decidable a
rw :
  (¬∃ (b : F.σ), a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) → a ∈ s ↔
    (∀ (b : F.σ), a ∈ F.F.f b → ∃ (z : α), z ∈ F.F.f b ∩ s) → a ∈ s
⊢ (a ∉ s → ∃ (b : F.σ), a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔
    (∀ (b : F.σ), a ∈ F.F.f b → ∃ (z : α), z ∈ F.F.f b ∩ s) → a ∈ s

Tactic:
rw [not_imp_comm]

Premises used: not_imp_comm
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (¬∃ (b : F.σ), a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) → a ∈ s ↔
    (∀ (b : F.σ), a ∈ F.F.f b → ∃ (z : α), z ∈ F.F.f b ∩ s) → a ∈ s

Tactic:
simp [not_exists, not_and, not_forall, and_comm]

Premises used: not_exists, and_comm, not_and, Classical.not_forall
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
s : Set α
a : α
⊢ a ∈ interior s ↔ ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s

Tactic:
mem_interior_iff_mem_nhds.trans F.mem_nhds

Premises used: mem_interior_iff_mem_nhds, Ctop.Realizer.mem_nhds, Iff.trans
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
s : F.σ
a : α
m : a ∈ F.F.f s
⊢ 𝓝 a ≤ 𝓟 (F.F.f s)

Tactic:
simpa using F.mem_nhds.2 ⟨s, m, Subset.refl _⟩

Premises used: Iff.mpr, Set.Subset.refl, Ctop.Realizer.mem_nhds, And.intro, Exists.intro
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ (b : σ), a ∈ F.f b ∧ F.f b ⊆ s
⊢ F.toTopsp = T

Tactic:
TopologicalSpace.ext_nhds fun x ↦ ?_

Premises used: TopologicalSpace.ext_nhds
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ (b : σ), a ∈ F.f b ∧ F.f b ⊆ s
refine : ∀ (x : α), 𝓝 x = 𝓝 x
⊢ F.toTopsp = T

Tactic:
refine TopologicalSpace.ext_nhds fun x ↦ ?_

Premises used: TopologicalSpace.ext_nhds
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ (b : σ), a ∈ F.f b ∧ F.f b ⊆ s
x : α
h : ∀ (s : Set α), s ∈ 𝓝 x ↔ s ∈ 𝓝 x
⊢ 𝓝 x = 𝓝 x

Tactic:
ext s
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ (b : σ), a ∈ F.f b ∧ F.f b ⊆ s
x : α
s : Set α
h : (∃ (b : σ), x ∈ F.f b ∧ F.f b ⊆ s) ↔ s ∈ 𝓝 x
h₁ h₂ : (∃ (b : σ), x ∈ F.f b ∧ F.f b ⊆ s) ↔ ∃ (b : σ), x ∈ F.f b ∧ F.f b ⊆ s
⊢ s ∈ 𝓝 x ↔ s ∈ 𝓝 x

Tactic:
rw [mem_nhds_toTopsp, H]

Premises used: Ctop.mem_nhds_toTopsp
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H₁ : ∀ (a : σ), IsOpen[T] (F.f a)
H₂ : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ (b : σ), a ∈ F.f b ∧ F.f b ⊆ s
⊢ F.toTopsp = T

Tactic:
ext' fun a s ↦ ⟨H₂ a s, fun ⟨_b, h₁, h₂⟩ ↦ mem_nhds_iff.2 ⟨_, h₂, H₁ _, h₁⟩⟩

Premises used: Iff.mpr, mem_nhds_iff, Membership.mem, nhds, Ctop.f, Ctop.Realizer.ext', _private.0.Ctop.Realizer.ext.match_1, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
E : Equiv.{u_5 + 1, u_4 + 1} F.σ τ
a : α
s_1 : Set α
h_1 : ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s_1
s : F.σ
h : a ∈ F.F.f s ∧ F.F.f s ⊆ s_1
⊢ a ∈ (Ctop.ofEquiv E F.F).f ((E : (a : F.σ) → τ) s) ∧ (Ctop.ofEquiv E F.F).f ((E : (a : F.σ) → τ) s) ⊆ s_1

Tactic:
simpa using h
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
E : Equiv.{u_5 + 1, u_4 + 1} F.σ τ
a : α
s : Set α
h_1 : ∃ (b : τ), a ∈ (Ctop.ofEquiv E F.F).f b ∧ (Ctop.ofEquiv E F.F).f b ⊆ s
t : τ
h : a ∈ (Ctop.ofEquiv E F.F).f t ∧ (Ctop.ofEquiv E F.F).f t ⊆ s
⊢ a ∈ F.F.f ((E.symm : (a : τ) → F.σ) t) ∧ F.F.f ((E.symm : (a : τ) → F.σ) t) ⊆ s

Tactic:
simpa using h
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
τ : Type u_4
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
E : Equiv.{u_5 + 1, u_4 + 1} F.σ τ
⊢ (F.ofEquiv E).σ = τ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
τ : Type u_4
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
E : Equiv.{u_5 + 1, u_4 + 1} F.σ τ
s : τ
delta : { σ := τ, F := Ctop.ofEquiv E F.F, eq := ⋯ : Realizer.{u_4, u_1} α }.F.f s = F.F.f ((E.symm : (a : τ) → F.σ) s)
⊢ (F.ofEquiv E).F.f s = F.F.f ((E.symm : (a : τ) → F.σ) s)

Tactic:
delta ofEquiv

Premises used: Ctop.Realizer.ofEquiv
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
τ : Type u_4
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
E : Equiv.{u_5 + 1, u_4 + 1} F.σ τ
s : τ
⊢ { σ := τ, F := Ctop.ofEquiv E F.F, eq := ⋯ : Realizer.{u_4, u_1} α }.F.f s = F.F.f ((E.symm : (a : τ) → F.σ) s)

Tactic:
simp
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
a : α
⊢ (F.nhds a).σ = { s : F.σ // a ∈ F.F.f s }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
a : α
s : (F.nhds a).σ
⊢ (F.nhds a).F.f s = F.F.f (↑s : F.σ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
m : β → α
f : Filter β
F : Filter.Realizer.{u_2, u_5} f
R : Realizer.{u_6, u_1} α
a : α
⊢ Tendsto m f (𝓝 a) ↔ ∀ (t : R.σ), a ∈ R.F.f t → ∃ (s : F.σ), ∀ x ∈ F.F.f s, m x ∈ R.F.f t

Tactic:
(F.tendsto_iff _ (R.nhds a)).trans Subtype.forall

Premises used: Subtype.forall, Ctop.Realizer.nhds, Iff.trans, Filter.Realizer.tendsto_iff
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
F : Ctop.Realizer.{u_5, u_1} α
f : β → Set α
R : Realizer F f
⊢ LocallyFinite f

Tactic:
fun a ↦
  ⟨_, F.mem_nhds.2 ⟨(R.bas a).1, (R.bas a).2, Subset.rfl⟩, have := R.sets a; Set.toFinite _⟩

Premises used: Iff.mpr, setOf, Ctop.f, Ctop.Realizer.mem_nhds, LocallyFinite, Inter.inter, Set.toFinite, Set.Nonempty, Set.Subset.rfl, And.intro, Exists.intro, LocallyFinite.Realizer.bas, LocallyFinite.Realizer.sets, Subtype.val, Ctop.Realizer.F, Subtype.property