awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.FiberPartition
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
w : (↑(Set.range f) : Type u_2)
val : S
hx_1 :
  val ∈
    (↑(Subtype.mk (p := fun (x : Set S) ↦
          Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) x)
          ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w) ⋯) :
      Set S)
hx : f val = (↑w : Y)
w_1 : (↑(Set.range f) : Type u_2)
val_1 : S
hy_1 :
  val_1 ∈
    (↑(Subtype.mk (p := fun (x : Set S) ↦
          Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) x)
          ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w_1) ⋯) :
      Set S)
hy : f val_1 = (↑w_1 : Y)
h : val = val_1
⊢ Sigma.fst (β := fun (a : Fiber f) ↦ { x : S // x ∈ (↑a : Set S) })
      (Sigma.mk (β := fun (x : Fiber f) ↦ (↑(↑x : Set S) : Type u_1))
        (Subtype.mk (p := fun (x : Set S) ↦
          Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) x)
          ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w) ⋯)
        (Subtype.mk (p := fun (x : S) ↦
          x ∈
            (↑(Subtype.mk (p := fun (x : Set S) ↦
                  Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)})
                    x)
                  ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w) ⋯) :
              Set S))
          val hx_1)) =
    Sigma.fst (β := fun (a : Fiber f) ↦ { x : S // x ∈ (↑a : Set S) })
      (Sigma.mk (β := fun (x : Fiber f) ↦ (↑(↑x : Set S) : Type u_1))
        (Subtype.mk (p := fun (x : Set S) ↦
          Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) x)
          ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w_1) ⋯)
        (Subtype.mk (p := fun (x : S) ↦
          x ∈
            (↑(Subtype.mk (p := fun (x : Set S) ↦
                  Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)})
                    x)
                  ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w_1) ⋯) :
              Set S))
          val_1 hy_1))

Tactic:
simp [← hx, ← hy, h]
-- Module: Mathlib.Topology.FiberPartition
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
⊢ Surjective (α := (x : Fiber f) × (↑(↑x : Set S) : Type u_1)) (β := S)
    (⇑(sigmaIsoHom f) : (a : (x : Fiber f) × (↑(↑x : Set S) : Type u_1)) → S)

Tactic:
fun _ ↦ ⟨⟨⟨_, ⟨⟨_, Set.mem_range_self _⟩, rfl⟩⟩, ⟨_, rfl⟩⟩, rfl⟩

Premises used: Set.mem_range_self, Subtype.mk, Set.preimage, Exists.intro, Sigma.mk, Singleton.singleton, Subtype.val, Function.Surjective, rfl
-- Module: Mathlib.Topology.FiberPartition
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (Y := (↑(↑a : Set S) : Type u_1)) (f ∘ (⇑(sigmaIncl (g ∘ f) a) : (a : (↑(↑a : Set S) : Type u_1)) → S))
x : (↑(↑b : Set (↑(↑a : Set S) : Type u_1)) : Type u_1)
⊢ (↑x : (↑(↑a : Set S) : Type u_1)) ∈ (↑b : Set (↑(↑a : Set S) : Type u_1))

Tactic:
have := x.prop
-- Module: Mathlib.Topology.FiberPartition
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (Y := (↑(↑a : Set S) : Type u_1)) (f ∘ (⇑(sigmaIncl (g ∘ f) a) : (a : (↑(↑a : Set S) : Type u_1)) → S))
x : (↑(↑b : Set (↑(↑a : Set S) : Type u_1)) : Type u_1)
this : (↑x : (↑(↑a : Set S) : Type u_1)) ∈ (↑b : Set (↑(↑a : Set S) : Type u_1))
⊢ f (↑(↑x : (↑(↑a : Set S) : Type u_1)) : S) = Fiber.image (f ∘ fun (x : (↑(↑a : Set S) : Type u_1)) ↦ (↑x : S)) b

Tactic:
simp only [sigmaIncl, ContinuousMap.coe_mk, Fiber.mem_iff_eq_image, comp_apply] at this

Premises used: Function.Fiber.mem_iff_eq_image, ContinuousMap.coe_mk, Function.comp_apply, TopologicalSpace.Fiber.sigmaIncl
-- Module: Mathlib.Topology.FiberPartition
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (Y := (↑(↑a : Set S) : Type u_1)) (f ∘ (⇑(sigmaIncl (g ∘ f) a) : (a : (↑(↑a : Set S) : Type u_1)) → S))
x : (↑(↑b : Set (↑(↑a : Set S) : Type u_1)) : Type u_1)
this : f (↑(↑x : (↑(↑a : Set S) : Type u_1)) : S) = Fiber.image (f ∘ fun (x : (↑(↑a : Set S) : Type u_1)) ↦ (↑x : S)) b
rw :
  (f ∘ fun (x : (↑(↑a : Set S) : Type u_1)) ↦ (↑x : S))
      (Fiber.preimage (f ∘ fun (x : (↑(↑a : Set S) : Type u_1)) ↦ (↑x : S)) b) =
    f (↑(Fiber.preimage (f ∘ (⇑(sigmaIncl (g ∘ f) a) : (a : (↑(↑a : Set S) : Type u_1)) → S)) b) : S)
⊢ (↑(↑x : (↑(↑a : Set S) : Type u_1)) : S) ∈
    (↑(Fiber.mk f (↑(Fiber.preimage (f ∘ (⇑(sigmaIncl (g ∘ f) a) : (a : (↑(↑a : Set S) : Type u_1)) → S)) b) : S)) :
      Set S)

Tactic:
rw [Fiber.mem_iff_eq_image, Fiber.mk_image, this, ← Fiber.map_preimage_eq_image]

Premises used: Function.Fiber.mem_iff_eq_image, Function.Fiber.mk_image, Function.Fiber.map_preimage_eq_image
-- Module: Mathlib.Topology.FiberPartition
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (Y := (↑(↑a : Set S) : Type u_1)) (f ∘ (⇑(sigmaIncl (g ∘ f) a) : (a : (↑(↑a : Set S) : Type u_1)) → S))
x : (↑(↑b : Set (↑(↑a : Set S) : Type u_1)) : Type u_1)
this : f (↑(↑x : (↑(↑a : Set S) : Type u_1)) : S) = Fiber.image (f ∘ fun (x : (↑(↑a : Set S) : Type u_1)) ↦ (↑x : S)) b
⊢ (f ∘ fun (x : (↑(↑a : Set S) : Type u_1)) ↦ (↑x : S))
      (Fiber.preimage (f ∘ fun (x : (↑(↑a : Set S) : Type u_1)) ↦ (↑x : S)) b) =
    f (↑(Fiber.preimage (f ∘ (⇑(sigmaIncl (g ∘ f) a) : (a : (↑(↑a : Set S) : Type u_1)) → S)) b) : S)

Tactic:
simp [sigmaIncl]

Premises used: TopologicalSpace.Fiber.sigmaIncl
-- Module: Mathlib.Topology.FiberPartition
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
l : LocallyConstant S Y
inst_1 : CompactSpace S
x : Fiber.{u_1, u_2} (Y := S) (Z := Y) (⇑l : (a : S) → Y)
obtain :
  ∀ (y : (↑(Set.range.{u_2, u_1 + 1} (ι := S) (⇑l : (a : S) → Y)) : Type u_2))
    (hy :
      (fun (x : (↑(Set.range.{u_2, u_1 + 1} (ι := S) (⇑l : (a : S) → Y)) : Type u_2)) ↦
            (Set.preimage (β := Y) (⇑l : (a : S) → Y) {(↑x : Y)} : Set S))
          y =
        (↑x : Set S)),
    CompactSpace.{u_1} (↑(↑x : Set S) : Type u_1)
⊢ CompactSpace.{u_1} (↑(↑x : Set S) : Type u_1)

Tactic:
obtain ⟨y, hy⟩ := x.prop

Premises used: Subtype.prop
-- Module: Mathlib.Topology.FiberPartition
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
l : LocallyConstant S Y
inst_1 : CompactSpace S
x : Fiber.{u_1, u_2} (Y := S) (Z := Y) (⇑l : (a : S) → Y)
y : (↑(Set.range.{u_2, u_1 + 1} (ι := S) (⇑l : (a : S) → Y)) : Type u_2)
hy :
  (fun (x : (↑(Set.range.{u_2, u_1 + 1} (ι := S) (⇑l : (a : S) → Y)) : Type u_2)) ↦
        (Set.preimage (β := Y) (⇑l : (a : S) → Y) {(↑x : Y)} : Set S))
      y =
    (↑x : Set S)
rw :
  IsCompact.{u_1} (X := S)
    ((fun (x : (↑(Set.range.{u_2, u_1 + 1} (ι := S) (⇑l : (a : S) → Y)) : Type u_2)) ↦
        (Set.preimage (β := Y) (⇑l : (a : S) → Y) {(↑x : Y)} : Set S))
      y)
⊢ CompactSpace.{u_1} (↑(↑x : Set S) : Type u_1)

Tactic:
rw [← isCompact_iff_compactSpace, ← hy]

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.Topology.FiberPartition
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
l : LocallyConstant S Y
inst_1 : CompactSpace S
x : Fiber.{u_1, u_2} (Y := S) (Z := Y) (⇑l : (a : S) → Y)
y : (↑(Set.range.{u_2, u_1 + 1} (ι := S) (⇑l : (a : S) → Y)) : Type u_2)
hy :
  (fun (x : (↑(Set.range.{u_2, u_1 + 1} (ι := S) (⇑l : (a : S) → Y)) : Type u_2)) ↦
        (Set.preimage (β := Y) (⇑l : (a : S) → Y) {(↑x : Y)} : Set S))
      y =
    (↑x : Set S)
⊢ IsCompact.{u_1} (X := S)
    ((fun (x : (↑(Set.range.{u_2, u_1 + 1} (ι := S) (⇑l : (a : S) → Y)) : Type u_2)) ↦
        (Set.preimage (β := Y) (⇑l : (a : S) → Y) {(↑x : Y)} : Set S))
      y)

Tactic:
(l.2.isClosed_fiber _).isCompact

Premises used: Set.Mem, IsLocallyConstant.isClosed_fiber, setOf, LocallyConstant.isLocallyConstant, Set.preimage, IsClosed.isCompact, Set.singleton
-- Module: Mathlib.Topology.FiberPartition
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
l : LocallyConstant S Y
inst_1 : CompactSpace S
x : Fiber.{u_1, u_2} (Y := S) (Z := Y) (⇑l : (a : S) → Y)
y : (↑(Set.range.{u_2, u_1 + 1} (ι := S) (⇑l : (a : S) → Y)) : Type u_2)
hy :
  (fun (x : (↑(Set.range.{u_2, u_1 + 1} (ι := S) (⇑l : (a : S) → Y)) : Type u_2)) ↦
        (Set.preimage (β := Y) (⇑l : (a : S) → Y) {(↑x : Y)} : Set S))
      y =
    (↑x : Set S)
⊢ IsCompact.{u_1} (X := S)
    ((fun (x : (↑(Set.range.{u_2, u_1 + 1} (ι := S) (⇑l : (a : S) → Y)) : Type u_2)) ↦
        (Set.preimage (β := Y) (⇑l : (a : S) → Y) {(↑x : Y)} : Set S))
      y)

Tactic:
exact (l.2.isClosed_fiber _).isCompact

Premises used: IsLocallyConstant.isClosed_fiber, LocallyConstant.isLocallyConstant, IsClosed.isCompact
-- Module: Mathlib.Topology.FiberPartition
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
l : LocallyConstant S Y
inst_1 : CompactSpace S
⊢ Finite.{u_1 + 1} (Fiber.{u_1, u_2} (Y := S) (Z := Y) (⇑l : (a : S) → Y))

Tactic:
have : Finite (Set.range l) := l.range_finite
  Finite.Set.finite_range _

Premises used: LocallyConstant.range_finite, Finite.Set.finite_range, Set.preimage, Singleton.singleton, Subtype.val, DFunLike.coe, Function.Fiber
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
s : Set α
⊢ IsOpen (Iic (𝓟 s))

Tactic:
GenerateOpen.basic _ (mem_range_self _)

Premises used: Set.mem_range_self, TopologicalSpace.GenerateOpen.basic, IsOpen
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
s : Set α
⊢ IsOpen.{u_2} (X := Filter α) {l : Filter α | s ∈ l}

Tactic:
simpa only [Iic_principal] using isOpen_Iic_principal

Premises used: Filter.Iic_principal, Filter.isOpen_Iic_principal
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
s t : Set α
l : Filter α
hl : l ∈ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ (Iic ∘ 𝓟) (s ∩ t) = Iic (𝓟 s) ∩ Iic (𝓟 t)

Tactic:
simp
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
s t : Set α
l : Filter α
hl : l ∈ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ ∃ (t₃ : Set (Filter α)),
    Membership.mem (γ := Set (Set (Filter α))) (range (Iic ∘ 𝓟)) t₃ ∧ l ∈ t₃ ∧ t₃ ⊆ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t

Tactic:
exact ⟨Iic (𝓟 s) ∩ Iic (𝓟 t), ⟨s ∩ t, by simp⟩, hl, Subset.rfl⟩
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
s : Set (Filter α)
⊢ (∃ S ⊆ range (Iic ∘ 𝓟), s = ⋃₀ S) ↔ ∃ (T : Set (Set α)), s = ⋃ t ∈ T, Iic (𝓟 t)

Tactic:
simp only [exists_subset_range_and_iff, sUnion_image, (· ∘ ·)]

Premises used: Set.exists_subset_range_and_iff, Function.comp, Set.sUnion_image
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
l : Filter α
⊢ ⨅ (s : Set (Filter α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Filter α)))
          {s : Set (Filter α) | l ∈ s ∧ Membership.mem (γ := Set (Set (Filter α))) (range (Iic ∘ 𝓟)) s} s),
        𝓟 s =
    l.lift' (Iic ∘ 𝓟)

Tactic:
simp only [mem_setOf_eq, @and_comm (l ∈ _), iInf_and, iInf_range, Filter.lift', Filter.lift,
      (· ∘ ·), mem_Iic, le_principal_iff]

Premises used: Filter.le_principal_iff, iInf_range, Function.comp, Set.mem_setOf_eq, and_comm, Filter.lift', Filter.lift, iInf_and, Set.mem_Iic
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
l : Filter α
⊢ 𝓝 l = l.lift' fun (s : Set α) ↦ {l' : Filter α | s ∈ l'}

Tactic:
simpa only [Function.comp_def, Iic_principal] using nhds_eq l

Premises used: Filter.nhds_eq, Function.comp_def, Filter.Iic_principal
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
β : Type u_3
la : Filter α
lb : Filter β
f : α → Filter β
⊢ Tendsto f la (𝓝 lb) ↔ ∀ s ∈ lb, ∀ᶠ (a : α) in la, s ∈ f a

Tactic:
simp only [nhds_eq', tendsto_lift', mem_setOf_eq]

Premises used: Filter.tendsto_lift', Filter.nhds_eq', Set.mem_setOf_eq
-- Module: Mathlib.Topology.Filter
Goal:
ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
rw : (l.lift' (Iic ∘ 𝓟)).HasBasis p fun (i : ι) ↦ Iic (𝓟 (s i))
⊢ (𝓝 l).HasBasis p fun (i : ι) ↦ Iic (𝓟 (s i))

Tactic:
rw [nhds_eq]

Premises used: Filter.nhds_eq
-- Module: Mathlib.Topology.Filter
Goal:
ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (l.lift' (Iic ∘ 𝓟)).HasBasis p fun (i : ι) ↦ Iic (𝓟 (s i))

Tactic:
h.lift' monotone_principal.Iic

Premises used: setOf, Set.Iic, Monotone.Iic, Filter.HasBasis.lift', Filter.monotone_principal
-- Module: Mathlib.Topology.Filter
Goal:
ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (l.lift' (Iic ∘ 𝓟)).HasBasis p fun (i : ι) ↦ Iic (𝓟 (s i))

Tactic:
exact h.lift' monotone_principal.Iic

Premises used: Monotone.Iic, Filter.HasBasis.lift', Filter.monotone_principal
-- Module: Mathlib.Topology.Filter
Goal:
X : Type u_4
l : Filter X
rw : ∀ s ∈ l, ∀ᶠ (a : X) in l, Membership.mem (γ := Filter X) (pure a) s
⊢ Tendsto pure l (𝓝 l)

Tactic:
rw [Filter.tendsto_nhds]

Premises used: Filter.tendsto_nhds
-- Module: Mathlib.Topology.Filter
Goal:
X : Type u_4
l : Filter X
⊢ ∀ s ∈ l, ∀ᶠ (a : X) in l, Membership.mem (γ := Filter X) (pure a) s

Tactic:
fun s hs ↦ Eventually.mono hs fun x ↦ id

Premises used: id, Filter.Eventually.mono
-- Module: Mathlib.Topology.Filter
Goal:
X : Type u_4
l : Filter X
⊢ ∀ s ∈ l, ∀ᶠ (a : X) in l, Membership.mem (γ := Filter X) (pure a) s

Tactic:
exact fun s hs ↦ Eventually.mono hs fun x ↦ id

Premises used: id, Filter.Eventually.mono
-- Module: Mathlib.Topology.Filter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter α
inst : l.IsCountablyGenerated
⊢ (𝓝 l).IsCountablyGenerated

Tactic:
let ⟨_b, hb⟩ := l.exists_antitone_basis
  HasCountableBasis.isCountablyGenerated <| ⟨hb.nhds, Set.to_countable _⟩

Premises used: Filter.HasCountableBasis.mk, Filter.HasAntitoneBasis.toHasBasis, setOf, Filter.HasBasis.nhds, nhds, Filter.HasCountableBasis.isCountablyGenerated, Filter.IsCountablyGenerated, True, Set.to_countable, Filter.exists_antitone_basis, _private.0.Filter.instIsCountablyGeneratedNhds.match_1
-- Module: Mathlib.Topology.Filter
Goal:
ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (𝓝 l).HasBasis p fun (i : ι) ↦ {l' : Filter α | s i ∈ l'}

Tactic:
simpa only [Iic_principal] using h.nhds

Premises used: Filter.HasBasis.nhds, Filter.Iic_principal
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
l : Filter α
S : Set (Filter α)
⊢ S ∈ 𝓝 l ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ S

Tactic:
l.basis_sets.nhds.mem_iff

Premises used: Filter.HasBasis.mem_iff, Filter.HasBasis.nhds, Filter.basis_sets
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
l : Filter α
S : Set (Filter α)
⊢ S ∈ 𝓝 l ↔ ∃ t ∈ l, ∀ ⦃l' : Filter α⦄, t ∈ l' → l' ∈ S

Tactic:
l.basis_sets.nhds'.mem_iff

Premises used: Filter.HasBasis.mem_iff, Set.Mem, setOf, Set.Subset, Filter.basis_sets, Filter.HasBasis.nhds'
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
⊢ Eq.{u_2 + 1} (α := Filter (Filter α)) (𝓝 ⊥) (pure ⊥)

Tactic:
simp [nhds_eq, Function.comp_def, lift'_bot monotone_principal.Iic]

Premises used: Filter.lift'_bot, Filter.nhds_eq, Function.comp_def, Monotone.Iic, Filter.monotone_principal
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
⊢ Eq.{u_2 + 1} (α := Filter (Filter α)) (𝓝 ⊤) ⊤

Tactic:
simp [nhds_eq]

Premises used: Filter.nhds_eq
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
s : Set α
⊢ 𝓝 (𝓟 s) = 𝓟 (Iic (𝓟 s))

Tactic:
(hasBasis_principal s).nhds.eq_of_same_basis (hasBasis_principal _)

Premises used: Filter.HasBasis.nhds, Filter.hasBasis_principal, Filter.HasBasis.eq_of_same_basis
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
x : α
rw : Eq (α := Filter (Filter α)) (𝓝 (𝓟 {x})) (𝓟 {⊥, 𝓟 {x}})
rw₁ : Eq (α := Filter (Filter α)) (𝓟 (Iic (𝓟 {x}))) (𝓟 {⊥, 𝓟 {x}})
rw₂ : Eq (α := Filter (Filter α)) (𝓟 (Iic (pure x))) (𝓟 {⊥, pure x})
rw₃ rw₄ : Eq (α := Filter (Filter α)) (𝓟 {⊥, pure x}) (𝓟 {⊥, pure x})
⊢ Eq (α := Filter (Filter α)) (𝓝 (pure x)) (𝓟 {⊥, pure x})

Tactic:
rw [← principal_singleton, nhds_principal, principal_singleton, Iic_pure]

Premises used: Filter.Iic_pure, Filter.nhds_principal, Filter.principal_singleton
-- Module: Mathlib.Topology.Filter
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
simp :
  Eq.{u_2 + 1} (α := Filter (Filter α)) (Filter.lift' (⨅ (i : ι), f i) (Iic ∘ 𝓟)) (⨅ (i : ι), (f i).lift' (Iic ∘ 𝓟))
⊢ Eq.{u_2 + 1} (α := Filter (Filter α)) (𝓝 (⨅ (i : ι), f i)) (⨅ (i : ι), 𝓝 (f i))

Tactic:
simp only [nhds_eq]

Premises used: Filter.nhds_eq
-- Module: Mathlib.Topology.Filter
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
hg : ∀ {s t : Set α}, (Iic ∘ 𝓟) (s ∩ t) = (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
hg' : Eq.{u_2 + 1} (α := Set (Filter α)) ((Iic ∘ 𝓟) univ) univ
⊢ Eq.{u_2 + 1} (α := Filter (Filter α)) (Filter.lift' (⨅ (i : ι), f i) (Iic ∘ 𝓟)) (⨅ (i : ι), (f i).lift' (Iic ∘ 𝓟))

Tactic:
apply lift'_iInf_of_map_univ

Premises used: Filter.lift'_iInf_of_map_univ
-- Module: Mathlib.Topology.Filter
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ ∀ {s t : Set α}, (Iic ∘ 𝓟) (s ∩ t) = (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t

Tactic:
simp
-- Module: Mathlib.Topology.Filter
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ Eq.{u_2 + 1} (α := Set (Filter α)) ((Iic ∘ 𝓟) univ) univ

Tactic:
simp
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
l₁ l₂ : Filter α
⊢ 𝓝 (l₁ ⊓ l₂) = 𝓝 l₁ ⊓ 𝓝 l₂

Tactic:
simpa only [iInf_bool_eq] using Filter.nhds_iInf fun b => cond b l₁ l₂

Premises used: cond, iInf_bool_eq, Filter.nhds_iInf
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
⊢ Monotone.{u_2, u_2} (α := Filter α) 𝓝

Tactic:
Monotone.of_map_inf Filter.nhds_inf

Premises used: Monotone.of_map_inf, Filter.nhds_inf
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
l : Filter α
simp_rw : ⋂₀ {s : Set (Filter α) | s ∈ l.lift' (Iic ∘ 𝓟)} = Iic l
simp_rw₁ :
  ⋂₀ {s : Set (Filter α) | Membership.mem (γ := Filter (Filter α)) (l.lift' fun (x : Set α) ↦ Iic (𝓟 x)) s} = Iic l
simp_rw₂ : ⋂ s ∈ l, Iic (𝓟 s) = Iic l
simp_rw₃ : Eq.{u_2 + 1} (α := Set (Filter α)) (⋂ s ∈ l, {x : Filter α | x ≤ 𝓟 s}) {x : Filter α | x ≤ l}
simp_rw₄ : Eq.{u_2 + 1} (α := Set (Filter α)) (⋂ s ∈ l, {x : Filter α | s ∈ x}) {x : Filter α | x ≤ l}
simp_rw₅ : Eq.{u_2 + 1} (α := Set (Filter α)) {x : Filter α | ∀ (i : Set α) (i_1 : i ∈ l), i ∈ x} {x : Filter α | x ≤ l}
⊢ ⋂₀ {s : Set (Filter α) | s ∈ 𝓝 l} = Iic l

Tactic:
simp_rw [nhds_eq, Function.comp_def, sInter_lift'_sets monotone_principal.Iic, Iic,
    le_principal_iff, ← setOf_forall, ← Filter.le_def]

Premises used: Filter.le_principal_iff, Filter.nhds_eq, Filter.sInter_lift'_sets, Function.comp_def, Set.Iic, Monotone.Iic, Set.setOf_forall, Filter.le_def, Filter.monotone_principal
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
l₁ l₂ : Filter α
⊢ 𝓝 l₁ ≤ 𝓝 l₂ ↔ l₁ ≤ l₂

Tactic:
⟨fun h => ?_, fun h => monotone_nhds h⟩

Premises used: Filter.monotone_nhds, Iff.intro
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
l₁ l₂ : Filter α
refine : ∀ (h : 𝓝 l₁ ≤ 𝓝 l₂), l₁ ≤ l₂
⊢ 𝓝 l₁ ≤ 𝓝 l₂ ↔ l₁ ≤ l₂

Tactic:
refine ⟨fun h => ?_, fun h => monotone_nhds h⟩
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
rw : Subset.{u_2} (α := Set (Filter α)) (⋂₀ {s : Set (Filter α) | s ∈ 𝓝 l₁}) (⋂₀ {s : Set (Filter α) | s ∈ 𝓝 l₂})
⊢ l₁ ≤ l₂

Tactic:
rw [← Iic_subset_Iic, ← sInter_nhds, ← sInter_nhds]

Premises used: Set.Iic_subset_Iic, Filter.sInter_nhds
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ Subset.{u_2} (α := Set (Filter α)) (⋂₀ {s : Set (Filter α) | s ∈ 𝓝 l₁}) (⋂₀ {s : Set (Filter α) | s ∈ 𝓝 l₂})

Tactic:
sInter_subset_sInter h

Premises used: Set.sInter_subset_sInter
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ Subset.{u_2} (α := Set (Filter α)) (⋂₀ {s : Set (Filter α) | s ∈ 𝓝 l₁}) (⋂₀ {s : Set (Filter α) | s ∈ 𝓝 l₂})

Tactic:
exact sInter_subset_sInter h

Premises used: Set.sInter_subset_sInter
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
s : Set (Filter α)
l : Filter α
rw : s ∈ 𝓝 l ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s
rw₁ rw₂ : (∃ t ∈ l, Iic (𝓟 t) ⊆ s) ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s
⊢ l ∈ interior s ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s

Tactic:
rw [mem_interior_iff_mem_nhds, Filter.mem_nhds_iff]

Premises used: mem_interior_iff_mem_nhds, Filter.mem_nhds_iff
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
s : Set (Filter α)
l : Filter α
⊢ l ∈ closure s ↔ ∀ t ∈ l, ∃ l' ∈ s, t ∈ l'

Tactic:
simp only [closure_eq_compl_interior_compl, Filter.mem_interior, mem_compl_iff, not_exists,
    not_forall, Classical.not_not, exists_prop, not_and, and_comm, subset_def, mem_Iic,
    le_principal_iff]

Premises used: Filter.le_principal_iff, Set.subset_def, Classical.not_not, not_exists, and_comm, exists_prop, Filter.mem_interior, Set.mem_Iic, closure_eq_compl_interior_compl, not_and, Classical.not_forall, Set.mem_compl_iff
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
l : Filter α
h : ∀ (l' : Filter α), Membership.mem (γ := Set (Filter α)) (closure {l}) l' ↔ l' ∈ Ici l
⊢ closure {l} = Ici l

Tactic:
ext l'
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
l l' : Filter α
⊢ Membership.mem (γ := Set (Filter α)) (closure {l}) l' ↔ l' ∈ Ici l

Tactic:
simp [Filter.mem_closure, Filter.le_def]

Premises used: Filter.mem_closure, Filter.le_def
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
l₁ l₂ : Filter α
⊢ l₁ ⤳ l₂ ↔ l₁ ≤ l₂

Tactic:
simp only [specializes_iff_closure_subset, Filter.closure_singleton, Ici_subset_Ici]

Premises used: Set.Ici_subset_Ici, Filter.closure_singleton, specializes_iff_closure_subset
-- Module: Mathlib.Topology.Filter
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
⊢ T0Space.{u_2} (Filter α)

Tactic:
⟨fun _ _ h => (specializes_iff_le.1 h.specializes).antisymm
    (specializes_iff_le.1 h.symm.specializes)⟩

Premises used: LE.le.antisymm, T0Space.mk, Inseparable.specializes, Inseparable.symm, Iff.mp, Filter.specializes_iff_le
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
inst : Preorder α
⊢ Eq.{u_2 + 1} (α := Filter (Filter α)) (𝓝 atTop) (⨅ (x : α), 𝓟 (Iic (𝓟 (Ici x))))

Tactic:
simp only [atTop, Filter.nhds_iInf, nhds_principal]

Premises used: Filter.atTop, Filter.nhds_principal, Filter.nhds_iInf
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
β : Type u_3
inst : Preorder β
l : Filter α
f : α → Filter β
⊢ Tendsto f l (𝓝 atTop) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Ici y ∈ f a

Tactic:
simp only [nhds_atTop, tendsto_iInf, tendsto_principal, mem_Iic, le_principal_iff]

Premises used: Filter.le_principal_iff, Filter.tendsto_principal, Set.mem_Iic, Filter.tendsto_iInf, Filter.nhds_atTop
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
inst : Preorder α
⊢ Eq.{u_2 + 1} (α := Filter (Filter α)) (𝓝 atBot) (⨅ (x : α), 𝓟 (Iic (𝓟 (Iic x))))

Tactic:
@nhds_atTop αᵒᵈ _

Premises used: Set.Mem, setOf, Filter.atBot, Set.Iic, OrderDual, Filter.nhds_atTop
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
β : Type u_3
inst : Preorder β
l : Filter α
f : α → Filter β
⊢ Tendsto f l (𝓝 atBot) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Iic y ∈ f a

Tactic:
@Filter.tendsto_nhds_atTop_iff α βᵒᵈ _ _ _

Premises used: Set.Mem, setOf, Filter.tendsto_nhds_atTop_iff, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Topology.Filter
Goal:
X : Type u_4
inst : TopologicalSpace X
x : X
⊢ 𝓝 (𝓝 x) = ⨅ (s : Set X), ⨅ (_ : IsOpen[inst] s), ⨅ (_ : x ∈ s), 𝓟 (Iic (𝓟 s))

Tactic:
simp only [(nhds_basis_opens x).nhds.eq_biInf, iInf_and, @iInf_comm _ (_ ∈ _)]

Premises used: Filter.HasBasis.nhds, Filter.HasBasis.eq_biInf, iInf_and, iInf_comm, nhds_basis_opens
-- Module: Mathlib.Topology.Filter
Goal:
X : Type u_4
inst : TopologicalSpace X
x : X
⊢ ⨅ (s : Set X), ⨅ (_ : IsOpen[inst] s), ⨅ (_ : x ∈ s), 𝓟 s = comap 𝓝 (𝓝 (𝓝 x))

Tactic:
simp +contextual only [nhds_nhds, comap_iInf, comap_principal,
        Iic_principal, preimage_setOf_eq, ← mem_interior_iff_mem_nhds, setOf_mem_eq,
        IsOpen.interior_eq]

Premises used: mem_interior_iff_mem_nhds, Filter.comap_iInf, Set.setOf_mem_eq, Set.preimage_setOf_eq, Filter.comap_principal, Filter.nhds_nhds, IsOpen.interior_eq, Filter.Iic_principal
-- Module: Mathlib.Topology.Filter
Goal:
X : Type u_4
inst : TopologicalSpace X
⊢ Continuous[inst, _] 𝓝

Tactic:
isInducing_nhds.continuous

Premises used: Filter.isInducing_nhds, Topology.IsInducing.continuous