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
hf : IsOpenMap f
rw : IsOpen[inst_1] (f '' univ)
⊢ IsOpen[inst_1] (range f)

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- 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 : IsOpenMap f
⊢ IsOpen[inst_1] (f '' univ)

Tactic:
hf _ isOpen_univ

Premises used: isOpen_univ
-- 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 : IsOpenMap f
⊢ IsOpen[inst_1] (f '' univ)

Tactic:
exact hf _ isOpen_univ

Premises used: isOpen_univ
-- 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 : IsOpenMap f
x : X
s : Set X
hx : s ∈ 𝓝 x
⊢ f '' s ∈ 𝓝 (f x)

Tactic:
let ⟨t, hts, ht, hxt⟩ := mem_nhds_iff.1 hx
  mem_of_superset (IsOpen.mem_nhds (hf t ht) (mem_image_of_mem _ hxt)) (image_mono hts)

Premises used: mem_nhds_iff, Set.image_mono, _private.0.IsOpenMap.image_mem_nhds.match_1, Membership.mem, nhds, Set.mem_image_of_mem, IsOpen.mem_nhds, Iff.mp, Set.image, Filter.mem_of_superset
-- 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 : IsOpenMap f
x : X
⊢ range f ∈ 𝓝 (f x)

Tactic:
hf.isOpen_range.mem_nhds <| mem_range_self _

Premises used: Set.mem_range_self, IsOpen.mem_nhds, IsOpenMap.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 : IsOpenMap f
s : Set X
t : Set Y
h : MapsTo f s t
⊢ MapsTo f (interior s) (interior t)

Tactic:
mapsTo_iff_image_subset.2 <|
    interior_maximal (h.mono interior_subset Subset.rfl).image_subset (hf _ isOpen_interior)

Premises used: Iff.mpr, interior_subset, isOpen_interior, interior_maximal, Set.mapsTo_iff_image_subset, Set.MapsTo.mono, Set.Subset.rfl, Set.MapsTo.image_subset
-- 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 : IsOpenMap f
s : Set X
⊢ f '' interior s ⊆ interior (f '' s)

Tactic:
(hf.mapsTo_interior (mapsTo_image f s)).image_subset

Premises used: Set.mapsTo_image, IsOpenMap.mapsTo_interior, Set.MapsTo.image_subset
-- 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 : IsOpenMap f
x : X
⊢ 𝓝 (f x) ≤ map f (𝓝 x)

Tactic:
le_map fun _ => hf.image_mem_nhds

Premises used: IsOpenMap.image_mem_nhds, Filter.le_map
-- 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 : IsOpenMap f
x : X
hf' : ContinuousAt f x
⊢ map f (𝓝 x) = 𝓝 (f x)

Tactic:
le_antisymm hf' (hf.nhds_le x)

Premises used: IsOpenMap.nhds_le, le_antisymm
-- 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 : IsOpenMap f
hf' : Continuous[inst, inst_1] f
s : Set X
rw : map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (f '' ⋃ x ∈ s, {x})
⊢ map f (𝓝ˢ s) = 𝓝ˢ (f '' s)

Tactic:
rw [← 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
hf : IsOpenMap f
hf' : Continuous[inst, inst_1] f
s : Set X
simp_rw : map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (⋃ i ∈ s, f '' {i})
simp_rw₁ : map f (⨆ i ∈ s, 𝓝ˢ {i}) = ⨆ i ∈ s, 𝓝ˢ (f '' {i})
simp_rw₂ : Eq.{u_2 + 1} (α := Filter Y) (⨆ i ∈ s, map f (𝓝ˢ {i})) (⨆ i ∈ s, 𝓝ˢ (f '' {i}))
simp_rw₃ : Eq.{u_2 + 1} (α := Filter Y) (⨆ i ∈ s, map f (𝓝ˢ {i})) (⨆ i ∈ s, 𝓝ˢ {f i})
simp_rw₄ : Eq.{u_2 + 1} (α := Filter Y) (⨆ i ∈ s, map f (𝓝 i)) (⨆ i ∈ s, 𝓝 (f i))
⊢ map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (f '' ⋃ x ∈ s, {x})

Tactic:
simp_rw [image_iUnion, nhdsSet_iUnion, map_iSup, image_singleton, nhdsSet_singleton,
    hf.map_nhds_eq hf'.continuousAt]

Premises used: Set.image_singleton, nhdsSet_iUnion, Filter.map_iSup, Set.image_iUnion, IsOpenMap.map_nhds_eq, Continuous.continuousAt, 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
hf : ∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)
⊢ IsOpenMap f

Tactic:
fun _s hs =>
  isOpen_iff_mem_nhds.2 fun _y ⟨_x, hxs, hxy⟩ => hxy ▸ hf _ (image_mem_map <| hs.mem_nhds hxs)

Premises used: Iff.mpr, _private.0.IsOpenMap.of_nhds_le.match_1, Membership.mem, nhds, IsOpenMap, Eq.rec, Filter.image_mem_map, IsOpen.mem_nhds, Set.image, isOpen_iff_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
h : ∀ (x : X), ∃ (g : Y → X), ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f
x : X
g : Y → X
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : RightInverse g f
rw : 𝓝 (f x) = map (f ∘ g) (𝓝 (f x))
rw₁ : 𝓝 (f x) = map id (𝓝 (f x))
rw₂ rw₃ : 𝓝 (f x) = 𝓝 (f x)
⊢ 𝓝 (f x) = map f (map g (𝓝 (f x)))

Tactic:
rw [map_map, hgf.comp_eq_id, map_id]

Premises used: Filter.map_map, Function.RightInverse.comp_eq_id, Filter.map_id
-- 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 : ∀ (x : X), ∃ (g : Y → X), ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f
x : X
g : Y → X
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : RightInverse g f
rw rw₁ : map f (𝓝 x) = map f (𝓝 x)
⊢ map f (𝓝 (g (f x))) = map f (𝓝 x)

Tactic:
rw [hgx]
-- 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'
⊢ IsOpenMap f

Tactic:
of_sections fun _ => ⟨f', h.continuousAt, r_inv _, l_inv⟩

Premises used: IsOpenMap.of_sections, Continuous.continuousAt, And.intro, Exists.intro
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
open_map : IsOpenMap f
cont : Continuous[inst, inst_1] f
surj : Surjective f
rw : IsCoinducing f ∧ Surjective f
⊢ IsQuotientMap f

Tactic:
rw [isQuotientMap_iff]

Premises used: Topology.isQuotientMap_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
open_map : IsOpenMap f
cont : Continuous[inst, inst_1] f
surj : Surjective f
⊢ IsCoinducing f ∧ Surjective f

Tactic:
⟨.of_isOpen_preimage_iff_isOpen fun s ↦ ?_, surj⟩

Premises used: Topology.IsCoinducing.of_isOpen_preimage_iff_isOpen, And.intro
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
open_map : IsOpenMap f
cont : Continuous[inst, inst_1] f
surj : Surjective f
refine : ∀ (s : Set Y), IsOpen[inst] (f ⁻¹' s) ↔ IsOpen[inst_1] s
⊢ IsCoinducing f ∧ Surjective f

Tactic:
refine ⟨.of_isOpen_preimage_iff_isOpen fun s ↦ ?_, surj⟩
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
open_map : IsOpenMap f
cont : Continuous[inst, inst_1] f
surj : Surjective f
s : Set Y
⊢ IsOpen[inst] (f ⁻¹' s) ↔ IsOpen[inst_1] s

Tactic:
⟨fun h => surj.image_preimage s ▸ open_map _ h, fun h => h.preimage cont⟩

Premises used: Eq.rec, Set.preimage, Iff.intro, Function.Surjective.image_preimage, IsOpen.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
open_map : IsOpenMap f
cont : Continuous[inst, inst_1] f
surj : Surjective f
s : Set Y
⊢ IsOpen[inst] (f ⁻¹' s) ↔ IsOpen[inst_1] s

Tactic:
exact ⟨fun h => surj.image_preimage s ▸ open_map _ h, fun h => h.preimage cont⟩
-- 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 : IsOpenMap f
s : Set Y
⊢ interior (f ⁻¹' s) ⊆ f ⁻¹' interior s

Tactic:
hf.mapsTo_interior (mapsTo_preimage _ _)

Premises used: Set.Mem, setOf, Set.sUnion, Set.Subset, Set.mapsTo_preimage, Set.preimage, Set.MapsTo, interior, IsOpenMap.mapsTo_interior
-- 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₁ : IsOpenMap f
hf₂ : Continuous[inst, inst_1] f
s : Set Y
⊢ f ⁻¹' interior s = interior (f ⁻¹' s)

Tactic:
Subset.antisymm (preimage_interior_subset_interior_preimage hf₂)
    (interior_preimage_subset_preimage_interior hf₁)

Premises used: Set.Subset.antisymm, preimage_interior_subset_interior_preimage, IsOpenMap.interior_preimage_subset_preimage_interior
-- 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 : IsOpenMap f
s : Set Y
rw : (closure[inst] (f ⁻¹' s))ᶜ ⊆ (f ⁻¹' closure[inst_1] s)ᶜ
⊢ f ⁻¹' closure[inst_1] s ⊆ closure[inst] (f ⁻¹' s)

Tactic:
rw [← compl_subset_compl]

Premises used: Set.compl_subset_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 : IsOpenMap f
s : Set Y
⊢ (closure[inst] (f ⁻¹' s))ᶜ ⊆ (f ⁻¹' closure[inst_1] s)ᶜ

Tactic:
simp only [← interior_compl, ← preimage_compl, hf.interior_preimage_subset_preimage_interior]

Premises used: IsOpenMap.interior_preimage_subset_preimage_interior, interior_compl, Set.preimage_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 : IsOpenMap f
hfc : Continuous[inst, inst_1] f
s : Set Y
⊢ f ⁻¹' closure[inst_1] s = closure[inst] (f ⁻¹' s)

Tactic:
hf.preimage_closure_subset_closure_preimage.antisymm (hfc.closure_preimage_subset s)

Premises used: HasSubset.Subset.antisymm, IsOpenMap.preimage_closure_subset_closure_preimage, Continuous.closure_preimage_subset
-- 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₁ : IsOpenMap f
h₂ : Injective f
h₃ : Continuous[inst, inst_1] f
s : Set X
hs' : IsClosed[inst] s
rw : closure[inst] (f ⁻¹' f '' s) = s
rw₁ : closure[inst] s = s
rw₂ rw₃ : s = s
⊢ f ⁻¹' closure[inst_1] (f '' s) = s

Tactic:
rw [h₁.preimage_closure_eq_closure_preimage h₃, Set.preimage_image_eq _ h₂, hs'.closure_eq]

Premises used: IsOpenMap.preimage_closure_eq_closure_preimage, IsClosed.closure_eq, Set.preimage_image_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
hf : IsOpenMap f
s : Set Y
⊢ f ⁻¹' frontier s ⊆ frontier (f ⁻¹' s)

Tactic:
simpa only [frontier_eq_closure_inter_closure, preimage_inter] using
    inter_subset_inter hf.preimage_closure_subset_closure_preimage
      hf.preimage_closure_subset_closure_preimage

Premises used: Set.preimage_inter, Set.inter_subset_inter, frontier_eq_closure_inter_closure, IsOpenMap.preimage_closure_subset_closure_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
hf : IsOpenMap f
hfc : Continuous[inst, inst_1] f
s : Set Y
⊢ f ⁻¹' frontier s = frontier (f ⁻¹' s)

Tactic:
simp only [frontier_eq_closure_inter_closure, preimage_inter, preimage_compl,
    hf.preimage_closure_eq_closure_preimage hfc]

Premises used: Set.preimage_inter, IsOpenMap.preimage_closure_eq_closure_preimage, frontier_eq_closure_inter_closure, Set.preimage_compl
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : IsEmpty X
f : X → Y
⊢ IsOpenMap f

Tactic:
of_nhds_le h.elim

Premises used: IsEmpty.elim, IsOpenMap.of_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 : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) l
rw : (map f (𝓝 x) ⊓ l).NeBot
⊢ ClusterPt x (comap f l)

Tactic:
rw [ClusterPt, ← map_neBot_iff, Filter.push_pull]

Premises used: ClusterPt, Filter.push_pull, 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 : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) l
⊢ (map f (𝓝 x) ⊓ l).NeBot

Tactic:
h.neBot.mono <| inf_le_inf_right _ <| hf.nhds_le _

Premises used: Filter.NeBot.mono, ClusterPt.neBot, IsOpenMap.nhds_le, inf_le_inf_right
-- 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 : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) l
⊢ (map f (𝓝 x) ⊓ l).NeBot

Tactic:
exact h.neBot.mono <| inf_le_inf_right _ <| hf.nhds_le _

Premises used: Filter.NeBot.mono, ClusterPt.neBot, IsOpenMap.nhds_le, inf_le_inf_right
-- 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 : IsOpenMap f
x : X
l : Filter Y
h : AccPt (f x) l
rw : ∀ (h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)), ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l)
⊢ AccPt x (comap f l)

Tactic:
rw [accPt_iff_clusterPt] at h ⊢

Premises used: accPt_iff_clusterPt
-- 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 : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
apply : comap f (𝓟 {f x}ᶜ ⊓ l) ≤ 𝓟 {x}ᶜ ⊓ comap f l
⊢ ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l)

Tactic:
apply (hf.clusterPt_comap h).mono

Premises used: ClusterPt.mono, IsOpenMap.clusterPt_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 : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw : 𝓟 (f ⁻¹' {f x})ᶜ ⊓ comap f l ≤ 𝓟 {x}ᶜ ⊓ comap f l
⊢ comap f (𝓟 {f x}ᶜ ⊓ l) ≤ 𝓟 {x}ᶜ ⊓ comap f l

Tactic:
rw [comap_inf, comap_principal, preimage_compl]

Premises used: Filter.comap_inf, Filter.comap_principal, Set.preimage_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 : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ 𝓟 (f ⁻¹' {f x})ᶜ ≤ 𝓟 {x}ᶜ

Tactic:
simp
-- 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 : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ 𝓟 (f ⁻¹' {f x})ᶜ ⊓ comap f l ≤ 𝓟 {x}ᶜ ⊓ comap f l

Tactic:
exact inf_le_inf_right (comap f l) (by simp)

Premises used: inf_le_inf_right, Filter.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 : IsOpenMap f
hfc : Continuous[inst, inst_1] f
x : X
l : Filter Y
⊢ ClusterPt x (comap f l) ↔ ClusterPt (f x) l

Tactic:
⟨fun h => h.map hfc.continuousAt tendsto_comap, hf.clusterPt_comap⟩

Premises used: Filter.tendsto_comap, Continuous.continuousAt, ClusterPt.map, IsOpenMap.clusterPt_comap, Iff.intro
-- 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), IsOpen[inst] xᶜ → IsOpen[inst_1] (f '' xᶜ)) ↔
    ∀ {u : Set X}, IsClosed[inst] u → IsClosed[inst_1] (kernImage f u)
⊢ IsOpenMap f ↔ ∀ {u : Set X}, IsClosed[inst] u → IsClosed[inst_1] (kernImage f u)

Tactic:
rw [IsOpenMap, compl_surjective.forall]

Premises used: Function.Surjective.forall, IsOpenMap, 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), IsOpen[inst] xᶜ → IsOpen[inst_1] (f '' xᶜ)) ↔
    ∀ {u : Set X}, IsClosed[inst] u → IsClosed[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
⊢ IsOpenMap f ↔ ∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)

Tactic:
⟨fun hf => hf.nhds_le, IsOpenMap.of_nhds_le⟩

Premises used: IsOpenMap.nhds_le, Iff.intro, IsOpenMap.of_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
⊢ IsOpenMap f ↔ ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)

Tactic:
⟨fun hf _ _ ↦ hf.clusterPt_comap, fun h ↦ ?_⟩

Premises used: IsOpenMap.clusterPt_comap, Iff.intro
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
refine : ∀ (h : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)), IsOpenMap f
⊢ IsOpenMap f ↔ ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)

Tactic:
refine ⟨fun hf _ _ ↦ hf.clusterPt_comap, fun 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 : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
simp : ∀ (x : X), ∀ s ∈ 𝓝 x, f '' s ∈ 𝓝 (f x)
⊢ IsOpenMap f

Tactic:
simp only [isOpenMap_iff_nhds_le, le_map_iff]

Premises used: Filter.le_map_iff, isOpenMap_iff_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
h : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : s ∈ 𝓝 x
contrapose : ∀ (hs : f '' s ∉ 𝓝 (f x)), s ∉ 𝓝 x
⊢ f '' s ∈ 𝓝 (f x)

Tactic:
contrapose hs
-- 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 : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : f '' s ∉ 𝓝 (f x)
rw : ∀ (hs : ClusterPt (f x) (𝓟 (f '' s)ᶜ)), ClusterPt x (𝓟 sᶜ)
⊢ s ∉ 𝓝 x

Tactic:
rw [← mem_interior_iff_mem_nhds, mem_interior_iff_not_clusterPt_compl, not_not] at hs ⊢

Premises used: mem_interior_iff_mem_nhds, Classical.not_not, mem_interior_iff_not_clusterPt_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
h : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : ClusterPt (f x) (𝓟 (f '' s)ᶜ)
⊢ comap f (𝓟 (f '' s)ᶜ) ≤ 𝓟 sᶜ

Tactic:
simp [subset_preimage_image]

Premises used: Set.subset_preimage_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
h : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : ClusterPt (f x) (𝓟 (f '' s)ᶜ)
⊢ ClusterPt x (𝓟 sᶜ)

Tactic:
exact (h _ _ hs).mono <| by simp [subset_preimage_image]

Premises used: ClusterPt.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
hs : ∀ (s : Set X), f '' interior s ⊆ interior (f '' s)
u : Set X
hu : IsOpen[inst] u
⊢ f '' u ⊆ interior (f '' u)

Tactic:
simpa only [hu.interior_eq] using hs u

Premises used: IsOpen.interior_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), f '' interior xᶜ ⊆ interior (f '' xᶜ)) ↔
    ∀ {s : Set X}, closure[inst_1] (kernImage f s) ⊆ kernImage f (closure[inst] s)
⊢ IsOpenMap f ↔ ∀ {s : Set X}, closure[inst_1] (kernImage f s) ⊆ kernImage f (closure[inst] s)

Tactic:
rw [isOpenMap_iff_image_interior, compl_surjective.forall]

Premises used: Function.Surjective.forall, isOpenMap_iff_image_interior, 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), f '' interior xᶜ ⊆ interior (f '' xᶜ)) ↔
    ∀ {s : Set X}, closure[inst_1] (kernImage f s) ⊆ kernImage f (closure[inst] 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
hi : IsInducing f
ho : IsOpen[inst_1] (range f)
⊢ IsOpenMap f

Tactic:
IsOpenMap.of_nhds_le fun _ => (hi.map_nhds_of_mem _ <| IsOpen.mem_nhds ho <| mem_range_self _).ge

Premises used: Set.mem_range_self, Topology.IsInducing.map_nhds_of_mem, Eq.ge, IsOpen.mem_nhds, IsOpenMap.of_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
s : Set Y
hs : Dense s
hf : IsOpenMap f
⊢ Dense (f ⁻¹' s)

Tactic:
fun x ↦
  hf.preimage_closure_subset_closure_preimage <| hs (f x)

Premises used: Dense, IsOpenMap.preimage_closure_subset_closure_preimage
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs rwa rwa₁ rwa₂ rwa₃ : IsClosed[inst] s
⊢ IsClosed[inst] (id '' s)

Tactic:
rwa [image_id]

Premises used: Set.image_id
-- 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
hg : IsClosedMap g
hf : IsClosedMap f
s : Set X
hs : IsClosed[inst] s
rw : IsClosed[inst_2] (g '' f '' s)
⊢ IsClosed[inst_2] (g ∘ f '' s)

Tactic:
rw [image_comp]

Premises used: Set.image_comp
-- 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
hg : IsClosedMap g
hf : IsClosedMap f
s : Set X
hs : IsClosed[inst] s
⊢ IsClosed[inst_2] (g '' f '' s)

Tactic:
hg _ (hf _ hs)
-- 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
hg : IsClosedMap g
hf : IsClosedMap f
s : Set X
hs : IsClosed[inst] s
⊢ IsClosed[inst_2] (g '' f '' s)

Tactic:
exact hg _ (hf _ hs)
-- 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 : Surjective f
hf' : Continuous[inst, inst_1] f
hfg : IsClosedMap (g ∘ f)
K : Set Y
hK : IsClosed[inst_1] K
rw : IsClosed[inst_2] (g ∘ f '' f ⁻¹' K)
⊢ IsClosed[inst_2] (g '' K)

Tactic:
rw [← image_preimage_eq K hf, ← image_comp]

Premises used: Set.image_preimage_eq, Set.image_comp
-- 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 : Surjective f
hf' : Continuous[inst, inst_1] f
hfg : IsClosedMap (g ∘ f)
K : Set Y
hK : IsClosed[inst_1] K
⊢ IsClosed[inst_2] (g ∘ f '' f ⁻¹' K)

Tactic:
hfg _ (hK.preimage hf')

Premises used: IsClosed.preimage
-- 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 : Surjective f
hf' : Continuous[inst, inst_1] f
hfg : IsClosedMap (g ∘ f)
K : Set Y
hK : IsClosed[inst_1] K
⊢ IsClosed[inst_2] (g ∘ f '' f ⁻¹' K)

Tactic:
exact hfg _ (hK.preimage hf')

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
hf : IsClosedMap f
s : Set X
⊢ closure[inst_1] (f '' s) ⊆ f '' closure[inst] s

Tactic:
closure_minimal (image_mono subset_closure) (hf _ isClosed_closure)

Premises used: subset_closure, closure_minimal, Set.image_mono, isClosed_closure