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
h : IsLocalHomeomorph f
inst_2 : DiscreteTopology Y
⊢ DiscreteTopology X

Tactic:
(Homeomorph.Set.univ X).discreteTopology_iff.mp h.isLocalHomeomorphOn.discreteTopology_of_image

Premises used: Homeomorph.Set.univ, IsLocalHomeomorph.isLocalHomeomorphOn, Homeomorph.discreteTopology_iff, IsLocalHomeomorphOn.discreteTopology_of_image, Iff.mp
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsLocalHomeomorph f
rw : DiscreteTopology.{u_2} (↑(f '' Set.univ) : Type u_2) ↔ DiscreteTopology.{u_1} (↑Set.univ : Type u_1)
⊢ DiscreteTopology.{u_2} (↑(Set.range f) : Type u_2) ↔ DiscreteTopology X

Tactic:
rw [← Set.image_univ, ← (Homeomorph.Set.univ X).discreteTopology_iff]

Premises used: Homeomorph.Set.univ, Set.image_univ, Homeomorph.discreteTopology_iff
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsLocalHomeomorph f
⊢ DiscreteTopology.{u_2} (↑(f '' Set.univ) : Type u_2) ↔ DiscreteTopology.{u_1} (↑Set.univ : Type u_1)

Tactic:
h.isLocalHomeomorphOn.discreteTopology_image_iff isOpen_univ

Premises used: IsLocalHomeomorph.isLocalHomeomorphOn, isOpen_univ, IsLocalHomeomorphOn.discreteTopology_image_iff
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsLocalHomeomorph f
⊢ DiscreteTopology.{u_2} (↑(f '' Set.univ) : Type u_2) ↔ DiscreteTopology.{u_1} (↑Set.univ : Type u_1)

Tactic:
exact h.isLocalHomeomorphOn.discreteTopology_image_iff isOpen_univ

Premises used: IsLocalHomeomorph.isLocalHomeomorphOn, isOpen_univ, IsLocalHomeomorphOn.discreteTopology_image_iff
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsLocalHomeomorph f
hs : Function.Surjective f
rw : DiscreteTopology X ↔ DiscreteTopology.{u_2} (↑Set.univ : Type u_2)
rw₁ : DiscreteTopology X ↔ DiscreteTopology.{u_2} (↑(Set.range f) : Type u_2)
rw₂ rw₃ : DiscreteTopology X ↔ DiscreteTopology X
⊢ DiscreteTopology X ↔ DiscreteTopology Y

Tactic:
rw [← (Homeomorph.Set.univ Y).discreteTopology_iff, ← hs.range_eq, h.discreteTopology_range_iff]

Premises used: Homeomorph.Set.univ, Homeomorph.discreteTopology_iff, Function.Surjective.range_eq, IsLocalHomeomorph.discreteTopology_range_iff
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : ∀ (x : X), ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
⊢ IsLocalHomeomorph f

Tactic:
isLocalHomeomorph_iff_isLocalHomeomorphOn_univ.mpr
    (IsLocalHomeomorphOn.mk f Set.univ fun x _hx ↦ h x)

Premises used: IsLocalHomeomorphOn.mk, Iff.mpr, isLocalHomeomorph_iff_isLocalHomeomorphOn_univ, Set.univ
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ IsLocalHomeomorph.{u_1, u_2} (X := X) (Y := Y) (⇑h : (a : X) → Y)

Tactic:
fun _ ↦ ⟨h.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
hf : IsLocalHomeomorph f
x : X
obtain :
  ∀ (f : OpenPartialHomeomorph X Y) (hx : x ∈ f.source) (hf : IsLocalHomeomorph (↑f : X → Y)),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ Set.InjOn (↑f : X → Y) U
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ Set.InjOn f U

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

Premises used: rfl
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
f : OpenPartialHomeomorph X Y
hx : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ Set.InjOn (↑f : X → Y) U

Tactic:
⟨f.source, f.open_source, hx, f.injOn⟩

Premises used: OpenPartialHomeomorph.open_source, And.intro, OpenPartialHomeomorph.injOn, 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
x : X
f : OpenPartialHomeomorph X Y
hx : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ Set.InjOn (↑f : X → Y) U

Tactic:
exact ⟨f.source, f.open_source, hx, f.injOn⟩
-- 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
hgf : IsLocalHomeomorph (g ∘ f)
hg : IsLocalHomeomorph g
cont : Continuous[inst, inst_1] f
⊢ IsLocalHomeomorph f

Tactic:
isLocalHomeomorph_iff_isLocalHomeomorphOn_univ.mpr <|
    hgf.isLocalHomeomorphOn.of_comp_left hg.isLocalHomeomorphOn fun _ _ ↦ cont.continuousAt

Premises used: Iff.mpr, isLocalHomeomorph_iff_isLocalHomeomorphOn_univ, IsLocalHomeomorph.isLocalHomeomorphOn, Continuous.continuousAt, IsLocalHomeomorphOn.of_comp_left
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
⊢ Filter.map f (𝓝 x) = 𝓝 (f x)

Tactic:
hf.isLocalHomeomorphOn.map_nhds_eq (Set.mem_univ x)

Premises used: IsLocalHomeomorph.isLocalHomeomorphOn, Set.mem_univ, 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
hf : IsLocalHomeomorph f
⊢ Continuous[inst, inst_1] f

Tactic:
continuousOn_univ.mp hf.isLocalHomeomorphOn.continuousOn

Premises used: IsLocalHomeomorph.isLocalHomeomorphOn, IsLocalHomeomorphOn.continuousOn, Iff.mp, continuousOn_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 : IsLocalHomeomorph f
⊢ IsOpenMap f

Tactic:
IsOpenMap.of_nhds_le fun x ↦ ge_of_eq (hf.map_nhds_eq x)

Premises used: ge_of_eq, IsLocalHomeomorph.map_nhds_eq, IsOpenMap.of_nhds_le
-- 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
hg : IsLocalHomeomorph g
hf : IsLocalHomeomorph f
⊢ IsLocalHomeomorph (g ∘ f)

Tactic:
isLocalHomeomorph_iff_isLocalHomeomorphOn_univ.mpr
    (hg.isLocalHomeomorphOn.comp hf.isLocalHomeomorphOn (Set.univ.mapsTo_univ f))

Premises used: Iff.mpr, isLocalHomeomorph_iff_isLocalHomeomorphOn_univ, Set.mapsTo_univ, IsLocalHomeomorph.isLocalHomeomorphOn, Set.univ, IsLocalHomeomorphOn.comp
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
hi : Function.Injective f
⊢ IsOpenEmbedding f

Tactic:
.of_continuous_injective_isOpenMap hf.continuous hi hf.isOpenMap

Premises used: IsLocalHomeomorph.continuous, Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap, IsLocalHomeomorph.isOpenMap
-- 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
hf : IsLocalHomeomorph g
hgf : IsOpenEmbedding (g ∘ f)
cont : Continuous[inst, inst_1] f
⊢ IsOpenEmbedding f

Tactic:
(hgf.isLocalHomeomorph.of_comp hf cont).isOpenEmbedding_of_injective hgf.injective.of_comp

Premises used: IsLocalHomeomorph.isOpenEmbedding_of_injective, Topology.IsOpenEmbedding.isLocalHomeomorph, Topology.IsOpenEmbedding.toIsEmbedding, IsLocalHomeomorph.of_comp, Topology.IsEmbedding.injective, Function.Injective.of_comp
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
⊢ IsTopologicalBasis.{u_1} (α := X)
    {U : Set X |
      ∃ (V : Set Y),
        IsOpen[inst_1] V ∧
          ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
            Eq (α := (↑V : Type u_2) → Y) (f ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
              Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}

Tactic:
isTopologicalBasis_of_isOpen_of_nhds ?_ fun x U hx hU ↦ ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
refine_1 :
  ∀ (u : Set X),
    Membership.mem (γ := Set (Set X))
        {U : Set X |
          ∃ (V : Set Y),
            IsOpen[inst_1] V ∧
              ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
                Eq (α := (↑V : Type u_2) → Y) (f ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                    (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
                  Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}
        u →
      IsOpen[inst] u
refine_2 :
  ∀ (x : X) (U : Set X) (hx : x ∈ U) (hU : IsOpen[inst] U),
    ∃ (v : Set X),
      Membership.mem (γ := Set (Set X))
          {U : Set X |
            ∃ (V : Set Y),
              IsOpen[inst_1] V ∧
                ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
                  Eq (α := (↑V : Type u_2) → Y) (f ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                      (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
                    Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}
          v ∧
        x ∈ v ∧ v ⊆ U
⊢ IsTopologicalBasis.{u_1} (α := X)
    {U : Set X |
      ∃ (V : Set Y),
        IsOpen[inst_1] V ∧
          ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
            Eq (α := (↑V : Type u_2) → Y) (f ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
              Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}

Tactic:
refine isTopologicalBasis_of_isOpen_of_nhds ?_ fun x U hx hU ↦ ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
U : Set Y
hU : IsOpen[inst_1] U
s : ContinuousMap.{u_2, u_1} (↑U : Type u_2) X
hs : Eq (α := (↑U : Type u_2) → Y) (f ∘ (⇑s : (a : (↑U : Type u_2)) → X)) (Subtype.val (p := fun (x : Y) ↦ x ∈ U))
⊢ IsOpen[inst] (Set.range.{u_1, u_2 + 1} (ι := (↑U : Type u_2)) (⇑s : (a : (↑U : Type u_2)) → X))

Tactic:
(isOpenEmbedding_of_comp hf (hs ▸ ⟨IsEmbedding.subtypeVal, ?_⟩)
      s.continuous).isOpen_range

Premises used: ContinuousMap.continuous, IsLocalHomeomorph.isOpenEmbedding_of_comp, Topology.IsOpenEmbedding.isOpen_range
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
U : Set Y
hU : IsOpen[inst_1] U
s : ContinuousMap.{u_2, u_1} (↑U : Type u_2) X
hs : Eq (α := (↑U : Type u_2) → Y) (f ∘ (⇑s : (a : (↑U : Type u_2)) → X)) (Subtype.val (p := fun (x : Y) ↦ x ∈ U))
refine_1 : IsOpen[inst_1] (Set.range (ι := (↑U : Type u_2)) (Subtype.val (p := fun (x : Y) ↦ x ∈ U)))
⊢ IsOpen[inst] (Set.range.{u_1, u_2 + 1} (ι := (↑U : Type u_2)) (⇑s : (a : (↑U : Type u_2)) → X))

Tactic:
refine (isOpenEmbedding_of_comp hf (hs ▸ ⟨IsEmbedding.subtypeVal, ?_⟩)
      s.continuous).isOpen_range

Premises used: ContinuousMap.continuous, IsLocalHomeomorph.isOpenEmbedding_of_comp, Topology.IsOpenEmbedding.isOpen_range
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
U : Set Y
hU : IsOpen[inst_1] U
s : ContinuousMap.{u_2, u_1} (↑U : Type u_2) X
hs : Eq (α := (↑U : Type u_2) → Y) (f ∘ (⇑s : (a : (↑U : Type u_2)) → X)) (Subtype.val (p := fun (x : Y) ↦ x ∈ U))
refine_1 refine_1₁ refine_1₂ refine_1₃ : IsOpen[inst_1] U
⊢ IsOpen[inst_1] (Set.range (ι := (↑U : Type u_2)) (Subtype.val (p := fun (x : Y) ↦ x ∈ U)))

Tactic:
rwa [Subtype.range_val]

Premises used: Subtype.range_val
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
refine_2 :
  ∀ (f : OpenPartialHomeomorph X Y) (hxf : x ∈ f.source) (hf : IsLocalHomeomorph (↑f : X → Y)),
    ∃ (v : Set X),
      Membership.mem (γ := Set (Set X))
          {U : Set X |
            ∃ (V : Set Y),
              IsOpen[inst_1] V ∧
                ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
                  Eq (α := (↑V : Type u_2) → Y) ((↑f : X → Y) ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                      (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
                    Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}
          v ∧
        x ∈ v ∧ v ⊆ U
⊢ ∃ (v : Set X),
    Membership.mem (γ := Set (Set X))
        {U : Set X |
          ∃ (V : Set Y),
            IsOpen[inst_1] V ∧
              ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
                Eq (α := (↑V : Type u_2) → Y) (f ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                    (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
                  Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}
        v ∧
      x ∈ v ∧ v ⊆ U

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

Premises used: rfl
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
⊢ ∃ (v : Set X),
    Membership.mem (γ := Set (Set X))
        {U : Set X |
          ∃ (V : Set Y),
            IsOpen[inst_1] V ∧
              ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
                Eq (α := (↑V : Type u_2) → Y) ((↑f : X → Y) ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                    (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
                  Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}
        v ∧
      x ∈ v ∧ v ⊆ U

Tactic:
⟨f.source ∩ U, ⟨f.target ∩ f.symm ⁻¹' U, f.symm.isOpen_inter_preimage hU,
      ⟨_, continuousOn_iff_continuous_restrict.mp (f.continuousOn_invFun.mono fun _ h ↦ h.1)⟩,
      ?_, (Set.range_restrict _ _).trans ?_⟩, ⟨hxf, hx⟩, fun _ h ↦ h.2⟩

Premises used: PartialEquiv.target, ContinuousMap.mk, OpenPartialHomeomorph.toFun', Set.range_restrict, OpenPartialHomeomorph.continuousOn_invFun, Inter.inter, OpenPartialHomeomorph.isOpen_inter_preimage, And.right, Set.preimage, And.left, continuousOn_iff_continuous_restrict, And.intro, Exists.intro, Iff.mp, PartialEquiv.source, ContinuousOn.mono, OpenPartialHomeomorph.toPartialEquiv, Eq.trans, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
refine_2 :
  Eq (α := (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2) → Y)
    ((↑f : X → Y) ∘
      (⇑{ toFun := (f.target ∩ (↑f.symm : Y → X) ⁻¹' U).restrict (π := fun (a : Y) ↦ X) f.invFun,
            continuous_toFun := ⋯ : ContinuousMap.{u_2, u_1} (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2) X } :
        (a : (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2)) → X))
    (Subtype.val (p := fun (x : Y) ↦ x ∈ f.target ∩ (↑f.symm : Y → X) ⁻¹' U))
refine_2₁ : f.toPartialEquiv.2 '' (f.target ∩ (↑f.symm : Y → X) ⁻¹' U) = f.source ∩ U
⊢ ∃ (v : Set X),
    Membership.mem (γ := Set (Set X))
        {U : Set X |
          ∃ (V : Set Y),
            IsOpen[inst_1] V ∧
              ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
                Eq (α := (↑V : Type u_2) → Y) ((↑f : X → Y) ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                    (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
                  Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}
        v ∧
      x ∈ v ∧ v ⊆ U

Tactic:
refine ⟨f.source ∩ U, ⟨f.target ∩ f.symm ⁻¹' U, f.symm.isOpen_inter_preimage hU,
      ⟨_, continuousOn_iff_continuous_restrict.mp (f.continuousOn_invFun.mono fun _ h ↦ h.1)⟩,
      ?_, (Set.range_restrict _ _).trans ?_⟩, ⟨hxf, hx⟩, fun _ h ↦ h.2⟩
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
refine_2 :
  ∀ (y : (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2)),
    ((↑f : X → Y) ∘
          (⇑{ toFun := (f.target ∩ (↑f.symm : Y → X) ⁻¹' U).restrict (π := fun (a : Y) ↦ X) f.invFun,
                continuous_toFun := ⋯ :
                ContinuousMap.{u_2, u_1} (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2) X } :
            (a : (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2)) → X))
        y =
      (↑y : Y)
⊢ Eq (α := (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2) → Y)
    ((↑f : X → Y) ∘
      (⇑{ toFun := (f.target ∩ (↑f.symm : Y → X) ⁻¹' U).restrict (π := fun (a : Y) ↦ X) f.invFun,
            continuous_toFun := ⋯ : ContinuousMap.{u_2, u_1} (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2) X } :
        (a : (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2)) → X))
    (Subtype.val (p := fun (x : Y) ↦ x ∈ f.target ∩ (↑f.symm : Y → X) ⁻¹' U))

Tactic:
ext y
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
y : (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2)
⊢ ((↑f : X → Y) ∘
        (⇑{ toFun := (f.target ∩ (↑f.symm : Y → X) ⁻¹' U).restrict (π := fun (a : Y) ↦ X) f.invFun,
              continuous_toFun := ⋯ : ContinuousMap.{u_2, u_1} (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2) X } :
          (a : (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2)) → X))
      y =
    (↑y : Y)

Tactic:
f.right_inv y.2.1

Premises used: OpenPartialHomeomorph.toFun', And.left, Set.restrict, Subtype.property, OpenPartialHomeomorph.right_inv
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
y : (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2)
⊢ ((↑f : X → Y) ∘
        (⇑{ toFun := (f.target ∩ (↑f.symm : Y → X) ⁻¹' U).restrict (π := fun (a : Y) ↦ X) f.invFun,
              continuous_toFun := ⋯ : ContinuousMap.{u_2, u_1} (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2) X } :
          (a : (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2)) → X))
      y =
    (↑y : Y)

Tactic:
exact f.right_inv y.2.1

Premises used: And.left, Subtype.property, OpenPartialHomeomorph.right_inv
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
refine_2 : f.source ∩ (↑f : X → Y) ⁻¹' (f.target ∩ (↑f.symm : Y → X) ⁻¹' U) = f.source ∩ U
⊢ f.toPartialEquiv.2 '' (f.target ∩ (↑f.symm : Y → X) ⁻¹' U) = f.source ∩ U

Tactic:
apply (f.symm_image_target_inter_eq _).trans

Premises used: OpenPartialHomeomorph.symm_image_target_inter_eq, Eq.trans
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
refine_2 : f.source ∩ ((↑f : X → Y) ⁻¹' f.target ∩ (↑f : X → Y) ⁻¹' (↑f.symm : Y → X) ⁻¹' U) = f.source ∩ U
refine_2₁ : f.source ∩ (↑f : X → Y) ⁻¹' f.target ∩ (↑f : X → Y) ⁻¹' (↑f.symm : Y → X) ⁻¹' U = f.source ∩ U
refine_2₂ : f.source ∩ (↑f : X → Y) ⁻¹' (↑f.symm : Y → X) ⁻¹' U = f.source ∩ U
refine_2₃ refine_2₄ : f.source ∩ U = f.source ∩ U
⊢ f.source ∩ (↑f : X → Y) ⁻¹' (f.target ∩ (↑f.symm : Y → X) ⁻¹' U) = f.source ∩ U

Tactic:
rw [Set.preimage_inter, ← Set.inter_assoc, Set.inter_eq_self_of_subset_left
        f.source_preimage_target, f.source_inter_preimage_inv_preimage]

Premises used: Set.preimage_inter, OpenPartialHomeomorph.source_inter_preimage_inv_preimage, OpenPartialHomeomorph.source_preimage_target, Set.inter_assoc, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
⊢ x ∈ (hf.localInverseAt x).target

Tactic:
(hf x).choose_spec.1

Premises used: Exists.choose_spec, Set.Mem, And.left
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
⊢ (↑(hf.localInverseAt x).symm : X → Y) = f

Tactic:
(hf x).choose_spec.2.symm

Premises used: Exists.choose_spec, PartialEquiv.symm, And.right, Eq.symm, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
rw : (↑(hf.localInverseAt x).symm : X → Y) x ∈ (hf.localInverseAt x).source
⊢ f x ∈ (hf.localInverseAt x).source

Tactic:
rw [← congrFun (hf.localInverseAt_symm x)]

Premises used: IsLocalHomeomorph.localInverseAt_symm, congrFun
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
⊢ (↑(hf.localInverseAt x).symm : X → Y) x ∈ (hf.localInverseAt x).source

Tactic:
(hf.localInverseAt x).map_target hf.self_mem_localInverseAt_target

Premises used: IsLocalHomeomorph.self_mem_localInverseAt_target, IsLocalHomeomorph.localInverseAt, OpenPartialHomeomorph.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
hf : IsLocalHomeomorph f
x : X
⊢ (↑(hf.localInverseAt x).symm : X → Y) x ∈ (hf.localInverseAt x).source

Tactic:
exact (hf.localInverseAt x).map_target hf.self_mem_localInverseAt_target

Premises used: IsLocalHomeomorph.self_mem_localInverseAt_target, IsLocalHomeomorph.localInverseAt, OpenPartialHomeomorph.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
hf : IsLocalHomeomorph f
x y : X
h : y ∈ (hf.localInverseAt x).target
⊢ f y = (↑(hf.localInverseAt x).symm : X → Y) y

Tactic:
simp
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
rw : Set.InjOn (↑(hf.localInverseAt x).symm : X → Y) (hf.localInverseAt x).target
⊢ Set.InjOn f (hf.localInverseAt x).target

Tactic:
rw [Set.EqOn.injOn_iff (f₂ := (hf.localInverseAt x).symm) (fun y _ ↦ by simp)]

Premises used: Set.EqOn.injOn_iff
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
⊢ Set.InjOn (↑(hf.localInverseAt x).symm : X → Y) (hf.localInverseAt x).target

Tactic:
(hf.localInverseAt x).symm.injOn

Premises used: IsLocalHomeomorph.localInverseAt, OpenPartialHomeomorph.injOn, OpenPartialHomeomorph.symm