[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : α ≃ₜ β
s : Set α
hs : IsOpen s
t : Set β
h : ↑e '' s = t
⊢ IsOpen (Equiv.toLocalEquivOfImageEq e.toEquiv s t h).target
[PROOFSTEP]
simpa [← h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : α ≃ₜ β
⊢ ↑e '' univ = univ
[PROOFSTEP]
rw [image_univ, e.surjective.range_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e : LocalHomeomorph α β
e' : LocalEquiv α β
h : e.toLocalEquiv = e'
⊢ replaceEquiv e e' h = e
[PROOFSTEP]
cases e
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e' toLocalEquiv✝ : LocalEquiv α β
open_source✝ : IsOpen toLocalEquiv✝.source
open_target✝ : IsOpen toLocalEquiv✝.target
continuous_toFun✝ : ContinuousOn (↑toLocalEquiv✝) toLocalEquiv✝.source
continuous_invFun✝ : ContinuousOn toLocalEquiv✝.invFun toLocalEquiv✝.target
h :
  { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
        continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.toLocalEquiv =
    e'
⊢ replaceEquiv
      { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
        continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }
      e' h =
    { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
      continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }
[PROOFSTEP]
subst e'
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
toLocalEquiv✝ : LocalEquiv α β
open_source✝ : IsOpen toLocalEquiv✝.source
open_target✝ : IsOpen toLocalEquiv✝.target
continuous_toFun✝ : ContinuousOn (↑toLocalEquiv✝) toLocalEquiv✝.source
continuous_invFun✝ : ContinuousOn toLocalEquiv✝.invFun toLocalEquiv✝.target
⊢ replaceEquiv
      { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
        continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }
      { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
          continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.toLocalEquiv
      (_ :
        { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
              continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.toLocalEquiv =
          { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
              continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.toLocalEquiv) =
    { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
      continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
hx : x ∈ e.source
x' : α
hx' : ↑(LocalHomeomorph.symm e) (↑e x') = x'
h : ↑e x' = ↑e x
⊢ x' ∈ {x}
[PROOFSTEP]
rw [mem_singleton_iff, ← e.left_inv hx, ← h, hx']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
⊢ e = e' →
    (∀ (x : α), ↑e x = ↑e' x) ∧
      (∀ (x : β), ↑(LocalHomeomorph.symm e) x = ↑(LocalHomeomorph.symm e') x) ∧ e.source = e'.source
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
⊢ (∀ (x : α), ↑e x = ↑e x) ∧
    (∀ (x : β), ↑(LocalHomeomorph.symm e) x = ↑(LocalHomeomorph.symm e) x) ∧ e.source = e.source
[PROOFSTEP]
exact ⟨fun x => rfl, fun x => rfl, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
x : α
hx : x ∈ e.source
⊢ Tendsto (↑(LocalHomeomorph.symm e)) (𝓝 (↑e x)) (𝓝 x)
[PROOFSTEP]
simpa only [ContinuousAt, e.left_inv hx] using e.continuousAt_symm (e.map_source hx)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
x : α
hx : x ∈ e.source
⊢ 𝓝 (↑(LocalHomeomorph.symm e) (↑e x)) = 𝓝 x
[PROOFSTEP]
rw [e.left_inv hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
hx : x ∈ e.source
s : Set β
⊢ map (↑e) (𝓝[↑e ⁻¹' s] x) = 𝓝[s] ↑e x
[PROOFSTEP]
rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.target_inter_inv_preimage_preimage,
  e.nhdsWithin_target_inter (e.map_source hx)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
p : β → Prop
hx : x ∈ e.source
⊢ (∀ᶠ (y : β) in 𝓝 (↑e x), p y) ↔ ∀ᶠ (b : β) in map (fun x => ↑e x) (𝓝 x), p b
[PROOFSTEP]
rw [e.map_nhds_eq hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
p : α → Prop
hx : x ∈ e.source
⊢ (∀ᶠ (y : β) in 𝓝 (↑e x), p (↑(LocalHomeomorph.symm e) y)) ↔ ∀ᶠ (x : α) in 𝓝 x, p x
[PROOFSTEP]
rw [e.eventually_nhds _ hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
p : α → Prop
hx : x ∈ e.source
⊢ (∀ᶠ (x : α) in 𝓝 x, p (↑(LocalHomeomorph.symm e) (↑e x))) ↔ ∀ᶠ (x : α) in 𝓝 x, p x
[PROOFSTEP]
refine' eventually_congr ((e.eventually_left_inverse hx).mono fun y hy => _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
p : α → Prop
hx : x ∈ e.source
y : α
hy : ↑(LocalHomeomorph.symm e) (↑e y) = y
⊢ p (↑(LocalHomeomorph.symm e) (↑e y)) ↔ p y
[PROOFSTEP]
rw [hy]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
p : β → Prop
s : Set α
hx : x ∈ e.source
⊢ (∀ᶠ (y : β) in 𝓝[↑(LocalHomeomorph.symm e) ⁻¹' s] ↑e x, p y) ↔ ∀ᶠ (x : α) in 𝓝[s] x, p (↑e x)
[PROOFSTEP]
refine' Iff.trans _ eventually_map
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
p : β → Prop
s : Set α
hx : x ∈ e.source
⊢ (∀ᶠ (y : β) in 𝓝[↑(LocalHomeomorph.symm e) ⁻¹' s] ↑e x, p y) ↔ ∀ᶠ (b : β) in map (fun x => ↑e x) (𝓝[s] x), p b
[PROOFSTEP]
rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.nhdsWithin_target_inter (e.mapsTo hx)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
p : α → Prop
s : Set α
hx : x ∈ e.source
⊢ (∀ᶠ (y : β) in 𝓝[↑(LocalHomeomorph.symm e) ⁻¹' s] ↑e x, p (↑(LocalHomeomorph.symm e) y)) ↔ ∀ᶠ (x : α) in 𝓝[s] x, p x
[PROOFSTEP]
rw [e.eventually_nhdsWithin _ hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
p : α → Prop
s : Set α
hx : x ∈ e.source
⊢ (∀ᶠ (x : α) in 𝓝[s] x, p (↑(LocalHomeomorph.symm e) (↑e x))) ↔ ∀ᶠ (x : α) in 𝓝[s] x, p x
[PROOFSTEP]
refine
  eventually_congr <| (eventually_nhdsWithin_of_eventually_nhds <| e.eventually_left_inverse hx).mono fun y hy => ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
p : α → Prop
s : Set α
hx : x ∈ e.source
y : α
hy : ↑(LocalHomeomorph.symm e) (↑e y) = y
⊢ p (↑(LocalHomeomorph.symm e) (↑e y)) ↔ p y
[PROOFSTEP]
rw [hy]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
s : Set α
t : Set γ
x : α
f : α → γ
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ↑(LocalHomeomorph.symm e) ⁻¹' s =ᶠ[𝓝 (↑e x)] e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (s ∩ f ⁻¹' t)
[PROOFSTEP]
rw [eventuallyEq_set, e.eventually_nhds _ hxe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
s : Set α
t : Set γ
x : α
f : α → γ
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ∀ᶠ (x : α) in 𝓝 x,
    ↑e x ∈ ↑(LocalHomeomorph.symm e) ⁻¹' s ↔ ↑e x ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (s ∩ f ⁻¹' t)
[PROOFSTEP]
filter_upwards [e.open_source.mem_nhds hxe, mem_nhdsWithin_iff_eventually.mp (hf.preimage_mem_nhdsWithin ht)]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
s : Set α
t : Set γ
x : α
f : α → γ
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ∀ (a : α),
    a ∈ e.source →
      (a ∈ s → a ∈ f ⁻¹' t) →
        (↑e a ∈ ↑(LocalHomeomorph.symm e) ⁻¹' s ↔ ↑e a ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (s ∩ f ⁻¹' t))
[PROOFSTEP]
intro y hy hyu
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
s : Set α
t : Set γ
x : α
f : α → γ
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : α
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e y ∈ ↑(LocalHomeomorph.symm e) ⁻¹' s ↔ ↑e y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (s ∩ f ⁻¹' t)
[PROOFSTEP]
simp_rw [mem_inter_iff, mem_preimage, mem_inter_iff, e.mapsTo hy, true_and_iff, iff_self_and, e.left_inv hy,
  iff_true_intro hyu]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
t : Set β
x : α
y : β
⊢ IsImage e s t ↔ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (e.source ∩ s) = e.target ∩ t
[PROOFSTEP]
rw [iff_symm_preimage_eq, ← image_source_inter_eq, ← image_source_inter_eq']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
t : Set β
x : α
y : β
h : IsImage e s t
hx : x ∈ e.source
⊢ map (↑e) (𝓝[s] x) = 𝓝[t] ↑e x
[PROOFSTEP]
rw [e.map_nhdsWithin_eq hx, h.image_eq, e.nhdsWithin_target_inter (e.map_source hx)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
t : Set β
x✝ : α
y : β
h : IsImage e s t
x : α
hx : x ∈ e.source
⊢ ↑e x ∈ closure t ↔ x ∈ closure s
[PROOFSTEP]
simp only [mem_closure_iff_nhdsWithin_neBot, ← h.map_nhdsWithin_eq hx, map_neBot_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
t : Set β
x : α
y : β
h : IsImage e s t
⊢ IsImage e (interior s) (interior t)
[PROOFSTEP]
simpa only [closure_compl, compl_compl] using h.compl.closure.compl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
h : s ⊆ e.source
⊢ IsOpen (↑e '' s)
[PROOFSTEP]
have : e '' s = e.target ∩ e.symm ⁻¹' s := e.toLocalEquiv.image_eq_target_inter_inv_preimage h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
h : s ⊆ e.source
this : ↑e '' s = e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s
⊢ IsOpen (↑e '' s)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
h : s ⊆ e.source
this : ↑e '' s = e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s
⊢ IsOpen (e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s)
[PROOFSTEP]
exact e.continuousOn_symm.preimage_open_of_open e.open_target hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalEquiv α β
hc : ContinuousOn (↑e) e.source
ho : IsOpenMap (restrict e.source ↑e)
hs : IsOpen e.source
⊢ IsOpen e.target
[PROOFSTEP]
simpa only [range_restrict, e.image_source_eq_target] using ho.isOpen_range
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
⊢ (LocalHomeomorph.restr e s).toLocalEquiv.source = e.source ∩ s
[PROOFSTEP]
rw [e.restr_source, hs.interior_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
⊢ (LocalHomeomorph.restr e s).toLocalEquiv = LocalEquiv.restr e.toLocalEquiv s
[PROOFSTEP]
rw [e.restr_toLocalEquiv, hs.interior_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
⊢ LocalHomeomorph.restr e (e.source ∩ s) = LocalHomeomorph.restr e s
[PROOFSTEP]
refine' LocalHomeomorph.ext _ _ (fun x => rfl) (fun x => rfl) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
⊢ (LocalHomeomorph.restr e (e.source ∩ s)).toLocalEquiv.source = (LocalHomeomorph.restr e s).toLocalEquiv.source
[PROOFSTEP]
simp [e.open_source.interior_eq, ← inter_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
⊢ ofSet univ (_ : IsOpen univ) = LocalHomeomorph.refl α
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
x✝ : α
⊢ ↑(ofSet univ (_ : IsOpen univ)) x✝ = ↑(LocalHomeomorph.refl α) x✝
[PROOFSTEP]
simp
[GOAL]
case hinv
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
x✝ : α
⊢ ↑(LocalHomeomorph.symm (ofSet univ (_ : IsOpen univ))) x✝ = ↑(LocalHomeomorph.symm (LocalHomeomorph.refl α)) x✝
[PROOFSTEP]
simp
[GOAL]
case hs.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
x✝ : α
⊢ x✝ ∈ (ofSet univ (_ : IsOpen univ)).toLocalEquiv.source ↔ x✝ ∈ (LocalHomeomorph.refl α).toLocalEquiv.source
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
⊢ (LocalHomeomorph.symm
          (LocalHomeomorph.restrOpen (LocalHomeomorph.symm e) e'.source (_ : IsOpen e'.source))).toLocalEquiv.target =
    (LocalHomeomorph.restrOpen e' e.target (_ : IsOpen e.target)).toLocalEquiv.source
[PROOFSTEP]
simp [inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set β
hs : IsOpen s
⊢ (LocalHomeomorph.trans e (ofSet s hs)).toLocalEquiv.source = (LocalHomeomorph.restr e (↑e ⁻¹' s)).toLocalEquiv.source
[PROOFSTEP]
rw [trans_source, restr_source, ofSet_source, ← preimage_interior, hs.interior_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set β
hs : IsOpen s
⊢ LocalHomeomorph.trans e (ofSet s hs) = LocalHomeomorph.restr e (e.source ∩ ↑e ⁻¹' s)
[PROOFSTEP]
rw [trans_ofSet, restr_source_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
⊢ (LocalHomeomorph.trans (ofSet s hs) e).toLocalEquiv.source = (LocalHomeomorph.restr e s).toLocalEquiv.source
[PROOFSTEP]
simp [hs.interior_eq, inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
⊢ LocalHomeomorph.trans (ofSet s hs) e = LocalHomeomorph.restr e (e.source ∩ s)
[PROOFSTEP]
rw [ofSet_trans, restr_source_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
s' : Set α
hs' : IsOpen s'
⊢ LocalHomeomorph.trans (ofSet s hs) (ofSet s' hs') = ofSet (s ∩ s') (_ : IsOpen (s ∩ s'))
[PROOFSTEP]
rw [(ofSet s hs).trans_ofSet hs']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
s' : Set α
hs' : IsOpen s'
⊢ LocalHomeomorph.restr (ofSet s hs) (↑(ofSet s hs) ⁻¹' s') = ofSet (s ∩ s') (_ : IsOpen (s ∩ s'))
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
s' : Set α
hs' : IsOpen s'
x✝ : α
⊢ ↑(LocalHomeomorph.restr (ofSet s hs) (↑(ofSet s hs) ⁻¹' s')) x✝ = ↑(ofSet (s ∩ s') (_ : IsOpen (s ∩ s'))) x✝
[PROOFSTEP]
simp [hs'.interior_eq]
[GOAL]
case hinv
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
s' : Set α
hs' : IsOpen s'
x✝ : α
⊢ ↑(LocalHomeomorph.symm (LocalHomeomorph.restr (ofSet s hs) (↑(ofSet s hs) ⁻¹' s'))) x✝ =
    ↑(LocalHomeomorph.symm (ofSet (s ∩ s') (_ : IsOpen (s ∩ s')))) x✝
[PROOFSTEP]
simp [hs'.interior_eq]
[GOAL]
case hs.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
s' : Set α
hs' : IsOpen s'
x✝ : α
⊢ x✝ ∈ (LocalHomeomorph.restr (ofSet s hs) (↑(ofSet s hs) ⁻¹' s')).toLocalEquiv.source ↔
    x✝ ∈ (ofSet (s ∩ s') (_ : IsOpen (s ∩ s'))).toLocalEquiv.source
[PROOFSTEP]
simp [hs'.interior_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ LocalHomeomorph.restr e e'.source ≈ LocalHomeomorph.restr e' e.source
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ (LocalHomeomorph.restr e e'.source).toLocalEquiv.source = (LocalHomeomorph.restr e' e.source).toLocalEquiv.source
[PROOFSTEP]
rw [e'.restr_source' _ e.open_source]
[GOAL]
case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ (LocalHomeomorph.restr e e'.source).toLocalEquiv.source = e'.source ∩ e.source
[PROOFSTEP]
rw [e.restr_source' _ e'.open_source]
[GOAL]
case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ e.source ∩ e'.source = e'.source ∩ e.source
[PROOFSTEP]
exact Set.inter_comm _ _
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑(LocalHomeomorph.restr e e'.source)) (↑(LocalHomeomorph.restr e' e.source))
    (LocalHomeomorph.restr e e'.source).toLocalEquiv.source
[PROOFSTEP]
rw [e.restr_source' _ e'.open_source]
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑(LocalHomeomorph.restr e e'.source)) (↑(LocalHomeomorph.restr e' e.source)) (e.source ∩ e'.source)
[PROOFSTEP]
refine' (EqOn.trans _ h).trans _
[GOAL]
case right.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑(LocalHomeomorph.restr e e'.source)) (↑e) (e.source ∩ e'.source)
[PROOFSTEP]
simp only [mfld_simps, eqOn_refl]
[GOAL]
case right.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑e') (↑(LocalHomeomorph.restr e' e.source)) (e.source ∩ e'.source)
[PROOFSTEP]
simp only [mfld_simps, eqOn_refl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
[PROOFSTEP]
obtain ⟨⟨x, y⟩, -⟩ := id h
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
x : α
y : γ
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
[PROOFSTEP]
haveI : Nonempty α := ⟨x⟩
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
x : α
y : γ
this : Nonempty α
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
[PROOFSTEP]
haveI : Nonempty β := ⟨e₁ x⟩
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
x : α
y : γ
this✝ : Nonempty α
this : Nonempty β
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
[PROOFSTEP]
haveI : Nonempty γ := ⟨y⟩
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
x : α
y : γ
this✝¹ : Nonempty α
this✝ : Nonempty β
this : Nonempty γ
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
[PROOFSTEP]
haveI : Nonempty δ := ⟨e₂ y⟩
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
x : α
y : γ
this✝² : Nonempty α
this✝¹ : Nonempty β
this✝ : Nonempty γ
this : Nonempty δ
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
[PROOFSTEP]
simp_rw [LocalHomeomorph.ext_iff, prod_apply, prod_symm_apply, prod_source, Prod.ext_iff,
  Set.prod_eq_prod_iff_of_nonempty h, forall_and, Prod.forall, forall_const, and_assoc, and_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁' e₂').toLocalEquiv.source
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
[PROOFSTEP]
rw [eq_comm, prod_eq_prod_of_nonempty h, eq_comm, @eq_comm _ e₂']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
inst✝¹ : (x : α) → Decidable (x ∈ e.source)
inst✝ : (y : β) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
⊢ e.source ∩ frontier e.source = e'.source ∩ frontier e.source
[PROOFSTEP]
rw [e.open_source.inter_frontier_eq, (Hs.symm.frontier_right e'.open_source).inter_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
inst✝¹ : (x : α) → Decidable (x ∈ e.source)
inst✝ : (y : β) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
⊢ EqOn (↑e) (↑e') (e.source ∩ frontier e.source)
[PROOFSTEP]
rw [e.open_source.inter_frontier_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
inst✝¹ : (x : α) → Decidable (x ∈ e.source)
inst✝ : (y : β) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
⊢ EqOn ↑e ↑e' ∅
[PROOFSTEP]
exact eqOn_empty _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
x : β
h : x ∈ e.target
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' s) (↑(LocalHomeomorph.symm e) x)
[PROOFSTEP]
simp_rw [ContinuousWithinAt, ← @tendsto_map'_iff _ _ _ _ e, e.map_nhdsWithin_preimage_eq (e.map_target h), (· ∘ ·),
  e.right_inv h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
x : β
h : x ∈ e.target
⊢ ContinuousAt f x ↔ ContinuousAt (f ∘ ↑e) (↑(LocalHomeomorph.symm e) x)
[PROOFSTEP]
rw [← continuousWithinAt_univ, e.continuousWithinAt_iff_continuousWithinAt_comp_right h, preimage_univ,
  continuousWithinAt_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
h : s ⊆ e.target
⊢ ContinuousOn f s ↔ ContinuousOn (f ∘ ↑e) (e.source ∩ ↑e ⁻¹' s)
[PROOFSTEP]
simp only [← e.symm_image_eq_source_inter_preimage h, ContinuousOn, ball_image_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
h : s ⊆ e.target
⊢ (∀ (x : β), x ∈ s → ContinuousWithinAt f s x) ↔
    ∀ (x : β), x ∈ s → ContinuousWithinAt (f ∘ ↑e) (↑(LocalHomeomorph.symm e) '' s) (↑(LocalHomeomorph.symm e) x)
[PROOFSTEP]
refine' forall₂_congr fun x hx => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
h : s ⊆ e.target
x : β
hx : x ∈ s
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑(LocalHomeomorph.symm e) '' s) (↑(LocalHomeomorph.symm e) x)
[PROOFSTEP]
rw [e.continuousWithinAt_iff_continuousWithinAt_comp_right (h hx), e.symm_image_eq_source_inter_preimage h, inter_comm,
  continuousWithinAt_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
h : s ⊆ e.target
x : β
hx : x ∈ s
⊢ e.source ∈ 𝓝 (↑(LocalHomeomorph.symm e) x)
[PROOFSTEP]
exact IsOpen.mem_nhds e.open_source (e.map_target (h hx))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
s : Set γ
x : γ
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (↑e ∘ f) s x
[PROOFSTEP]
refine' ⟨(e.continuousAt hx).comp_continuousWithinAt, fun fe_cont => _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
s : Set γ
x : γ
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) s x
⊢ ContinuousWithinAt f s x
[PROOFSTEP]
rw [← continuousWithinAt_inter' h] at fe_cont ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
s : Set γ
x : γ
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x
⊢ ContinuousWithinAt f (s ∩ f ⁻¹' e.source) x
[PROOFSTEP]
have : ContinuousWithinAt (e.symm ∘ e ∘ f) (s ∩ f ⁻¹' e.source) x :=
  haveI : ContinuousWithinAt e.symm univ (e (f x)) := (e.continuousAt_symm (e.map_source hx)).continuousWithinAt
  ContinuousWithinAt.comp this fe_cont (subset_univ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
s : Set γ
x : γ
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt (↑(LocalHomeomorph.symm e) ∘ ↑e ∘ f) (s ∩ f ⁻¹' e.source) x
⊢ ContinuousWithinAt f (s ∩ f ⁻¹' e.source) x
[PROOFSTEP]
exact this.congr (fun y hy => by simp [e.left_inv hy.2]) (by simp [e.left_inv hx])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
s : Set γ
x : γ
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt (↑(LocalHomeomorph.symm e) ∘ ↑e ∘ f) (s ∩ f ⁻¹' e.source) x
y : γ
hy : y ∈ s ∩ f ⁻¹' e.source
⊢ f y = (↑(LocalHomeomorph.symm e) ∘ ↑e ∘ f) y
[PROOFSTEP]
simp [e.left_inv hy.2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
s : Set γ
x : γ
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt (↑(LocalHomeomorph.symm e) ∘ ↑e ∘ f) (s ∩ f ⁻¹' e.source) x
⊢ f x = (↑(LocalHomeomorph.symm e) ∘ ↑e ∘ f) x
[PROOFSTEP]
simp [e.left_inv hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
x : γ
h : f ⁻¹' e.source ∈ 𝓝 x
⊢ ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x
[PROOFSTEP]
have hx : f x ∈ e.source := (mem_of_mem_nhds h : _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
x : γ
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
⊢ ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x
[PROOFSTEP]
have h' : f ⁻¹' e.source ∈ 𝓝[univ] x := by rwa [nhdsWithin_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
x : γ
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
⊢ f ⁻¹' e.source ∈ 𝓝[univ] x
[PROOFSTEP]
rwa [nhdsWithin_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
x : γ
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
h' : f ⁻¹' e.source ∈ 𝓝[univ] x
⊢ ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x
[PROOFSTEP]
rw [← continuousWithinAt_univ, ← continuousWithinAt_univ, e.continuousWithinAt_iff_continuousWithinAt_comp_left hx h']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
h : f ⁻¹' e.source = univ
⊢ Continuous f ↔ Continuous (↑e ∘ f)
[PROOFSTEP]
simp only [continuous_iff_continuousOn_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
h : f ⁻¹' e.source = univ
⊢ ContinuousOn f univ ↔ ContinuousOn (↑e ∘ f) univ
[PROOFSTEP]
exact e.continuousOn_iff_continuousOn_comp_left (Eq.symm h).subset
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
x : α
hx : x ∈ e.source
⊢ 𝓝 x = comap (↑e) (𝓝 (↑e x)) ⊓ 𝓟 e.source
[PROOFSTEP]
lift x to e.source using hx
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
x : { x // x ∈ e.source }
⊢ 𝓝 ↑x = comap (↑e) (𝓝 (↑e ↑x)) ⊓ 𝓟 e.source
[PROOFSTEP]
rw [← e.open_source.nhdsWithin_eq x.2, ← map_nhds_subtype_val, ← map_comap_setCoe_val,
  e.toHomeomorphSourceTarget.nhds_eq_comap, nhds_subtype_eq_comap]
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
x : { x // x ∈ e.source }
⊢ map Subtype.val (comap (↑(toHomeomorphSourceTarget e)) (comap Subtype.val (𝓝 ↑(↑(toHomeomorphSourceTarget e) x)))) =
    map Subtype.val (comap Subtype.val (comap (↑e) (𝓝 (↑e ↑x))))
[PROOFSTEP]
simp only [(· ∘ ·), toHomeomorphSourceTarget_apply_coe, comap_comap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
h' : e.target = univ
x : α
⊢ x ∈ e.source
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
h' : e.target = univ
x : α
⊢ x ∈ univ
[PROOFSTEP]
exact mem_univ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
h' : e.target = univ
x : β
⊢ x ∈ e.target
[PROOFSTEP]
rw [h']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
h' : e.target = univ
x : β
⊢ x ∈ univ
[PROOFSTEP]
exact mem_univ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
h' : e.target = univ
⊢ Continuous
    { toFun := ↑e, invFun := ↑(LocalHomeomorph.symm e),
        left_inv := (_ : ∀ (x : α), ↑(LocalHomeomorph.symm e) (↑e x) = x),
        right_inv := (_ : ∀ (x : β), ↑e (↑(LocalHomeomorph.symm e) x) = x) }.toFun
[PROOFSTEP]
simpa only [continuous_iff_continuousOn_univ, h] using e.continuousOn
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
h' : e.target = univ
⊢ Continuous
    { toFun := ↑e, invFun := ↑(LocalHomeomorph.symm e),
        left_inv := (_ : ∀ (x : α), ↑(LocalHomeomorph.symm e) (↑e x) = x),
        right_inv := (_ : ∀ (x : β), ↑e (↑(LocalHomeomorph.symm e) x) = x) }.invFun
[PROOFSTEP]
simpa only [continuous_iff_continuousOn_univ, h'] using e.continuousOn_symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ OpenEmbedding ↑e
[PROOFSTEP]
apply openEmbedding_of_continuous_injective_open
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ Continuous ↑e
[PROOFSTEP]
apply continuous_iff_continuousOn_univ.mpr
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ ContinuousOn (↑e) univ
[PROOFSTEP]
rw [← h]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ ContinuousOn (↑e) e.source
[PROOFSTEP]
exact e.continuousOn
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ Injective ↑e
[PROOFSTEP]
apply Set.injective_iff_injOn_univ.mpr
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ InjOn (↑e) univ
[PROOFSTEP]
rw [← h]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ InjOn (↑e) e.source
[PROOFSTEP]
exact e.injOn
[GOAL]
case h₃
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ IsOpenMap ↑e
[PROOFSTEP]
intro U hU
[GOAL]
case h₃
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
U : Set α
hU : IsOpen U
⊢ IsOpen (↑e '' U)
[PROOFSTEP]
simpa only [h, subset_univ, mfld_simps] using e.image_open_of_open hU
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
⊢ (localHomeomorphSubtypeCoe s).toLocalEquiv.target = ↑s
[PROOFSTEP]
simp only [localHomeomorphSubtypeCoe, Subtype.range_coe_subtype, mfld_simps]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
⊢ {x | x ∈ s.carrier} = ↑s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
⊢ (subtypeRestr e s).toLocalEquiv.source = Subtype.val ⁻¹' e.source
[PROOFSTEP]
simp only [subtypeRestr_def, mfld_simps]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
x : { x // x ∈ s }
hxe : ↑x ∈ e.source
⊢ ↑e ↑x ∈ (subtypeRestr e s).toLocalEquiv.target
[PROOFSTEP]
refine' ⟨e.map_source hxe, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
x : { x // x ∈ s }
hxe : ↑x ∈ e.source
⊢ ↑e ↑x ∈ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe s).toLocalEquiv.target
[PROOFSTEP]
rw [s.localHomeomorphSubtypeCoe_target, mem_preimage, e.leftInvOn hxe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
x : { x // x ∈ s }
hxe : ↑x ∈ e.source
⊢ ↑x ∈ ↑s
[PROOFSTEP]
exact x.prop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
⊢ LocalHomeomorph.trans (LocalHomeomorph.symm (subtypeRestr f s)) (subtypeRestr f' s) ≈
    LocalHomeomorph.restr (LocalHomeomorph.trans (LocalHomeomorph.symm f) f')
      (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
[PROOFSTEP]
simp only [subtypeRestr_def, trans_symm_eq_symm_trans_symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
⊢ LocalHomeomorph.trans
      (LocalHomeomorph.trans (LocalHomeomorph.symm f) (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe s)))
      (LocalHomeomorph.trans (Opens.localHomeomorphSubtypeCoe s) f') ≈
    LocalHomeomorph.restr (LocalHomeomorph.trans (LocalHomeomorph.symm f) f')
      (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
[PROOFSTEP]
have openness₁ : IsOpen (f.target ∩ f.symm ⁻¹' s) := f.preimage_open_of_open_symm s.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
⊢ LocalHomeomorph.trans
      (LocalHomeomorph.trans (LocalHomeomorph.symm f) (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe s)))
      (LocalHomeomorph.trans (Opens.localHomeomorphSubtypeCoe s) f') ≈
    LocalHomeomorph.restr (LocalHomeomorph.trans (LocalHomeomorph.symm f) f')
      (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
[PROOFSTEP]
rw [← ofSet_trans _ openness₁, ← trans_assoc, ← trans_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
⊢ LocalHomeomorph.trans
      (LocalHomeomorph.trans
        (LocalHomeomorph.trans (LocalHomeomorph.symm f) (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe s)))
        (Opens.localHomeomorphSubtypeCoe s))
      f' ≈
    LocalHomeomorph.trans
      (LocalHomeomorph.trans (ofSet (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) openness₁) (LocalHomeomorph.symm f))
      f'
[PROOFSTEP]
refine'
  EqOnSource.trans' _
    (eqOnSource_refl _)
      -- f' has been eliminated !!!
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
⊢ LocalHomeomorph.trans
      (LocalHomeomorph.trans (LocalHomeomorph.symm f) (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe s)))
      (Opens.localHomeomorphSubtypeCoe s) ≈
    LocalHomeomorph.trans (ofSet (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) openness₁) (LocalHomeomorph.symm f)
[PROOFSTEP]
have sets_identity : f.symm.source ∩ (f.target ∩ f.symm ⁻¹' s) = f.symm.source ∩ f.symm ⁻¹' s := by mfld_set_tac
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
⊢ (LocalHomeomorph.symm f).toLocalEquiv.source ∩ (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) =
    (LocalHomeomorph.symm f).toLocalEquiv.source ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s
[PROOFSTEP]
mfld_set_tac
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
sets_identity :
  (LocalHomeomorph.symm f).toLocalEquiv.source ∩ (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) =
    (LocalHomeomorph.symm f).toLocalEquiv.source ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s
⊢ LocalHomeomorph.trans
      (LocalHomeomorph.trans (LocalHomeomorph.symm f) (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe s)))
      (Opens.localHomeomorphSubtypeCoe s) ≈
    LocalHomeomorph.trans (ofSet (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) openness₁) (LocalHomeomorph.symm f)
[PROOFSTEP]
have openness₂ : IsOpen (s : Set α) := s.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
sets_identity :
  (LocalHomeomorph.symm f).toLocalEquiv.source ∩ (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) =
    (LocalHomeomorph.symm f).toLocalEquiv.source ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s
openness₂ : IsOpen ↑s
⊢ LocalHomeomorph.trans
      (LocalHomeomorph.trans (LocalHomeomorph.symm f) (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe s)))
      (Opens.localHomeomorphSubtypeCoe s) ≈
    LocalHomeomorph.trans (ofSet (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) openness₁) (LocalHomeomorph.symm f)
[PROOFSTEP]
rw [ofSet_trans', sets_identity, ← trans_of_set' _ openness₂, trans_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
sets_identity :
  (LocalHomeomorph.symm f).toLocalEquiv.source ∩ (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) =
    (LocalHomeomorph.symm f).toLocalEquiv.source ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s
openness₂ : IsOpen ↑s
⊢ LocalHomeomorph.trans (LocalHomeomorph.symm f)
      (LocalHomeomorph.trans (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe s))
        (Opens.localHomeomorphSubtypeCoe s)) ≈
    LocalHomeomorph.trans (LocalHomeomorph.symm f) (ofSet (↑s) openness₂)
[PROOFSTEP]
refine'
  EqOnSource.trans' (eqOnSource_refl _)
    _
      -- f has been eliminated !!!
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
sets_identity :
  (LocalHomeomorph.symm f).toLocalEquiv.source ∩ (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) =
    (LocalHomeomorph.symm f).toLocalEquiv.source ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s
openness₂ : IsOpen ↑s
⊢ LocalHomeomorph.trans (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe s)) (Opens.localHomeomorphSubtypeCoe s) ≈
    ofSet (↑s) openness₂
[PROOFSTEP]
refine' Setoid.trans (trans_symm_self s.localHomeomorphSubtypeCoe) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
sets_identity :
  (LocalHomeomorph.symm f).toLocalEquiv.source ∩ (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) =
    (LocalHomeomorph.symm f).toLocalEquiv.source ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s
openness₂ : IsOpen ↑s
⊢ ofSet (Opens.localHomeomorphSubtypeCoe s).toLocalEquiv.target
      (_ : IsOpen (Opens.localHomeomorphSubtypeCoe s).toLocalEquiv.target) ≈
    ofSet (↑s) openness₂
[PROOFSTEP]
simp only [mfld_simps, Setoid.refl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
⊢ EqOn (↑(LocalHomeomorph.symm (subtypeRestr e V))) (inclusion hUV ∘ ↑(LocalHomeomorph.symm (subtypeRestr e U)))
    (subtypeRestr e U).toLocalEquiv.target
[PROOFSTEP]
set i := Set.inclusion hUV
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
⊢ EqOn (↑(LocalHomeomorph.symm (subtypeRestr e V))) (i ∘ ↑(LocalHomeomorph.symm (subtypeRestr e U)))
    (subtypeRestr e U).toLocalEquiv.target
[PROOFSTEP]
intro y hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ (subtypeRestr e U).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm (subtypeRestr e V)) y = (i ∘ ↑(LocalHomeomorph.symm (subtypeRestr e U))) y
[PROOFSTEP]
dsimp [LocalHomeomorph.subtypeRestr_def] at hy ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe V)) (↑(LocalHomeomorph.symm e) y) =
    inclusion hUV (↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe U)) (↑(LocalHomeomorph.symm e) y))
[PROOFSTEP]
have hyV : e.symm y ∈ V.localHomeomorphSubtypeCoe.target :=
  by
  rw [Opens.localHomeomorphSubtypeCoe_target] at hy ⊢
  exact hUV hy.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
[PROOFSTEP]
rw [Opens.localHomeomorphSubtypeCoe_target] at hy ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' ↑U
⊢ ↑(LocalHomeomorph.symm e) y ∈ ↑V
[PROOFSTEP]
exact hUV hy.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
hyV : ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe V)) (↑(LocalHomeomorph.symm e) y) =
    inclusion hUV (↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe U)) (↑(LocalHomeomorph.symm e) y))
[PROOFSTEP]
refine' V.localHomeomorphSubtypeCoe.injOn _ trivial _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
hyV : ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe V)) (↑(LocalHomeomorph.symm e) y) ∈
    (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.source
[PROOFSTEP]
rw [← LocalHomeomorph.symm_target]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
hyV : ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe V)) (↑(LocalHomeomorph.symm e) y) ∈
    (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe V)).toLocalEquiv.target
[PROOFSTEP]
apply LocalHomeomorph.map_source
[GOAL]
case refine'_1.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
hyV : ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm e) y ∈ (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe V)).toLocalEquiv.source
[PROOFSTEP]
rw [LocalHomeomorph.symm_source]
[GOAL]
case refine'_1.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
hyV : ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
[PROOFSTEP]
exact hyV
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
hyV : ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
⊢ ↑(Opens.localHomeomorphSubtypeCoe V)
      (↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe V)) (↑(LocalHomeomorph.symm e) y)) =
    ↑(Opens.localHomeomorphSubtypeCoe V)
      (inclusion hUV (↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe U)) (↑(LocalHomeomorph.symm e) y)))
[PROOFSTEP]
rw [V.localHomeomorphSubtypeCoe.right_inv hyV]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
hyV : ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm e) y =
    ↑(Opens.localHomeomorphSubtypeCoe V)
      (inclusion hUV (↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe U)) (↑(LocalHomeomorph.symm e) y)))
[PROOFSTEP]
show _ = U.localHomeomorphSubtypeCoe _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
hyV : ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm e) y =
    ↑(Opens.localHomeomorphSubtypeCoe U)
      (↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe U)) (↑(LocalHomeomorph.symm e) y))
[PROOFSTEP]
rw [U.localHomeomorphSubtypeCoe.right_inv hy.2]
