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 Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
h : ∀ (x : X), x ∈ closure[inst_1] s ↔ x ∈ f ⁻¹' closure[inst] (f '' s)
⊢ closure[inst_1] s = f ⁻¹' closure[inst] (f '' s)

Tactic:
ext x
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
x : X
h : x ∈ closure[inst_1] s ↔ f x ∈ closure[inst] (f '' s)
h₁ : x ∈ closure[inst_1] s ↔ x ∈ closure[induced f inst] s
h₂ h₃ : x ∈ closure[induced f inst] s ↔ x ∈ closure[induced f inst] s
⊢ x ∈ closure[inst_1] s ↔ x ∈ f ⁻¹' closure[inst] (f '' s)

Tactic:
rw [Set.mem_preimage, ← closure_induced, hf.eq_induced]

Premises used: closure_induced, Topology.IsInducing.eq_induced, Set.mem_preimage
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
rw : IsClosed[induced f inst] s ↔ ∃ (t : Set Y), IsClosed[inst] t ∧ f ⁻¹' t = s
rw₁ rw₂ : (∃ (t : Set Y), IsClosed[inst] t ∧ f ⁻¹' t = s) ↔ ∃ (t : Set Y), IsClosed[inst] t ∧ f ⁻¹' t = s
⊢ IsClosed[inst_1] s ↔ ∃ (t : Set Y), IsClosed[inst] t ∧ f ⁻¹' t = s

Tactic:
rw [hf.eq_induced, isClosed_induced_iff]

Premises used: isClosed_induced_iff, Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
hs : IsClosed[inst_1] s
obtain :
  ∀ (c : Set Y) (hc : IsClosed[inst] c) (hs : IsClosed[inst_1] (f ⁻¹' c)),
    ∃ (c_1 : Set Y), IsClosed[inst] c_1 ∧ f '' f ⁻¹' c = c_1 ∩ range f
⊢ ∃ (c : Set Y), IsClosed[inst] c ∧ f '' s = c ∩ range f

Tactic:
obtain ⟨c, hc, rfl⟩ := hf.isClosed_iff.1 hs

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 Y
inst_1 : TopologicalSpace X
hf : IsInducing f
c : Set Y
hc : IsClosed[inst] c
hs : IsClosed[inst_1] (f ⁻¹' c)
⊢ ∃ (c_1 : Set Y), IsClosed[inst] c_1 ∧ f '' f ⁻¹' c = c_1 ∩ range f

Tactic:
⟨c, hc, image_preimage_eq_inter_range⟩

Premises used: Set.image_preimage_eq_inter_range, And.intro, Exists.intro
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
c : Set Y
hc : IsClosed[inst] c
hs : IsClosed[inst_1] (f ⁻¹' c)
⊢ ∃ (c_1 : Set Y), IsClosed[inst] c_1 ∧ f '' f ⁻¹' c = c_1 ∩ range f

Tactic:
exact ⟨c, hc, image_preimage_eq_inter_range⟩
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
rw : IsClosed[induced f inst] s ↔ ∀ (x : X), f x ∈ closure[inst] (f '' s) → x ∈ s
rw₁ rw₂ : (∀ (a : X), f a ∈ closure[inst] (f '' s) → a ∈ s) ↔ ∀ (x : X), f x ∈ closure[inst] (f '' s) → x ∈ s
⊢ IsClosed[inst_1] s ↔ ∀ (x : X), f x ∈ closure[inst] (f '' s) → x ∈ s

Tactic:
rw [hf.eq_induced, isClosed_induced_iff']

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

Tactic:
(isClosed_iff h).mpr ⟨s, hs, rfl⟩

Premises used: Iff.mpr, And.intro, Exists.intro, rfl, Topology.IsInducing.isClosed_iff
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
rw : IsOpen[induced f inst] s ↔ ∃ (t : Set Y), IsOpen[inst] t ∧ f ⁻¹' t = s
rw₁ rw₂ : (∃ (t : Set Y), IsOpen[inst] t ∧ f ⁻¹' t = s) ↔ ∃ (t : Set Y), IsOpen[inst] t ∧ f ⁻¹' t = s
⊢ IsOpen[inst_1] s ↔ ∃ (t : Set Y), IsOpen[inst] t ∧ f ⁻¹' t = s

Tactic:
rw [hf.eq_induced, isOpen_induced_iff]

Premises used: Topology.IsInducing.eq_induced, isOpen_induced_iff
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
hs : IsOpen[inst_1] s
obtain :
  ∀ (c : Set Y) (hc : IsOpen[inst] c) (hs : IsOpen[inst_1] (f ⁻¹' c)),
    ∃ (c_1 : Set Y), IsOpen[inst] c_1 ∧ f '' f ⁻¹' c = c_1 ∩ range f
⊢ ∃ (c : Set Y), IsOpen[inst] c ∧ f '' s = c ∩ range f

Tactic:
obtain ⟨c, hc, rfl⟩ := hf.isOpen_iff.1 hs

Premises used: Topology.IsInducing.isOpen_iff, Iff.mp, rfl
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
c : Set Y
hc : IsOpen[inst] c
hs : IsOpen[inst_1] (f ⁻¹' c)
⊢ ∃ (c_1 : Set Y), IsOpen[inst] c_1 ∧ f '' f ⁻¹' c = c_1 ∩ range f

Tactic:
⟨c, hc, image_preimage_eq_inter_range⟩

Premises used: Set.image_preimage_eq_inter_range, And.intro, Exists.intro
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
c : Set Y
hc : IsOpen[inst] c
hs : IsOpen[inst_1] (f ⁻¹' c)
⊢ ∃ (c_1 : Set Y), IsOpen[inst] c_1 ∧ f '' f ⁻¹' c = c_1 ∩ range f

Tactic:
exact ⟨c, hc, image_preimage_eq_inter_range⟩
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
⊢ {s : Set X | IsOpen[inst_1] s} = preimage f '' {t : Set Y | IsOpen[inst] t}

Tactic:
Set.ext fun _ ↦ hf.isOpen_iff

Premises used: Set.ext, Topology.IsInducing.isOpen_iff
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ Dense s ↔ ∀ (x : X), f x ∈ closure[inst] (f '' s)

Tactic:
simp only [Dense, hf.closure_eq_preimage_closure_image, mem_preimage]

Premises used: Dense, Topology.IsInducing.closure_eq_preimage_closure_image, Set.mem_preimage
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : Subsingleton X
f : X → Y
⊢ IsInducing f

Tactic:
⟨Subsingleton.elim _ _⟩

Premises used: Topology.IsInducing.mk, Subsingleton.elim
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : IndiscreteTopology Y
f : X → Y
hf : IsInducing f
⊢ IndiscreteTopology Y

Tactic:
cases IndiscreteTopology.eq_top Y

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

Tactic:
cases IndiscreteTopology.eq_top Y

Premises used: IndiscreteTopology.eq_top
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
inst_1 : IndiscreteTopology Y
hf : IsInducing f
this : TopologicalSpace Y := ⊤
refl : induced f ⊤ = ⊤
refl₁ refl₂ : Eq.{u_1 + 1} (α := TopologicalSpace X) ⊤ ⊤
⊢ inst = ⊤

Tactic:
rw [hf.eq_induced, induced_top]

Premises used: induced_top, Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : NontrivialTopology X
f : X → Y
hf : IsInducing f
⊢ ¬NontrivialTopology Y → ¬NontrivialTopology X

Tactic:
simpa using (fun _ : IndiscreteTopology Y => hf.indiscreteTopology)

Premises used: Topology.IsInducing.indiscreteTopology
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
hf : Injective f
⊢ IsEmbedding f

Tactic:
@IsEmbedding.mk X Y (t.induced f) t _ (.induced f) hf

Premises used: Topology.IsInducing.induced, 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
hf : IsEmbedding f
⊢ IsInducing f

Tactic:
hf.toIsInducing

Premises used: Topology.IsEmbedding.toIsInducing
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inj : Injective f
induced : ∀ (x : X), comap f (𝓝 (f x)) = 𝓝 x
⊢ IsEmbedding f

Tactic:
⟨isInducing_iff_nhds.2 fun x => (induced x).symm, inj⟩

Premises used: Iff.mpr, Topology.isInducing_iff_nhds, Eq.symm, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsEmbedding.{u_1, u_1} (X := X) id

Tactic:
⟨.id, fun _ _ h => h⟩

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

Tactic:
{ hg.isInducing.comp hf.isInducing with injective := fun _ _ h => hf.injective <| hg.injective h }

Premises used: Topology.IsInducing.comp, Topology.IsEmbedding.isInducing, Topology.IsEmbedding.injective, Topology.IsEmbedding.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 : IsEmbedding g
simp_rw : IsInducing (g ∘ f) ∧ Injective (g ∘ f) ↔ IsInducing f ∧ Injective f
simp_rw₁ : IsInducing f ∧ Injective (g ∘ f) ↔ IsInducing f ∧ Injective f
⊢ IsEmbedding (g ∘ f) ↔ IsEmbedding f

Tactic:
simp_rw [isEmbedding_iff, hg.isInducing.of_comp_iff, hg.injective.of_comp_iff f]

Premises used: Topology.isEmbedding_iff, Topology.IsInducing.of_comp_iff, Topology.IsEmbedding.isInducing, Topology.IsEmbedding.injective, Function.Injective.of_comp_iff
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
g : Y → X
h : LeftInverse f g
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst] g
⊢ IsEmbedding g

Tactic:
.of_comp hg hf <| h.comp_eq_id.symm ▸ .id

Premises used: Eq.rec, Topology.IsEmbedding.id, Function.LeftInverse.comp_eq_id, Topology.IsEmbedding.of_comp, Eq.symm
-- 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
x : X
⊢ map f (𝓝 x) = 𝓝[range f] f x

Tactic:
hf.1.map_nhds_eq x

Premises used: Topology.IsEmbedding.toIsInducing, Topology.IsInducing.map_nhds_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 : IsEmbedding f
x : X
h : range f ∈ 𝓝 (f x)
⊢ map f (𝓝 x) = 𝓝 (f x)

Tactic:
hf.1.map_nhds_of_mem x h

Premises used: Topology.IsInducing.map_nhds_of_mem, Topology.IsEmbedding.toIsInducing
-- 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 : IsEmbedding g
⊢ Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y))

Tactic:
hg.isInducing.tendsto_nhds_iff

Premises used: Topology.IsInducing.tendsto_nhds_iff, Topology.IsEmbedding.isInducing
-- 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
⊢ Continuous[inst, inst_1] f ↔ Continuous[inst, inst_2] (g ∘ f)

Tactic:
hg.isInducing.continuous_iff

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

Tactic:
hf.isInducing.continuous

Premises used: Topology.IsEmbedding.isInducing, Topology.IsInducing.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 : IsEmbedding f
s : Set X
⊢ closure[inst] s = f ⁻¹' closure[inst_1] (f '' s)

Tactic:
hf.1.closure_eq_preimage_closure_image s

Premises used: Topology.IsEmbedding.toIsInducing, Topology.IsInducing.closure_eq_preimage_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
inst_2 : DiscreteTopology Y
hf : IsEmbedding f
⊢ DiscreteTopology X

Tactic:
.of_continuous_injective hf.continuous hf.injective

Premises used: DiscreteTopology.of_continuous_injective, Topology.IsEmbedding.injective, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Subsingleton X
f : X → Y
⊢ IsEmbedding f

Tactic:
⟨.of_subsingleton f, f.injective_of_subsingleton⟩

Premises used: Topology.IsInducing.of_subsingleton, Function.injective_of_subsingleton, 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
⊢ IsCoinducing f ↔ ∀ (s : Set Y), IsOpen[inst] (f ⁻¹' s) ↔ IsOpen[inst_1] s

Tactic:
(isCoinducing_iff' _).trans <| eq_comm.trans TopologicalSpace.ext_iff

Premises used: TopologicalSpace.ext_iff, Topology.isCoinducing_iff', eq_comm, Iff.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
⊢ (∀ (x : Set Y), IsOpen[inst] (f ⁻¹' xᶜ) ↔ IsOpen[inst_1] xᶜ) ↔
    ∀ (s : Set Y), IsClosed[inst] (f ⁻¹' s) ↔ IsClosed[inst_1] s

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 : IsCoinducing f
s : Set Y
⊢ IsOpen[inst] (f ⁻¹' s) ↔ IsOpen[inst_1] s

Tactic:
isCoinducing_iff.mp hf _

Premises used: Iff.mp, Topology.isCoinducing_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 : IsCoinducing f
s : Set Y
⊢ IsClosed[inst] (f ⁻¹' s) ↔ IsClosed[inst_1] s

Tactic:
isCoinducing_iff_isClosed.mp hf _

Premises used: Iff.mp, Topology.isCoinducing_iff_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
hf : IsCoinducing f
s : Set Y
hs rwa rwa₁ rwa₂ rwa₃ : IsOpen[inst_1] s
⊢ IsOpen[inst] (f ⁻¹' s)

Tactic:
rwa [hf.isOpen_preimage]

Premises used: Topology.IsCoinducing.isOpen_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
hg : IsCoinducing g
hf : IsCoinducing f
rw : coinduced g inst_1 = coinduced (g ∘ f) inst
rw₁ : coinduced g (coinduced f inst) = coinduced (g ∘ f) inst
rw₂ rw₃ : coinduced (g ∘ f) inst = coinduced (g ∘ f) inst
⊢ inst_2 = coinduced (g ∘ f) inst

Tactic:
rw [hg.eq_coinduced, hf.eq_coinduced, coinduced_compose]

Premises used: Topology.IsCoinducing.eq_coinduced, coinduced_compose
-- 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 : IsCoinducing f
⊢ IsCoinducing (g ∘ f) ↔ IsCoinducing g

Tactic:
⟨fun hgf ↦ .of_isOpen_preimage_iff_isOpen fun s ↦ ?_, fun hg ↦ hg.comp hf⟩

Premises used: Topology.IsCoinducing.of_isOpen_preimage_iff_isOpen, Topology.IsCoinducing.comp, Iff.intro
-- 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 : IsCoinducing f
refine : ∀ (hgf : IsCoinducing (g ∘ f)) (s : Set Z), IsOpen[inst_1] (g ⁻¹' s) ↔ IsOpen[inst_2] s
⊢ IsCoinducing (g ∘ f) ↔ IsCoinducing g

Tactic:
refine ⟨fun hgf ↦ .of_isOpen_preimage_iff_isOpen fun s ↦ ?_, fun hg ↦ hg.comp hf⟩
-- 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 : IsCoinducing f
hgf : IsCoinducing (g ∘ f)
s : Set Z
rw : IsOpen[inst_1] (g ⁻¹' s) ↔ IsOpen[inst] (g ∘ f ⁻¹' s)
rw₁ : IsOpen[inst_1] (g ⁻¹' s) ↔ IsOpen[inst] (f ⁻¹' g ⁻¹' s)
rw₂ rw₃ : IsOpen[inst_1] (g ⁻¹' s) ↔ IsOpen[inst_1] (g ⁻¹' s)
⊢ IsOpen[inst_1] (g ⁻¹' s) ↔ IsOpen[inst_2] s

Tactic:
rw [← hgf.isOpen_preimage, Set.preimage_comp, hf.isOpen_preimage]

Premises used: Set.preimage_comp, Topology.IsCoinducing.isOpen_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 : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsCoinducing (g ∘ f)
grw : coinduced (g ∘ f) inst ≤ coinduced g inst_1
grw₁ : coinduced g (coinduced f inst) ≤ coinduced g inst_1
grw₂ grw₃ : coinduced g inst_1 ≤ coinduced g inst_1
⊢ inst_2 ≤ coinduced g inst_1

Tactic:
grw [hgf.eq_coinduced, ← coinduced_compose, hf.coinduced_le]

Premises used: Topology.IsCoinducing.eq_coinduced, coinduced_compose, Continuous.coinduced_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 : IsCoinducing f
hf' : Injective f
s : Set X
hs : IsOpen[inst] s
rwa : IsOpen[inst] (f ⁻¹' f '' s)
rwa₁ rwa₂ rwa₃ rwa₄ : IsOpen[inst] s
⊢ IsOpen[inst_1] (f '' s)

Tactic:
rwa [← hf.isOpen_preimage, preimage_image_eq _ hf']

Premises used: Topology.IsCoinducing.isOpen_preimage, 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
simp_rw : IsCoinducing f ∧ Surjective f ↔ Surjective f ∧ ∀ (s : Set Y), IsClosed[inst_1] s ↔ IsClosed[inst] (f ⁻¹' s)
simp_rw₁ :
  (∀ (s : Set Y), IsClosed[inst] (f ⁻¹' s) ↔ IsClosed[inst_1] s) ∧ Surjective f ↔
    Surjective f ∧ ∀ (s : Set Y), IsClosed[inst_1] s ↔ IsClosed[inst] (f ⁻¹' s)
simp_rw₂ :
  (Surjective f ∧ ∀ (s : Set Y), IsClosed[inst] (f ⁻¹' s) ↔ IsClosed[inst_1] s) ↔
    Surjective f ∧ ∀ (s : Set Y), IsClosed[inst_1] s ↔ IsClosed[inst] (f ⁻¹' s)
⊢ IsQuotientMap f ↔ Surjective f ∧ ∀ (s : Set Y), IsClosed[inst_1] s ↔ IsClosed[inst] (f ⁻¹' s)

Tactic:
simp_rw [isQuotientMap_iff, isCoinducing_iff_isClosed, and_comm, iff_comm]

Premises used: Topology.isQuotientMap_iff, iff_comm, and_comm, Topology.isCoinducing_iff_isClosed
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsQuotientMap.{u_1, u_1} (X := X) id

Tactic:
⟨.id _, fun x => ⟨x, rfl⟩⟩

Premises used: Topology.IsCoinducing.id, Exists.intro, Topology.IsQuotientMap.mk, 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
hg : IsQuotientMap g
hf : IsQuotientMap f
⊢ IsQuotientMap (g ∘ f)

Tactic:
⟨.comp hg.1 hf.1, hg.surjective.comp hf.surjective, ⟩

Premises used: Topology.IsQuotientMap.surjective, Topology.IsCoinducing.comp, Topology.IsQuotientMap.isCoinducing, Topology.IsQuotientMap.mk, Function.Surjective.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 : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsQuotientMap (g ∘ f)
⊢ IsQuotientMap g

Tactic:
⟨.of_comp hf hg hgf.1, hgf.2.of_comp⟩

Premises used: Topology.IsQuotientMap.surjective, Function.Surjective.of_comp, Topology.IsCoinducing.of_comp, Topology.IsQuotientMap.isCoinducing, Topology.IsQuotientMap.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
hgf : IsQuotientMap (g ∘ f)
hf : IsCoinducing f
⊢ IsQuotientMap g

Tactic:
⟨hf.of_comp_iff.mp hgf.1, hgf.2.of_comp⟩

Premises used: Topology.IsQuotientMap.surjective, Topology.IsCoinducing.of_comp_iff, Function.Surjective.of_comp, Topology.IsQuotientMap.isCoinducing, Topology.IsQuotientMap.mk, Iff.mp
-- 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 : IsQuotientMap f
rw : IsCoinducing (g ∘ f) ∧ Surjective (g ∘ f) ↔ IsQuotientMap g
rw₁ : IsCoinducing (g ∘ f) ∧ Surjective (g ∘ f) ↔ IsCoinducing g ∧ Surjective g
rw₂ : IsCoinducing g ∧ Surjective (g ∘ f) ↔ IsCoinducing g ∧ Surjective g
rw₃ rw₄ : IsCoinducing g ∧ Surjective g ↔ IsCoinducing g ∧ Surjective g
⊢ IsQuotientMap (g ∘ f) ↔ IsQuotientMap g

Tactic:
rw [isQuotientMap_iff, isQuotientMap_iff, hf.isCoinducing.of_comp_iff, hf.surjective.of_comp_iff]

Premises used: Topology.IsQuotientMap.surjective, Topology.IsCoinducing.of_comp_iff, Topology.isQuotientMap_iff, Function.Surjective.of_comp_iff, Topology.IsQuotientMap.isCoinducing
-- 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 : IsQuotientMap f
hgf : IsQuotientMap (g ∘ f)
⊢ IsQuotientMap g

Tactic:
of_comp_of_isCoinducing hgf hf.isCoinducing

Premises used: Topology.IsQuotientMap.of_comp_of_isCoinducing, Topology.IsQuotientMap.isCoinducing
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
g : Y → X
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst] g
h : LeftInverse g f
⊢ IsQuotientMap g

Tactic:
.of_comp hf hg <| h.comp_eq_id.symm ▸ IsQuotientMap.id

Premises used: Topology.IsQuotientMap.id, Eq.rec, Function.LeftInverse.comp_eq_id, Topology.IsQuotientMap.of_comp, Eq.symm
-- 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 : IsQuotientMap f
rw : coinduced g inst_1 ≤ inst_2 ↔ Continuous[inst, inst_2] (g ∘ f)
rw₁ : coinduced g inst_1 ≤ inst_2 ↔ coinduced (g ∘ f) inst ≤ inst_2
rw₂ : coinduced g (coinduced f inst) ≤ inst_2 ↔ coinduced (g ∘ f) inst ≤ inst_2
rw₃ rw₄ : coinduced (g ∘ f) inst ≤ inst_2 ↔ coinduced (g ∘ f) inst ≤ inst_2
⊢ Continuous[inst_1, inst_2] g ↔ Continuous[inst, inst_2] (g ∘ f)

Tactic:
rw [continuous_iff_coinduced_le, continuous_iff_coinduced_le, hf.eq_coinduced, coinduced_compose]

Premises used: Topology.IsCoinducing.eq_coinduced, coinduced_compose, Topology.IsQuotientMap.isCoinducing, continuous_iff_coinduced_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 : IsQuotientMap f
⊢ Continuous[inst, inst_1] f

Tactic:
hf.continuous_iff.mp continuous_id

Premises used: continuous_id, Iff.mp, Topology.IsQuotientMap.continuous_iff
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs rwa rwa₁ rwa₂ rwa₃ : IsOpen[inst] s
⊢ IsOpen[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 : IsOpenMap g
hf : IsOpenMap f
s : Set X
hs : IsOpen[inst] s
rw : IsOpen[inst_2] (g '' f '' s)
⊢ IsOpen[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 : IsOpenMap g
hf : IsOpenMap f
s : Set X
hs : IsOpen[inst] s
⊢ IsOpen[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 : IsOpenMap g
hf : IsOpenMap f
s : Set X
hs : IsOpen[inst] s
⊢ IsOpen[inst_2] (g '' f '' s)

Tactic:
exact hg _ (hf _ hs)