awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
x : X
hx_1 : x ∈ s
e : OpenPartialHomeomorph X Y
hx_2 : x ∈ e.source
he : Set.EqOn f (↑e : X → Y) e.source
_x : X
hx : _x ∈ e.source
rw : (↑e : X → Y) _x ∈ e.target
⊢ f _x ∈ e.target

Tactic:
rw [he hx]
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
x : X
hx_1 : x ∈ s
e : OpenPartialHomeomorph X Y
hx_2 : x ∈ e.source
he : Set.EqOn f (↑e : X → Y) e.source
_x : X
hx : _x ∈ e.source
⊢ (↑e : X → Y) _x ∈ e.target

Tactic:
e.map_source' hx

Premises used: PartialEquiv.map_source', Set.Mem, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
x : X
hx_1 : x ∈ s
e : OpenPartialHomeomorph X Y
hx_2 : x ∈ e.source
he : Set.EqOn f (↑e : X → Y) e.source
_x : X
hx : _x ∈ e.source
⊢ (↑e : X → Y) _x ∈ e.target

Tactic:
exact e.map_source' hx

Premises used: PartialEquiv.map_source', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
x : X
hx_1 : x ∈ s
e : OpenPartialHomeomorph X Y
hx_2 : x ∈ e.source
he : Set.EqOn f (↑e : X → Y) e.source
_x : X
hx : _x ∈ e.source
rw : e.invFun ((↑e : X → Y) _x) = _x
⊢ e.invFun (f _x) = _x

Tactic:
rw [he hx]
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
x : X
hx_1 : x ∈ s
e : OpenPartialHomeomorph X Y
hx_2 : x ∈ e.source
he : Set.EqOn f (↑e : X → Y) e.source
_x : X
hx : _x ∈ e.source
⊢ e.invFun ((↑e : X → Y) _x) = _x

Tactic:
e.left_inv' hx

Premises used: OpenPartialHomeomorph.toFun', PartialEquiv.left_inv', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
x : X
hx_1 : x ∈ s
e : OpenPartialHomeomorph X Y
hx_2 : x ∈ e.source
he : Set.EqOn f (↑e : X → Y) e.source
_x : X
hx : _x ∈ e.source
⊢ e.invFun ((↑e : X → Y) _x) = _x

Tactic:
exact e.left_inv' hx

Premises used: PartialEquiv.left_inv', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
x : X
hx_1 : x ∈ s
e : OpenPartialHomeomorph X Y
hx : x ∈ e.source
he : Set.EqOn f (↑e : X → Y) e.source
_y : Y
hy : _y ∈ e.target
rw : (↑e : X → Y) (e.invFun _y) = _y
⊢ f (e.invFun _y) = _y

Tactic:
rw [he (e.map_target' hy)]

Premises used: OpenPartialHomeomorph.toPartialEquiv, PartialEquiv.map_target'
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
x : X
hx_1 : x ∈ s
e : OpenPartialHomeomorph X Y
hx : x ∈ e.source
he : Set.EqOn f (↑e : X → Y) e.source
_y : Y
hy : _y ∈ e.target
⊢ (↑e : X → Y) (e.invFun _y) = _y

Tactic:
e.right_inv' hy

Premises used: PartialEquiv.right_inv', OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
x : X
hx_1 : x ∈ s
e : OpenPartialHomeomorph X Y
hx : x ∈ e.source
he : Set.EqOn f (↑e : X → Y) e.source
_y : Y
hy : _y ∈ e.target
⊢ (↑e : X → Y) (e.invFun _y) = _y

Tactic:
exact e.right_inv' hy

Premises used: PartialEquiv.right_inv', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
x : X
hx_1 : x ∈ s
e : OpenPartialHomeomorph X Y
hx : x ∈ e.source
he : Set.EqOn f (↑e : X → Y) e.source
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)

Tactic:
exact
    ⟨{ e with
        toFun := f
        map_source' := fun _x hx ↦ by rw [he hx]; exact e.map_source' hx
        left_inv' := fun _x hx ↦ by rw [he hx]; exact e.left_inv' hx
        right_inv' := fun _y hy ↦ by rw [he (e.map_target' hy)]; exact e.right_inv' hy
        continuousOn_toFun := (continuousOn_congr he).mpr e.continuousOn_toFun },
      hx, rfl⟩
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ IsLocalHomeomorphOn (↑e : X → Y) e.source

Tactic:
fun _ hx ↦ ⟨e, hx, rfl⟩

Premises used: IsLocalHomeomorphOn, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s t : Set X
hf : IsLocalHomeomorphOn f t
hst : s ⊆ t
⊢ IsLocalHomeomorphOn f s

Tactic:
fun x hx ↦ hf x (hst hx)

Premises used: IsLocalHomeomorphOn
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
hgf : IsLocalHomeomorphOn (g ∘ f) s
hg : IsLocalHomeomorphOn g (f '' s)
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
obtain :
  ∀ (g : OpenPartialHomeomorph Y Z) (hxg : f x ∈ g.source) (hgf : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s)
    (hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)),
    ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source

Tactic:
obtain ⟨g, hxg, rfl⟩ := hg (f x) ⟨x, hx, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s
hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)
obtain :
  ∀ (gf : OpenPartialHomeomorph X Z) (hgf : x ∈ gf.source) (he : (↑g : Y → Z) ∘ f = (↑gf : X → Z)),
    ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source

Tactic:
obtain ⟨gf, hgf, he⟩ := hgf x hx
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf_1 : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s
hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : (↑g : Y → Z) ∘ f = (↑gf : X → Z)
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source

Tactic:
⟨(gf.restr <| f ⁻¹' g.source).trans g.symm, ⟨⟨hgf, mem_interior_iff_mem_nhds.mpr
    ((cont x hx).preimage_mem_nhds <| g.open_source.mem_nhds hxg)⟩, he ▸ g.map_source hxg⟩,
    fun y hy ↦ ?_⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, OpenPartialHomeomorph.open_source, ContinuousAt.preimage_mem_nhds, OpenPartialHomeomorph.trans, Eq.rec, OpenPartialHomeomorph.map_source, Set.preimage, And.intro, IsOpen.mem_nhds, Exists.intro, PartialEquiv.source, OpenPartialHomeomorph.toPartialEquiv, OpenPartialHomeomorph.restr, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf_1 : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s
hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : (↑g : Y → Z) ∘ f = (↑gf : X → Z)
refine :
  ∀ (y : X) (hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source),
    f y = (↑((gf.restr (f ⁻¹' g.source)).trans g.symm) : X → Y) y
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source

Tactic:
refine ⟨(gf.restr <| f ⁻¹' g.source).trans g.symm, ⟨⟨hgf, mem_interior_iff_mem_nhds.mpr
    ((cont x hx).preimage_mem_nhds <| g.open_source.mem_nhds hxg)⟩, he ▸ g.map_source hxg⟩,
    fun y hy ↦ ?_⟩
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf_1 : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s
hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : (↑g : Y → Z) ∘ f = (↑gf : X → Z)
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
change : f y = (↑g.symm : Z → Y) ((↑gf : X → Z) y)
⊢ f y = (↑((gf.restr (f ⁻¹' g.source)).trans g.symm) : X → Y) y

Tactic:
change f y = g.symm (gf y)

Premises used: OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf_1 : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s
hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : (↑g : Y → Z) ∘ f = (↑gf : X → Z)
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
⊢ f y ∈ g.source

Tactic:
apply interior_subset hy.1.2

Premises used: interior_subset, And.right, And.left
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf_1 : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s
hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : (↑g : Y → Z) ∘ f = (↑gf : X → Z)
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
⊢ f y ∈ g.source

Tactic:
have : f y ∈ g.source := by apply interior_subset hy.1.2
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf_1 : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s
hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : (↑g : Y → Z) ∘ f = (↑gf : X → Z)
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
this : f y ∈ g.source
⊢ ((↑g : Y → Z) ∘ f) y ∈ g.target

Tactic:
apply g.map_source this

Premises used: OpenPartialHomeomorph.map_source
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf_1 : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s
hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : (↑g : Y → Z) ∘ f = (↑gf : X → Z)
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
this : f y ∈ g.source
rw : f y = (↑g.symm : Z → Y) (((↑g : Y → Z) ∘ f) y)
rw₁ : (↑g : Y → Z) (f y) = ((↑g : Y → Z) ∘ f) y
rw₂ rw₃ : (↑g : Y → Z) (f y) = (↑g : Y → Z) (f y)
⊢ f y = (↑g.symm : Z → Y) ((↑gf : X → Z) y)

Tactic:
rw [← he, g.eq_symm_apply this (by apply g.map_source this), Function.comp_apply]

Premises used: OpenPartialHomeomorph.eq_symm_apply, Function.comp_apply
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
hgf : IsLocalHomeomorphOn (g ∘ f) s
hf : IsLocalHomeomorphOn f s
x : X
hx : x ∈ s
obtain :
  ∀ (f : OpenPartialHomeomorph X Y) (hxf : x ∈ f.source) (hgf : IsLocalHomeomorphOn (g ∘ (↑f : X → Y)) s)
    (hf : IsLocalHomeomorphOn (↑f : X → Y) s),
    ∃ (e : OpenPartialHomeomorph Y Z), (↑f : X → Y) x ∈ e.source ∧ Set.EqOn g (↑e : Y → Z) e.source
⊢ ∃ (e : OpenPartialHomeomorph Y Z), f x ∈ e.source ∧ Set.EqOn g (↑e : Y → Z) e.source

Tactic:
obtain ⟨f, hxf, rfl⟩ := hf x hx

Premises used: rfl
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf : IsLocalHomeomorphOn (g ∘ (↑f : X → Y)) s
hf : IsLocalHomeomorphOn (↑f : X → Y) s
obtain :
  ∀ (gf : OpenPartialHomeomorph X Z) (hgf : x ∈ gf.source) (he : g ∘ (↑f : X → Y) = (↑gf : X → Z)),
    ∃ (e : OpenPartialHomeomorph Y Z), (↑f : X → Y) x ∈ e.source ∧ Set.EqOn g (↑e : Y → Z) e.source
⊢ ∃ (e : OpenPartialHomeomorph Y Z), (↑f : X → Y) x ∈ e.source ∧ Set.EqOn g (↑e : Y → Z) e.source

Tactic:
obtain ⟨gf, hgf, he⟩ := hgf x hx
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf_1 : IsLocalHomeomorphOn (g ∘ (↑f : X → Y)) s
hf : IsLocalHomeomorphOn (↑f : X → Y) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ (↑f : X → Y) = (↑gf : X → Z)
⊢ ∃ (e : OpenPartialHomeomorph Y Z), (↑f : X → Y) x ∈ e.source ∧ Set.EqOn g (↑e : Y → Z) e.source

Tactic:
⟨f.symm.trans gf, ⟨f.map_source hxf, ?_⟩, fun y hy ↦ ?_⟩

Premises used: OpenPartialHomeomorph.trans, OpenPartialHomeomorph.map_source, And.intro, Exists.intro, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf_1 : IsLocalHomeomorphOn (g ∘ (↑f : X → Y)) s
hf : IsLocalHomeomorphOn (↑f : X → Y) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ (↑f : X → Y) = (↑gf : X → Z)
refine_1 : (↑f : X → Y) x ∈ (↑f.symm.symm.symm : Y → X) ⁻¹' gf.source
refine_2 : ∀ (y : Y) (hy : y ∈ (f.symm.trans gf).source), g y = (↑(f.symm.trans gf) : Y → Z) y
⊢ ∃ (e : OpenPartialHomeomorph Y Z), (↑f : X → Y) x ∈ e.source ∧ Set.EqOn g (↑e : Y → Z) e.source

Tactic:
refine ⟨f.symm.trans gf, ⟨f.map_source hxf, ?_⟩, fun y hy ↦ ?_⟩
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf_1 : IsLocalHomeomorphOn (g ∘ (↑f : X → Y)) s
hf : IsLocalHomeomorphOn (↑f : X → Y) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ (↑f : X → Y) = (↑gf : X → Z)
⊢ (↑f : X → Y) x ∈ (↑f.symm.symm.symm : Y → X) ⁻¹' gf.source

Tactic:
apply (f.left_inv hxf).symm ▸ hgf
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf_1 : IsLocalHomeomorphOn (g ∘ (↑f : X → Y)) s
hf : IsLocalHomeomorphOn (↑f : X → Y) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ (↑f : X → Y) = (↑gf : X → Z)
y : Y
hy : y ∈ (f.symm.trans gf).source
refine_2 : g y = (↑gf : X → Z) ((↑f.symm : Y → X) y)
⊢ g y = (↑(f.symm.trans gf) : Y → Z) y

Tactic:
change g y = gf (f.symm y)

Premises used: OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf_1 : IsLocalHomeomorphOn (g ∘ (↑f : X → Y)) s
hf : IsLocalHomeomorphOn (↑f : X → Y) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ (↑f : X → Y) = (↑gf : X → Z)
y : Y
hy : y ∈ (f.symm.trans gf).source
refine_2 : g y = (g ∘ (↑f : X → Y)) ((↑f.symm : Y → X) y)
refine_2₁ : g y = g ((↑f : X → Y) ((↑f.symm : Y → X) y))
refine_2₂ refine_2₃ : g y = g y
⊢ g y = (↑gf : X → Z) ((↑f.symm : Y → X) y)

Tactic:
rw [← he, Function.comp_apply, f.right_inv hy.1]

Premises used: And.left, Function.comp_apply, OpenPartialHomeomorph.right_inv
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsLocalHomeomorphOn f s
x : X
hx : x ∈ s
⊢ Filter.map f (𝓝 x) = 𝓝 (f x)

Tactic:
let ⟨e, hx, he⟩ := hf x hx
  he.symm ▸ e.map_nhds_eq hx

Premises used: Filter.map, _private.0.IsLocalHomeomorphOn.map_nhds_eq.match_1, nhds, Eq.rec, OpenPartialHomeomorph.map_nhds_eq, Eq.symm, Eq
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsLocalHomeomorphOn f s
x : X
hx : x ∈ s
⊢ ContinuousAt f x

Tactic:
(hf.map_nhds_eq hx).le

Premises used: ContinuousAt, Eq.le, Filter.Tendsto, IsLocalHomeomorphOn.map_nhds_eq
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsLocalHomeomorphOn f s
⊢ ContinuousOn f s

Tactic:
continuousOn_of_forall_continuousAt fun _x ↦ hf.continuousAt

Premises used: continuousOn_of_forall_continuousAt, IsLocalHomeomorphOn.continuousAt
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
hg : IsLocalHomeomorphOn g t
hf : IsLocalHomeomorphOn f s
h : Set.MapsTo f s t
x : X
hx : x ∈ s
obtain :
  ∀ (eg : OpenPartialHomeomorph Y Z) (hxg : f x ∈ eg.source) (hg : IsLocalHomeomorphOn (↑eg : Y → Z) t),
    ∃ (e : OpenPartialHomeomorph X Z), x ∈ e.source ∧ (↑eg : Y → Z) ∘ f = (↑e : X → Z)
⊢ ∃ (e : OpenPartialHomeomorph X Z), x ∈ e.source ∧ g ∘ f = (↑e : X → Z)

Tactic:
obtain ⟨eg, hxg, rfl⟩ := hg (f x) (h hx)

Premises used: rfl
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
s : Set X
t : Set Y
hf : IsLocalHomeomorphOn f s
h : Set.MapsTo f s t
x : X
hx : x ∈ s
eg : OpenPartialHomeomorph Y Z
hxg : f x ∈ eg.source
hg : IsLocalHomeomorphOn (↑eg : Y → Z) t
obtain :
  ∀ (ef : OpenPartialHomeomorph X Y) (hxf : x ∈ ef.source) (hf : IsLocalHomeomorphOn (↑ef : X → Y) s)
    (h : Set.MapsTo (↑ef : X → Y) s t) (hxg : (↑ef : X → Y) x ∈ eg.source),
    ∃ (e : OpenPartialHomeomorph X Z), x ∈ e.source ∧ (↑eg : Y → Z) ∘ (↑ef : X → Y) = (↑e : X → Z)
⊢ ∃ (e : OpenPartialHomeomorph X Z), x ∈ e.source ∧ (↑eg : Y → Z) ∘ f = (↑e : X → Z)

Tactic:
obtain ⟨ef, hxf, rfl⟩ := hf x hx

Premises used: rfl
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
s : Set X
t : Set Y
x : X
hx : x ∈ s
eg : OpenPartialHomeomorph Y Z
hg : IsLocalHomeomorphOn (↑eg : Y → Z) t
ef : OpenPartialHomeomorph X Y
hxf : x ∈ ef.source
hf : IsLocalHomeomorphOn (↑ef : X → Y) s
h : Set.MapsTo (↑ef : X → Y) s t
hxg : (↑ef : X → Y) x ∈ eg.source
⊢ ∃ (e : OpenPartialHomeomorph X Z), x ∈ e.source ∧ (↑eg : Y → Z) ∘ (↑ef : X → Y) = (↑e : X → Z)

Tactic:
⟨ef.trans eg, ⟨hxf, hxg⟩, rfl⟩

Premises used: OpenPartialHomeomorph.trans, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
s : Set X
t : Set Y
x : X
hx : x ∈ s
eg : OpenPartialHomeomorph Y Z
hg : IsLocalHomeomorphOn (↑eg : Y → Z) t
ef : OpenPartialHomeomorph X Y
hxf : x ∈ ef.source
hf : IsLocalHomeomorphOn (↑ef : X → Y) s
h : Set.MapsTo (↑ef : X → Y) s t
hxg : (↑ef : X → Y) x ∈ eg.source
⊢ ∃ (e : OpenPartialHomeomorph X Z), x ∈ e.source ∧ (↑eg : Y → Z) ∘ (↑ef : X → Y) = (↑e : X → Z)

Tactic:
exact ⟨ef.trans eg, ⟨hxf, hxg⟩, rfl⟩
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X ≃ₜ Y
⊢ IsLocalHomeomorph.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)

Tactic:
fun _ ↦ ⟨f.toOpenPartialHomeomorph, trivial, rfl⟩

Premises used: trivial, And.intro, Exists.intro, IsLocalHomeomorph, rfl, Homeomorph.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsLocalHomeomorph f ↔ IsLocalHomeomorphOn f Set.univ

Tactic:
⟨fun h x _ ↦ h x, fun h x ↦ h x trivial⟩

Premises used: trivial, Iff.intro
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsLocalHomeomorph f
⊢ IsLocalHomeomorphOn f s

Tactic:
fun x _ ↦ hf x

Premises used: IsLocalHomeomorphOn
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
simp_rw : IsLocalHomeomorphOn f Set.univ ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
simp_rw₁ :
  (∀ (x : X),
      Membership.mem (γ := Set X) Set.univ x → ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)) ↔
    ∀ (x : X), ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
⊢ IsLocalHomeomorph f ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)

Tactic:
simp_rw [isLocalHomeomorph_iff_isLocalHomeomorphOn_univ,
    isLocalHomeomorphOn_iff_isOpenEmbedding_restrict, imp_iff_right (Set.mem_univ _)]

Premises used: isLocalHomeomorph_iff_isLocalHomeomorphOn_univ, imp_iff_right, isLocalHomeomorphOn_iff_isOpenEmbedding_restrict, Set.mem_univ
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
⊢ IsLocalHomeomorph f

Tactic:
isLocalHomeomorph_iff_isOpenEmbedding_restrict.mpr fun _ ↦
    ⟨_, Filter.univ_mem, hf.comp (Homeomorph.Set.univ X).isOpenEmbedding⟩

Premises used: Homeomorph.Set.univ, Iff.mpr, Set.univ, isLocalHomeomorph_iff_isOpenEmbedding_restrict, And.intro, Exists.intro, Homeomorph.isOpenEmbedding, Filter.univ_mem, Topology.IsOpenEmbedding.comp