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
h : X ≃ₜ Y
f : Z → X
hf : IsOpenMap.{u_4, u_2} (Y := Y) ((⇑h : (a : X) → Y) ∘ f)
rw :
  IsOpenMap.{u_4, u_1} (Y := X)
    (Function.comp.{u_4 + 1, u_2 + 1, u_1 + 1} (β := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) ∘ f))
⊢ IsOpenMap f

Tactic:
rw [← Function.id_comp f, ← h.symm_comp_self, Function.comp_assoc]

Premises used: Homeomorph.symm_comp_self, Function.comp_assoc, Function.id_comp
-- 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
hf : IsOpenMap.{u_4, u_2} (Y := Y) ((⇑h : (a : X) → Y) ∘ f)
⊢ IsOpenMap.{u_4, u_1} (Y := X)
    (Function.comp.{u_4 + 1, u_2 + 1, u_1 + 1} (β := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) ∘ f))

Tactic:
h.symm.isOpenMap.comp hf

Premises used: IsOpenMap.comp, Homeomorph.symm, 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
hf : IsOpenMap.{u_4, u_2} (Y := Y) ((⇑h : (a : X) → Y) ∘ f)
⊢ IsOpenMap.{u_4, u_1} (Y := X)
    (Function.comp.{u_4 + 1, u_2 + 1, u_1 + 1} (β := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) ∘ f))

Tactic:
exact h.symm.isOpenMap.comp hf

Premises used: IsOpenMap.comp, Homeomorph.symm, 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 : Y → Z
⊢ IsOpenMap.{u_1, u_4} (X := X) (f ∘ (⇑h : (a : X) → Y)) ↔ IsOpenMap f

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

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 : Y → Z
refine : IsOpenMap.{u_1, u_4} (X := X) (f ∘ (⇑h : (a : X) → Y)) → IsOpenMap f
⊢ IsOpenMap.{u_1, u_4} (X := X) (f ∘ (⇑h : (a : X) → Y)) ↔ IsOpenMap f

Tactic:
refine ⟨?_, fun hf => hf.comp h.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 : Y → Z
hf : IsOpenMap.{u_1, u_4} (X := X) (f ∘ (⇑h : (a : X) → Y))
rw :
  IsOpenMap.{u_2, u_4} (X := Y)
    (Function.comp.{u_2 + 1, u_1 + 1, u_4 + 1} (β := X) (f ∘ (⇑h : (a : X) → Y)) (⇑h.symm : (a : Y) → X))
⊢ IsOpenMap f

Tactic:
rw [← Function.comp_id f, ← h.self_comp_symm, ← Function.comp_assoc]

Premises used: Function.comp_id, Homeomorph.self_comp_symm, Function.comp_assoc
-- 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
hf : IsOpenMap.{u_1, u_4} (X := X) (f ∘ (⇑h : (a : X) → Y))
⊢ IsOpenMap.{u_2, u_4} (X := Y)
    (Function.comp.{u_2 + 1, u_1 + 1, u_4 + 1} (β := X) (f ∘ (⇑h : (a : X) → Y)) (⇑h.symm : (a : Y) → X))

Tactic:
hf.comp h.symm.isOpenMap

Premises used: IsOpenMap.comp, Homeomorph.symm, 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 : Y → Z
hf : IsOpenMap.{u_1, u_4} (X := X) (f ∘ (⇑h : (a : X) → Y))
⊢ IsOpenMap.{u_2, u_4} (X := Y)
    (Function.comp.{u_2 + 1, u_1 + 1, u_4 + 1} (β := X) (f ∘ (⇑h : (a : X) → Y)) (⇑h.symm : (a : Y) → X))

Tactic:
exact hf.comp h.symm.isOpenMap

Premises used: IsOpenMap.comp, Homeomorph.symm, 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
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
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
x : X
rw : 𝓝 ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) = 𝓝 x
rw₁ rw₂ : 𝓝 x = 𝓝 x
⊢ map.{u_2, u_1} (α := Y) ((⇑h.symm : (a : Y) → X) : (a : Y) → X) (𝓝 ((h : (a : X) → Y) x) : Filter Y) = 𝓝 x

Tactic:
rw [h.symm.map_nhds_eq, h.symm_apply_apply]

Premises used: Homeomorph.map_nhds_eq, Homeomorph.symm, 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
x : X
⊢ 𝓝 x = comap.{u_1, u_2} (β := Y) ((⇑h : (a : X) → Y) : (a : X) → Y) (𝓝 ((h : (a : X) → Y) x) : Filter Y)

Tactic:
h.isInducing.nhds_eq_comap x

Premises used: Homeomorph.isInducing, Topology.IsInducing.nhds_eq_comap
-- 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
rw :
  Eq.{u_1 + 1} (α := Filter X) (comap (⇑h : (a : X) → Y) (𝓝 y))
    (comap.{u_1, u_2} (β := Y) ((⇑h : (a : X) → Y) : (a : X) → Y)
      (𝓝 ((h : (a : X) → Y) ((h.symm : (a : Y) → X) y : X)) : Filter Y))
rw₁ rw₂ : Eq.{u_1 + 1} (α := Filter X) (comap (⇑h : (a : X) → Y) (𝓝 y)) (comap (⇑h : (a : X) → Y) (𝓝 y))
⊢ Eq.{u_1 + 1} (α := Filter X) (comap (⇑h : (a : X) → Y) (𝓝 y) : Filter X) (𝓝 ((h.symm : (a : Y) → X) y) : Filter X)

Tactic:
rw [h.nhds_eq_comap, h.apply_symm_apply]

Premises used: Homeomorph.nhds_eq_comap, 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
p : X → Prop
q : Y → Prop
f : X ≃ₜ Y
hs : IsClopen.{u_1} (X := X) {x : X | p x}
ht : IsClopen.{u_2} (X := Y) {y : Y | q y}
⊢ IsClosed[inst] {x : X | p x ↔ q ((f : (a : X) → Y) x)}

Tactic:
simpa [iff_def] using (isClosed_imp hs.2 (f.isClosed_preimage.2 ht.1)).inter
    (isClosed_imp (f.isOpen_preimage.2 ht.2) hs.1)

Premises used: Homeomorph.isClosed_preimage, Iff.mpr, iff_def, isClosed_imp, And.right, And.left, IsClosed.inter, Homeomorph.isOpen_preimage
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
W : Type u_3
Z_1 : Type u_4
Z : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
e : X ≃ Y
he : ∀ (s : Set Y), IsOpen[inst] ((⇑e : (a : X) → Y) ⁻¹' s) ↔ IsOpen[inst_1] s
s : Set X
⊢ IsOpen[inst] s → IsOpen[inst_1] (e.invFun ⁻¹' s)

Tactic:
simpa using (he (e.symm ⁻¹' s)).1

Premises used: Set.preimage, Iff.mp, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ Y
he : ∀ (s : Set Y), IsOpen[inst] ((⇑e : (a : X) → Y) ⁻¹' s) ↔ IsOpen[inst_1] s
⊢ Eq (α := (a : X) → Y) (⇑(e.toHomeomorph he) : (a : X) → Y) (⇑e : (a : X) → Y)

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
e : X ≃ Y
he : ∀ (s : Set Y), IsOpen[inst] ((⇑e : (a : X) → Y) ⁻¹' s) ↔ IsOpen[inst_1] s
x : X
⊢ Eq.{u_2 + 1} (α := Y) ((e.toHomeomorph he : (a : X) → Y) x : Y) ((e : (a : X) → Y) x : Y)

Tactic:
rfl

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

Tactic:
rfl

Premises used: Homeomorph.refl, Equiv.toHomeomorph, rfl
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
W : Type u_3
Z_1 : Type u_4
Z : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
e : X ≃ Y
he : ∀ (s : Set Y), IsOpen[inst] ((⇑e : (a : X) → Y) ⁻¹' s) ↔ IsOpen[inst_1] s
s : Set X
⊢ IsOpen[inst_1] ((⇑e.symm : (a : Y) → X) ⁻¹' s) ↔
    IsOpen[inst] (preimage.{u_1, u_2} (β := Y) (⇑e : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' s))

Tactic:
(he _).symm

Premises used: Iff.symm
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
W : Type u_3
Z_1 : Type u_4
Z : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
e : X ≃ Y
he : ∀ (s : Set Y), IsOpen[inst] ((⇑e : (a : X) → Y) ⁻¹' s) ↔ IsOpen[inst_1] s
s : Set X
h : s = preimage.{u_1, u_2} (β := Y) (⇑e : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' s)
⊢ IsOpen[inst_1] ((⇑e.symm : (a : Y) → X) ⁻¹' s) ↔ IsOpen[inst] s

Tactic:
convert! (he _).symm

Premises used: Iff.symm
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
W : Type u_3
Z_1 : Type u_4
Z : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
e : X ≃ Y
he : ∀ (s : Set Y), IsOpen[inst] ((⇑e : (a : X) → Y) ⁻¹' s) ↔ IsOpen[inst_1] s
s : Set X
⊢ s = preimage.{u_1, u_2} (β := Y) (⇑e : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' s)

Tactic:
simp
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ Y
he : ∀ (s : Set Y), IsOpen[inst] ((⇑e : (a : X) → Y) ⁻¹' s) ↔ IsOpen[inst_1] s
⊢ (e.toHomeomorph he).symm = e.symm.toHomeomorph ⋯

Tactic:
rfl

Premises used: Homeomorph.symm, Equiv.toHomeomorph, rfl
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
e : X ≃ Y
f : Y ≃ Z
he : ∀ (s : Set Y), IsOpen[inst] ((⇑e : (a : X) → Y) ⁻¹' s) ↔ IsOpen[inst_1] s
hf : ∀ (s : Set Z), IsOpen[inst_1] ((⇑f : (a : Y) → Z) ⁻¹' s) ↔ IsOpen[inst_2] s
⊢ (e.trans f).toHomeomorph ⋯ = (e.toHomeomorph he).trans (f.toHomeomorph hf)

Tactic:
rfl

Premises used: Homeomorph.trans, Equiv.toHomeomorph, rfl
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
W : Type u_3
Z_1 : Type u_4
Z : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X ≃ Y
hf : IsInducing.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)
⊢ Continuous[inst_1, inst_1] ((⇑f : (a : X) → Y) ∘ f.invFun)

Tactic:
simpa using continuous_id

Premises used: continuous_id
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X ≃ Y
hf : IsInducing.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)
⊢ Eq (α := (a : X) → Y) (⇑(f.toHomeomorphOfIsInducing hf) : (a : X) → Y) (⇑f : (a : X) → Y)

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
f : X ≃ Y
hf : IsInducing.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)
⊢ Eq (α := (a : Y) → X) (⇑(f.toHomeomorphOfIsInducing hf).symm : (a : Y) → X) (⇑f.symm : (a : 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
e : X ≃ Y
h₁ : Continuous[inst, inst_1] (⇑e : (a : X) → Y)
h₂ : IsOpenMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
⊢ Eq (α := (a : X) → Y) (⇑(e.toHomeomorphOfContinuousOpen h₁ h₂) : (a : X) → Y) (⇑e : (a : X) → Y)

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
e : X ≃ Y
h₁ : Continuous[inst, inst_1] (⇑e : (a : X) → Y)
h₂ : IsOpenMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
⊢ Eq (α := (a : Y) → X) (⇑(e.toHomeomorphOfContinuousOpen h₁ h₂).symm : (a : Y) → X) (⇑e.symm : (a : 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
e : X ≃ Y
h₁ : Continuous[inst, inst_1] (⇑e : (a : X) → Y)
h₂ : IsClosedMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
⊢ Eq (α := (a : X) → Y) (⇑(e.toHomeomorphOfContinuousClosed h₁ h₂) : (a : X) → Y) (⇑e : (a : X) → Y)

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
e : X ≃ Y
h₁ : Continuous[inst, inst_1] (⇑e : (a : X) → Y)
h₂ : IsClosedMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
⊢ Eq (α := (a : Y) → X) (⇑(e.toHomeomorphOfContinuousClosed h₁ h₂).symm : (a : Y) → X) (⇑e.symm : (a : Y) → X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
W : Type u_3
Z_1 : Type u_4
Z : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : DiscreteTopology X
inst_4 : DiscreteTopology Y
e : X ≃ Y
⊢ ∀ (s : Set Y), IsOpen[inst] ((⇑e : (a : X) → Y) ⁻¹' s) ↔ IsOpen[inst_1] s

Tactic:
simp
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
F : Type u_5
α : Type u_6
β : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : EquivLike F α β
h : HomeomorphClass F α β
f : F
⊢ Eq (α := (a : α) → β) (⇑(↑f : α ≃ₜ β) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
F : Type u_5
α : Type u_6
β : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : EquivLike F α β
inst_3 : HomeomorphClass F α β
⊢ Function.Injective (α := F) (β := α ≃ₜ β) toHomeomorph

Tactic:
fun _ _ e ↦ DFunLike.ext _ _ fun a ↦ congr_arg (fun e : α ≃ₜ β ↦ e.toFun a) e

Premises used: Homeomorph.toEquiv, DFunLike.ext, Equiv.toFun, congr_arg, Function.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
⊢ IsHomeomorph.{u_1, u_2} (X := X) (Y := Y) (⇑h : (a : X) → Y)

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

Premises used: Homeomorph.continuous, IsHomeomorph.mk, Homeomorph.bijective, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsHomeomorph f
⊢ Function.Injective f

Tactic:
hf.bijective.injective

Premises used: Function.Bijective.injective, IsHomeomorph.bijective
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsHomeomorph f
⊢ Function.Surjective f

Tactic:
hf.bijective.surjective

Premises used: Function.Bijective.surjective, IsHomeomorph.bijective
-- Module: Mathlib.Topology.Homeomorph.Defs
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsHomeomorph.{u_1, u_1} (X := X) id

Tactic:
⟨continuous_id, .id, Function.bijective_id⟩

Premises used: Function.bijective_id, IsHomeomorph.mk, continuous_id, IsOpenMap.id
-- 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
hg : IsHomeomorph g
hf : IsHomeomorph f
⊢ IsHomeomorph (g ∘ f)

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

Premises used: IsOpenMap.comp, IsHomeomorph.mk, Continuous.comp, IsHomeomorph.isOpenMap, IsHomeomorph.continuous, IsHomeomorph.bijective, Function.Bijective.comp
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology Y
h : X ≃ₜ Y
⊢ SecondCountableTopology X

Tactic:
h.isInducing.secondCountableTopology

Premises used: Homeomorph.isInducing, Topology.IsInducing.secondCountableTopology
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : BaireSpace X
f : X ≃ₜ Y
⊢ BaireSpace Y

Tactic:
f.isOpenQuotientMap.baireSpace

Premises used: IsOpenQuotientMap.baireSpace, Homeomorph.isOpenQuotientMap
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
⊢ IsCompact.{u_2} (X := Y) ((⇑h : (a : X) → Y) '' s) ↔ IsCompact s

Tactic:
h.isEmbedding.isCompact_iff.symm

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.isCompact_iff, Iff.symm
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
rw : IsCompact.{u_1} (X := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsCompact s
⊢ IsCompact.{u_1} (X := X) ((⇑h : (a : X) → Y) ⁻¹' s) ↔ IsCompact s

Tactic:
rw [← image_symm]

Premises used: Homeomorph.image_symm
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsCompact.{u_1} (X := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsCompact s

Tactic:
h.symm.isCompact_image

Premises used: Homeomorph.symm, Homeomorph.isCompact_image
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsCompact.{u_1} (X := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsCompact s

Tactic:
exact h.symm.isCompact_image

Premises used: Homeomorph.symm, Homeomorph.isCompact_image
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
⊢ IsSigmaCompact.{u_2} (X := Y) ((⇑h : (a : X) → Y) '' s) ↔ IsSigmaCompact s

Tactic:
h.isEmbedding.isSigmaCompact_iff.symm

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.isSigmaCompact_iff, Iff.symm
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
rw : IsSigmaCompact.{u_1} (X := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsSigmaCompact s
⊢ IsSigmaCompact.{u_1} (X := X) ((⇑h : (a : X) → Y) ⁻¹' s) ↔ IsSigmaCompact s

Tactic:
rw [← image_symm]

Premises used: Homeomorph.image_symm
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsSigmaCompact.{u_1} (X := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsSigmaCompact s

Tactic:
h.symm.isSigmaCompact_image

Premises used: Homeomorph.isSigmaCompact_image, Homeomorph.symm
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsSigmaCompact.{u_1} (X := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsSigmaCompact s

Tactic:
exact h.symm.isSigmaCompact_image

Premises used: Homeomorph.isSigmaCompact_image, Homeomorph.symm
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
hs : IsPreconnected.{u_2} (α := Y) ((⇑h : (a : X) → Y) '' s)
⊢ IsPreconnected s

Tactic:
simpa only [image_symm, preimage_image]
    using hs.image _ h.symm.continuous.continuousOn

Premises used: Continuous.continuousOn, Homeomorph.continuous, IsPreconnected.image, Homeomorph.image_symm, Homeomorph.symm, Homeomorph.preimage_image
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
rw : IsPreconnected.{u_1} (α := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsPreconnected s
rw₁ rw₂ : IsPreconnected s ↔ IsPreconnected s
⊢ IsPreconnected.{u_1} (α := X) ((⇑h : (a : X) → Y) ⁻¹' s) ↔ IsPreconnected s

Tactic:
rw [← image_symm, isPreconnected_image]

Premises used: Homeomorph.image_symm, Homeomorph.isPreconnected_image
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
⊢ IsConnected.{u_2} (α := Y) ((⇑h : (a : X) → Y) '' s) ↔ IsConnected s

Tactic:
image_nonempty.and h.isPreconnected_image

Premises used: Set.image_nonempty, IsConnected, Homeomorph.isPreconnected_image, Iff.and
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
rw : IsConnected.{u_1} (α := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsConnected s
rw₁ rw₂ : IsConnected s ↔ IsConnected s
⊢ IsConnected.{u_1} (α := X) ((⇑h : (a : X) → Y) ⁻¹' s) ↔ IsConnected s

Tactic:
rw [← image_symm, isConnected_image]

Premises used: Homeomorph.image_symm, Homeomorph.isConnected_image
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
⊢ Eq.{u_2 + 1} (α := Set Y) ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
    (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)

Tactic:
(h.continuous.image_connectedComponentIn_subset hx).antisymm ?_

Premises used: Continuous.image_connectedComponentIn_subset, Homeomorph.continuous, HasSubset.Subset.antisymm
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
refine :
  Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
    ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
⊢ Eq.{u_2 + 1} (α := Set Y) ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
    (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)

Tactic:
refine (h.continuous.image_connectedComponentIn_subset hx).antisymm ?_

Premises used: Continuous.image_connectedComponentIn_subset, Homeomorph.continuous, HasSubset.Subset.antisymm
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
⊢ Subset.{u_1} (α := Set X)
    (image.{u_2, u_1} (α := Y) ((⇑h.symm : (a : Y) → X) : (a : Y) → X)
        (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y) :
      Set X)
    (connectedComponentIn (image.{u_2, u_1} (α := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) '' s))
        ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
      Set X)

Tactic:
have := h.symm.continuous.image_connectedComponentIn_subset (mem_image_of_mem h hx)
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ comap (⇑h : (a : X) → Y) (cocompact Y) = cocompact X

Tactic:
(comap_cocompact_le h.continuous).antisymm <|
    (hasBasis_cocompact.le_basis_iff (hasBasis_cocompact.comap h)).2 fun K hK =>
      ⟨h ⁻¹' K, h.isCompact_preimage.2 hK, Subset.rfl⟩

Premises used: Iff.mpr, Homeomorph.continuous, Filter.comap_cocompact_le, LE.le.antisymm, Homeomorph.isCompact_preimage, Filter.HasBasis.le_basis_iff, Filter.HasBasis.comap, Set.Subset.rfl, Set.preimage, And.intro, Exists.intro, Filter.hasBasis_cocompact, DFunLike.coe
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
rw : map.{u_1, u_2} (α := X) (⇑h : (a : X) → Y) (comap (⇑h : (a : X) → Y) (cocompact Y)) = cocompact Y
rw₁ rw₂ : cocompact Y = cocompact Y
⊢ map (⇑h : (a : X) → Y) (cocompact X) = cocompact Y

Tactic:
rw [← h.comap_cocompact, map_comap_of_surjective h.surjective]

Premises used: Homeomorph.comap_cocompact, Filter.map_comap_of_surjective, Homeomorph.surjective
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ IsDenseEmbedding.{u_1, u_2} (α := X) (β := Y) (⇑h : (a : X) → Y)

Tactic:
{ h.isEmbedding with dense := h.surjective.denseRange }

Premises used: Homeomorph.isEmbedding, IsDenseEmbedding.mk, IsDenseInducing.mk, Function.Surjective.denseRange, Topology.IsEmbedding.injective, Topology.IsEmbedding.toIsInducing, Homeomorph.surjective