-- Mathlib/Topology/IsLocalHomeomorph.lean
theorem of_comp_right (hgf : IsLocalHomeomorphOn (g ∘ f) s) (hf : IsLocalHomeomorphOn f s) :
    IsLocalHomeomorphOn g (f '' s) := mk g _ <| by
  rintro _ ⟨x, hx, rfl⟩
  obtain ⟨f, hxf, rfl⟩ := hf x hx
  obtain ⟨gf, hgf, he⟩ := hgf x hx
  refine ⟨f.symm.trans gf, ⟨f.map_source hxf, ?_⟩, fun y hy ↦ ?_⟩
  · apply (f.left_inv hxf).symm ▸ hgf
  · change g y = gf (f.symm y)
    rw [← he, Function.comp_apply, f.right_inv hy.1]

Proof state:
case intro.intro.intro.intro.intro.intro.refine_1
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ ↑f = ↑gf
⊢ ↑f x ∈ ↑f.symm.symm.symm ⁻¹' gf.source

Tactic:
apply (f.left_inv hxf).symm ▸ hgf

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
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hgf : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
⊢ ∃ e, ↑f x ∈ e.source ∧ Set.EqOn g (↑e) e.source

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

Result:
case intro.intro.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
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ ↑f = ↑gf
⊢ ∃ e, ↑f x ∈ e.source ∧ Set.EqOn g (↑e) e.source

Proof state:
case intro.intro.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
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ ↑f = ↑gf
⊢ ∃ e, ↑f x ∈ e.source ∧ Set.EqOn g (↑e) e.source

Tactic:
refine ⟨f.symm.trans gf, ⟨f.map_source hxf, ?_⟩, fun y hy ↦ ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.refine_1
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ ↑f = ↑gf
⊢ ↑f x ∈ ↑f.symm.symm.symm ⁻¹' gf.source

case intro.intro.intro.intro.intro.intro.refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ ↑f = ↑gf
y : Y
hy : y ∈ (f.symm.trans gf).source
⊢ g y = ↑(f.symm.trans gf) y

Proof state:
case intro.intro.intro.intro.intro.intro.refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ ↑f = ↑gf
y : Y
hy : y ∈ (f.symm.trans gf).source
⊢ g y = ↑(f.symm.trans gf) y

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

Result:
case intro.intro.intro.intro.intro.intro.refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ ↑f = ↑gf
y : Y
hy : y ∈ (f.symm.trans gf).source
⊢ g y = ↑gf (↑f.symm y)

Proof state:
case intro.intro.intro.intro.intro.intro.refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
gf : PartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ ↑f = ↑gf
y : Y
hy : y ∈ (f.symm.trans gf).source
⊢ g y = ↑gf (↑f.symm y)

Tactic:
rw [← he, Function.comp_apply, f.right_inv hy.1]

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
hf : IsLocalHomeomorphOn f s
⊢ ∀ x ∈ f '' s, ∃ e, x ∈ e.source ∧ Set.EqOn g (↑e) e.source

Tactic:
rintro _ ⟨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
g : Y → Z
f : X → Y
s : Set X
hgf : IsLocalHomeomorphOn (g ∘ f) s
hf : IsLocalHomeomorphOn f s
x : X
hx : x ∈ s
⊢ ∃ e, f x ∈ e.source ∧ Set.EqOn g (↑e) e.source

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
g : Y → Z
f : X → Y
s : Set X
hgf : IsLocalHomeomorphOn (g ∘ f) s
hf : IsLocalHomeomorphOn f s
x : X
hx : x ∈ s
⊢ ∃ e, f x ∈ e.source ∧ Set.EqOn g (↑e) e.source

Tactic:
obtain ⟨f, hxf, rfl⟩ := hf 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
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hgf : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
⊢ ∃ e, ↑f x ∈ e.source ∧ Set.EqOn g (↑e) e.source