-- Mathlib/Topology/IsLocalHomeomorph.lean
theorem isLocalHomeomorphOn_iff_isOpenEmbedding_restrict {f : X → Y} :
    IsLocalHomeomorphOn f s ↔ ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict f)
⊢ IsOpenEmbedding ((interior U).restrict f)

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

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict f)
⊢ IsOpen (Set.range (Set.inclusion ⋯))

Proof state:
case refine_2.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict f)
⊢ ∃ e, x ∈ e.source ∧ f = ↑e

Tactic:
have : IsOpenEmbedding ((interior U).restrict f) := by
  refine emb.comp ⟨.inclusion interior_subset, ?_⟩
  rw [Set.range_inclusion]; exact isOpen_induced isOpen_interior

Result:
case refine_2.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict f)
this : IsOpenEmbedding ((interior U).restrict f)
⊢ ∃ e, x ∈ e.source ∧ f = ↑e

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict f)
⊢ IsOpen (Set.range (Set.inclusion ⋯))

Tactic:
rw [Set.range_inclusion]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict f)
⊢ IsOpen {x | ↑x ∈ interior U}

Proof state:
case refine_2.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict f)
this : IsOpenEmbedding ((interior U).restrict f)
cont : Continuous ((interior U).restrict f)
inj : Function.Injective ((interior U).restrict f)
openMap : IsOpenMap ((interior U).restrict f)
⊢ ∃ e, x ∈ e.source ∧ f = ↑e

Tactic:
haveI : Nonempty X := ⟨x⟩

Result:
case refine_2.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict f)
this✝ : IsOpenEmbedding ((interior U).restrict f)
cont : Continuous ((interior U).restrict f)
inj : Function.Injective ((interior U).restrict f)
openMap : IsOpenMap ((interior U).restrict f)
this : Nonempty X
⊢ ∃ e, x ∈ e.source ∧ f = ↑e

Proof state:
case refine_2.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict f)
this : IsOpenEmbedding ((interior U).restrict f)
⊢ ∃ e, x ∈ e.source ∧ f = ↑e

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

Result:
case refine_2.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict f)
this : IsOpenEmbedding ((interior U).restrict f)
cont : Continuous ((interior U).restrict f)
inj : Function.Injective ((interior U).restrict f)
openMap : IsOpenMap ((interior U).restrict f)
⊢ ∃ e, x ∈ e.source ∧ f = ↑e

Proof state:
case refine_2.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict f)
this✝ : IsOpenEmbedding ((interior U).restrict f)
cont : Continuous ((interior U).restrict f)
inj : Function.Injective ((interior U).restrict f)
openMap : IsOpenMap ((interior U).restrict f)
this : Nonempty X
⊢ ∃ e, x ∈ e.source ∧ f = ↑e

Tactic:
exact ⟨PartialHomeomorph.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⟩

Result:
no goals

Proof state:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : IsLocalHomeomorphOn f s
x : X
hx : x ∈ s
⊢ ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)

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

Result:
case refine_1.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
hx : x ∈ s
e : PartialHomeomorph X Y
hxe : x ∈ e.source
h : IsLocalHomeomorphOn (↑e) s
⊢ ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict ↑e)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict f)
⊢ IsOpen {x | ↑x ∈ interior U}

Tactic:
exact isOpen_induced isOpen_interior

Result:
no goals

Proof state:
case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ f = ↑e

Tactic:
obtain ⟨U, hU, emb⟩ := h x hx

Result:
case refine_2.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict f)
⊢ ∃ e, x ∈ e.source ∧ f = ↑e

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
⊢ IsLocalHomeomorphOn f s ↔ ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩

Result:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : IsLocalHomeomorphOn f s
x : X
hx : x ∈ s
⊢ ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)

case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ f = ↑e

Proof state:
case refine_1.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
hx : x ∈ s
e : PartialHomeomorph X Y
hxe : x ∈ e.source
h : IsLocalHomeomorphOn (↑e) s
⊢ ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict ↑e)

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

Result:
no goals