-- Mathlib/Geometry/Manifold/LocalDiffeomorph.lean
theorem IsLocalDiffeomorphOn.isLocalHomeomorphOn {s : Set M} (hf : IsLocalDiffeomorphOn I J n f s) :
    IsLocalHomeomorphOn f s

Proof state:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
⊢ ∀ x ∈ s, ∃ e, x ∈ e.source ∧ EqOn f (↑e) e.source

Tactic:
intro x hx

Result:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
x : M
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ EqOn f (↑e) e.source

Proof state:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
x : M
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ EqOn f (↑e) e.source

Tactic:
choose U hyp using hf ⟨x, hx⟩

Result:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
x : M
hx : x ∈ s
U : PartialDiffeomorph I J M N n
hyp : ↑⟨x, hx⟩ ∈ U.source ∧ EqOn f (↑U.toPartialEquiv) U.source
⊢ ∃ e, x ∈ e.source ∧ EqOn f (↑e) e.source

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
⊢ IsLocalHomeomorphOn f s

Tactic:
apply IsLocalHomeomorphOn.mk

Result:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
⊢ ∀ x ∈ s, ∃ e, x ∈ e.source ∧ EqOn f (↑e) e.source

Proof state:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
x : M
hx : x ∈ s
U : PartialDiffeomorph I J M N n
hyp : ↑⟨x, hx⟩ ∈ U.source ∧ EqOn f (↑U.toPartialEquiv) U.source
⊢ ∃ e, x ∈ e.source ∧ EqOn f (↑e) e.source

Tactic:
exact ⟨U.toPartialHomeomorph, hyp⟩

Result:
no goals