H : Type u
H' : Type ?u.33053
M : Type ?u.33056
M' : Type ?u.33059
M'' : Type ?u.33062
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : LocalHomeomorph H H
he' : e ≈ e'
he : Pregroupoid.property PG (↑e) e.source
⊢ Pregroupoid.property PG (↑e') e.source
H : Type u
H' : Type ?u.33053
M : Type ?u.33056
M' : Type ?u.33059
M'' : Type ?u.33062
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : LocalHomeomorph H H
he' : e ≈ e'
he : Pregroupoid.property PG (↑e) e.source
⊢ Pregroupoid.property PG (↑e') e'.source
rw [← he'.1]
no goals
H : Type u
H' : Type ?u.33053
M : Type ?u.33056
M' : Type ?u.33059
M'' : Type ?u.33062
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : LocalHomeomorph H H
he' : e ≈ e'
he : Pregroupoid.property PG (↑e) e.source
⊢ Pregroupoid.property PG (↑e') e.source
exact PG.congr e.open_source he'.eqOn.symm he