awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
toSetoid : Setoid X
isOpen_setOf_rel : ∀ (x : X), IsOpen[inst] (setOf ((toSetoid : X → X → Prop) x))
toSetoid_1 : Setoid X
isOpen_setOf_rel_1 : ∀ (x : X), IsOpen[inst] (setOf ((toSetoid_1 : X → X → Prop) x))
h :
  Eq.{u_2 + 1} (α := Set (Set X))
    ((fun (x : DiscreteQuotient X) ↦
        (match (motive := DiscreteQuotient X → Set (Set X)) x with
          | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
          Set (Set X)))
      { toSetoid := toSetoid, isOpen_setOf_rel := isOpen_setOf_rel })
    ((fun (x : DiscreteQuotient X) ↦
        (match (motive := DiscreteQuotient X → Set (Set X)) x with
          | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
          Set (Set X)))
      { toSetoid := toSetoid_1, isOpen_setOf_rel := isOpen_setOf_rel_1 })
⊢ toSetoid.classes = toSetoid_1.classes

Tactic:
exact h
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
α : Type u_1
X : Type u_2
inst : TopologicalSpace X
f : LocallyConstant X α
⊢ Eq (α := X → α) ((⇑f.lift : (a : Quotient f.discreteQuotient.toSetoid) → α) ∘ f.discreteQuotient.proj)
    (⇑f : (a : X) → α)

Tactic:
rfl

Premises used: Quotient.liftOn', rfl
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
Y : Type u_2
inst : TopologicalSpace Y
S : Set Y
simp_rw : (∀ (x : (↑S : Type u_2)), 𝓝[≠] x = ⊥) ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
simp_rw₁ : (∀ (x : (↑S : Type u_2)), 𝓝[≠] x = ⊥) ↔ ∀ (x : (↑S : Type u_2)), 𝓝[≠] (↑x : Y) ⊓ 𝓟 S = ⊥
⊢ DiscreteTopology.{u_2} (↑S : Type u_2) ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥

Tactic:
simp_rw [discreteTopology_iff_nhds_ne, SetCoe.forall', nhds_ne_subtype_eq_bot_iff]

Premises used: nhds_ne_subtype_eq_bot_iff, discreteTopology_iff_nhds_ne, SetCoe.forall'
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
Y : Type u_2
inst : TopologicalSpace Y
S : Set Y
rw : DiscreteTopology.{u_2} (↑S : Type u_2) ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
rw₁ rw₂ : (∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
⊢ IsDiscrete S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥

Tactic:
rw [isDiscrete_iff_discreteTopology, discreteTopology_subtype_iff]

Premises used: discreteTopology_subtype_iff, isDiscrete_iff_discreteTopology
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_3
inst : TopologicalSpace X
E : Set X
h : ∀ x ∈ E, ¬AccPt x (𝓟 E)
⊢ DiscreteTopology.{u_3} (↑E : Type u_3)

Tactic:
simpa [discreteTopology_subtype_iff, AccPt] using h

Premises used: discreteTopology_subtype_iff, AccPt
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
Y : Type u_2
inst : TopologicalSpace Y
S : Set Y
simp :
  (∀ (a : Y) (b : a ∈ S), ∃ (t : Set Y), IsOpen[inst] t ∧ ∀ (a_1 : Y) (b : a_1 ∈ S), a_1 ∈ t ↔ a_1 = a) ↔
    ∀ y ∈ S, ∃ (U : Set Y), IsOpen[inst] U ∧ ∀ (x : Y), x ∈ U ∧ x ∈ S ↔ x = y
⊢ DiscreteTopology.{u_2} (↑S : Type u_2) ↔ ∀ y ∈ S, ∃ (U : Set Y), IsOpen[inst] U ∧ U ∩ S = {y}

Tactic:
simp [discreteTopology_iff_isOpen_singleton, isOpen_induced_iff, Set.ext_iff]

Premises used: Set.ext_iff, discreteTopology_iff_isOpen_singleton, isOpen_induced_iff
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
Y : Type u_2
inst : TopologicalSpace Y
S : Set Y
⊢ (∀ (a : Y) (b : a ∈ S), ∃ (t : Set Y), IsOpen[inst] t ∧ ∀ (a_1 : Y) (b : a_1 ∈ S), a_1 ∈ t ↔ a_1 = a) ↔
    ∀ y ∈ S, ∃ (U : Set Y), IsOpen[inst] U ∧ ∀ (x : Y), x ∈ U ∧ x ∈ S ↔ x = y

Tactic:
grind
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
Y : Type u_2
inst : TopologicalSpace Y
S : Set Y
rw : DiscreteTopology.{u_2} (↑S : Type u_2) ↔ ∀ y ∈ S, ∃ (U : Set Y), IsOpen[inst] U ∧ U ∩ S = {y}
rw₁ rw₂ : (∀ y ∈ S, ∃ (U : Set Y), IsOpen[inst] U ∧ U ∩ S = {y}) ↔ ∀ y ∈ S, ∃ (U : Set Y), IsOpen[inst] U ∧ U ∩ S = {y}
⊢ IsDiscrete S ↔ ∀ y ∈ S, ∃ (U : Set Y), IsOpen[inst] U ∧ U ∩ S = {y}

Tactic:
rw [isDiscrete_iff_discreteTopology, discreteTopology_subtype_iff']

Premises used: discreteTopology_subtype_iff', isDiscrete_iff_discreteTopology
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : s.Subsingleton
⊢ IsDiscrete s

Tactic:
have : Subsingleton s := (Set.subsingleton_coe s).mpr hs
  ⟨inferInstance⟩

Premises used: Iff.mpr, inferInstance, IsDiscrete.mk, Set.subsingleton_coe
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsDiscrete s ↔ ∀ x ∈ s, 𝓝[s] x = pure x

Tactic:
simp [isDiscrete_iff_discreteTopology, discreteTopology_iff_isOpen_singleton,
    isOpen_singleton_iff_nhds_eq_pure, nhds_induced,
    ← (Filter.map_injective Subtype.val_injective).eq_iff,
    Filter.map_comap, nhdsWithin]

Premises used: Subtype.val_injective, nhdsWithin, Filter.map_comap, Function.Injective.eq_iff, Filter.map_injective, nhds_induced, isOpen_singleton_iff_nhds_eq_pure, isDiscrete_iff_discreteTopology, discreteTopology_iff_isOpen_singleton
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
H : ∀ x ∈ s, 𝓝[s] x ≤ pure x
⊢ IsDiscrete s

Tactic:
isDiscrete_iff_nhdsWithin.mpr fun x hx ↦ (H x hx).antisymm (pure_le_nhdsWithin hx)

Premises used: Iff.mpr, isDiscrete_iff_nhdsWithin, LE.le.antisymm, pure_le_nhdsWithin
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsDiscrete.{u_1} (X := X) univ ↔ DiscreteTopology X

Tactic:
simp [isDiscrete_iff_nhdsWithin, discreteTopology_iff_isOpen_singleton,
    isOpen_singleton_iff_nhds_eq_pure]

Premises used: isDiscrete_iff_nhdsWithin, isOpen_singleton_iff_nhds_eq_pure, discreteTopology_iff_isOpen_singleton
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 rwa rwa₁ rwa₂ rwa₃ : DiscreteTopology X
⊢ IsDiscrete.{u_1} (X := X) Set.univ

Tactic:
rwa [isDiscrete_univ_iff]

Premises used: isDiscrete_univ_iff
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
⊢ IsDiscrete (f '' s)

Tactic:
.of_nhdsWithin ?_

Premises used: IsDiscrete.of_nhdsWithin
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
refine : ∀ x ∈ f '' s, 𝓝[f '' s] x ≤ pure x
⊢ IsDiscrete (f '' s)

Tactic:
refine .of_nhdsWithin ?_
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
x : X
hx : x ∈ s
rw : 𝓝 (f x) ⊓ 𝓟 (f '' s) ≤ map f (𝓝 x) ⊓ 𝓟 (f '' s)
⊢ 𝓝[f '' s] f x ≤ pure (f x)

Tactic:
rw [← map_pure, ← hs.nhdsWithin x hx, nhdsWithin, nhdsWithin, map_inf hf', map_principal]

Premises used: Filter.map_inf, nhdsWithin, IsDiscrete.nhdsWithin, Filter.map_principal, Filter.map_pure
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
x : X
hx : x ∈ s
grw grw₁ : map f (𝓝 x) ⊓ 𝓟 (f '' s) ≤ map f (𝓝 x) ⊓ 𝓟 (f '' s)
⊢ 𝓝 (f x) ⊓ 𝓟 (f '' s) ≤ map f (𝓝 x) ⊓ 𝓟 (f '' s)

Tactic:
grw [hf.nhds_le x]

Premises used: IsOpenMap.nhds_le
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hs' : IsOpen[inst] s
⊢ IsDiscrete (f '' s)

Tactic:
.of_nhdsWithin ?_

Premises used: IsDiscrete.of_nhdsWithin
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hs' : IsOpen[inst] s
refine : ∀ x ∈ f '' s, 𝓝[f '' s] x ≤ pure x
⊢ IsDiscrete (f '' s)

Tactic:
refine .of_nhdsWithin ?_
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hs' : IsOpen[inst] s
x : X
hx : x ∈ s
rw : 𝓝 (f x) ≤ map f (𝓝 x)
⊢ 𝓝[f '' s] f x ≤ pure (f x)

Tactic:
rw [(hf _ hs').nhdsWithin_eq ⟨x, hx, rfl⟩, ← map_pure, ← hs.nhdsWithin x hx, hs'.nhdsWithin_eq hx]

Premises used: IsOpen.nhdsWithin_eq, IsDiscrete.nhdsWithin, And.intro, Exists.intro, Filter.map_pure, rfl
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hs' : IsOpen[inst] s
x : X
hx : x ∈ s
⊢ 𝓝 (f x) ≤ map f (𝓝 x)

Tactic:
hf.nhds_le x

Premises used: IsOpenMap.nhds_le
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hs' : IsOpen[inst] s
x : X
hx : x ∈ s
⊢ 𝓝 (f x) ≤ map f (𝓝 x)

Tactic:
exact hf.nhds_le x

Premises used: IsOpenMap.nhds_le
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : DiscreteTopology X
hf : IsOpenMap f
⊢ IsDiscrete (range f)

Tactic:
simpa using IsDiscrete.univ.image_of_isOpenMap_of_isOpen hf isOpen_univ

Premises used: IsDiscrete.univ, isOpen_univ, IsDiscrete.image_of_isOpenMap_of_isOpen
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsInducing f
⊢ IsDiscrete (f '' s)

Tactic:
simp_all [isDiscrete_iff_nhdsWithin, ← hf.map_nhdsWithin_eq s]

Premises used: Topology.IsInducing.map_nhdsWithin_eq, isDiscrete_iff_nhdsWithin
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : DiscreteTopology X
hf : IsInducing f
⊢ IsDiscrete (range f)

Tactic:
simpa using IsDiscrete.univ.image hf

Premises used: IsDiscrete.univ, IsDiscrete.image
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
hf' : Injective f
⊢ IsDiscrete (f ⁻¹' s)

Tactic:
.of_nhdsWithin fun x hx ↦ ?_

Premises used: IsDiscrete.of_nhdsWithin
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
hf' : Injective f
refine : ∀ (x : X) (hx : x ∈ f ⁻¹' s), 𝓝[f ⁻¹' s] x ≤ pure x
⊢ IsDiscrete (f ⁻¹' s)

Tactic:
refine .of_nhdsWithin fun x hx ↦ ?_
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
hf' : Injective f
x : X
hx : x ∈ f ⁻¹' s
rw : Tendsto f (𝓝[f ⁻¹' s] x) (𝓝[s] f x)
⊢ 𝓝[f ⁻¹' s] x ≤ pure x

Tactic:
rw [← map_le_map_iff hf', map_pure, ← hs.nhdsWithin _ hx, ← Tendsto]

Premises used: IsDiscrete.nhdsWithin, Filter.map_le_map_iff, Filter.Tendsto, Filter.map_pure
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
hf' : Injective f
x : X
hx : x ∈ f ⁻¹' s
⊢ Tendsto f (𝓝[f ⁻¹' s] x) (𝓝[s] f x)

Tactic:
(hf.continuousWithinAt hx).tendsto_nhdsWithin (Set.mapsTo_preimage _ _)

Premises used: ContinuousWithinAt.tendsto_nhdsWithin, Set.mapsTo_preimage, ContinuousOn.continuousWithinAt
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
hf' : Injective f
x : X
hx : x ∈ f ⁻¹' s
⊢ Tendsto f (𝓝[f ⁻¹' s] x) (𝓝[s] f x)

Tactic:
exact (hf.continuousWithinAt hx).tendsto_nhdsWithin (Set.mapsTo_preimage _ _)

Premises used: ContinuousWithinAt.tendsto_nhdsWithin, Set.mapsTo_preimage, ContinuousOn.continuousWithinAt
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
⊢ IsDiscrete (f ⁻¹' s)

Tactic:
.of_nhdsWithin fun x hx ↦ ?_

Premises used: IsDiscrete.of_nhdsWithin
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
refine : ∀ (x : X) (hx : x ∈ f ⁻¹' s), 𝓝[f ⁻¹' s] x ≤ pure x
⊢ IsDiscrete (f ⁻¹' s)

Tactic:
refine .of_nhdsWithin fun x hx ↦ ?_
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
⊢ 𝓝[f ⁻¹' {f x}] x ≤ pure x

Tactic:
have h := ((H (f x)).nhdsWithin _ rfl).le
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
h : 𝓝 x ⊓ comap f (𝓝[s] f x) ≤ pure x
x_1 : X
⊢ x_1 ∈ f ⁻¹' s → f x_1 ∈ s

Tactic:
id

Premises used: Set.Mem, setOf, id, Set.preimage
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
h : 𝓝 x ⊓ comap f (𝓝[s] f x) ≤ pure x
x_1 : X
⊢ x_1 ∈ f ⁻¹' s → f x_1 ∈ s

Tactic:
exact id

Premises used: id
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
h : 𝓝[f ⁻¹' {f x}] x ≤ pure x
⊢ 𝓝[f ⁻¹' s] x ≤ pure x

Tactic:
grw [nhdsWithin, ← comap_pure, ← hs.nhdsWithin _ hx, ← (hf.continuousWithinAt hx
    |>.tendsto_nhdsWithin fun _ ↦ by exact id).le_comap, inf_eq_right.mpr nhdsWithin_le_nhds] at h

Premises used: Iff.mpr, Filter.Tendsto.le_comap, nhdsWithin, ContinuousWithinAt.tendsto_nhdsWithin, Filter.comap_pure, IsDiscrete.nhdsWithin, nhdsWithin_le_nhds, inf_eq_right, ContinuousOn.continuousWithinAt
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
h : 𝓝[f ⁻¹' s] x ≤ pure x
⊢ 𝓝[f ⁻¹' s] x ≤ pure x

Tactic:
h
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
h : 𝓝[f ⁻¹' s] x ≤ pure x
⊢ 𝓝[f ⁻¹' s] x ≤ pure x

Tactic:
exact h
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
a b : X
hab : a ⤳ b
ha : a ∈ s
hb : b ∈ s
this : DiscreteTopology.{u_1} (↑s : Type u_1) := ⋯
⊢ a = b

Tactic:
simpa only [← Topology.IsInducing.subtypeVal.specializes_iff, hab, Subtype.mk.injEq,
    true_iff] using specializes_iff_eq (X := s) (x := ⟨a, ha⟩) (y := ⟨b, hb⟩)

Premises used: Topology.IsInducing.specializes_iff, true_iff, specializes_iff_eq, Subtype.mk.injEq, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
f : X → Y
rw : (∀ (i : Set Y), IsCompact i → ∀ᶠ (x : X) in cofinite, f x ∈ iᶜ) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite
⊢ Tendsto f cofinite (cocompact Y) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite

Tactic:
rw [hasBasis_cocompact.tendsto_right_iff]

Premises used: Filter.hasBasis_cocompact, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
f : X → Y
⊢ (∀ (i : Set Y), IsCompact i → ∀ᶠ (x : X) in cofinite, f x ∈ iᶜ) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite

Tactic:
forall₂_congr (fun K _ ↦ ?_)

Premises used: forall₂_congr
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
f : X → Y
refine : ∀ (K : Set Y), IsCompact K → ((∀ᶠ (x : X) in cofinite, f x ∈ Kᶜ) ↔ (f ⁻¹' K).Finite)
⊢ (∀ (i : Set Y), IsCompact i → ∀ᶠ (x : X) in cofinite, f x ∈ iᶜ) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite

Tactic:
refine forall₂_congr (fun K _ ↦ ?_)

Premises used: forall₂_congr
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
f : X → Y
K : Set Y
h : IsCompact K
⊢ (∀ᶠ (x : X) in cofinite, f x ∈ Kᶜ) ↔ (f ⁻¹' K).Finite

Tactic:
simp only [mem_compl_iff, eventually_cofinite, not_not, preimage]

Premises used: Classical.not_not, Filter.eventually_cofinite, Set.preimage, Set.mem_compl_iff
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space X
inst_3 : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst, inst_1] f
hf : Tendsto f cofinite (cocompact Y)
⊢ DiscreteTopology X

Tactic:
discreteTopology_iff_isOpen_singleton.mpr (fun x ↦ ?_)

Premises used: Iff.mpr, discreteTopology_iff_isOpen_singleton
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space X
inst_3 : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst, inst_1] f
hf : Tendsto f cofinite (cocompact Y)
refine : ∀ (x : X), IsOpen[inst] {x}
⊢ DiscreteTopology X

Tactic:
refine discreteTopology_iff_isOpen_singleton.mpr (fun x ↦ ?_)

Premises used: Iff.mpr, discreteTopology_iff_isOpen_singleton
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space X
inst_3 : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst, inst_1] f
hf : Tendsto f cofinite (cocompact Y)
x : X
obtain : ∀ (K : Set Y) (hK : IsCompact K) (hK' : K ∈ 𝓝 (f x)), IsOpen[inst] {x}
⊢ IsOpen[inst] {x}

Tactic:
obtain ⟨K : Set Y, hK : IsCompact K, hK' : K ∈ 𝓝 (f x)⟩ := exists_compact_mem_nhds (f x)

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds, nhds, Set
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space X
inst_3 : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst, inst_1] f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
obtain : ∀ (U : Set Y) (hU₁ : U ⊆ K) (hU₂ : IsOpen[inst_1] U) (hU₃ : f x ∈ U), IsOpen[inst] {x}
⊢ IsOpen[inst] {x}

Tactic:
obtain ⟨U : Set Y, hU₁ : U ⊆ K, hU₂ : IsOpen U, hU₃ : f x ∈ U⟩ := mem_nhds_iff.mp hK'

Premises used: mem_nhds_iff, Iff.mp, Set
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space X
inst_3 : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst, inst_1] f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
U : Set Y
hU₁ : U ⊆ K
hU₂ : IsOpen[inst_1] U
hU₃ : f x ∈ U
⊢ (f ⁻¹' U).Finite

Tactic:
have hU₄ : Set.Finite (f ⁻¹' U) :=
    Finite.subset (tendsto_cofinite_cocompact_iff.mp hf K hK) (preimage_mono hU₁)
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space X
inst_3 : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst, inst_1] f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
U : Set Y
hU₁ : U ⊆ K
hU₂ : IsOpen[inst_1] U
hU₃ : f x ∈ U
hU₄ : (f ⁻¹' U).Finite
⊢ IsOpen[inst] {x}

Tactic:
isOpen_singleton_of_finite_mem_nhds _ ((hU₂.preimage hf').mem_nhds hU₃) hU₄

Premises used: isOpen_singleton_of_finite_mem_nhds, IsOpen.mem_nhds, IsOpen.preimage
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space X
inst_3 : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst, inst_1] f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
U : Set Y
hU₁ : U ⊆ K
hU₂ : IsOpen[inst_1] U
hU₃ : f x ∈ U
hU₄ : (f ⁻¹' U).Finite
⊢ IsOpen[inst] {x}

Tactic:
exact isOpen_singleton_of_finite_mem_nhds _ ((hU₂.preimage hf').mem_nhds hU₃) hU₄

Premises used: isOpen_singleton_of_finite_mem_nhds, IsOpen.mem_nhds, IsOpen.preimage
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ Tendsto f (cocompact X) (cocompact Y)

Tactic:
hf
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
h : cofinite = cocompact X
⊢ Tendsto f cofinite (cocompact Y)

Tactic:
convert! hf
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
h h₁ : Eq.{u_1 + 1} (α := Filter X) cofinite cofinite
⊢ cofinite = cocompact X

Tactic:
rw [cocompact_eq_cofinite X]

Premises used: Filter.cocompact_eq_cofinite
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsClosed[inst] s
hs' : IsDiscrete s
⊢ Tendsto (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) cofinite (cocompact X)

Tactic:
haveI := hs'.to_subtype
  tendsto_cofinite_cocompact_of_discrete hs.isClosedEmbedding_subtypeVal.tendsto_cocompact

Premises used: Topology.IsClosedEmbedding.tendsto_cocompact, tendsto_cofinite_cocompact_of_discrete, IsClosed.isClosedEmbedding_subtypeVal
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : WeaklyLocallyCompactSpace X
s : Set X
hs : IsClosed[inst] s
⊢ Tendsto (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) cofinite (cocompact X) ↔ IsDiscrete s

Tactic:
⟨fun h ↦ ⟨continuous_subtype_val.discrete_of_tendsto_cofinite_cocompact h⟩,
   fun hs' ↦ hs.tendsto_coe_cofinite_of_isDiscrete hs'⟩

Premises used: IsClosed.tendsto_coe_cofinite_of_isDiscrete, continuous_subtype_val, Continuous.discrete_of_tendsto_cofinite_cocompact, IsDiscrete.mk, Iff.intro
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
rw : (∀ (x : X), (ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥)) ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)
⊢ IsClosed[inst] S ∧ IsDiscrete S ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
rw [isDiscrete_iff_nhdsNE, isClosed_iff_clusterPt, ← forall_and]

Premises used: isDiscrete_iff_nhdsNE, isClosed_iff_clusterPt, forall_and
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
a : ∀ (x : X), (ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ Disjoint (𝓝[≠] x) (𝓟 S)
⊢ (∀ (x : X), (ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥)) ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
congrm (∀ x, ?_)
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
x : X
a : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S)) ↔ Disjoint (𝓝[≠] x) (𝓟 S)
⊢ (ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
rw [← not_imp_not, clusterPt_iff_not_disjoint, not_not, ← disjoint_iff]

Premises used: Classical.not_not, disjoint_iff, clusterPt_iff_not_disjoint, not_imp_not