H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
⊢ ∃ s, IsOpen s ∧ x ∈ s ∧ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
⊢ LocalHomeomorph.symm e ≫ₕ e' ∈ G
refine' G.locality fun x hx ↦ _
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
⊢ ∃ s, IsOpen s ∧ x ∈ s ∧ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
⊢ ∃ s, IsOpen s ∧ x ∈ s ∧ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
set f := chartAt (H := H) (e.symm x)
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
⊢ ∃ s, IsOpen s ∧ x ∈ s ∧ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
⊢ ∃ s, IsOpen s ∧ x ∈ s ∧ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
let s := e.target ∩ e.symm ⁻¹' f.source
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
⊢ ∃ s, IsOpen s ∧ x ∈ s ∧ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
⊢ ∃ s, IsOpen s ∧ x ∈ s ∧ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
have hs : IsOpen s := by
  apply e.symm.continuous_toFun.preimage_open_of_open <;> apply open_source
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
⊢ ∃ s, IsOpen s ∧ x ∈ s ∧ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
⊢ ∃ s, IsOpen s ∧ x ∈ s ∧ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
have xs : x ∈ s := by
  simp only [mem_inter_iff, mem_preimage, mem_chart_source, and_true]
  exact ((mem_inter_iff _ _ _).1 hx).1
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
⊢ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
⊢ ∃ s, IsOpen s ∧ x ∈ s ∧ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
refine' ⟨s, hs, xs, _⟩
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
A : LocalHomeomorph.symm e ≫ₕ f ∈ G
⊢ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
⊢ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
have A : e.symm ≫ₕ f ∈ G := (mem_maximalAtlas_iff.1 he f (chart_mem_atlas _ _)).1
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
A : LocalHomeomorph.symm e ≫ₕ f ∈ G
B : LocalHomeomorph.symm f ≫ₕ e' ∈ G
⊢ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
A : LocalHomeomorph.symm e ≫ₕ f ∈ G
⊢ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
have B : f.symm ≫ₕ e' ∈ G := (mem_maximalAtlas_iff.1 he' f (chart_mem_atlas _ _)).2
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
A : LocalHomeomorph.symm e ≫ₕ f ∈ G
B : LocalHomeomorph.symm f ≫ₕ e' ∈ G
C : (LocalHomeomorph.symm e ≫ₕ f) ≫ₕ LocalHomeomorph.symm f ≫ₕ e' ∈ G
⊢ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
A : LocalHomeomorph.symm e ≫ₕ f ∈ G
B : LocalHomeomorph.symm f ≫ₕ e' ∈ G
⊢ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
have C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G := G.trans A B
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
A : LocalHomeomorph.symm e ≫ₕ f ∈ G
B : LocalHomeomorph.symm f ≫ₕ e' ∈ G
C : (LocalHomeomorph.symm e ≫ₕ f) ≫ₕ LocalHomeomorph.symm f ≫ₕ e' ∈ G
D :
  (LocalHomeomorph.symm e ≫ₕ f) ≫ₕ LocalHomeomorph.symm f ≫ₕ e' ≈ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s
⊢ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
A : LocalHomeomorph.symm e ≫ₕ f ∈ G
B : LocalHomeomorph.symm f ≫ₕ e' ∈ G
C : (LocalHomeomorph.symm e ≫ₕ f) ≫ₕ LocalHomeomorph.symm f ≫ₕ e' ∈ G
⊢ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
have D : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ≈ (e.symm ≫ₕ e').restr s := calc
  (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' = e.symm ≫ₕ (f ≫ₕ f.symm) ≫ₕ e' := by simp only [trans_assoc]
  _ ≈ e.symm ≫ₕ ofSet f.source f.open_source ≫ₕ e' :=
    EqOnSource.trans' (refl _) (EqOnSource.trans' (trans_self_symm _) (refl _))
  _ ≈ (e.symm ≫ₕ ofSet f.source f.open_source) ≫ₕ e' := by rw [trans_assoc]
  _ ≈ e.symm.restr s ≫ₕ e' := by rw [trans_of_set']; apply refl
  _ ≈ (e.symm ≫ₕ e').restr s := by rw [restr_trans]
no goals
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
A : LocalHomeomorph.symm e ≫ₕ f ∈ G
B : LocalHomeomorph.symm f ≫ₕ e' ∈ G
C : (LocalHomeomorph.symm e ≫ₕ f) ≫ₕ LocalHomeomorph.symm f ≫ₕ e' ∈ G
D :
  (LocalHomeomorph.symm e ≫ₕ f) ≫ₕ LocalHomeomorph.symm f ≫ₕ e' ≈ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s
⊢ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s ∈ G
exact G.eq_on_source C (Setoid.symm D)
no goals
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
⊢ IsOpen s
apply e.symm.continuous_toFun.preimage_open_of_open <;> apply open_source
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
⊢ x ∈ e.target
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
⊢ x ∈ s
simp only [mem_inter_iff, mem_preimage, mem_chart_source, and_true]
no goals
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
⊢ x ∈ e.target
exact ((mem_inter_iff _ _ _).1 hx).1
no goals
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
A : LocalHomeomorph.symm e ≫ₕ f ∈ G
B : LocalHomeomorph.symm f ≫ₕ e' ∈ G
C : (LocalHomeomorph.symm e ≫ₕ f) ≫ₕ LocalHomeomorph.symm f ≫ₕ e' ∈ G
⊢ (LocalHomeomorph.symm e ≫ₕ f) ≫ₕ LocalHomeomorph.symm f ≫ₕ e' =
    LocalHomeomorph.symm e ≫ₕ (f ≫ₕ LocalHomeomorph.symm f) ≫ₕ e'
simp only [trans_assoc]
no goals
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
A : LocalHomeomorph.symm e ≫ₕ f ∈ G
B : LocalHomeomorph.symm f ≫ₕ e' ∈ G
C : (LocalHomeomorph.symm e ≫ₕ f) ≫ₕ LocalHomeomorph.symm f ≫ₕ e' ∈ G
⊢ LocalHomeomorph.symm e ≫ₕ ofSet f.source (_ : IsOpen f.source) ≫ₕ e' ≈
    (LocalHomeomorph.symm e ≫ₕ ofSet f.source (_ : IsOpen f.source)) ≫ₕ e'
rw [trans_assoc]
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
A : LocalHomeomorph.symm e ≫ₕ f ∈ G
B : LocalHomeomorph.symm f ≫ₕ e' ∈ G
C : (LocalHomeomorph.symm e ≫ₕ f) ≫ₕ LocalHomeomorph.symm f ≫ₕ e' ∈ G
⊢ LocalHomeomorph.restr (LocalHomeomorph.symm e)
        ((LocalHomeomorph.symm e).toLocalEquiv.source ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source) ≫ₕ
      e' ≈
    LocalHomeomorph.restr (LocalHomeomorph.symm e) s ≫ₕ e'
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
A : LocalHomeomorph.symm e ≫ₕ f ∈ G
B : LocalHomeomorph.symm f ≫ₕ e' ∈ G
C : (LocalHomeomorph.symm e ≫ₕ f) ≫ₕ LocalHomeomorph.symm f ≫ₕ e' ∈ G
⊢ (LocalHomeomorph.symm e ≫ₕ ofSet f.source (_ : IsOpen f.source)) ≫ₕ e' ≈
    LocalHomeomorph.restr (LocalHomeomorph.symm e) s ≫ₕ e'
rw [trans_of_set']
no goals
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
A : LocalHomeomorph.symm e ≫ₕ f ∈ G
B : LocalHomeomorph.symm f ≫ₕ e' ∈ G
C : (LocalHomeomorph.symm e ≫ₕ f) ≫ₕ LocalHomeomorph.symm f ≫ₕ e' ∈ G
⊢ LocalHomeomorph.restr (LocalHomeomorph.symm e)
        ((LocalHomeomorph.symm e).toLocalEquiv.source ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source) ≫ₕ
      e' ≈
    LocalHomeomorph.restr (LocalHomeomorph.symm e) s ≫ₕ e'
apply refl
no goals
H : Type u
H' : Type ?u.67678
M : Type u_1
M' : Type ?u.67684
M'' : Type ?u.67687
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : LocalHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
f : LocalHomeomorph M H := chartAt H (↑(LocalHomeomorph.symm e) x)
s : Set H := e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
A : LocalHomeomorph.symm e ≫ₕ f ∈ G
B : LocalHomeomorph.symm f ≫ₕ e' ∈ G
C : (LocalHomeomorph.symm e ≫ₕ f) ≫ₕ LocalHomeomorph.symm f ≫ₕ e' ∈ G
⊢ LocalHomeomorph.restr (LocalHomeomorph.symm e) s ≫ₕ e' ≈ LocalHomeomorph.restr (LocalHomeomorph.symm e ≫ₕ e') s
rw [restr_trans]