awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Z
g : Y → Z
mp :
  ((IsInducing f ∧
        IsInducing g ∧
          Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))) ∧
      Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b) →
    (IsInducing f ∧ Injective f) ∧
      (IsInducing g ∧ Injective g) ∧
        Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))
mpr :
  (IsInducing f ∧ Injective f) ∧
      (IsInducing g ∧ Injective g) ∧
        Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g)) →
    (IsInducing f ∧
        IsInducing g ∧
          Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))) ∧
      Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b
⊢ ((IsInducing f ∧
        IsInducing g ∧
          Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))) ∧
      Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b) ↔
    (IsInducing f ∧ Injective f) ∧
      (IsInducing g ∧ Injective g) ∧
        Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))

Tactic:
constructor
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Z
g : Y → Z
hf₁ : IsInducing f
hg₁ : IsInducing g
hFg : Disjoint (closure[inst_2] (range f)) (range g)
hfG : Disjoint (range f) (closure[inst_2] (range g))
hf₂ : Injective f
hg₂ : Injective g
f_ne_g : ∀ (a : X) (b : Y), f a ≠ g b
⊢ (IsInducing f ∧ Injective f) ∧
    (IsInducing g ∧ Injective g) ∧
      Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))

Tactic:
⟨⟨hf₁, hf₂⟩, ⟨hg₁, hg₂⟩, hFg, hfG⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Z
g : Y → Z
hf₁ : IsInducing f
hg₁ : IsInducing g
hFg : Disjoint (closure[inst_2] (range f)) (range g)
hfG : Disjoint (range f) (closure[inst_2] (range g))
hf₂ : Injective f
hg₂ : Injective g
f_ne_g : ∀ (a : X) (b : Y), f a ≠ g b
⊢ (IsInducing f ∧ Injective f) ∧
    (IsInducing g ∧ Injective g) ∧
      Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))

Tactic:
exact ⟨⟨hf₁, hf₂⟩, ⟨hg₁, hg₂⟩, hFg, hfG⟩
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Z
g : Y → Z
hf₁ : IsInducing f
hf₂ : Injective f
hg₁ : IsInducing g
hg₂ : Injective g
hFg : Disjoint (closure[inst_2] (range f)) (range g)
hfG : Disjoint (range f) (closure[inst_2] (range g))
⊢ (IsInducing f ∧
      IsInducing g ∧ Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))) ∧
    Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b

Tactic:
⟨⟨hf₁, hg₁, hFg, hfG⟩, ⟨hf₂, hg₂, ?_⟩⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Z
g : Y → Z
hf₁ : IsInducing f
hf₂ : Injective f
hg₁ : IsInducing g
hg₂ : Injective g
hFg : Disjoint (closure[inst_2] (range f)) (range g)
hfG : Disjoint (range f) (closure[inst_2] (range g))
mpr : ∀ (a : X) (b : Y), f a ≠ g b
⊢ (IsInducing f ∧
      IsInducing g ∧ Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))) ∧
    Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b

Tactic:
refine ⟨⟨hf₁, hg₁, hFg, hfG⟩, ⟨hf₂, hg₂, ?_⟩⟩
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Z
g : Y → Z
hf₁ : IsInducing f
hf₂ : Injective f
hg₁ : IsInducing g
hg₂ : Injective g
hFg : Disjoint (closure[inst_2] (range f)) (range g)
hfG : Disjoint (range f) (closure[inst_2] (range g))
⊢ ∀ (a : X) (b : Y), f a ≠ g b

Tactic:
fun a b ↦ hfG.ne_of_mem (mem_range_self a) (subset_closure (mem_range_self b))

Premises used: Set.mem_range_self, subset_closure, Disjoint.ne_of_mem
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Z
g : Y → Z
hf₁ : IsInducing f
hf₂ : Injective f
hg₁ : IsInducing g
hg₂ : Injective g
hFg : Disjoint (closure[inst_2] (range f)) (range g)
hfG : Disjoint (range f) (closure[inst_2] (range g))
⊢ ∀ (a : X) (b : Y), f a ≠ g b

Tactic:
exact fun a b ↦ hfG.ne_of_mem (mem_range_self a) (subset_closure (mem_range_self b))

Premises used: Set.mem_range_self, subset_closure, Disjoint.ne_of_mem
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsEmbedding f
hg : IsEmbedding g
hFg : Disjoint (closure[inst_2] (range f)) (range g)
hfG : Disjoint (range f) (closure[inst_2] (range g))
⊢ IsEmbedding (Sum.elim f g)

Tactic:
isEmbedding_sumElim.mpr ⟨hf, hg, hFg, hfG⟩

Premises used: Iff.mpr, isEmbedding_sumElim, And.intro
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsEmbedding f
hg : IsEmbedding g
hsep : SeparatedNhds (range f) (range g)
⊢ IsEmbedding (Sum.elim f g)

Tactic:
hf.sumElim hg hsep.disjoint_closure_left hsep.disjoint_closure_right

Premises used: SeparatedNhds.disjoint_closure_left, Topology.IsEmbedding.sumElim, SeparatedNhds.disjoint_closure_right
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Continuous[inst, instTopologicalSpaceAdditive] (⇑ofMul : (a : X) → Additive X)

Tactic:
continuous_id

Premises used: Additive, continuous_id
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Continuous[instTopologicalSpaceAdditive, inst] (⇑toMul : (a : Additive X) → X)

Tactic:
continuous_id

Premises used: Additive, continuous_id
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Continuous[inst, instTopologicalSpaceMultiplicative] (⇑ofAdd : (a : X) → Multiplicative X)

Tactic:
continuous_id

Premises used: Multiplicative, continuous_id
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Continuous[instTopologicalSpaceMultiplicative, inst] (⇑toAdd : (a : Multiplicative X) → X)

Tactic:
continuous_id

Premises used: Multiplicative, continuous_id
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsOpenMap.{u, u} (X := X) (Y := Additive X) (⇑ofMul : (a : X) → Additive X)

Tactic:
IsOpenMap.id

Premises used: Additive, IsOpenMap.id
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsOpenMap.{u, u} (X := Additive X) (Y := X) (⇑toMul : (a : Additive X) → X)

Tactic:
IsOpenMap.id

Premises used: Additive, IsOpenMap.id
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsOpenMap.{u, u} (X := X) (Y := Multiplicative X) (⇑ofAdd : (a : X) → Multiplicative X)

Tactic:
IsOpenMap.id

Premises used: Multiplicative, IsOpenMap.id
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsOpenMap.{u, u} (X := Multiplicative X) (Y := X) (⇑toAdd : (a : Multiplicative X) → X)

Tactic:
IsOpenMap.id

Premises used: Multiplicative, IsOpenMap.id
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsClosedMap.{u, u} (X := X) (Y := Additive X) (⇑ofMul : (a : X) → Additive X)

Tactic:
IsClosedMap.id

Premises used: Additive, IsClosedMap.id
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsClosedMap.{u, u} (X := Additive X) (Y := X) (⇑toMul : (a : Additive X) → X)

Tactic:
IsClosedMap.id

Premises used: Additive, IsClosedMap.id
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsClosedMap.{u, u} (X := X) (Y := Multiplicative X) (⇑ofAdd : (a : X) → Multiplicative X)

Tactic:
IsClosedMap.id

Premises used: Multiplicative, IsClosedMap.id
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsClosedMap.{u, u} (X := Multiplicative X) (Y := X) (⇑toAdd : (a : Multiplicative X) → X)

Tactic:
IsClosedMap.id

Premises used: Multiplicative, IsClosedMap.id
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ Eq (α := Filter (Additive X)) (𝓝 ((ofMul : (a : X) → Additive X) x) : Filter (Additive X))
    (map (⇑ofMul : (a : X) → Additive X) (𝓝 x) : Filter (Additive X))

Tactic:
rfl

Premises used: Set.Mem, Additive, Filter.map, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ Eq (α := Filter (Multiplicative X)) (𝓝 ((ofAdd : (a : X) → Multiplicative X) x) : Filter (Multiplicative X))
    (map (⇑ofAdd : (a : X) → Multiplicative X) (𝓝 x) : Filter (Multiplicative X))

Tactic:
rfl

Premises used: Set.Mem, Filter.map, setOf, Multiplicative, Set.preimage, rfl
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
x : Additive X
⊢ Eq (α := Filter X) (𝓝 ((toMul : (a : Additive X) → X) x) : Filter X)
    (map (⇑toMul : (a : Additive X) → X) (𝓝 x) : Filter X)

Tactic:
rfl

Premises used: Set.Mem, Additive, Filter.map, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
x : Multiplicative X
⊢ Eq (α := Filter X) (𝓝 ((toAdd : (a : Multiplicative X) → X) x) : Filter X)
    (map (⇑toAdd : (a : Multiplicative X) → X) (𝓝 x) : Filter X)

Tactic:
rfl

Premises used: Set.Mem, Filter.map, setOf, Multiplicative, Set.preimage, rfl
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Continuous[inst, instTopologicalSpace] (⇑toDual : (a : X) → Xᵒᵈ)

Tactic:
continuous_id

Premises used: continuous_id, OrderDual
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Continuous[instTopologicalSpace, inst] (⇑ofDual : (a : Xᵒᵈ) → X)

Tactic:
continuous_id

Premises used: continuous_id, OrderDual
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsOpenMap.{u, u} (X := X) (Y := Xᵒᵈ) (⇑toDual : (a : X) → Xᵒᵈ)

Tactic:
IsOpenMap.id

Premises used: IsOpenMap.id, OrderDual
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsOpenMap.{u, u} (X := Xᵒᵈ) (Y := X) (⇑ofDual : (a : Xᵒᵈ) → X)

Tactic:
IsOpenMap.id

Premises used: IsOpenMap.id, OrderDual
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsClosedMap.{u, u} (X := X) (Y := Xᵒᵈ) (⇑toDual : (a : X) → Xᵒᵈ)

Tactic:
IsClosedMap.id

Premises used: IsClosedMap.id, OrderDual
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsClosedMap.{u, u} (X := Xᵒᵈ) (Y := X) (⇑ofDual : (a : Xᵒᵈ) → X)

Tactic:
IsClosedMap.id

Premises used: IsClosedMap.id, OrderDual
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ Eq (α := Filter Xᵒᵈ) (𝓝 ((toDual : (a : X) → Xᵒᵈ) x) : Filter Xᵒᵈ) (map (⇑toDual : (a : X) → Xᵒᵈ) (𝓝 x) : Filter Xᵒᵈ)

Tactic:
rfl

Premises used: Set.Mem, Filter.map, setOf, Set.preimage, OrderDual, rfl
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ Eq (α := Filter X) (𝓝 ((ofDual : (a : Xᵒᵈ) → X) x) : Filter X) (map (⇑ofDual : (a : Xᵒᵈ) → X) (𝓝 x) : Filter X)

Tactic:
rfl

Premises used: Set.Mem, Filter.map, setOf, Set.preimage, OrderDual, rfl
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Setoid X
V : Set (Quotient s)
x : X
hs : Membership.mem (γ := Filter (Quotient s)) (𝓝 (Quotient.mk' x)) V
⊢ Quotient.mk' ⁻¹' V ∈ 𝓝 x

Tactic:
preimage_nhds_coinduced hs

Premises used: preimage_nhds_coinduced
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : Setoid X
inst_1 : TopologicalSpace X
s : Set X
H : Dense s
⊢ Dense (X := Quotient inst) (Quotient.mk' '' s)

Tactic:
Quotient.mk''_surjective.denseRange.dense_image continuous_coinduced_rng H

Premises used: Function.Surjective.denseRange, Quotient.mk''_surjective, Quotient.mk', DenseRange.dense_image, continuous_coinduced_rng
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : Setoid X
inst_1 : TopologicalSpace X
f : Y → X
hf : DenseRange f
⊢ DenseRange (X := Quotient inst) (Quotient.mk' ∘ f)

Tactic:
Quotient.mk''_surjective.denseRange.comp hf continuous_coinduced_rng

Premises used: Function.Surjective.denseRange, Quotient.mk''_surjective, Quotient.mk', DenseRange.comp, continuous_coinduced_rng
-- Module: Mathlib.Topology.Constructions
Goal:
α : Type u_5
inst : TopologicalSpace α
s t : Setoid α
h : s ≤ t
⊢ Continuous[instTopologicalSpaceQuotient, instTopologicalSpaceQuotient] (Setoid.map_of_le h)

Tactic:
continuous_coinduced_rng

Premises used: Set.Mem, setOf, Quotient, Set.preimage, Quotient.mk', IsOpen, Setoid.map_of_le, continuous_coinduced_rng
-- Module: Mathlib.Topology.Constructions
Goal:
α : Type u_5
inst : TopologicalSpace α
S : Set (Setoid α)
s : Setoid α
h : s ∈ S
⊢ Continuous[instTopologicalSpaceQuotient, instTopologicalSpaceQuotient] (Setoid.map_sInf (S := S) h)

Tactic:
continuous_coinduced_rng

Premises used: Set.Mem, setOf, Setoid.map_sInf, Quotient, Set.preimage, Quotient.mk', IsOpen, Setoid.map_of_le, continuous_coinduced_rng
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
p : X → Prop
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
⊢ DiscreteTopology.{u} (Subtype p)

Tactic:
⟨bot_unique fun s _ => ⟨(↑) '' s, isOpen_discrete _, preimage_image_eq _ Subtype.val_injective⟩⟩

Premises used: DiscreteTopology.mk, And.intro, isOpen_discrete, Exists.intro, bot_unique, Set.image
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : DiscreteTopology X
hY : DiscreteTopology Y
⊢ Eq (α := TopologicalSpace (X ⊕ Y)) (coinduced inl inst) ⊥ ∧
    Eq (α := TopologicalSpace (X ⊕ Y)) (coinduced inr inst_1) ⊥

Tactic:
simp [h.eq_bot, hY.eq_bot]

Premises used: DiscreteTopology.eq_bot
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y_1 : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
Y : ι → Type v
inst : (i : ι) → TopologicalSpace (Y i)
h : ∀ (i : ι), DiscreteTopology.{v} (Y i)
x : ι
⊢ coinduced (mk (β := Y) x) (inst x) = ⊥

Tactic:
simp only [(h _).eq_bot, coinduced_bot]

Premises used: coinduced_bot, DiscreteTopology.eq_bot
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : IndiscreteTopology X
hY : IndiscreteTopology Y
⊢ Eq (α := TopologicalSpace (X × Y)) (induced fst inst) ⊤ ∧ Eq (α := TopologicalSpace (X × Y)) (induced snd inst_1) ⊤

Tactic:
simp [h.eq_top, hY.eq_top]

Premises used: IndiscreteTopology.eq_top
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y_1 : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
Y : ι → Type v
inst : (i : ι) → TopologicalSpace (Y i)
h : ∀ (i : ι), IndiscreteTopology.{v} (Y i)
x : ι
⊢ Eq (α := TopologicalSpace ((i : ι) → Y i)) (induced (fun (f : (i : ι) → Y i) ↦ f x) (inst x)) ⊤

Tactic:
simp only [(h _).eq_top, induced_top]

Premises used: IndiscreteTopology.eq_top, induced_top
-- Module: Mathlib.Topology.Constructions
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
f : α → β
y : β
⊢ comap f (𝓝[range f] y) = comap f (𝓝 y)

Tactic:
comap_inf_principal_range

Premises used: nhdsWithin, Filter.comap_inf_principal_range
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
x : { x : X // x ∈ s }
t : Set { x : X // x ∈ s }
⊢ t ∈ 𝓝 x ↔ ∃ u ∈ 𝓝 (↑x : X), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' u ⊆ t

Tactic:
mem_nhds_induced _ x t

Premises used: Set.Mem, mem_nhds_induced
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
x : { x : X // x ∈ s }
⊢ 𝓝 x = comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X))

Tactic:
nhds_induced _ x

Premises used: nhds_induced
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
x : { x : X // x ∈ s }
rw :
  Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X)))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[s] (↑x : X)))
rw₁ :
  Eq (α := Filter { x : X // x ∈ s })
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s))
      (𝓝[range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))] (↑x : X)))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[s] (↑x : X)))
rw₂ rw₃ :
  Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[s] (↑x : X)))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[s] (↑x : X)))
⊢ 𝓝 x = comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[s] (↑x : X))

Tactic:
rw [nhds_subtype, ← comap_nhdsWithin_range, Subtype.range_val]

Premises used: comap_nhdsWithin_range, Subtype.range_val, nhds_subtype
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
x : (↑s : Type u)
rw :
  𝓝[s ↓∩ t] x = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[t] (↑x : X))) ⊥
rw₁ :
  𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[t] (↑x : X))) ⊥
rw₂ :
  𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X) ⊓ 𝓟 t)) ⊥
rw₃ :
  𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s })
      (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X)) ⊓
        comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓟 t))
      ⊥
rw₄ :
  𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s })
      (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X)) ⊓ 𝓟 (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)) ⊥
rw₅ rw₆ :
  Eq (α := Filter (↑s : Type u)) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X)) ⊓ 𝓟 (s ↓∩ t)) ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s })
      (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X)) ⊓ 𝓟 (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)) ⊥
⊢ 𝓝[s ↓∩ t] x = ⊥ ↔ 𝓝[t] (↑x : X) ⊓ 𝓟 s = ⊥

Tactic:
rw [inf_principal_eq_bot_iff_comap, nhdsWithin, nhdsWithin, comap_inf, comap_principal,
    nhds_induced]

Premises used: Filter.inf_principal_eq_bot_iff_comap, nhdsWithin, Filter.comap_inf, nhds_induced, Filter.comap_principal
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
S : Set X
x : (↑S : Type u)
rw : 𝓝[≠] x = ⊥ ↔ 𝓝[S ↓∩ {(↑x : X)}ᶜ] x = ⊥
rw₁ : 𝓝[≠] x = ⊥ ↔ 𝓝[(S ↓∩ {(↑x : X)})ᶜ] x = ⊥
rw₂ : 𝓝[≠] x = ⊥ ↔ 𝓝[(S ↓∩ ↑{x})ᶜ] x = ⊥
rw₃ rw₄ : 𝓝[≠] x = ⊥ ↔ 𝓝[≠] x = ⊥
⊢ 𝓝[≠] x = ⊥ ↔ 𝓝[≠] (↑x : X) ⊓ 𝓟 S = ⊥

Tactic:
rw [← nhdsWithin_subtype_eq_bot_iff, preimage_compl, ← image_singleton,
    Subtype.coe_injective.preimage_image]

Premises used: Set.image_singleton, Subtype.coe_injective, Function.Injective.preimage_image, nhdsWithin_subtype_eq_bot_iff, Set.preimage_compl
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
S : Set X
x : (↑S : Type u)
rw : 𝓝[≠] x ≠ ⊥ ↔ (𝓝[≠] (↑x : X) ⊓ 𝓟 S).NeBot
rw₁ : 𝓝[≠] x ≠ ⊥ ↔ 𝓝[≠] (↑x : X) ⊓ 𝓟 S ≠ ⊥
rw₂ : 𝓝[≠] x = ⊥ ↔ 𝓝[≠] (↑x : X) ⊓ 𝓟 S = ⊥
rw₃ rw₄ : 𝓝[≠] (↑x : X) ⊓ 𝓟 S = ⊥ ↔ 𝓝[≠] (↑x : X) ⊓ 𝓟 S = ⊥
⊢ (𝓝[≠] x).NeBot ↔ (𝓝[≠] (↑x : X) ⊓ 𝓟 S).NeBot

Tactic:
rw [neBot_iff, neBot_iff, not_iff_not, nhds_ne_subtype_eq_bot_iff]

Premises used: not_iff_not, nhds_ne_subtype_eq_bot_iff, Filter.neBot_iff
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u_5
inst : TopologicalSpace X
s : Set X
⊢ IsDiscrete s ↔ DiscreteTopology.{u_5} (↑s : Type u_5)

Tactic:
⟨fun s ↦ s.to_subtype, fun s ↦ ⟨s⟩⟩

Premises used: IsDiscrete.to_subtype, IsDiscrete.mk, Iff.intro
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u_5
inst : TopologicalSpace X
S : Type u_6
inst_1 : SetLike S X
s : S
⊢ IsDiscrete (↑s : Set X) ↔ DiscreteTopology.{u_5} ↥s

Tactic:
⟨fun s ↦ s.to_subtype, fun s ↦ ⟨s⟩⟩

Premises used: IsDiscrete.to_subtype, IsDiscrete.mk, Iff.intro
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u_5
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology.{u_5} (↑s : Type u_5)
⊢ IsDiscrete s

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, IsDiscrete.mk
-- Module: Mathlib.Topology.Constructions
Goal:
X_1 : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
⊢ Set.Nonempty.{u_5} (α := X) univ → Set.Finite.{u_5} (α := X) univᶜ

Tactic:
simp
-- Module: Mathlib.Topology.Constructions
Goal:
X_1 : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
s t : Set X
hs : s.Nonempty → sᶜ.Finite
ht : t.Nonempty → tᶜ.Finite
x : X
hxs : x ∈ s
hxt : x ∈ t
rw : (sᶜ ∪ tᶜ).Finite
⊢ (s ∩ t)ᶜ.Finite

Tactic:
rw [compl_inter]

Premises used: Set.compl_inter
-- Module: Mathlib.Topology.Constructions
Goal:
X_1 : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
s t : Set X
hs : s.Nonempty → sᶜ.Finite
ht : t.Nonempty → tᶜ.Finite
x : X
hxs : x ∈ s
hxt : x ∈ t
⊢ (sᶜ ∪ tᶜ).Finite

Tactic:
(hs ⟨x, hxs⟩).union (ht ⟨x, hxt⟩)

Premises used: Set.Finite.union, Exists.intro
-- Module: Mathlib.Topology.Constructions
Goal:
X_1 : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
s t : Set X
hs : s.Nonempty → sᶜ.Finite
ht : t.Nonempty → tᶜ.Finite
x : X
hxs : x ∈ s
hxt : x ∈ t
⊢ (sᶜ ∪ tᶜ).Finite

Tactic:
exact (hs ⟨x, hxs⟩).union (ht ⟨x, hxt⟩)

Premises used: Set.Finite.union, Exists.intro
-- Module: Mathlib.Topology.Constructions
Goal:
X_1 : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
s : Set (Set X)
h : ∀ t ∈ s, t.Nonempty → tᶜ.Finite
x : X
t : Set X
hts : t ∈ s
hzt : x ∈ t
rw : (⋂₀ (compl '' s)).Finite
⊢ (⋃₀ s)ᶜ.Finite

Tactic:
rw [compl_sUnion]

Premises used: Set.compl_sUnion
-- Module: Mathlib.Topology.Constructions
Goal:
X_1 : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
s : Set (Set X)
h : ∀ t ∈ s, t.Nonempty → tᶜ.Finite
x : X
t : Set X
hts : t ∈ s
hzt : x ∈ t
⊢ (⋂₀ (compl '' s)).Finite

Tactic:
Finite.sInter (mem_image_of_mem _ hts) (h t hts ⟨x, hzt⟩)

Premises used: Set.Finite.sInter, Set.mem_image_of_mem, Exists.intro
-- Module: Mathlib.Topology.Constructions
Goal:
X_1 : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
s : Set (Set X)
h : ∀ t ∈ s, t.Nonempty → tᶜ.Finite
x : X
t : Set X
hts : t ∈ s
hzt : x ∈ t
⊢ (⋂₀ (compl '' s)).Finite

Tactic:
exact Finite.sInter (mem_image_of_mem _ hts) (h t hts ⟨x, hzt⟩)

Premises used: Set.Finite.sInter, Set.mem_image_of_mem, Exists.intro