awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
p : ι → Prop
Y : ι → Type u_8
inst_6 : (i : ι) → TopologicalSpace (Y i)
inst_7 : DecidablePred p
j : ι
dsimp :
  Continuous[instTopologicalSpaceProd, inst_6 j]
    fun (a : ((i : { x : ι // p x }) → Y (↑i : ι)) × ((i : { x : ι // ¬p x }) → Y (↑i : ι))) ↦
    if h : p j then a.1 (Subtype.mk (p := fun (x : ι) ↦ p x) j h) else a.2 (Subtype.mk (p := fun (x : ι) ↦ ¬p x) j h)
⊢ Continuous[instTopologicalSpaceProd, inst_6 j]
    fun (a : ((i : { x : ι // p x }) → Y (↑i : ι)) × ((i : { x : ι // ¬p x }) → Y (↑i : ι))) ↦
    (Equiv.piEquivPiSubtypeProd p Y).invFun a j

Tactic:
dsimp only [Equiv.piEquivPiSubtypeProd]

Premises used: Equiv.piEquivPiSubtypeProd
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
p : ι → Prop
Y : ι → Type u_8
inst_6 : (i : ι) → TopologicalSpace (Y i)
inst_7 : DecidablePred p
j : ι
pos :
  ∀ (h : p j),
    Continuous[instTopologicalSpaceProd, inst_6 j]
      fun (a : ((i : { x : ι // p x }) → Y (↑i : ι)) × ((i : { x : ι // ¬p x }) → Y (↑i : ι))) ↦
      a.1 (Subtype.mk (p := fun (x : ι) ↦ p x) j h)
neg :
  ∀ (h : ¬p j),
    Continuous[instTopologicalSpaceProd, inst_6 j]
      fun (a : ((i : { x : ι // p x }) → Y (↑i : ι)) × ((i : { x : ι // ¬p x }) → Y (↑i : ι))) ↦
      a.2 (Subtype.mk (p := fun (x : ι) ↦ ¬p x) j h)
⊢ Continuous[instTopologicalSpaceProd, inst_6 j]
    fun (a : ((i : { x : ι // p x }) → Y (↑i : ι)) × ((i : { x : ι // ¬p x }) → Y (↑i : ι))) ↦
    if h : p j then a.1 (Subtype.mk (p := fun (x : ι) ↦ p x) j h) else a.2 (Subtype.mk (p := fun (x : ι) ↦ ¬p x) j h)

Tactic:
split_ifs
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
p : ι → Prop
Y : ι → Type u_8
inst_6 : (i : ι) → TopologicalSpace (Y i)
inst_7 : DecidablePred p
j : ι
h : p j
⊢ Continuous[instTopologicalSpaceProd, inst_6 j]
    fun (a : ((i : { x : ι // p x }) → Y (↑i : ι)) × ((i : { x : ι // ¬p x }) → Y (↑i : ι))) ↦
    a.1 (Subtype.mk (p := fun (x : ι) ↦ p x) j h)

Tactic:
(continuous_apply _).comp continuous_fst

Premises used: Continuous.comp, continuous_fst, continuous_apply
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
p : ι → Prop
Y : ι → Type u_8
inst_6 : (i : ι) → TopologicalSpace (Y i)
inst_7 : DecidablePred p
j : ι
h : ¬p j
⊢ Continuous[instTopologicalSpaceProd, inst_6 j]
    fun (a : ((i : { x : ι // p x }) → Y (↑i : ι)) × ((i : { x : ι // ¬p x }) → Y (↑i : ι))) ↦
    a.2 (Subtype.mk (p := fun (x : ι) ↦ ¬p x) j h)

Tactic:
(continuous_apply _).comp continuous_snd

Premises used: Continuous.comp, continuous_snd, continuous_apply
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
p : ι → Prop
Y : ι → Type u_8
inst_6 : (i : ι) → TopologicalSpace (Y i)
inst_7 : DecidablePred p
j : ι
h : p j
⊢ Continuous[instTopologicalSpaceProd, inst_6 j]
    fun (a : ((i : { x : ι // p x }) → Y (↑i : ι)) × ((i : { x : ι // ¬p x }) → Y (↑i : ι))) ↦
    a.1 (Subtype.mk (p := fun (x : ι) ↦ p x) j h)

Tactic:
exacts [(continuous_apply _).comp continuous_fst, (continuous_apply _).comp continuous_snd]

Premises used: Continuous.comp, continuous_snd, continuous_fst, continuous_apply
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
inst_6 : DecidableEq ι
i : ι
Y : ι → Type u_8
inst_7 : (j : ι) → TopologicalSpace (Y j)
j : ι
dsimp :
  Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y i × ((j : { j : ι // j ≠ i }) → Y (↑j : ι))) ↦
    if h : j = i then Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ Y x) a.1 ⋯
    else a.2 (Subtype.mk (p := fun (j : ι) ↦ j ≠ i) j h)
⊢ Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y i × ((j : { j : ι // j ≠ i }) → Y (↑j : ι))) ↦
    (Equiv.piSplitAt i Y).invFun a j

Tactic:
dsimp only [Equiv.piSplitAt]

Premises used: Equiv.piSplitAt
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
inst_6 : DecidableEq ι
i : ι
Y : ι → Type u_8
inst_7 : (j : ι) → TopologicalSpace (Y j)
j : ι
pos :
  ∀ (h : j = i),
    Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y i × ((j : { j : ι // j ≠ i }) → Y (↑j : ι))) ↦
      Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ Y x) a.1 ⋯
neg :
  ∀ (h : ¬j = i),
    Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y i × ((j : { j : ι // j ≠ i }) → Y (↑j : ι))) ↦
      a.2 (Subtype.mk (p := fun (j : ι) ↦ j ≠ i) j h)
⊢ Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y i × ((j : { j : ι // j ≠ i }) → Y (↑j : ι))) ↦
    if h : j = i then Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ Y x) a.1 ⋯
    else a.2 (Subtype.mk (p := fun (j : ι) ↦ j ≠ i) j h)

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
inst_6 : DecidableEq ι
i : ι
Y : ι → Type u_8
inst_7 : (j : ι) → TopologicalSpace (Y j)
j : ι
h : j = i
pos :
  Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y j × ((j_1 : { j_1 : ι // j_1 ≠ j }) → Y (↑j_1 : ι))) ↦
    Eq.rec (motive := fun (x : ι) (x_1 : j = x) ↦ Y x) a.1 ⋯
⊢ Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y i × ((j : { j : ι // j ≠ i }) → Y (↑j : ι))) ↦
    Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ Y x) a.1 ⋯

Tactic:
subst h
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
inst_6 : DecidableEq ι
Y : ι → Type u_8
inst_7 : (j : ι) → TopologicalSpace (Y j)
j : ι
__Equiv : ((j : ι) → Y j) ≃ Y j × ((j_1 : { j_1 : ι // j_1 ≠ j }) → Y (↑j_1 : ι)) := Equiv.piSplitAt j Y
⊢ Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y j × ((j_1 : { j_1 : ι // j_1 ≠ j }) → Y (↑j_1 : ι))) ↦
    Eq.rec (motive := fun (x : ι) (x_1 : j = x) ↦ Y x) a.1 ⋯

Tactic:
continuous_fst

Premises used: continuous_fst
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
inst_6 : DecidableEq ι
Y : ι → Type u_8
inst_7 : (j : ι) → TopologicalSpace (Y j)
j : ι
__Equiv : ((j : ι) → Y j) ≃ Y j × ((j_1 : { j_1 : ι // j_1 ≠ j }) → Y (↑j_1 : ι)) := Equiv.piSplitAt j Y
⊢ Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y j × ((j_1 : { j_1 : ι // j_1 ≠ j }) → Y (↑j_1 : ι))) ↦
    Eq.rec (motive := fun (x : ι) (x_1 : j = x) ↦ Y x) a.1 ⋯

Tactic:
exact continuous_fst

Premises used: continuous_fst
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
inst_6 : DecidableEq ι
i : ι
Y : ι → Type u_8
inst_7 : (j : ι) → TopologicalSpace (Y j)
j : ι
h : ¬j = i
⊢ Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y i × ((j : { j : ι // j ≠ i }) → Y (↑j : ι))) ↦
    a.2 (Subtype.mk (p := fun (j : ι) ↦ j ≠ i) j h)

Tactic:
(continuous_apply _).comp continuous_snd

Premises used: Continuous.comp, continuous_snd, continuous_apply
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
inst_6 : DecidableEq ι
i : ι
Y : ι → Type u_8
inst_7 : (j : ι) → TopologicalSpace (Y j)
j : ι
h : ¬j = i
⊢ Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y i × ((j : { j : ι // j ≠ i }) → Y (↑j : ι))) ↦
    a.2 (Subtype.mk (p := fun (j : ι) ↦ j ≠ i) j h)

Tactic:
exact (continuous_apply _).comp continuous_snd

Premises used: Continuous.comp, continuous_snd, continuous_apply
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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
hf : IsEmbedding f
x : X
⊢ f x ∈ range f

Tactic:
simp
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsEmbedding f
x : X
a :
  Eq.{u_2 + 1} (α := Y)
    (↑((hf.toHomeomorph : (a : X) → (↑(range f) : Type u_2))
          ((hf.toHomeomorph.symm : (a : (↑(range f) : Type u_2)) → X)
            (Subtype.mk (p := fun (x : Y) ↦ x ∈ range f) (f x) ⋯))) :
      Y)
    (↑((hf.toHomeomorph : (a : X) → (↑(range f) : Type u_2)) x) : Y)
⊢ Eq.{u_2 + 1} (α := (↑(range f) : Type u_2))
    ((hf.toHomeomorph : (a : X) → (↑(range f) : Type u_2))
        ((hf.toHomeomorph.symm : (a : (↑(range f) : Type u_2)) → X)
          (Subtype.mk (p := fun (x : Y) ↦ x ∈ range f) (f x) ⋯)) :
      (↑(range f) : Type u_2))
    ((hf.toHomeomorph : (a : X) → (↑(range f) : Type u_2)) x : (↑(range f) : Type u_2))

Tactic:
ext
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsEmbedding f
x : X
⊢ Eq.{u_2 + 1} (α := Y)
    (↑((hf.toHomeomorph : (a : X) → (↑(range f) : Type u_2))
          ((hf.toHomeomorph.symm : (a : (↑(range f) : Type u_2)) → X)
            (Subtype.mk (p := fun (x : Y) ↦ x ∈ range f) (f x) ⋯))) :
      Y)
    (↑((hf.toHomeomorph : (a : X) → (↑(range f) : Type u_2)) x) : Y)

Tactic:
simp
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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
hf : IsEmbedding f
s : Set X
⊢ range (ι := { x : X // x ∈ s }) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s)) = f '' s

Tactic:
simp [Set.range_comp]

Premises used: Set.range_comp
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsEmbedding f
s : Set Y
hs : s ⊆ range f
x : (↑(f ⁻¹' s) : Type u_1)
⊢ (↑((hf.homeomorphOfSubsetRange (s := s) hs : (a : (↑(f ⁻¹' s) : Type u_1)) → (↑s : Type u_2)) x) : Y) = f (↑x : X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsEmbedding f
⊢ IsEmbedding (ULift.map f)

Tactic:
.comp Homeomorph.ulift.symm.isEmbedding (.comp hf <| Homeomorph.ulift.isEmbedding)

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.comp, Homeomorph.ulift, Homeomorph.symm, ULift.map
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
⊢ IsOpenEmbedding (ULift.map f)

Tactic:
.comp Homeomorph.ulift.symm.isOpenEmbedding (.comp hf <| Homeomorph.ulift.isOpenEmbedding)

Premises used: Homeomorph.ulift, Homeomorph.symm, Homeomorph.isOpenEmbedding, ULift.map, Topology.IsOpenEmbedding.comp
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsClosedEmbedding (ULift.map f)

Tactic:
.comp Homeomorph.ulift.symm.isClosedEmbedding (.comp hf <| Homeomorph.ulift.isClosedEmbedding)

Premises used: Topology.IsClosedEmbedding.comp, Homeomorph.ulift, Homeomorph.symm, ULift.map, Homeomorph.isClosedEmbedding
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
f : X ≃ Y
hf : Continuous[inst, inst_1] (⇑f : (a : X) → Y)
rw : ∀ (s : Set X), IsClosed[inst] s → IsClosed[inst_1] ((⇑f.symm : (a : Y) → X) ⁻¹' s)
⊢ Continuous[inst_1, inst] (⇑f.symm : (a : Y) → X)

Tactic:
rw [continuous_iff_isClosed]

Premises used: continuous_iff_isClosed
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
f : X ≃ Y
hf : Continuous[inst, inst_1] (⇑f : (a : X) → Y)
C : Set X
hC : IsClosed[inst] C
⊢ IsClosed[inst_1] ((⇑f : (a : X) → Y) '' C)

Tactic:
have hC' : IsClosed (f '' C) := (hC.isCompact.image hf).isClosed
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
f : X ≃ Y
hf : Continuous[inst, inst_1] (⇑f : (a : X) → Y)
C : Set X
hC : IsClosed[inst] C
hC' : IsClosed[inst_1] ((⇑f : (a : X) → Y) '' C)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hC' : IsClosed[inst_1] ((⇑f.symm : (a : Y) → X) ⁻¹' C)), IsClosed[inst_1] ((⇑f.symm : (a : Y) → X) ⁻¹' C)
⊢ IsClosed[inst_1] ((⇑f.symm : (a : Y) → X) ⁻¹' C)

Tactic:
rwa [Equiv.image_eq_preimage_symm] at hC'

Premises used: Equiv.image_eq_preimage_symm
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
W_1 : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
W : Type u_5
inst_3 : TopologicalSpace W
f : X → Y
hf : IsHomeomorph f
rw : ContinuousOn (Equiv.ofBijective f ⋯).invFun (range f)
⊢ Continuous[inst_1, inst] (Equiv.ofBijective f ⋯).invFun

Tactic:
rw [← continuousOn_univ, ← hf.bijective.2.range_eq]

Premises used: Function.Surjective.range_eq, And.right, IsHomeomorph.bijective, continuousOn_univ
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
W_1 : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
W : Type u_5
inst_3 : TopologicalSpace W
f : X → Y
hf : IsHomeomorph f
⊢ ContinuousOn (Equiv.ofBijective f ⋯).invFun (range f)

Tactic:
hf.isOpenMap.continuousOn_range_of_leftInverse
      (Equiv.ofBijective f hf.bijective).left_inv

Premises used: IsOpenMap.continuousOn_range_of_leftInverse, IsHomeomorph.isOpenMap, Equiv.ofBijective, IsHomeomorph.bijective, Equiv.left_inv
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
W_1 : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
W : Type u_5
inst_3 : TopologicalSpace W
f : X → Y
hf : IsHomeomorph f
⊢ ContinuousOn (Equiv.ofBijective f ⋯).invFun (range f)

Tactic:
exact hf.isOpenMap.continuousOn_range_of_leftInverse
      (Equiv.ofBijective f hf.bijective).left_inv

Premises used: IsOpenMap.continuousOn_range_of_leftInverse, IsHomeomorph.isOpenMap, Equiv.ofBijective, IsHomeomorph.bijective, Equiv.left_inv
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsHomeomorph f
⊢ IsClosedMap f

Tactic:
(hf.homeomorph f).isClosedMap

Premises used: IsHomeomorph.homeomorph, Homeomorph.isClosedMap
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsHomeomorph f
⊢ IsInducing f

Tactic:
(hf.homeomorph f).isInducing

Premises used: Homeomorph.isInducing, IsHomeomorph.homeomorph
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsHomeomorph f
⊢ IsQuotientMap f

Tactic:
(hf.homeomorph f).isQuotientMap

Premises used: IsHomeomorph.homeomorph, Homeomorph.isQuotientMap
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsHomeomorph f
⊢ IsEmbedding f

Tactic:
(hf.homeomorph f).isEmbedding

Premises used: IsHomeomorph.homeomorph, Homeomorph.isEmbedding
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsHomeomorph f
⊢ IsOpenEmbedding f

Tactic:
(hf.homeomorph f).isOpenEmbedding

Premises used: IsHomeomorph.homeomorph, Homeomorph.isOpenEmbedding
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsHomeomorph f
⊢ IsClosedEmbedding f

Tactic:
(hf.homeomorph f).isClosedEmbedding

Premises used: IsHomeomorph.homeomorph, Homeomorph.isClosedEmbedding
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsHomeomorph f
⊢ IsDenseEmbedding f

Tactic:
(hf.homeomorph f).isDenseEmbedding

Premises used: IsHomeomorph.homeomorph, Homeomorph.isDenseEmbedding
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsHomeomorph f ↔ ∃ (h : X ≃ₜ Y), (⇑h : (a : X) → Y) = f

Tactic:
⟨fun hf => ⟨hf.homeomorph f, rfl⟩, fun ⟨h, h'⟩ => h' ▸ h.isHomeomorph⟩

Premises used: IsHomeomorph.homeomorph, _private.0.isHomeomorph_iff_exists_homeomorph.match_1, Eq.rec, Homeomorph.isHomeomorph, Iff.intro, Exists.intro, rfl, IsHomeomorph
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsHomeomorph f ↔
    Continuous[inst, inst_1] f ∧ ∃ (g : Y → X), LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g

Tactic:
⟨fun hf ↦ ⟨hf.continuous, ?_⟩, fun ⟨hf, g, hg⟩ ↦ ?_⟩

Premises used: _private.0.isHomeomorph_iff_exists_inverse.match_1, IsHomeomorph.continuous, And.intro, Iff.intro, IsHomeomorph
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
refine_1 : ∀ (hf : IsHomeomorph f), ∃ (g : Y → X), LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g
refine_2 :
  (Continuous[inst, inst_1] f ∧ ∃ (g : Y → X), LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g) →
    ∀ (hf : Continuous[inst, inst_1] f) (g : Y → X)
      (hg : LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g), IsHomeomorph f
⊢ IsHomeomorph f ↔
    Continuous[inst, inst_1] f ∧ ∃ (g : Y → X), LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g

Tactic:
refine ⟨fun hf ↦ ⟨hf.continuous, ?_⟩, fun ⟨hf, g, hg⟩ ↦ ?_⟩
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsHomeomorph f
h : X ≃ₜ Y := IsHomeomorph.homeomorph f hf
⊢ ∃ (g : Y → X), LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g

Tactic:
⟨h.symm, h.left_inv, h.right_inv, h.continuous_invFun⟩

Premises used: Equiv.right_inv, Homeomorph.toEquiv, Homeomorph.continuous_invFun, Homeomorph.symm, And.intro, Exists.intro, DFunLike.coe, Equiv.left_inv
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsHomeomorph f
h : X ≃ₜ Y := IsHomeomorph.homeomorph f hf
⊢ ∃ (g : Y → X), LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g

Tactic:
exact ⟨h.symm, h.left_inv, h.right_inv, h.continuous_invFun⟩
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : Continuous[inst, inst_1] f ∧ ∃ (g : Y → X), LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g
hf : Continuous[inst, inst_1] f
g : Y → X
hg : LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g
⊢ IsHomeomorph f

Tactic:
(Homeomorph.mk ⟨f, g, hg.1, hg.2.1⟩ hf hg.2.2).isHomeomorph

Premises used: Homeomorph.mk, Equiv.mk, Homeomorph.isHomeomorph, And.right, And.left
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : Continuous[inst, inst_1] f ∧ ∃ (g : Y → X), LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g
hf : Continuous[inst, inst_1] f
g : Y → X
hg : LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g
⊢ IsHomeomorph f

Tactic:
exact (Homeomorph.mk ⟨f, g, hg.1, hg.2.1⟩ hf hg.2.2).isHomeomorph

Premises used: Homeomorph.mk, Equiv.mk, Homeomorph.isHomeomorph, And.right, And.left
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ Y
rw :
  IsHomeomorph.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y) ↔
    Continuous[inst, inst_1] (⇑e : (a : X) → Y) ∧ IsOpenMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
⊢ IsHomeomorph.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y) ↔
    Continuous[inst, inst_1] (⇑e : (a : X) → Y) ∧ Continuous[inst_1, inst] (⇑e.symm : (a : Y) → X)

Tactic:
rw [e.continuous_symm_iff]

Premises used: Equiv.continuous_symm_iff
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ Y
⊢ IsHomeomorph.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y) ↔
    Continuous[inst, inst_1] (⇑e : (a : X) → Y) ∧ IsOpenMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)

Tactic:
⟨fun h ↦ ⟨h.continuous, h.isOpenMap⟩, fun ⟨hc, ho⟩ ↦ ⟨hc, ho, e.bijective⟩⟩

Premises used: _private.0.Equiv.isHomeomorph_iff.match_1, Equiv.bijective, IsHomeomorph.mk, IsHomeomorph.isOpenMap, IsHomeomorph.continuous, And.intro, Iff.intro, DFunLike.coe, IsHomeomorph
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ Y
⊢ IsHomeomorph.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y) ↔
    Continuous[inst, inst_1] (⇑e : (a : X) → Y) ∧ IsOpenMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)

Tactic:
exact ⟨fun h ↦ ⟨h.continuous, h.isOpenMap⟩, fun ⟨hc, ho⟩ ↦ ⟨hc, ho, e.bijective⟩⟩