awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X ≃ₜ Y
g : Y ≃ₜ Z
z : Z
⊢ Eq.{u_1 + 1} (α := X) (((f.trans g).symm : (a : Z) → X) z : X)
    ((f.symm : (a : Y) → X) ((g.symm : (a : Z) → Y) z : Y) : X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
a : X ≃ Y
b : Continuous[inst, inst_1] a.toFun
c : Continuous[inst_1, inst] a.invFun
⊢ Eq (α := (a : Y) → X) (⇑{ toEquiv := a, continuous_toFun := b, continuous_invFun := c : X ≃ₜ Y }.symm : (a : Y) → X)
    (⇑a.symm : (a : Y) → X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Eq (α := X ≃ₜ X) (Homeomorph.symm (Homeomorph.refl X)) (Homeomorph.refl X)

Tactic:
rfl

Premises used: Homeomorph.symm, Homeomorph.refl, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ Continuous[inst, inst_1] (⇑h : (a : X) → Y)

Tactic:
h.continuous_toFun

Premises used: Homeomorph.continuous_toFun
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ Continuous[inst_1, inst] (⇑h.symm : (a : Y) → X)

Tactic:
h.continuous_invFun

Premises used: Homeomorph.continuous_invFun
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
y : Y
⊢ (h : (a : X) → Y) ((h.symm : (a : Y) → X) y : X) = y

Tactic:
h.toEquiv.apply_symm_apply y

Premises used: Equiv.apply_symm_apply, Homeomorph.toEquiv
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ (h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y) = x

Tactic:
h.toEquiv.symm_apply_apply x

Premises used: Equiv.symm_apply_apply, Homeomorph.toEquiv
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
x : X
y : Y
⊢ (h.symm : (a : Y) → X) y = x ↔ y = (h : (a : X) → Y) x

Tactic:
Equiv.symm_apply_eq _

Premises used: Equiv.symm_apply_eq
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
H : ∀ (x : X), Eq (α := X) ((h.trans h.symm : (a : X) → X) x : X) ((Homeomorph.refl X : (a : X) → X) x : X)
⊢ h.trans h.symm = Homeomorph.refl X

Tactic:
ext
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ Eq (α := X) ((h.trans h.symm : (a : X) → X) x : X) ((Homeomorph.refl X : (a : X) → X) x : X)

Tactic:
apply symm_apply_apply

Premises used: Homeomorph.symm_apply_apply
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
H : ∀ (x : Y), Eq (α := Y) ((h.symm.trans h : (a : Y) → Y) x : Y) ((Homeomorph.refl Y : (a : Y) → Y) x : Y)
⊢ h.symm.trans h = Homeomorph.refl Y

Tactic:
ext
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
x : Y
⊢ Eq (α := Y) ((h.symm.trans h : (a : Y) → Y) x : Y) ((Homeomorph.refl Y : (a : Y) → Y) x : Y)

Tactic:
apply apply_symm_apply

Premises used: Homeomorph.apply_symm_apply
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ (1 : (a : X) → X) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X ≃ₜ X
x : X
⊢ Eq (α := X) ((f⁻¹ : (a : X) → X) x : X) ((f.symm : (a : X) → X) x : X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
inst : TopologicalSpace X
f g : X ≃ₜ X
x : X
⊢ Eq (α := X) ((f * g : (a : X) → X) x : X) ((f : (a : X) → X) ((g : (a : X) → X) x : X) : X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := X) (β := Y) (⇑h : (a : X) → Y)

Tactic:
h.toEquiv.bijective

Premises used: Equiv.bijective, Homeomorph.toEquiv
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := X) (β := Y) (⇑h : (a : X) → Y)

Tactic:
h.toEquiv.injective

Premises used: Homeomorph.toEquiv, Equiv.injective
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := X) (β := Y) (⇑h : (a : X) → Y)

Tactic:
h.toEquiv.surjective

Premises used: Homeomorph.toEquiv, Equiv.surjective
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
f : X ≃ₜ Y
g : Y → X
hg : Function.RightInverse g (⇑f : (a : X) → Y)
this : g = (⇑f.symm : (a : Y) → X)
⊢ Function.LeftInverse f.invFun f.toFun

Tactic:
f.left_inv

Premises used: Homeomorph.toEquiv, Equiv.left_inv
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
f : X ≃ₜ Y
g : Y → X
hg : Function.RightInverse g (⇑f : (a : X) → Y)
this : g = (⇑f.symm : (a : Y) → X)
⊢ Function.LeftInverse g (⇑f : (a : X) → Y)

Tactic:
convert! f.left_inv

Premises used: Homeomorph.toEquiv, Equiv.left_inv
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
f : X ≃ₜ Y
g : Y → X
hg : Function.RightInverse g (⇑f : (a : X) → Y)
this : g = (⇑f.symm : (a : Y) → X)
⊢ Function.RightInverse f.invFun f.toFun

Tactic:
f.right_inv

Premises used: Equiv.right_inv, Homeomorph.toEquiv
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
f : X ≃ₜ Y
g : Y → X
hg : Function.RightInverse g (⇑f : (a : X) → Y)
this : g = (⇑f.symm : (a : Y) → X)
⊢ Function.RightInverse g (⇑f : (a : X) → Y)

Tactic:
convert! f.right_inv using 1

Premises used: Equiv.right_inv, Homeomorph.toEquiv
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
f : X ≃ₜ Y
g : Y → X
hg : Function.RightInverse g (⇑f : (a : X) → Y)
this : g = (⇑f.symm : (a : Y) → X)
⊢ Continuous[inst_1, inst] (⇑f.symm : (a : Y) → X)

Tactic:
f.symm.continuous

Premises used: Homeomorph.continuous, Homeomorph.symm
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
f : X ≃ₜ Y
g : Y → X
hg : Function.RightInverse g (⇑f : (a : X) → Y)
this : g = (⇑f.symm : (a : Y) → X)
⊢ Continuous[inst_1, inst] g

Tactic:
convert! f.symm.continuous

Premises used: Homeomorph.continuous, Homeomorph.symm
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ Eq.{u_1 + 1} (α := X → X)
    (Function.comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := Y) (⇑h.symm : (a : Y) → X) (⇑h : (a : X) → Y)) id

Tactic:
funext h.symm_apply_apply

Premises used: funext, Homeomorph.symm_apply_apply
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ Eq.{u_2 + 1} (α := Y → Y)
    (Function.comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := X) (⇑h : (a : X) → Y) (⇑h.symm : (a : Y) → X)) id

Tactic:
funext h.apply_symm_apply

Premises used: funext, Homeomorph.apply_symm_apply
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ Eq.{u_2 + 1} (α := Set Y) (range.{u_2, u_1 + 1} (ι := X) (⇑h : (a : X) → Y)) univ

Tactic:
simp
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ Eq (α := (s : Set Y) → Set X) (image (⇑h.symm : (a : Y) → X)) (preimage (⇑h : (a : X) → Y))

Tactic:
funext h.symm.toEquiv.image_eq_preimage_symm

Premises used: Homeomorph.toEquiv, funext, Equiv.image_eq_preimage_symm, Homeomorph.symm
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ Eq (α := (s : Set X) → Set Y) (preimage (⇑h.symm : (a : Y) → X)) (image (⇑h : (a : X) → Y))

Tactic:
(funext h.toEquiv.image_eq_preimage_symm).symm

Premises used: Homeomorph.toEquiv, funext, Equiv.image_eq_preimage_symm, Eq.symm
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set Y
⊢ image.{u_1, u_2} (α := X) (⇑h : (a : X) → Y) ((⇑h : (a : X) → Y) ⁻¹' s) = s

Tactic:
h.toEquiv.image_preimage s

Premises used: Homeomorph.toEquiv, Equiv.image_preimage
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ preimage.{u_1, u_2} (β := Y) (⇑h : (a : X) → Y) ((⇑h : (a : X) → Y) '' s) = s

Tactic:
h.toEquiv.preimage_image s

Premises used: Homeomorph.toEquiv, Equiv.preimage_image
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ Eq.{u_2 + 1} (α := Set Y) ((⇑h : (a : X) → Y) '' s) ((⇑h.symm : (a : Y) → X) ⁻¹' s)

Tactic:
h.toEquiv.image_eq_preimage_symm s

Premises used: Homeomorph.toEquiv, Equiv.image_eq_preimage_symm
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ Eq.{u_2 + 1} (α := Set Y) ((⇑h : (a : X) → Y) '' sᶜ) ((⇑h : (a : X) → Y) '' s)ᶜ

Tactic:
h.toEquiv.image_compl s

Premises used: Set.Mem, Homeomorph.toEquiv, setOf, Equiv.image_compl
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ IsInducing.{u_1, u_1} (X := X) (Y := X)
    (Function.comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := Y) (⇑h.symm : (a : Y) → X) (⇑h : (a : X) → Y))

Tactic:
simp only [symm_comp_self, IsInducing.id]

Premises used: Topology.IsInducing.id, Homeomorph.symm_comp_self
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ TopologicalSpace.induced (⇑h : (a : X) → Y) inst_1 = inst

Tactic:
h.isInducing.1.symm

Premises used: Homeomorph.isInducing, Eq.symm, Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ IsQuotientMap.{u_2, u_2} (X := Y) (Y := Y)
    (Function.comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := X) (⇑h : (a : X) → Y) (⇑h.symm : (a : Y) → X))

Tactic:
simp only [self_comp_symm, IsQuotientMap.id]

Premises used: Topology.IsQuotientMap.id, Homeomorph.self_comp_symm
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ TopologicalSpace.coinduced (⇑h : (a : X) → Y) inst = inst_1

Tactic:
h.isQuotientMap.isCoinducing.eq_coinduced.symm

Premises used: Topology.IsCoinducing.eq_coinduced, Topology.IsQuotientMap.isCoinducing, Eq.symm, Homeomorph.isQuotientMap
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ IsEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑h : (a : X) → Y)

Tactic:
⟨h.isInducing, h.injective⟩

Premises used: Homeomorph.isInducing, Homeomorph.injective, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : DiscreteTopology X
h : X ≃ₜ Y
⊢ DiscreteTopology Y

Tactic:
h.symm.isEmbedding.discreteTopology

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.discreteTopology, Homeomorph.symm
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ DiscreteTopology X ↔ DiscreteTopology Y

Tactic:
⟨fun _ ↦ h.discreteTopology, fun _ ↦ h.symm.discreteTopology⟩

Premises used: Homeomorph.symm, Iff.intro, Homeomorph.discreteTopology
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : IndiscreteTopology X
h : X ≃ₜ Y
⊢ IndiscreteTopology Y

Tactic:
h.symm.isInducing.indiscreteTopology

Premises used: Homeomorph.isInducing, Topology.IsInducing.indiscreteTopology, Homeomorph.symm
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ IndiscreteTopology X ↔ IndiscreteTopology Y

Tactic:
⟨fun _ ↦ h.indiscreteTopology, fun _ ↦ h.symm.indiscreteTopology⟩

Premises used: Homeomorph.symm, Iff.intro, Homeomorph.indiscreteTopology
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NontrivialTopology X
h : X ≃ₜ Y
⊢ NontrivialTopology Y

Tactic:
h.isInducing.nontrivialTopology

Premises used: Homeomorph.isInducing, Topology.IsInducing.nontrivialTopology
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ NontrivialTopology X ↔ NontrivialTopology Y

Tactic:
⟨fun _ ↦ h.nontrivialTopology, fun _ ↦ h.symm.nontrivialTopology⟩

Premises used: Homeomorph.nontrivialTopology, Homeomorph.symm, Iff.intro
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set Y
⊢ IsOpen[inst] ((⇑h : (a : X) → Y) ⁻¹' s) ↔ IsOpen[inst_1] s

Tactic:
h.isQuotientMap.isOpen_preimage

Premises used: Topology.IsCoinducing.isOpen_preimage, Topology.IsQuotientMap.isCoinducing, Homeomorph.isQuotientMap
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
rw : IsOpen[inst_1] ((⇑h.symm : (a : Y) → X) ⁻¹' s) ↔ IsOpen[inst] s
rw₁ rw₂ : IsOpen[inst] s ↔ IsOpen[inst] s
⊢ IsOpen[inst_1] ((⇑h : (a : X) → Y) '' s) ↔ IsOpen[inst] s

Tactic:
rw [← preimage_symm, isOpen_preimage]

Premises used: Homeomorph.preimage_symm, Homeomorph.isOpen_preimage
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ IsOpenMap.{u_1, u_2} (X := X) (Y := Y) (⇑h : (a : X) → Y)

Tactic:
fun _ => h.isOpen_image.2

Premises used: Iff.mpr, IsOpenMap, Homeomorph.isOpen_image
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ IsOpenQuotientMap.{u_1, u_2} (X := X) (Y := Y) (⇑h : (a : X) → Y)

Tactic:
⟨h.surjective, h.continuous, h.isOpenMap⟩

Premises used: Homeomorph.continuous, IsOpenQuotientMap.mk, Homeomorph.surjective, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set Y
⊢ IsClosed[inst] ((⇑h : (a : X) → Y) ⁻¹' s) ↔ IsClosed[inst_1] s

Tactic:
simp only [← isOpen_compl_iff, ← preimage_compl, isOpen_preimage]

Premises used: Set.preimage_compl, isOpen_compl_iff, Homeomorph.isOpen_preimage
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
rw : IsClosed[inst_1] ((⇑h.symm : (a : Y) → X) ⁻¹' s) ↔ IsClosed[inst] s
rw₁ rw₂ : IsClosed[inst] s ↔ IsClosed[inst] s
⊢ IsClosed[inst_1] ((⇑h : (a : X) → Y) '' s) ↔ IsClosed[inst] s

Tactic:
rw [← preimage_symm, isClosed_preimage]

Premises used: Homeomorph.isClosed_preimage, Homeomorph.preimage_symm
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ IsClosedMap.{u_1, u_2} (X := X) (Y := Y) (⇑h : (a : X) → Y)

Tactic:
fun _ => h.isClosed_image.2

Premises used: Iff.mpr, Homeomorph.isClosed_image, IsClosedMap
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ IsOpenEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑h : (a : X) → Y)

Tactic:
.of_isEmbedding_isOpenMap h.isEmbedding h.isOpenMap

Premises used: Homeomorph.isEmbedding, Topology.IsOpenEmbedding.of_isEmbedding_isOpenMap, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑h : (a : X) → Y)

Tactic:
.of_isEmbedding_isClosedMap h.isEmbedding h.isClosedMap

Premises used: Homeomorph.isEmbedding, Topology.IsClosedEmbedding.of_isEmbedding_isClosedMap, Homeomorph.isClosedMap
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set Y
⊢ Eq.{u_1 + 1} (α := Set X) ((⇑h : (a : X) → Y) ⁻¹' closure[inst_1] s) (closure[inst] ((⇑h : (a : X) → Y) ⁻¹' s))

Tactic:
h.isOpenMap.preimage_closure_eq_closure_preimage h.continuous _

Premises used: Homeomorph.continuous, IsOpenMap.preimage_closure_eq_closure_preimage, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
rw :
  Eq.{u_2 + 1} (α := Set Y) ((⇑h.symm : (a : Y) → X) ⁻¹' closure[inst] s)
    (closure[inst_1] ((⇑h.symm : (a : Y) → X) ⁻¹' s))
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := Set Y) (closure[inst_1] ((⇑h.symm : (a : Y) → X) ⁻¹' s))
    (closure[inst_1] ((⇑h.symm : (a : Y) → X) ⁻¹' s))
⊢ Eq.{u_2 + 1} (α := Set Y) ((⇑h : (a : X) → Y) '' closure[inst] s) (closure[inst_1] ((⇑h : (a : X) → Y) '' s))

Tactic:
rw [← preimage_symm, preimage_closure]

Premises used: Homeomorph.preimage_symm, Homeomorph.preimage_closure
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set Y
⊢ Eq.{u_1 + 1} (α := Set X) ((⇑h : (a : X) → Y) ⁻¹' interior s) (interior ((⇑h : (a : X) → Y) ⁻¹' s))

Tactic:
h.isOpenMap.preimage_interior_eq_interior_preimage h.continuous _

Premises used: Homeomorph.continuous, IsOpenMap.preimage_interior_eq_interior_preimage, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
rw : Eq.{u_2 + 1} (α := Set Y) ((⇑h.symm : (a : Y) → X) ⁻¹' interior s) (interior ((⇑h.symm : (a : Y) → X) ⁻¹' s))
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := Set Y) (interior ((⇑h.symm : (a : Y) → X) ⁻¹' s)) (interior ((⇑h.symm : (a : Y) → X) ⁻¹' s))
⊢ Eq.{u_2 + 1} (α := Set Y) ((⇑h : (a : X) → Y) '' interior s) (interior ((⇑h : (a : X) → Y) '' s))

Tactic:
rw [← preimage_symm, preimage_interior]

Premises used: Homeomorph.preimage_symm, Homeomorph.preimage_interior
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set Y
⊢ Eq.{u_1 + 1} (α := Set X) ((⇑h : (a : X) → Y) ⁻¹' frontier s) (frontier ((⇑h : (a : X) → Y) ⁻¹' s))

Tactic:
h.isOpenMap.preimage_frontier_eq_frontier_preimage h.continuous _

Premises used: Homeomorph.continuous, IsOpenMap.preimage_frontier_eq_frontier_preimage, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
rw : Eq.{u_2 + 1} (α := Set Y) ((⇑h.symm : (a : Y) → X) ⁻¹' frontier s) (frontier ((⇑h.symm : (a : Y) → X) ⁻¹' s))
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := Set Y) (frontier ((⇑h.symm : (a : Y) → X) ⁻¹' s)) (frontier ((⇑h.symm : (a : Y) → X) ⁻¹' s))
⊢ Eq.{u_2 + 1} (α := Set Y) ((⇑h : (a : X) → Y) '' frontier s) (frontier ((⇑h : (a : X) → Y) '' s))

Tactic:
rw [← preimage_symm, preimage_frontier]

Premises used: Homeomorph.preimage_symm, Homeomorph.preimage_frontier
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
⊢ Continuous[inst_2, inst_1] ((⇑h : (a : X) → Y) ∘ f) ↔ Continuous[inst_2, inst] f

Tactic:
h.isInducing.continuous_iff.symm

Premises used: Homeomorph.isInducing, Topology.IsInducing.continuous_iff, Iff.symm
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
⊢ Continuous[inst, inst_2] (f ∘ (⇑h : (a : X) → Y)) ↔ Continuous[inst_1, inst_2] f

Tactic:
h.isQuotientMap.continuous_iff.symm

Premises used: Topology.IsQuotientMap.continuous_iff, Iff.symm, Homeomorph.isQuotientMap
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
z : Z
⊢ ContinuousAt.{u_4, u_2} (Y := Y) ((⇑h : (a : X) → Y) ∘ f) z ↔ ContinuousAt f z

Tactic:
h.isInducing.continuousAt_iff.symm

Premises used: Homeomorph.isInducing, Topology.IsInducing.continuousAt_iff, Iff.symm
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
x : X
⊢ Membership.mem (γ := Filter Y) (𝓝 ((h : (a : X) → Y) x) : Filter Y) (range.{u_2, u_1 + 1} (ι := X) (⇑h : (a : X) → Y))

Tactic:
simp
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
⊢ IsOpenMap.{u_4, u_2} (Y := Y) ((⇑h : (a : X) → Y) ∘ f) ↔ IsOpenMap f

Tactic:
⟨?_, fun hf => h.isOpenMap.comp hf⟩

Premises used: IsOpenMap.comp, Iff.intro, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
refine : IsOpenMap.{u_4, u_2} (Y := Y) ((⇑h : (a : X) → Y) ∘ f) → IsOpenMap f
⊢ IsOpenMap.{u_4, u_2} (Y := Y) ((⇑h : (a : X) → Y) ∘ f) ↔ IsOpenMap f

Tactic:
refine ⟨?_, fun hf => h.isOpenMap.comp hf⟩