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
h₁ : IsEmbedding f
h₂ : IsOpenMap f
⊢ IsOpenEmbedding f

Tactic:
⟨h₁, h₂.isOpen_range⟩

Premises used: IsOpenMap.isOpen_range, Topology.IsOpenEmbedding.mk
-- 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 : IsEmbedding f
hsurj : Surjective f
⊢ IsOpenEmbedding f

Tactic:
⟨hf, hsurj.range_eq ▸ isOpen_univ⟩

Premises used: Eq.rec, isOpen_univ, Function.Surjective.range_eq, Eq.symm, Topology.IsOpenEmbedding.mk
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsOpenEmbedding f ↔ IsEmbedding f ∧ IsOpenMap f

Tactic:
⟨fun h => ⟨h.1, h.isOpenMap⟩, fun h => .of_isEmbedding_isOpenMap h.1 h.2⟩

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap, And.right, Topology.IsOpenEmbedding.of_isEmbedding_isOpenMap, And.left, And.intro, 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
h₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsOpenMap f
simp : ∀ (x : X), 𝓝 x = comap f (𝓝 (f x))
⊢ IsOpenEmbedding f

Tactic:
simp only [isOpenEmbedding_iff_isEmbedding_isOpenMap, isEmbedding_iff, isInducing_iff_nhds, *,
    and_true]

Premises used: and_true, Topology.isEmbedding_iff, Topology.isOpenEmbedding_iff_isEmbedding_isOpenMap, Topology.isInducing_iff_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₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ ∀ (x : X), 𝓝 x = comap f (𝓝 (f x))

Tactic:
fun x =>
    le_antisymm (h₁.tendsto _).le_comap (@comap_map _ _ (𝓝 x) _ h₂ ▸ comap_mono (h₃.nhds_le _))

Premises used: Filter.Tendsto.le_comap, Filter.comap_map, Eq.rec, IsOpenMap.nhds_le, Filter.comap_mono, Continuous.tendsto, 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
h₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ ∀ (x : X), 𝓝 x = comap f (𝓝 (f x))

Tactic:
exact fun x =>
    le_antisymm (h₁.tendsto _).le_comap (@comap_map _ _ (𝓝 x) _ h₂ ▸ comap_mono (h₃.nhds_le _))

Premises used: Filter.Tendsto.le_comap, Continuous.tendsto, 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
⊢ IsOpenEmbedding f ↔ Continuous[inst, inst_1] f ∧ Injective f ∧ IsOpenMap f

Tactic:
⟨fun h => ⟨h.continuous, h.injective, h.isOpenMap⟩, fun h =>
    .of_continuous_injective_isOpenMap h.1 h.2.1 h.2.2⟩

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap, Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap, Topology.IsOpenEmbedding.continuous, And.right, And.left, And.intro, Iff.intro, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsOpenEmbedding.{u_1, u_1} (X := X) id

Tactic:
⟨.id, IsOpenMap.id.isOpen_range⟩

Premises used: Topology.IsEmbedding.id, IsOpenMap.id, IsOpenMap.isOpen_range, Topology.IsOpenEmbedding.mk
-- 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 : IsOpenEmbedding g
hf : IsOpenEmbedding f
⊢ IsOpenEmbedding (g ∘ f)

Tactic:
⟨hg.1.comp hf.1, (hg.isOpenMap.comp hf.isOpenMap).isOpen_range⟩

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap, IsOpenMap.comp, Topology.IsEmbedding.comp, IsOpenMap.isOpen_range, Topology.IsOpenEmbedding.mk
-- 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 : IsOpenEmbedding g
simp_rw : (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), 𝓝 ((g ∘ f) x) ≤ map (g ∘ f) (𝓝 x)
simp_rw₁ : (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), 𝓝 ((g ∘ f) x) ≤ map g (map f (𝓝 x))
simp_rw₂ : (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), 𝓝 (g (f x)) ≤ map g (map f (𝓝 x))
simp_rw₃ : (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), map g (𝓝 (f x)) ≤ map g (map f (𝓝 x))
⊢ IsOpenMap f ↔ IsOpenMap (g ∘ f)

Tactic:
simp_rw [isOpenMap_iff_nhds_le, ← map_map, comp, ← hg.map_nhds_eq, map_le_map_iff hg.injective]

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, Topology.IsOpenEmbedding.toIsEmbedding, isOpenMap_iff_nhds_le, Function.comp, Filter.map_map, Filter.map_le_map_iff, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
g : Y → Z
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
hg : IsOpenEmbedding g
⊢ IsOpenEmbedding (g ∘ f) ↔ IsOpenEmbedding f

Tactic:
simp only [isOpenEmbedding_iff_continuous_injective_isOpenMap, ← hg.isOpenMap_iff, ←
    hg.1.continuous_iff, hg.injective.of_comp_iff]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap_iff, Topology.isOpenEmbedding_iff_continuous_injective_isOpenMap, Topology.IsEmbedding.injective, Topology.IsEmbedding.continuous_iff, Function.Injective.of_comp_iff
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
g : Y → Z
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
hg : IsOpenEmbedding g
h : IsOpenEmbedding (g ∘ f)
⊢ IsOpenEmbedding f

Tactic:
(IsOpenEmbedding.of_comp_iff f hg).1 h

Premises used: Iff.mp, Topology.IsOpenEmbedding.of_comp_iff
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : IsEmpty X
f : X → Y
⊢ IsOpenEmbedding f

Tactic:
of_isEmbedding_isOpenMap (.of_subsingleton f) (.of_isEmpty f)

Premises used: IsOpenMap.of_isEmpty, Topology.IsOpenEmbedding.of_isEmbedding_isOpenMap, Topology.IsEmbedding.of_subsingleton
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
x : X
rw : f '' s ∈ map f (𝓝 x) ↔ s ∈ 𝓝 x
rw₁ : f ⁻¹' f '' s ∈ 𝓝 x ↔ s ∈ 𝓝 x
rw₂ rw₃ : s ∈ 𝓝 x ↔ s ∈ 𝓝 x
⊢ f '' s ∈ 𝓝 (f x) ↔ s ∈ 𝓝 x

Tactic:
rw [← hf.map_nhds_eq, mem_map, preimage_image_eq _ hf.injective]

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsEmbedding.injective, Set.preimage_image_eq, Filter.mem_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 : IsOpenEmbedding f
x : X
l : Filter Y
rw : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ AccPt (f x) l
rw₁ : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₂ : ClusterPt x (𝓟 (f ⁻¹' f '' {x})ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₃ : ClusterPt x (𝓟 (f ⁻¹' {f x})ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₄ : ClusterPt x (𝓟 (f ⁻¹' {f x}ᶜ) ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₅ : ClusterPt x (comap f (𝓟 {f x}ᶜ) ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₆ : ClusterPt x (comap f (𝓟 {f x}ᶜ ⊓ l)) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₇ rw₈ : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ AccPt x (comap f l) ↔ AccPt (f x) l

Tactic:
rw [accPt_iff_clusterPt, accPt_iff_clusterPt, ← hf.injective.preimage_image {x}, image_singleton,
    ← preimage_compl, ← comap_principal, ← comap_inf,
    hf.isOpenMap.clusterPt_comap_iff hf.continuous]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap, Set.image_singleton, Topology.IsOpenEmbedding.continuous, Filter.comap_inf, IsOpenMap.clusterPt_comap_iff, Function.Injective.preimage_image, Topology.IsEmbedding.injective, Filter.comap_principal, Set.preimage_compl, Singleton.singleton, 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 : IsClosedEmbedding f
⊢ IsEmbedding f

Tactic:
hf.toIsEmbedding

Premises used: Topology.IsClosedEmbedding.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 : IsClosedEmbedding f
⊢ IsInducing f

Tactic:
hf.isEmbedding.isInducing

Premises used: Topology.IsClosedEmbedding.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 : IsClosedEmbedding f
⊢ Continuous[inst, inst_1] f

Tactic:
hf.isEmbedding.continuous

Premises used: Topology.IsClosedEmbedding.isEmbedding, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
ι : Type u_4
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
g : ι → X
l : Filter ι
x : X
hf : IsClosedEmbedding f
⊢ Tendsto g l (𝓝 x) ↔ Tendsto (f ∘ g) l (𝓝 (f x))

Tactic:
hf.isEmbedding.tendsto_nhds_iff

Premises used: Topology.IsClosedEmbedding.isEmbedding, Topology.IsEmbedding.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 : IsClosedEmbedding f
⊢ IsClosedMap f

Tactic:
hf.isEmbedding.isInducing.isClosedMap hf.isClosed_range

Premises used: Topology.IsClosedEmbedding.isEmbedding, Topology.IsEmbedding.isInducing, Topology.IsInducing.isClosedMap, Topology.IsClosedEmbedding.isClosed_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 : IsClosedEmbedding f
s : Set X
h : IsClosed[inst_1] (f '' s)
rw : IsClosed[inst] (f ⁻¹' f '' s)
⊢ IsClosed[inst] s

Tactic:
rw [← preimage_image_eq s hf.injective]

Premises used: Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsEmbedding.injective, 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 : IsClosedEmbedding f
s : Set X
h : IsClosed[inst_1] (f '' s)
⊢ IsClosed[inst] (f ⁻¹' f '' s)

Tactic:
h.preimage hf.continuous

Premises used: Topology.IsClosedEmbedding.continuous, 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 : IsClosedEmbedding f
s : Set X
h : IsClosed[inst_1] (f '' s)
⊢ IsClosed[inst] (f ⁻¹' f '' s)

Tactic:
exact h.preimage hf.continuous

Premises used: Topology.IsClosedEmbedding.continuous, 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 : IsClosedEmbedding f
s : Set Y
hs : s ⊆ range f
rw : IsClosed[inst_1] s ↔ IsClosed[inst_1] (f '' f ⁻¹' s)
rw₁ rw₂ : IsClosed[inst_1] s ↔ IsClosed[inst_1] s
⊢ IsClosed[inst_1] s ↔ IsClosed[inst] (f ⁻¹' s)

Tactic:
rw [hf.isClosed_iff_image_isClosed, image_preimage_eq_of_subset hs]

Premises used: Set.image_preimage_eq_of_subset, Topology.IsClosedEmbedding.isClosed_iff_image_isClosed
-- 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₁ : IsEmbedding f
h₂ : IsClosedMap f
⊢ IsClosedEmbedding f

Tactic:
⟨h₁, image_univ (f := f) ▸ h₂ univ isClosed_univ⟩

Premises used: isClosed_univ, Set.image_univ, Set.univ, Eq.rec, Topology.IsClosedEmbedding.mk
-- 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₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsClosedMap f
⊢ IsClosedEmbedding f

Tactic:
.of_isEmbedding_isClosedMap ⟨⟨?_⟩, h₂⟩ h₃

Premises used: Topology.IsClosedEmbedding.of_isEmbedding_isClosedMap, Topology.IsInducing.mk, Topology.IsEmbedding.mk
-- 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₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsClosedMap f
refine : inst = induced f inst_1
⊢ IsClosedEmbedding f

Tactic:
refine .of_isEmbedding_isClosedMap ⟨⟨?_⟩, h₂⟩ 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₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsClosedMap f
⊢ inst = induced f inst_1

Tactic:
h₁.le_induced.antisymm fun s hs => ?_

Premises used: LE.le.antisymm, Continuous.le_induced
-- 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₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsClosedMap f
refine : ∀ (s : Set X) (hs : IsOpen[inst] s), IsOpen[induced f inst_1] s
⊢ inst = induced f inst_1

Tactic:
refine h₁.le_induced.antisymm fun s hs => ?_

Premises used: LE.le.antisymm, Continuous.le_induced
-- 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₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set X
hs : IsOpen[inst] s
⊢ IsOpen[induced f inst_1] s

Tactic:
⟨(f '' sᶜ)ᶜ, (h₃ _ hs.isClosed_compl).isOpen_compl, ?_⟩

Premises used: IsClosed.isOpen_compl, Compl.compl, And.intro, Exists.intro, Set.image, IsOpen
-- 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₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set X
hs : IsOpen[inst] s
refine : f ⁻¹' (f '' sᶜ)ᶜ = s
⊢ IsOpen[induced f inst_1] s

Tactic:
refine ⟨(f '' sᶜ)ᶜ, (h₃ _ hs.isClosed_compl).isOpen_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₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set X
hs : IsOpen[inst] s
rw : (f ⁻¹' f '' sᶜ)ᶜ = s
rw₁ : sᶜᶜ = s
rw₂ rw₃ : s = s
⊢ f ⁻¹' (f '' sᶜ)ᶜ = s

Tactic:
rw [preimage_compl, preimage_image_eq _ h₂, compl_compl]

Premises used: compl_compl, Set.preimage_image_eq, Set.preimage_compl
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsClosedEmbedding.{u_1, u_1} (X := X) id

Tactic:
⟨.id, IsClosedMap.id.isClosed_range⟩

Premises used: Topology.IsEmbedding.id, IsClosedMap.id, Topology.IsClosedEmbedding.mk, IsClosedMap.isClosed_range
-- 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 : IsClosedEmbedding g
hf : IsClosedEmbedding f
⊢ IsClosedEmbedding (g ∘ f)

Tactic:
⟨hg.isEmbedding.comp hf.isEmbedding, (hg.isClosedMap.comp hf.isClosedMap).isClosed_range⟩

Premises used: Topology.IsClosedEmbedding.isClosedMap, Topology.IsClosedEmbedding.isEmbedding, Topology.IsEmbedding.comp, IsClosedMap.comp, Topology.IsClosedEmbedding.mk, IsClosedMap.isClosed_range
-- 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 : IsClosedEmbedding g
simp_rw : IsEmbedding (g ∘ f) ∧ IsClosed[inst_2] (range (g ∘ f)) ↔ IsEmbedding f ∧ IsClosed[inst_1] (range f)
simp_rw₁ : IsEmbedding f ∧ IsClosed[inst_2] (range (g ∘ f)) ↔ IsEmbedding f ∧ IsClosed[inst_1] (range f)
simp_rw₂ : IsEmbedding f ∧ IsClosed[inst_2] (g '' range f) ↔ IsEmbedding f ∧ IsClosed[inst_1] (range f)
⊢ IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f

Tactic:
simp_rw [isClosedEmbedding_iff, hg.isEmbedding.of_comp_iff, Set.range_comp,
    ← hg.isClosed_iff_image_isClosed]

Premises used: Set.range_comp, Topology.IsClosedEmbedding.isEmbedding, Topology.isClosedEmbedding_iff, Topology.IsClosedEmbedding.isClosed_iff_image_isClosed, Topology.IsEmbedding.of_comp_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
inst_2 : TopologicalSpace Z
hg : IsEmbedding g
hgf : IsClosedEmbedding (g ∘ f)
⊢ IsClosed[inst_1] (g ⁻¹' range (g ∘ f))

Tactic:
hg.isClosed_preimage _ hgf.isClosed_range

Premises used: Topology.IsInducing.isClosed_preimage, Topology.IsEmbedding.toIsInducing, Topology.IsClosedEmbedding.isClosed_range
-- 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 : IsEmbedding g
hgf : IsClosedEmbedding (g ∘ f)
h : range f = g ⁻¹' range (g ∘ f)
⊢ IsClosed[inst_1] (range f)

Tactic:
convert! hg.isClosed_preimage _ hgf.isClosed_range

Premises used: Topology.IsInducing.isClosed_preimage, Topology.IsEmbedding.toIsInducing, Topology.IsClosedEmbedding.isClosed_range
-- 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 : IsEmbedding g
hgf : IsClosedEmbedding (g ∘ f)
h : range f = g ⁻¹' g '' range f
h₁ h₂ : range f = range f
⊢ range f = g ⁻¹' range (g ∘ f)

Tactic:
rw [range_comp, hg.injective.preimage_image]

Premises used: Set.range_comp, Function.Injective.preimage_image, Topology.IsEmbedding.injective
-- 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 : IsClosedEmbedding f
s : Set X
⊢ closure[inst_1] (f '' s) = f '' closure[inst] s

Tactic:
hf.isClosedMap.closure_image_eq_of_continuous hf.continuous s

Premises used: Topology.IsClosedEmbedding.isClosedMap, Topology.IsClosedEmbedding.continuous, IsClosedMap.closure_image_eq_of_continuous
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsOpenQuotientMap.{u_1, u_1} (X := X) id

Tactic:
⟨surjective_id, continuous_id, .id⟩

Premises used: IsOpenQuotientMap.mk, continuous_id, Function.surjective_id, IsOpenMap.id
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsOpenQuotientMap f
⊢ IsQuotientMap f

Tactic:
h.isOpenMap.isQuotientMap h.continuous h.surjective

Premises used: IsOpenMap.isQuotientMap, IsOpenQuotientMap.continuous, IsOpenQuotientMap.surjective, IsOpenQuotientMap.isOpenMap
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsOpenQuotientMap f ↔ IsOpenMap f ∧ IsQuotientMap f

Tactic:
⟨fun h ↦ ⟨h.isOpenMap, h.isQuotientMap⟩, fun ⟨ho, hq⟩ ↦ ⟨hq.surjective, hq.continuous, ho⟩⟩

Premises used: Topology.IsQuotientMap.surjective, IsOpenQuotientMap.mk, Topology.IsQuotientMap.continuous, And.intro, Iff.intro, IsOpenQuotientMap, IsOpenQuotientMap.isQuotientMap, IsOpenQuotientMap.isOpenMap, _private.0.IsOpenQuotientMap.iff_isOpenMap_isQuotientMap.match_1
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
ho : IsOpenMap f
hq : IsQuotientMap f
⊢ IsOpenQuotientMap f

Tactic:
iff_isOpenMap_isQuotientMap.2 ⟨ho, hq⟩

Premises used: Iff.mpr, And.intro, IsOpenQuotientMap.iff_isOpenMap_isQuotientMap
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hg : IsOpenQuotientMap g
hf : IsOpenQuotientMap f
⊢ IsOpenQuotientMap (g ∘ f)

Tactic:
⟨.comp hg.1 hf.1, .comp hg.2 hf.2, .comp hg.3 hf.3⟩

Premises used: IsOpenQuotientMap.continuous, IsOpenMap.comp, Continuous.comp, IsOpenQuotientMap.mk, IsOpenQuotientMap.surjective, Function.Surjective.comp, IsOpenQuotientMap.isOpenMap
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsOpenQuotientMap f
x : X
⊢ map f (𝓝 x) = 𝓝 (f x)

Tactic:
le_antisymm h.continuous.continuousAt <| h.isOpenMap.nhds_le _

Premises used: IsOpenQuotientMap.continuous, IsOpenMap.nhds_le, Continuous.continuousAt, le_antisymm, IsOpenQuotientMap.isOpenMap
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
h : IsOpenQuotientMap f
g : Y → Z
⊢ Continuous[inst, inst_2] (g ∘ f) ↔ Continuous[inst_1, inst_2] g

Tactic:
h.isQuotientMap.continuous_iff.symm

Premises used: Topology.IsQuotientMap.continuous_iff, IsOpenQuotientMap.isQuotientMap, Iff.symm
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
h : IsOpenQuotientMap f
g : Y → Z
x : X
⊢ ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

Tactic:
simp only [ContinuousAt, ← h.map_nhds_eq, tendsto_map'_iff, comp_def]

Premises used: ContinuousAt, Filter.tendsto_map'_iff, IsOpenQuotientMap.map_nhds_eq, Function.comp_def
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsOpenQuotientMap f
s : Set Y
⊢ Dense (f ⁻¹' s) ↔ Dense s

Tactic:
⟨fun hs ↦ h.surjective.denseRange.dense_of_mapsTo h.continuous hs (mapsTo_preimage _ _),
    fun hs ↦ hs.preimage h.isOpenMap⟩

Premises used: DenseRange.dense_of_mapsTo, IsOpenQuotientMap.continuous, Function.Surjective.denseRange, IsOpenQuotientMap.surjective, Set.mapsTo_preimage, Iff.intro, IsOpenQuotientMap.isOpenMap, Dense.preimage
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : BaireSpace X
hf : IsOpenQuotientMap f
baire_property :
  ∀ (f : ℕ → Set Y),
    (∀ (n : ℕ), IsOpen[inst_1] (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense.{u_2} (X := Y) (⋂ (n : ℕ), f n)
⊢ BaireSpace Y

Tactic:
constructor
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : BaireSpace X
hf : IsOpenQuotientMap f
u : ℕ → Set Y
hou : ∀ (n : ℕ), IsOpen[inst_1] (u n)
hdu : ∀ (n : ℕ), Dense (u n)
⊢ Dense.{u_1} (X := X) (⋂ (n : ℕ), f ⁻¹' u n)

Tactic:
have := dense_iInter_of_isOpen_nat (fun n => hf.continuous.isOpen_preimage (u n) (hou n))
    (fun n => (IsOpenQuotientMap.dense_preimage_iff hf).mpr (hdu n))
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : BaireSpace X
hf : IsOpenQuotientMap f
u : ℕ → Set Y
hou : ∀ (n : ℕ), IsOpen[inst_1] (u n)
hdu : ∀ (n : ℕ), Dense (u n)
this : Dense.{u_1} (X := X) (⋂ (n : ℕ), f ⁻¹' u n)
⊢ Dense.{u_2} (X := Y) (⋂ (n : ℕ), u n)

Tactic:
simp_all [← preimage_iInter, IsOpenQuotientMap.dense_preimage_iff]

Premises used: IsOpenQuotientMap.dense_preimage_iff, Set.preimage_iInter
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
ind : IsInducing f
surj : Surjective f
U : Set X
U_open : IsOpen[inst] U
obtain : ∀ (V : Set Y) (hV : IsOpen[inst_1] V) (U_open : IsOpen[inst] (f ⁻¹' V)), IsOpen[inst_1] (f '' f ⁻¹' V)
⊢ IsOpen[inst_1] (f '' U)

Tactic:
obtain ⟨V, hV, rfl⟩ := ind.isOpen_iff.mp U_open

Premises used: Topology.IsInducing.isOpen_iff, Iff.mp, rfl
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
ind : IsInducing f
surj : Surjective f
V : Set Y
hV : IsOpen[inst_1] V
U_open : IsOpen[inst] (f ⁻¹' V)
rwa rwa₁ rwa₂ rwa₃ : IsOpen[inst_1] V
⊢ IsOpen[inst_1] (f '' f ⁻¹' V)

Tactic:
rwa [V.image_preimage_eq surj]

Premises used: Set.image_preimage_eq