H : Type u
H' : Type ?u.32686
M : Type ?u.32689
M' : Type ?u.32692
M'' : Type ?u.32695
inst✝ : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), Pregroupoid.property PG₁ f s → Pregroupoid.property PG₂ f s
e : LocalHomeomorph H H
he : e ∈ Pregroupoid.groupoid PG₁
⊢ e ∈ Pregroupoid.groupoid PG₂
H : Type u
H' : Type ?u.32686
M : Type ?u.32689
M' : Type ?u.32692
M'' : Type ?u.32695
inst✝ : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), Pregroupoid.property PG₁ f s → Pregroupoid.property PG₂ f s
⊢ Pregroupoid.groupoid PG₁ ≤ Pregroupoid.groupoid PG₂
refine' StructureGroupoid.le_iff.2 fun e he ↦ _
H : Type u
H' : Type ?u.32686
M : Type ?u.32689
M' : Type ?u.32692
M'' : Type ?u.32695
inst✝ : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), Pregroupoid.property PG₁ f s → Pregroupoid.property PG₂ f s
e : LocalHomeomorph H H
he : Pregroupoid.property PG₁ (↑e) e.source ∧ Pregroupoid.property PG₁ (↑(LocalHomeomorph.symm e)) e.target
⊢ Pregroupoid.property PG₂ (↑e) e.source ∧ Pregroupoid.property PG₂ (↑(LocalHomeomorph.symm e)) e.target
H : Type u
H' : Type ?u.32686
M : Type ?u.32689
M' : Type ?u.32692
M'' : Type ?u.32695
inst✝ : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), Pregroupoid.property PG₁ f s → Pregroupoid.property PG₂ f s
e : LocalHomeomorph H H
he : e ∈ Pregroupoid.groupoid PG₁
⊢ e ∈ Pregroupoid.groupoid PG₂
rw [mem_groupoid_of_pregroupoid] at he⊢
no goals
H : Type u
H' : Type ?u.32686
M : Type ?u.32689
M' : Type ?u.32692
M'' : Type ?u.32695
inst✝ : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), Pregroupoid.property PG₁ f s → Pregroupoid.property PG₂ f s
e : LocalHomeomorph H H
he : Pregroupoid.property PG₁ (↑e) e.source ∧ Pregroupoid.property PG₁ (↑(LocalHomeomorph.symm e)) e.target
⊢ Pregroupoid.property PG₂ (↑e) e.source ∧ Pregroupoid.property PG₂ (↑(LocalHomeomorph.symm e)) e.target
exact ⟨h _ _ he.1, h _ _ he.2⟩