-- Mathlib/Topology/IsLocalHomeomorph.lean
theorem of_comp_left (hgf : IsLocalHomeomorphOn (g ∘ f) s) (hg : IsLocalHomeomorphOn g (f '' s))
    (cont : ∀ x ∈ s, ContinuousAt f x) : IsLocalHomeomorphOn f s := mk f s fun x hx ↦ by
  obtain ⟨g, hxg, rfl⟩ := hg (f x) ⟨x, hx, rfl⟩
  obtain ⟨gf, hgf, he⟩ := hgf x hx
  refine ⟨(gf.restr <| f ⁻¹' g.source).trans g.symm, ⟨⟨hgf, mem_interior_iff_mem_nhds.mpr
    ((cont x hx).preimage_mem_nhds <| g.open_source.mem_nhds hxg)⟩, he ▸ g.map_source hxg⟩,
    fun y hy ↦ ?_⟩
  change f y = g.symm (gf y)
  have : f y ∈ g.source

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : PartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
this : f y ∈ g.source
⊢ (↑g ∘ f) y ∈ g.target

Tactic:
apply g.map_source this

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : PartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
⊢ f y ∈ g.source

Tactic:
apply interior_subset hy.1.2

Result:
no goals

Proof state:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : PartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
⊢ f y = ↑((gf.restr (f ⁻¹' g.source)).trans g.symm) y

Tactic:
change f y = g.symm (gf y)

Result:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : PartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
⊢ f y = ↑g.symm (↑gf y)

Proof state:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : PartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
⊢ ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source

Tactic:
refine ⟨(gf.restr <| f ⁻¹' g.source).trans g.symm, ⟨⟨hgf, mem_interior_iff_mem_nhds.mpr
  ((cont x hx).preimage_mem_nhds <| g.open_source.mem_nhds hxg)⟩, he ▸ g.map_source hxg⟩,
  fun y hy ↦ ?_⟩

Result:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : PartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
⊢ f y = ↑((gf.restr (f ⁻¹' g.source)).trans g.symm) y

Proof state:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : PartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
this : f y ∈ g.source
⊢ f y = ↑g.symm (↑gf y)

Tactic:
rw [← he, g.eq_symm_apply this (by apply g.map_source this), Function.comp_apply]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
hgf : IsLocalHomeomorphOn (g ∘ f) s
hg : IsLocalHomeomorphOn g (f '' s)
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source

Tactic:
obtain ⟨g, hxg, rfl⟩ := hg (f x) ⟨x, hx, rfl⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : PartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
⊢ ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source

Proof state:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : PartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
⊢ f y = ↑g.symm (↑gf y)

Tactic:
have : f y ∈ g.source := by apply interior_subset hy.1.2

Result:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : PartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
this : f y ∈ g.source
⊢ f y = ↑g.symm (↑gf y)

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : PartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
⊢ ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source

Tactic:
obtain ⟨gf, hgf, he⟩ := hgf x hx

Result:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : PartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
⊢ ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source