awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f' : Y → X
h : Continuous[inst_1, inst] f'
l_inv : LeftInverse f f'
r_inv : RightInverse f f'
s : Set X
hs : IsClosed[inst] s
rw : IsClosed[inst_1] (f' ⁻¹' s)
⊢ IsClosed[inst_1] (f '' s)

Tactic:
rw [image_eq_preimage_of_inverse r_inv l_inv]

Premises used: Set.image_eq_preimage_of_inverse
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f' : Y → X
h : Continuous[inst_1, inst] f'
l_inv : LeftInverse f f'
r_inv : RightInverse f f'
s : Set X
hs : IsClosed[inst] s
⊢ IsClosed[inst_1] (f' ⁻¹' s)

Tactic:
hs.preimage h

Premises used: IsClosed.preimage
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f' : Y → X
h : Continuous[inst_1, inst] f'
l_inv : LeftInverse f f'
r_inv : RightInverse f f'
s : Set X
hs : IsClosed[inst] s
⊢ IsClosed[inst_1] (f' ⁻¹' s)

Tactic:
exact hs.preimage h

Premises used: IsClosed.preimage
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed[inst] s → s.Nonempty → IsClosed[inst_1] (f '' s)
s : Set X
hs : IsClosed[inst] s
inl : ∀ (h2s : s = ∅), IsClosed[inst_1] (f '' s)
inr : ∀ (h2s : s.Nonempty), IsClosed[inst_1] (f '' s)
⊢ IsClosed[inst_1] (f '' s)

Tactic:
rcases eq_empty_or_nonempty s with h2s | h2s

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed[inst] s → s.Nonempty → IsClosed[inst_1] (f '' s)
s : Set X
hs : IsClosed[inst] s
h2s : s = ∅
inl : IsClosed[inst_1] (f '' ∅)
inl₁ : IsClosed[inst_1] ∅
⊢ IsClosed[inst_1] (f '' s)

Tactic:
simp_rw [h2s, image_empty, isClosed_empty]

Premises used: isClosed_empty, Set.image_empty
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed[inst] s → s.Nonempty → IsClosed[inst_1] (f '' s)
s : Set X
hs : IsClosed[inst] s
h2s : s.Nonempty
⊢ IsClosed[inst_1] (f '' s)

Tactic:
h s hs h2s
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed[inst] s → s.Nonempty → IsClosed[inst_1] (f '' s)
s : Set X
hs : IsClosed[inst] s
h2s : s.Nonempty
⊢ IsClosed[inst_1] (f '' s)

Tactic:
exact h s hs h2s
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsClosedMap f
⊢ IsClosed[inst_1] (range f)

Tactic:
@image_univ _ _ f ▸ hf _ isClosed_univ

Premises used: isClosed_univ, Set.image_univ, Eq.rec
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hcl : IsClosedMap f
hcont : Continuous[inst, inst_1] f
hsurj : Surjective f
⊢ IsQuotientMap f

Tactic:
isQuotientMap_iff_isClosed.2 ⟨hsurj, fun s =>
    ⟨fun hs => hs.preimage hcont, fun hs => hsurj.image_preimage s ▸ hcl _ hs⟩⟩

Premises used: Iff.mpr, Topology.isQuotientMap_iff_isClosed, Eq.rec, Set.preimage, And.intro, Iff.intro, IsClosed.preimage, Function.Surjective.image_preimage
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
rw :
  (∀ (x : Set X), IsClosed[inst] xᶜ → IsClosed[inst_1] (f '' xᶜ)) ↔
    ∀ {u : Set X}, IsOpen[inst] u → IsOpen[inst_1] (kernImage f u)
⊢ IsClosedMap f ↔ ∀ {u : Set X}, IsOpen[inst] u → IsOpen[inst_1] (kernImage f u)

Tactic:
rw [IsClosedMap, compl_surjective.forall]

Premises used: Function.Surjective.forall, IsClosedMap, compl_surjective
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ (∀ (x : Set X), IsClosed[inst] xᶜ → IsClosed[inst_1] (f '' xᶜ)) ↔
    ∀ {u : Set X}, IsOpen[inst] u → IsOpen[inst_1] (kernImage f u)

Tactic:
simp [kernImage_eq_compl]

Premises used: Set.kernImage_eq_compl
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsInducing f
h : IsClosed[inst_1] (range f)
s : Set X
hs : IsClosed[inst] s
rcases : ∀ (t : Set Y) (ht : IsClosed[inst_1] t) (hs : IsClosed[inst] (f ⁻¹' t)), IsClosed[inst_1] (f '' f ⁻¹' t)
⊢ IsClosed[inst_1] (f '' s)

Tactic:
rcases hf.isClosed_iff.1 hs with ⟨t, ht, rfl⟩

Premises used: Iff.mp, rfl, Topology.IsInducing.isClosed_iff
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsInducing f
h : IsClosed[inst_1] (range f)
t : Set Y
ht : IsClosed[inst_1] t
hs : IsClosed[inst] (f ⁻¹' t)
rw : IsClosed[inst_1] (t ∩ range f)
⊢ IsClosed[inst_1] (f '' f ⁻¹' t)

Tactic:
rw [image_preimage_eq_inter_range]

Premises used: Set.image_preimage_eq_inter_range
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsInducing f
h : IsClosed[inst_1] (range f)
t : Set Y
ht : IsClosed[inst_1] t
hs : IsClosed[inst] (f ⁻¹' t)
⊢ IsClosed[inst_1] (t ∩ range f)

Tactic:
ht.inter h

Premises used: IsClosed.inter
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsInducing f
h : IsClosed[inst_1] (range f)
t : Set Y
ht : IsClosed[inst_1] t
hs : IsClosed[inst] (f ⁻¹' t)
⊢ IsClosed[inst_1] (t ∩ range f)

Tactic:
exact ht.inter h

Premises used: IsClosed.inter
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hs : ∀ (s : Set X), closure[inst_1] (f '' s) ⊆ f '' closure[inst] s
c : Set X
hc : IsClosed[inst] c
rw rw₁ : f '' c = f '' c
⊢ f '' closure[inst] c = f '' c

Tactic:
rw [hc.closure_eq]

Premises used: IsClosed.closure_eq
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
rw :
  (∀ (x : Set X), closure[inst_1] (f '' xᶜ) ⊆ f '' closure[inst] xᶜ) ↔
    ∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)
⊢ IsClosedMap f ↔ ∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)

Tactic:
rw [isClosedMap_iff_closure_image, compl_surjective.forall]

Premises used: Function.Surjective.forall, isClosedMap_iff_closure_image, compl_surjective
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ (∀ (x : Set X), closure[inst_1] (f '' xᶜ) ⊆ f '' closure[inst] xᶜ) ↔
    ∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)

Tactic:
simp [kernImage_eq_compl]

Premises used: Set.kernImage_eq_compl
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsClosedMap f ↔ ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ (x : X), f x = y ∧ ClusterPt x (𝓟 s)

Tactic:
simp [MapClusterPt, isClosedMap_iff_closure_image, subset_def, mem_closure_iff_clusterPt,
    and_comm]

Premises used: Set.subset_def, isClosedMap_iff_closure_image, mem_closure_iff_clusterPt, and_comm, MapClusterPt
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
simp_rw :
  (∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)) ↔
    ∀ {s : Set Y} (x : Set X), s ⊆ kernImage f (interior x) → s ⊆ interior (kernImage f x)
⊢ IsClosedMap f ↔ ∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)

Tactic:
simp_rw [Filter.le_def, mem_comap'', ← subset_interior_iff_mem_nhdsSet,
    ← subset_kernImage_iff, isClosedMap_iff_kernImage_interior]

Premises used: isClosedMap_iff_kernImage_interior, Filter.mem_comap'', Set.subset_kernImage_iff, subset_interior_iff_mem_nhdsSet, Filter.le_def
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ (∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)) ↔
    ∀ {s : Set Y} (x : Set X), s ⊆ kernImage f (interior x) → s ⊆ interior (kernImage f x)

Tactic:
⟨fun H s t hst ↦ hst.trans H, fun H s ↦ H _ subset_rfl⟩

Premises used: HasSubset.Subset.trans, Iff.intro, subset_rfl
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ (∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)) ↔
    ∀ {s : Set Y} (x : Set X), s ⊆ kernImage f (interior x) → s ⊆ interior (kernImage f x)

Tactic:
exact ⟨fun H s t hst ↦ hst.trans H, fun H s ↦ H _ subset_rfl⟩
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
rw : (∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)) ↔ ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
⊢ IsClosedMap f ↔ ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})

Tactic:
rw [isClosedMap_iff_comap_nhdsSet_le]

Premises used: isClosedMap_iff_comap_nhdsSet_le
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
mp : (∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)) → ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
mpr : (∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})) → ∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)
⊢ (∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)) ↔ ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})

Tactic:
constructor
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ (∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)) → ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})

Tactic:
fun H y ↦ nhdsSet_singleton (x := y) ▸ H

Premises used: Eq.rec, nhdsSet_singleton
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ (∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)) → ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})

Tactic:
exact fun H y ↦ nhdsSet_singleton (x := y) ▸ H
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
mpr : comap f (𝓝ˢ (⋃ x ∈ s, {x})) ≤ 𝓝ˢ (f ⁻¹' ⋃ x ∈ s, {x})
⊢ comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)

Tactic:
rw [← Set.biUnion_of_singleton s]

Premises used: Set.biUnion_of_singleton
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
mpr : LE.le.{u_1} (α := Filter X) (⨆ i ∈ s, comap f (𝓝 i)) (⨆ i ∈ s, 𝓝ˢ (f ⁻¹' {i}))
⊢ comap f (𝓝ˢ (⋃ x ∈ s, {x})) ≤ 𝓝ˢ (f ⁻¹' ⋃ x ∈ s, {x})

Tactic:
simp_rw [preimage_iUnion, nhdsSet_iUnion, comap_iSup, nhdsSet_singleton]

Premises used: nhdsSet_iUnion, Filter.comap_iSup, Set.preimage_iUnion, nhdsSet_singleton
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
⊢ LE.le.{u_1} (α := Filter X) (⨆ i ∈ s, comap f (𝓝 i)) (⨆ i ∈ s, 𝓝ˢ (f ⁻¹' {i}))

Tactic:
iSup₂_mono fun _ _ ↦ H

Premises used: iSup₂_mono, Set.Mem, setOf
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
⊢ LE.le.{u_1} (α := Filter X) (⨆ i ∈ s, comap f (𝓝 i)) (⨆ i ∈ s, 𝓝ˢ (f ⁻¹' {i}))

Tactic:
exact iSup₂_mono fun _ _ ↦ H

Premises used: iSup₂_mono
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsClosedMap f
hf' : Continuous[inst, inst_1] f
y : Y
⊢ comap f (𝓝 y) = 𝓝ˢ (f ⁻¹' {y})

Tactic:
le_antisymm (isClosedMap_iff_comap_nhds_le.mp hf)
  -- Note: below should be an application of `Continuous.tendsto_nhdsSet_nhds`, but this is only
  -- proven later...
    (nhdsSet_le.mpr fun x hx ↦ hx ▸ (hf'.tendsto x).le_comap)

Premises used: Iff.mpr, Filter.Tendsto.le_comap, isClosedMap_iff_comap_nhds_le, nhdsSet_le, Eq.rec, Continuous.tendsto, le_antisymm, Iff.mp
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsClosedMap f
hf' : Continuous[inst, inst_1] f
s : Set Y
⊢ comap f (𝓝ˢ s) = 𝓝ˢ (f ⁻¹' s)

Tactic:
le_antisymm (isClosedMap_iff_comap_nhdsSet_le.mp hf)
  -- Note: below should be an application of `Continuous.tendsto_nhdsSet_nhdsSet`, but this is only
  -- proven later...
    (nhdsSet_le.mpr fun x hx ↦ (hf'.tendsto x).le_comap.trans (comap_mono (nhds_le_nhdsSet hx)))

Premises used: Iff.mpr, Filter.Tendsto.le_comap, nhds_le_nhdsSet, nhdsSet_le, Filter.comap_mono, isClosedMap_iff_comap_nhdsSet_le, Continuous.tendsto, le_antisymm, Iff.mp, LE.le.trans
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsClosedMap f
p : X → Prop
y₀ : Y
H : ∀ x₀ ∈ f ⁻¹' {y₀}, ∀ᶠ (x : X) in 𝓝 x₀, p x
⊢ ∀ᶠ (x : X) in 𝓝ˢ (f ⁻¹' {y₀}), p x

Tactic:
rw [← eventually_nhdsSet_iff_forall] at H

Premises used: eventually_nhdsSet_iff_forall
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsClosedMap f
p : X → Prop
y₀ : Y
H : ∀ᶠ (x : X) in 𝓝ˢ (f ⁻¹' {y₀}), p x
⊢ ∀ᶠ (x : X) in comap f (𝓝 y₀), p x

Tactic:
replace H := H.filter_mono hf.comap_nhds_le
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsClosedMap f
p : X → Prop
y₀ : Y
H : ∀ᶠ (x : X) in comap f (𝓝 y₀), p x
rwa rwa₁ rwa₂ rwa₃ : ∀ (H : ∀ᶠ (b : Y) in 𝓝 y₀, ∀ (a : X), f a = b → p a), ∀ᶠ (y : Y) in 𝓝 y₀, ∀ x ∈ f ⁻¹' {y}, p x
⊢ ∀ᶠ (y : Y) in 𝓝 y₀, ∀ x ∈ f ⁻¹' {y}, p x

Tactic:
rwa [eventually_comap] at H

Premises used: Filter.eventually_comap
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsClosedMap f
p : X → Prop
y₀ : Y
H : ∃ᶠ (y : Y) in 𝓝 y₀, ∃ x ∈ f ⁻¹' {y}, p x
contrapose! :
  ∀ (H : ∀ (x₀ : X) (_ : x₀ ∈ f ⁻¹' {y₀}), ∀ᶠ (x : X) in 𝓝 x₀, ¬p x),
    ∀ᶠ (x : Y) in 𝓝 y₀, ∀ (x_1 : X) (_ : x_1 ∈ f ⁻¹' {x}), ¬p x_1
⊢ ∃ x₀ ∈ f ⁻¹' {y₀}, ∃ᶠ (x : X) in 𝓝 x₀, p x

Tactic:
contrapose! H
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsClosedMap f
p : X → Prop
y₀ : Y
H : ∀ (x₀ : X) (_ : x₀ ∈ f ⁻¹' {y₀}), ∀ᶠ (x : X) in 𝓝 x₀, ¬p x
⊢ ∀ᶠ (x : Y) in 𝓝 y₀, ∀ (x_1 : X) (_ : x_1 ∈ f ⁻¹' {x}), ¬p x_1

Tactic:
hf.eventually_nhds_fiber y₀ H

Premises used: IsClosedMap.eventually_nhds_fiber
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsClosedMap f
p : X → Prop
y₀ : Y
H : ∀ (x₀ : X) (_ : x₀ ∈ f ⁻¹' {y₀}), ∀ᶠ (x : X) in 𝓝 x₀, ¬p x
⊢ ∀ᶠ (x : Y) in 𝓝 y₀, ∀ (x_1 : X) (_ : x_1 ∈ f ⁻¹' {x}), ¬p x_1

Tactic:
exact hf.eventually_nhds_fiber y₀ H

Premises used: IsClosedMap.eventually_nhds_fiber
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
s : Set X
⊢ closure[inst_1] (f '' s) = f '' closure[inst] s

Tactic:
subset_antisymm (f_closed.closure_image_subset s) (image_closure_subset_closure_image f_cont)

Premises used: IsClosedMap.closure_image_subset, subset_antisymm, image_closure_subset_closure_image
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
F : Filter X
rw : F.lift' (closure[inst_1] ∘ image f) = F.lift' (image f ∘ closure[inst])
⊢ (map f F).lift' closure[inst_1] = map f (F.lift' closure[inst])

Tactic:
rw [map_lift'_eq2 (monotone_closure Y), map_lift'_eq (monotone_closure X)]

Premises used: Filter.map_lift'_eq2, Filter.map_lift'_eq, monotone_closure
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
F : Filter X
e_h : closure[inst_1] ∘ image f = image f ∘ closure[inst]
⊢ F.lift' (closure[inst_1] ∘ image f) = F.lift' (image f ∘ closure[inst])

Tactic:
congr 1
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
F : Filter X
e_h : ∀ (s : Set X), (closure[inst_1] ∘ image f) s = (image f ∘ closure[inst]) s
⊢ closure[inst_1] ∘ image f = image f ∘ closure[inst]

Tactic:
ext s : 1
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
F : Filter X
s : Set X
⊢ (closure[inst_1] ∘ image f) s = (image f ∘ closure[inst]) s

Tactic:
f_closed.closure_image_eq_of_continuous f_cont s

Premises used: setOf, closure, Set.image, IsClosedMap.closure_image_eq_of_continuous, Set.sInter
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
F : Filter X
s : Set X
⊢ (closure[inst_1] ∘ image f) s = (image f ∘ closure[inst]) s

Tactic:
exact f_closed.closure_image_eq_of_continuous f_cont s

Premises used: IsClosedMap.closure_image_eq_of_continuous
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
y : Y
rw : ClusterPt y (map f F) ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
rw₁ : ((map f F).lift' closure[inst_1] ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
rw₂ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
rw₃ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ comap f (𝓟 {y})).NeBot
rw₄ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (map f (F.lift' closure[inst] ⊓ comap f (𝓟 {y}))).NeBot
rw₅ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (map f (F.lift' closure[inst]) ⊓ 𝓟 {y}).NeBot
rw₆ rw₇ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (map f (F.lift' closure[inst]) ⊓ pure y).NeBot
⊢ MapClusterPt y F f ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot

Tactic:
rw [MapClusterPt, clusterPt_iff_lift'_closure', f_closed.lift'_closure_map_eq f_cont,
      ← comap_principal, ← map_neBot_iff f, Filter.push_pull, principal_singleton]

Premises used: clusterPt_iff_lift'_closure', IsClosedMap.lift'_closure_map_eq, Filter.push_pull, Filter.principal_singleton, MapClusterPt, Filter.comap_principal, Filter.map_neBot_iff
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
⊢ IsEmbedding f

Tactic:
hf.toIsEmbedding

Premises used: Topology.IsOpenEmbedding.toIsEmbedding
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
⊢ IsInducing f

Tactic:
hf.isEmbedding.isInducing

Premises used: Topology.IsOpenEmbedding.isEmbedding, Topology.IsEmbedding.isInducing
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
⊢ IsOpenMap f

Tactic:
hf.isEmbedding.isInducing.isOpenMap hf.isOpen_range

Premises used: Topology.IsInducing.isOpenMap, Topology.IsOpenEmbedding.isEmbedding, Topology.IsEmbedding.isInducing, Topology.IsOpenEmbedding.isOpen_range
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
⊢ map f (𝓝 x) = 𝓝 (f x)

Tactic:
hf.isEmbedding.map_nhds_of_mem _ <| hf.isOpen_range.mem_nhds <| mem_range_self _

Premises used: Set.mem_range_self, Topology.IsEmbedding.map_nhds_of_mem, Topology.IsOpenEmbedding.isEmbedding, Topology.IsOpenEmbedding.isOpen_range, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
s : Set X
h : IsOpen[inst_1] (f '' s)
⊢ IsOpen[inst] (f ⁻¹' f '' s)

Tactic:
h.preimage hf.isEmbedding.continuous

Premises used: Topology.IsOpenEmbedding.isEmbedding, IsOpen.preimage, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
s : Set X
h : IsOpen[inst_1] (f '' s)
h₁ : f ⁻¹' f '' s = s
⊢ IsOpen[inst] s

Tactic:
convert! ← h.preimage hf.isEmbedding.continuous

Premises used: Topology.IsOpenEmbedding.isEmbedding, IsOpen.preimage, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
s : Set X
h : IsOpen[inst_1] (f '' s)
⊢ f ⁻¹' f '' s = s

Tactic:
apply preimage_image_eq _ hf.injective

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsEmbedding.injective, Set.preimage_image_eq
-- Module: Mathlib.Topology.Maps.Basic
Goal:
Y : Type u_2
Z : Type u_3
ι : Type u_4
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
f : ι → Y
l : Filter ι
y : Y
hg : IsOpenEmbedding g
⊢ Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y))

Tactic:
hg.isEmbedding.tendsto_nhds_iff

Premises used: Topology.IsOpenEmbedding.isEmbedding, Topology.IsEmbedding.tendsto_nhds_iff
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
l : Filter Z
x : X
rw : map g (𝓝 (f x)) ≤ l ↔ Tendsto g (𝓝 (f x)) l
⊢ Tendsto (g ∘ f) (𝓝 x) l ↔ Tendsto g (𝓝 (f x)) l

Tactic:
rw [Tendsto, ← map_map, hf.map_nhds_eq]

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, Filter.map_map, Filter.Tendsto
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
l : Filter Z
x : X
⊢ map g (𝓝 (f x)) ≤ l ↔ Tendsto g (𝓝 (f x)) l

Tactic:
rfl
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
hf : IsOpenEmbedding f
x : X
⊢ ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

Tactic:
hf.tendsto_nhds_iff'

Premises used: ContinuousAt, Topology.IsOpenEmbedding.tendsto_nhds_iff'
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
⊢ Continuous[inst, inst_1] f

Tactic:
hf.isEmbedding.continuous

Premises used: Topology.IsOpenEmbedding.isEmbedding, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
s : Set Y
hs : s ⊆ range f
rw : IsOpen[inst_1] s ↔ IsOpen[inst_1] (f '' f ⁻¹' s)
rw₁ : IsOpen[inst_1] s ↔ IsOpen[inst_1] (s ∩ range f)
rw₂ rw₃ : IsOpen[inst_1] s ↔ IsOpen[inst_1] s
⊢ IsOpen[inst_1] s ↔ IsOpen[inst] (f ⁻¹' s)

Tactic:
rw [hf.isOpen_iff_image_isOpen, image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs]

Premises used: Topology.IsOpenEmbedding.isOpen_iff_image_isOpen, Set.image_preimage_eq_inter_range, Set.inter_eq_self_of_subset_left