-- Mathlib/Topology/PartialHomeomorph.lean
theorem continuousWithinAt_iff_continuousWithinAt_comp_left {f : Z → X} {s : Set Z} {x : Z}
    (hx : f x ∈ e.source) (h : f ⁻¹' e.source ∈ 𝓝[s] x) :
    ContinuousWithinAt f s x ↔ ContinuousWithinAt (e ∘ f) s x

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt (↑e.symm ∘ ↑e ∘ f) (s ∩ f ⁻¹' e.source) x
⊢ ContinuousWithinAt f (s ∩ f ⁻¹' e.source) x

Tactic:
exact this.congr (fun y hy => by simp [e.left_inv hy.2]) (by simp [e.left_inv hx])

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt (↑e.symm ∘ ↑e ∘ f) (s ∩ f ⁻¹' e.source) x
y : Z
hy : y ∈ s ∩ f ⁻¹' e.source
⊢ f y = (↑e.symm ∘ ↑e ∘ f) y

Tactic:
simp [e.left_inv hy.2]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
s : Set Z
x : Z
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

Tactic:
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 _)

Result:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt (↑e.symm ∘ ↑e ∘ f) (s ∩ f ⁻¹' e.source) x
⊢ ContinuousWithinAt f (s ∩ f ⁻¹' e.source) x

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (↑e ∘ f) s x

Tactic:
refine ⟨(e.continuousAt hx).comp_continuousWithinAt, fun fe_cont => ?_⟩

Result:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) s x
⊢ ContinuousWithinAt f s x

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt (↑e.symm ∘ ↑e ∘ f) (s ∩ f ⁻¹' e.source) x
⊢ f x = (↑e.symm ∘ ↑e ∘ f) x

Tactic:
simp [e.left_inv hx]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) s x
⊢ ContinuousWithinAt f s x

Tactic:
rw [← continuousWithinAt_inter' h] at fe_cont ⊢

Result:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
s : Set Z
x : Z
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