[GOAL]
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
x : E
I : Type u_3
inst✝ : TopologicalSpace I
h✝ : IsEvenlyCovered f (f x) I
e : Trivialization I f := Classical.choose (_ : ∃ t, f x ∈ t.baseSet)
h : f x ∈ (Classical.choose (_ : ∃ t, f x ∈ t.baseSet)).baseSet := Classical.choose_spec h✝.right
he : (f x, (↑e x).snd) = ↑e x := Trivialization.mk_proj_snd' e h
⊢ (f x, (↑e x).snd) ∈ e.target
[PROOFSTEP]
rwa [he, e.mem_target, e.coe_fst (e.mem_source.mpr h)]
[GOAL]
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
hf : IsCoveringMapOn f s
⊢ IsLocallyHomeomorphOn f (f ⁻¹' s)
[PROOFSTEP]
refine' IsLocallyHomeomorphOn.mk f (f ⁻¹' s) fun x hx => _
[GOAL]
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
⊢ ∃ e, x ∈ e.source ∧ ∀ (y : E), y ∈ e.source → f y = ↑e y
[PROOFSTEP]
let e := (hf (f x) hx).toTrivialization
[GOAL]
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
e : Trivialization (↑(f ⁻¹' {f x})) f := IsEvenlyCovered.toTrivialization (_ : IsEvenlyCovered f (f x) ↑(f ⁻¹' {f x}))
⊢ ∃ e, x ∈ e.source ∧ ∀ (y : E), y ∈ e.source → f y = ↑e y
[PROOFSTEP]
have h := (hf (f x) hx).mem_toTrivialization_baseSet
[GOAL]
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
e : Trivialization (↑(f ⁻¹' {f x})) f := IsEvenlyCovered.toTrivialization (_ : IsEvenlyCovered f (f x) ↑(f ⁻¹' {f x}))
h : f x ∈ (IsEvenlyCovered.toTrivialization (_ : IsEvenlyCovered f (f x) ↑(f ⁻¹' {f x}))).baseSet
⊢ ∃ e, x ∈ e.source ∧ ∀ (y : E), y ∈ e.source → f y = ↑e y
[PROOFSTEP]
let he := e.mem_source.2 h
[GOAL]
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
e : Trivialization (↑(f ⁻¹' {f x})) f := IsEvenlyCovered.toTrivialization (_ : IsEvenlyCovered f (f x) ↑(f ⁻¹' {f x}))
h : f x ∈ (IsEvenlyCovered.toTrivialization (_ : IsEvenlyCovered f (f x) ↑(f ⁻¹' {f x}))).baseSet
he : x ∈ e.source := Iff.mpr (Trivialization.mem_source e) h
⊢ ∃ e, x ∈ e.source ∧ ∀ (y : E), y ∈ e.source → f y = ↑e y
[PROOFSTEP]
refine'
  ⟨e.toLocalHomeomorph.trans
      { toFun := fun p => p.1
        invFun := fun p => ⟨p, x, rfl⟩
        source := e.baseSet ×ˢ ({⟨x, rfl⟩} : Set (f ⁻¹' {f x}))
        target := e.baseSet
        open_source := e.open_baseSet.prod (singletons_open_iff_discrete.2 (hf (f x) hx).1 ⟨x, rfl⟩)
        open_target := e.open_baseSet
        map_source' := fun p => And.left
        map_target' := fun p hp => ⟨hp, rfl⟩
        left_inv' := fun p hp => Prod.ext rfl hp.2.symm
        right_inv' := fun p _ => rfl
        continuous_toFun := continuous_fst.continuousOn
        continuous_invFun := (continuous_id'.prod_mk continuous_const).continuousOn },
    ⟨he, by rwa [e.toLocalHomeomorph.symm_symm, e.proj_toFun x he], (hf (f x) hx).toTrivialization_apply⟩, fun p h =>
    (e.proj_toFun p h.1).symm⟩
[GOAL]
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
e : Trivialization (↑(f ⁻¹' {f x})) f := IsEvenlyCovered.toTrivialization (_ : IsEvenlyCovered f (f x) ↑(f ⁻¹' {f x}))
h : f x ∈ (IsEvenlyCovered.toTrivialization (_ : IsEvenlyCovered f (f x) ↑(f ⁻¹' {f x}))).baseSet
he : x ∈ e.source := Iff.mpr (Trivialization.mem_source e) h
⊢ (↑(LocalHomeomorph.symm (LocalHomeomorph.symm e.toLocalHomeomorph)) x).fst ∈ e.baseSet
[PROOFSTEP]
rwa [e.toLocalHomeomorph.symm_symm, e.proj_toFun x he]
[GOAL]
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
⊢ IsCoveringMap f ↔ IsCoveringMapOn f Set.univ
[PROOFSTEP]
simp only [IsCoveringMap, IsCoveringMapOn, Set.mem_univ, forall_true_left]
