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
s : Set X
f : X → Y
h : IsLocalHomeomorphOn f s
x : X
hx : x ∈ s
refine_1 :
  ∀ (e : OpenPartialHomeomorph X Y) (hxe : x ∈ e.source) (h : IsLocalHomeomorphOn (↑e : X → Y) s),
    ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) (↑e : X → Y))
⊢ ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)

Tactic:
obtain ⟨e, hxe, rfl⟩ := h x hx

Premises used: rfl
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
x : X
hx : x ∈ s
e : OpenPartialHomeomorph X Y
hxe : x ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
⊢ ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) (↑e : X → Y))

Tactic:
⟨e.source, e.open_source.mem_nhds hxe, e.isOpenEmbedding_restrict⟩

Premises used: OpenPartialHomeomorph.open_source, OpenPartialHomeomorph.isOpenEmbedding_restrict, And.intro, IsOpen.mem_nhds, Exists.intro, PartialEquiv.source, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
x : X
hx : x ∈ s
e : OpenPartialHomeomorph X Y
hxe : x ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
⊢ ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) (↑e : X → Y))

Tactic:
exact ⟨e.source, e.open_source.mem_nhds hxe, e.isOpenEmbedding_restrict⟩
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
refine_2 :
  ∀ (U : Set X) (hU : U ∈ 𝓝 x) (emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)),
    ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)

Tactic:
obtain ⟨U, hU, emb⟩ := h x hx
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
⊢ IsOpenEmbedding ((interior U).restrict (π := fun (a : X) ↦ Y) f)

Tactic:
emb.comp ⟨.inclusion interior_subset, ?_⟩

Premises used: Topology.IsEmbedding.inclusion, interior_subset, Set.restrict, Topology.IsOpenEmbedding.mk, Topology.IsOpenEmbedding.comp
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
refine :
  IsOpen[instTopologicalSpaceSubtype]
    (Set.range (ι := (↑(interior U) : Type u_1)) (Set.inclusion (s := interior U) (t := U) ⋯))
⊢ IsOpenEmbedding ((interior U).restrict (π := fun (a : X) ↦ Y) f)

Tactic:
refine emb.comp ⟨.inclusion interior_subset, ?_⟩

Premises used: Topology.IsEmbedding.inclusion, interior_subset, Topology.IsOpenEmbedding.mk, Topology.IsOpenEmbedding.comp
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
rw : IsOpen[instTopologicalSpaceSubtype] {x : (↑U : Type u_1) | (↑x : X) ∈ interior U}
⊢ IsOpen[instTopologicalSpaceSubtype]
    (Set.range (ι := (↑(interior U) : Type u_1)) (Set.inclusion (s := interior U) (t := U) ⋯))

Tactic:
rw [Set.range_inclusion]

Premises used: Set.range_inclusion
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
⊢ IsOpen[instTopologicalSpaceSubtype] {x : (↑U : Type u_1) | (↑x : X) ∈ interior U}

Tactic:
isOpen_induced isOpen_interior

Premises used: isOpen_interior, isOpen_induced, Set.preimage
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
⊢ IsOpen[instTopologicalSpaceSubtype] {x : (↑U : Type u_1) | (↑x : X) ∈ interior U}

Tactic:
exact isOpen_induced isOpen_interior

Premises used: isOpen_interior, isOpen_induced
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
⊢ IsOpenEmbedding ((interior U).restrict (π := fun (a : X) ↦ Y) f)

Tactic:
have : IsOpenEmbedding ((interior U).restrict f) := by
      refine emb.comp ⟨.inclusion interior_subset, ?_⟩
      rw [Set.range_inclusion]; exact isOpen_induced isOpen_interior
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
this : IsOpenEmbedding ((interior U).restrict (π := fun (a : X) ↦ Y) f)
⊢ Continuous[instTopologicalSpaceSubtype, inst_1] ((interior U).restrict (π := fun (a : X) ↦ Y) f)

Tactic:
obtain ⟨cont, inj, openMap⟩ := isOpenEmbedding_iff_continuous_injective_isOpenMap.mp this

Premises used: Topology.isOpenEmbedding_iff_continuous_injective_isOpenMap, Iff.mp
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
this : IsOpenEmbedding ((interior U).restrict (π := fun (a : X) ↦ Y) f)
cont : Continuous[instTopologicalSpaceSubtype, inst_1] ((interior U).restrict (π := fun (a : X) ↦ Y) f)
⊢ Function.Injective ((interior U).restrict (π := fun (a : X) ↦ Y) f)

Tactic:
obtain ⟨cont, inj, openMap⟩ := isOpenEmbedding_iff_continuous_injective_isOpenMap.mp this

Premises used: Topology.isOpenEmbedding_iff_continuous_injective_isOpenMap, Iff.mp
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
this : IsOpenEmbedding ((interior U).restrict (π := fun (a : X) ↦ Y) f)
cont : Continuous[instTopologicalSpaceSubtype, inst_1] ((interior U).restrict (π := fun (a : X) ↦ Y) f)
inj : Function.Injective ((interior U).restrict (π := fun (a : X) ↦ Y) f)
⊢ IsOpenMap ((interior U).restrict (π := fun (a : X) ↦ Y) f)

Tactic:
obtain ⟨cont, inj, openMap⟩ := isOpenEmbedding_iff_continuous_injective_isOpenMap.mp this

Premises used: Topology.isOpenEmbedding_iff_continuous_injective_isOpenMap, Iff.mp
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
this : IsOpenEmbedding ((interior U).restrict (π := fun (a : X) ↦ Y) f)
cont : Continuous[instTopologicalSpaceSubtype, inst_1] ((interior U).restrict (π := fun (a : X) ↦ Y) f)
inj : Function.Injective ((interior U).restrict (π := fun (a : X) ↦ Y) f)
openMap : IsOpenMap ((interior U).restrict (π := fun (a : X) ↦ Y) f)
⊢ Nonempty X

Tactic:
haveI : Nonempty X := ⟨x⟩
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
this_1 : IsOpenEmbedding ((interior U).restrict (π := fun (a : X) ↦ Y) f)
cont : Continuous[instTopologicalSpaceSubtype, inst_1] ((interior U).restrict (π := fun (a : X) ↦ Y) f)
inj : Function.Injective ((interior U).restrict (π := fun (a : X) ↦ Y) f)
openMap : IsOpenMap ((interior U).restrict (π := fun (a : X) ↦ Y) f)
this : Nonempty X
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)

Tactic:
⟨OpenPartialHomeomorph.ofContinuousOpenRestrict
      (Set.injOn_iff_injective.mpr inj).toPartialEquiv
      (continuousOn_iff_continuous_restrict.mpr cont) openMap isOpen_interior,
      mem_interior_iff_mem_nhds.mpr hU, rfl⟩

Premises used: Iff.mpr, Set.InjOn.toPartialEquiv, mem_interior_iff_mem_nhds, isOpen_interior, Set.injOn_iff_injective, continuousOn_iff_continuous_restrict, And.intro, Exists.intro, OpenPartialHomeomorph.ofContinuousOpenRestrict, rfl
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
this_1 : IsOpenEmbedding ((interior U).restrict (π := fun (a : X) ↦ Y) f)
cont : Continuous[instTopologicalSpaceSubtype, inst_1] ((interior U).restrict (π := fun (a : X) ↦ Y) f)
inj : Function.Injective ((interior U).restrict (π := fun (a : X) ↦ Y) f)
openMap : IsOpenMap ((interior U).restrict (π := fun (a : X) ↦ Y) f)
this : Nonempty X
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)

Tactic:
exact ⟨OpenPartialHomeomorph.ofContinuousOpenRestrict
      (Set.injOn_iff_injective.mpr inj).toPartialEquiv
      (continuousOn_iff_continuous_restrict.mpr cont) openMap isOpen_interior,
      mem_interior_iff_mem_nhds.mpr hU, 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 : Set X
h : IsLocalHomeomorphOn f s
inst_2 : DiscreteTopology.{u_2} (↑(f '' s) : Type u_2)
x : (↑s : Type u_1)
obtain :
  ∀ (e : OpenPartialHomeomorph X Y) (hx : (↑x : X) ∈ e.source) (h : IsLocalHomeomorphOn (↑e : X → Y) s)
    [DiscreteTopology.{u_2} (↑((↑e : X → Y) '' s) : Type u_2)], IsOpen[instTopologicalSpaceSubtype] {x}
⊢ IsOpen[instTopologicalSpaceSubtype] {x}

Tactic:
obtain ⟨e, hx, rfl⟩ := h x x.2

Premises used: Subtype.val, rfl, Subtype.property
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
x : (↑s : Type u_1)
e : OpenPartialHomeomorph X Y
hx : (↑x : X) ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
inst_2 : DiscreteTopology.{u_2} (↑((↑e : X → Y) '' s) : Type u_2)
have :
  ∀ (U : Set Y) (hU : IsOpen[inst_1] U)
    (eq :
      Eq (α := Set { x : Y // x ∈ (↑e : X → Y) '' s }) (Subtype.val (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ⁻¹' U)
        {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) (↑x : X)) ⋯}),
    IsOpen[instTopologicalSpaceSubtype] {x}
⊢ IsOpen[instTopologicalSpaceSubtype] {x}

Tactic:
have ⟨U, hU, eq⟩ := isOpen_discrete {(⟨_, _, x.2, rfl⟩ : e '' s)}
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
x : (↑s : Type u_1)
e : OpenPartialHomeomorph X Y
hx : (↑x : X) ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
inst_2 : DiscreteTopology.{u_2} (↑((↑e : X → Y) '' s) : Type u_2)
U : Set Y
hU : IsOpen[inst_1] U
eq :
  Eq (α := Set { x : Y // x ∈ (↑e : X → Y) '' s }) (Subtype.val (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ⁻¹' U)
    {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) (↑x : X)) ⋯}
⊢ IsOpen[instTopologicalSpaceSubtype] {x}

Tactic:
⟨e.source ∩ e ⁻¹' U, e.continuousOn_toFun.isOpen_inter_preimage e.open_source hU,
      subset_antisymm (fun x' mem ↦ Subtype.ext <| e.injOn mem.1 hx ?_) ?_⟩

Premises used: OpenPartialHomeomorph.open_source, ContinuousOn.isOpen_inter_preimage, subset_antisymm, OpenPartialHomeomorph.toFun', Inter.inter, Set.preimage, And.intro, OpenPartialHomeomorph.injOn, Exists.intro, PartialEquiv.source, OpenPartialHomeomorph.continuousOn_toFun, IsOpen, OpenPartialHomeomorph.toPartialEquiv, Subtype.ext
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
x : (↑s : Type u_1)
e : OpenPartialHomeomorph X Y
hx : (↑x : X) ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
inst_2 : DiscreteTopology.{u_2} (↑((↑e : X → Y) '' s) : Type u_2)
U : Set Y
hU : IsOpen[inst_1] U
eq :
  Eq (α := Set { x : Y // x ∈ (↑e : X → Y) '' s }) (Subtype.val (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ⁻¹' U)
    {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) (↑x : X)) ⋯}
refine_1 :
  ∀ (x' : { x : X // x ∈ s })
    (mem :
      Membership.mem (γ := Set { x : X // x ∈ s })
        (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' (e.source ∩ (↑e : X → Y) ⁻¹' U)) x'),
    (↑e : X → Y) (↑x' : X) = (↑e : X → Y) (↑x : X)
refine_2 :
  Subset (α := Set { x : X // x ∈ s }) {x} (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' (e.source ∩ (↑e : X → Y) ⁻¹' U))
⊢ IsOpen[instTopologicalSpaceSubtype] {x}

Tactic:
refine ⟨e.source ∩ e ⁻¹' U, e.continuousOn_toFun.isOpen_inter_preimage e.open_source hU,
      subset_antisymm (fun x' mem ↦ Subtype.ext <| e.injOn mem.1 hx ?_) ?_⟩
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
x : (↑s : Type u_1)
e : OpenPartialHomeomorph X Y
hx : (↑x : X) ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
inst_2 : DiscreteTopology.{u_2} (↑((↑e : X → Y) '' s) : Type u_2)
U : Set Y
hU : IsOpen[inst_1] U
eq :
  Eq (α := Set { x : Y // x ∈ (↑e : X → Y) '' s }) (Subtype.val (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ⁻¹' U)
    {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) (↑x : X)) ⋯}
x' : { x : X // x ∈ s }
mem :
  Membership.mem (γ := Set { x : X // x ∈ s })
    (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' (e.source ∩ (↑e : X → Y) ⁻¹' U)) x'
⊢ (↑e : X → Y) (↑x' : X) = (↑e : X → Y) (↑x : X)

Tactic:
simpa using Set.subset_singleton_iff.1 eq.subset ⟨_, x', x'.2, rfl⟩ mem.2

Premises used: Set.subset_singleton_iff, Subtype.mk, Eq.subset, And.right, And.intro, Exists.intro, Iff.mp, Subtype.val, rfl, Subtype.property
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
e : OpenPartialHomeomorph X Y
h : IsLocalHomeomorphOn (↑e : X → Y) s
inst_2 : DiscreteTopology.{u_2} (↑((↑e : X → Y) '' s) : Type u_2)
U : Set Y
hU : IsOpen[inst_1] U
x : { x : X // x ∈ s }
hx : (↑x : X) ∈ e.source
eq :
  Eq (α := Set { x : Y // x ∈ (↑e : X → Y) '' s }) (Subtype.val (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ⁻¹' U)
    {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) (↑x : X)) ⋯}
⊢ Membership.mem (γ := Set { x : X // x ∈ s })
    (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' (e.source ∩ (↑e : X → Y) ⁻¹' U)) x

Tactic:
⟨hx, eq.superset rfl⟩

Premises used: Set.Mem, setOf, Set.inter, Set.preimage, And.intro, Eq.superset, rfl
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
e : OpenPartialHomeomorph X Y
h : IsLocalHomeomorphOn (↑e : X → Y) s
inst_2 : DiscreteTopology.{u_2} (↑((↑e : X → Y) '' s) : Type u_2)
U : Set Y
hU : IsOpen[inst_1] U
x : { x : X // x ∈ s }
hx : (↑x : X) ∈ e.source
eq :
  Eq (α := Set { x : Y // x ∈ (↑e : X → Y) '' s }) (Subtype.val (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ⁻¹' U)
    {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) (↑x : X)) ⋯}
⊢ Membership.mem (γ := Set { x : X // x ∈ s })
    (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' (e.source ∩ (↑e : X → Y) ⁻¹' U)) x

Tactic:
exact ⟨hx, eq.superset 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 : Set X
h : IsLocalHomeomorphOn f s
hs : IsDiscrete (f '' s)
⊢ IsDiscrete s

Tactic:
have := hs.1; ⟨discreteTopology_of_image h⟩

Premises used: IsDiscrete.to_subtype, IsDiscrete.mk, IsLocalHomeomorphOn.discreteTopology_of_image
-- 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 : IsLocalHomeomorphOn f s
hs : IsOpen[inst] s
⊢ DiscreteTopology.{u_2} (↑(f '' s) : Type u_2) ↔ DiscreteTopology.{u_1} (↑s : Type u_1)

Tactic:
⟨fun _ ↦ h.discreteTopology_of_image, ?_⟩

Premises used: Iff.intro, IsLocalHomeomorphOn.discreteTopology_of_image
-- 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 : IsLocalHomeomorphOn f s
hs : IsOpen[inst] s
refine : DiscreteTopology.{u_1} (↑s : Type u_1) → DiscreteTopology.{u_2} (↑(f '' s) : Type u_2)
⊢ DiscreteTopology.{u_2} (↑(f '' s) : Type u_2) ↔ DiscreteTopology.{u_1} (↑s : Type u_1)

Tactic:
refine ⟨fun _ ↦ h.discreteTopology_of_image, ?_⟩
-- 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 : IsLocalHomeomorphOn f s
hs : IsOpen[inst] s
simp_rw :
  (∀ (a : (↑s : Type u_1)), IsOpen[instTopologicalSpaceSubtype] {a}) →
    ∀ (a : (↑(f '' s) : Type u_2)), IsOpen[instTopologicalSpaceSubtype] {a}
⊢ DiscreteTopology.{u_1} (↑s : Type u_1) → DiscreteTopology.{u_2} (↑(f '' s) : Type u_2)

Tactic:
simp_rw [discreteTopology_iff_isOpen_singleton]

Premises used: discreteTopology_iff_isOpen_singleton
-- 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 : IsLocalHomeomorphOn f s
hs : IsOpen[inst] s
hX : ∀ (a : (↑s : Type u_1)), IsOpen[instTopologicalSpaceSubtype] {a}
x : X
hx : x ∈ s
obtain :
  ∀ (e : OpenPartialHomeomorph X Y) (hxe : x ∈ e.source) (h : IsLocalHomeomorphOn (↑e : X → Y) s),
    IsOpen[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) x) ⋯}
⊢ IsOpen[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : Y) ↦ x ∈ f '' s) (f x) ⋯}

Tactic:
obtain ⟨e, hxe, rfl⟩ := h x hx

Premises used: rfl
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsOpen[inst] s
hX : ∀ (a : (↑s : Type u_1)), IsOpen[instTopologicalSpaceSubtype] {a}
x : X
hx : x ∈ s
e : OpenPartialHomeomorph X Y
hxe : x ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
⊢ IsOpen[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) x) ⋯}

Tactic:
⟨e '' {x}, e.isOpen_image_of_subset_source ?_ (Set.singleton_subset_iff.mpr hxe), ?_⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, OpenPartialHomeomorph.isOpen_image_of_subset_source, OpenPartialHomeomorph.toFun', And.intro, Exists.intro, Set.image, IsOpen, Singleton.singleton
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsOpen[inst] s
hX : ∀ (a : (↑s : Type u_1)), IsOpen[instTopologicalSpaceSubtype] {a}
x : X
hx : x ∈ s
e : OpenPartialHomeomorph X Y
hxe : x ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
refine_1 : IsOpen[inst] {x}
refine_2 :
  Eq (α := Set { x : Y // x ∈ (↑e : X → Y) '' s })
    (Subtype.val (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ⁻¹' (↑e : X → Y) '' {x})
    {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) x) ⋯}
⊢ IsOpen[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) x) ⋯}

Tactic:
refine ⟨e '' {x}, e.isOpen_image_of_subset_source ?_ (Set.singleton_subset_iff.mpr hxe), ?_⟩
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsOpen[inst] s
hX : ∀ (a : (↑s : Type u_1)), IsOpen[instTopologicalSpaceSubtype] {a}
x : X
hx : x ∈ s
e : OpenPartialHomeomorph X Y
hxe : x ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
⊢ IsOpen[inst] {x}

Tactic:
simpa using hs.isOpenMap_subtype_val _ (hX ⟨x, hx⟩)

Premises used: Subtype.mk, IsOpen.isOpenMap_subtype_val
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsOpen[inst] s
hX : ∀ (a : (↑s : Type u_1)), IsOpen[instTopologicalSpaceSubtype] {a}
x : X
hx : x ∈ s
e : OpenPartialHomeomorph X Y
hxe : x ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
refine_2 :
  ∀ (x_1 : { x : Y // x ∈ (↑e : X → Y) '' s }),
    Membership.mem (γ := Set { x : Y // x ∈ (↑e : X → Y) '' s })
        (Subtype.val (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ⁻¹' (↑e : X → Y) '' {x}) x_1 ↔
      Membership.mem (γ := Set { x : Y // x ∈ (↑e : X → Y) '' s })
        {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) x) ⋯} x_1
⊢ Eq (α := Set { x : Y // x ∈ (↑e : X → Y) '' s })
    (Subtype.val (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ⁻¹' (↑e : X → Y) '' {x})
    {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) x) ⋯}

Tactic:
ext
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsOpen[inst] s
hX : ∀ (a : (↑s : Type u_1)), IsOpen[instTopologicalSpaceSubtype] {a}
x : X
hx : x ∈ s
e : OpenPartialHomeomorph X Y
hxe : x ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
x_1 : { x : Y // x ∈ (↑e : X → Y) '' s }
⊢ Membership.mem (γ := Set { x : Y // x ∈ (↑e : X → Y) '' s })
      (Subtype.val (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ⁻¹' (↑e : X → Y) '' {x}) x_1 ↔
    Membership.mem (γ := Set { x : Y // x ∈ (↑e : X → Y) '' s })
      {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) x) ⋯} x_1

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- 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 : IsLocalHomeomorphOn f s
hs : IsOpen[inst] s
⊢ IsDiscrete (f '' s) ↔ IsDiscrete s

Tactic:
⟨h.isDiscrete_of_image, fun hs' ↦ ⟨h.discreteTopology_image_iff hs |>.mpr hs'.to_subtype⟩⟩

Premises used: Iff.mpr, IsDiscrete.to_subtype, IsDiscrete.mk, IsLocalHomeomorphOn.discreteTopology_image_iff, Iff.intro, IsLocalHomeomorphOn.isDiscrete_of_image
-- 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 : x ∈ s
obtain :
  ∀ (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)
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)

Tactic:
obtain ⟨e, hx, he⟩ := h x hx