H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ P ((g ∘ ↑(LocalHomeomorph.symm e)) ∘ ↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')))
      (↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')) ⁻¹' (↑(LocalHomeomorph.symm e) ⁻¹' s))
      (↑(LocalHomeomorph.symm e ≫ₕ e') (↑e x)) ↔
    P (g ∘ ↑(LocalHomeomorph.symm e')) (↑(LocalHomeomorph.symm e') ⁻¹' s) (↑e' x)

H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ ↑e x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ P (g ∘ ↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x) ↔
    P (g ∘ ↑(LocalHomeomorph.symm e')) (↑(LocalHomeomorph.symm e') ⁻¹' s) (↑e' x)
rw [← hG.right_invariance (compatible_of_mem_maximalAtlas he he')]
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ ↑e x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source

H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ P ((g ∘ ↑(LocalHomeomorph.symm e)) ∘ ↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')))
      (↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')) ⁻¹' (↑(LocalHomeomorph.symm e) ⁻¹' s))
      (↑(LocalHomeomorph.symm e ≫ₕ e') (↑e x)) ↔
    P (g ∘ ↑(LocalHomeomorph.symm e')) (↑(LocalHomeomorph.symm e') ⁻¹' s) (↑e' x)
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ P ((g ∘ ↑(LocalHomeomorph.symm e)) ∘ ↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')))
      (↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')) ⁻¹' (↑(LocalHomeomorph.symm e) ⁻¹' s))
      (↑(LocalHomeomorph.symm e ≫ₕ e') (↑e x)) ↔
    P (g ∘ ↑(LocalHomeomorph.symm e')) (↑(LocalHomeomorph.symm e') ⁻¹' s) (↑e' x)

H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ ↑e x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
swap
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ P ((g ∘ ↑(LocalHomeomorph.symm e)) ∘ ↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')))
      (↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')) ⁻¹' (↑(LocalHomeomorph.symm e) ⁻¹' s)) (↑e' x) ↔
    P (g ∘ ↑(LocalHomeomorph.symm e')) (↑(LocalHomeomorph.symm e') ⁻¹' s) (↑e' x)
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ P ((g ∘ ↑(LocalHomeomorph.symm e)) ∘ ↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')))
      (↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')) ⁻¹' (↑(LocalHomeomorph.symm e) ⁻¹' s))
      (↑(LocalHomeomorph.symm e ≫ₕ e') (↑e x)) ↔
    P (g ∘ ↑(LocalHomeomorph.symm e')) (↑(LocalHomeomorph.symm e') ⁻¹' s) (↑e' x)
simp_rw [LocalHomeomorph.trans_apply, e.left_inv xe]
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ P ?m.17803 (↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')) ⁻¹' (↑(LocalHomeomorph.symm e) ⁻¹' s)) (↑e' x) ↔
    P (g ∘ ↑(LocalHomeomorph.symm e')) (↑(LocalHomeomorph.symm e') ⁻¹' s) (↑e' x)

H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ (g ∘ ↑(LocalHomeomorph.symm e)) ∘ ↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')) =ᶠ[𝓝 (↑e' x)] ?m.17803

H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ H → H'
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ P ((g ∘ ↑(LocalHomeomorph.symm e)) ∘ ↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')))
      (↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')) ⁻¹' (↑(LocalHomeomorph.symm e) ⁻¹' s)) (↑e' x) ↔
    P (g ∘ ↑(LocalHomeomorph.symm e')) (↑(LocalHomeomorph.symm e') ⁻¹' s) (↑e' x)
rw [hG.congr_iff]
no goals
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ ↑e x ∈ (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source
simp only [xe, xe', mfld_simps]
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ ↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')) ⁻¹' (↑(LocalHomeomorph.symm e) ⁻¹' s) =ᶠ[𝓝 (↑e' x)]
    ↑(LocalHomeomorph.symm e') ⁻¹' s
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ P ?m.17803 (↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')) ⁻¹' (↑(LocalHomeomorph.symm e) ⁻¹' s)) (↑e' x) ↔
    P (g ∘ ↑(LocalHomeomorph.symm e')) (↑(LocalHomeomorph.symm e') ⁻¹' s) (↑e' x)
refine' hG.congr_set _
case refine'_1
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ ↑(LocalHomeomorph.symm e') ⁻¹' e.source ∈ 𝓝 (↑e' x)

case refine'_2
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
y : H
hy : y ∈ ↑(LocalHomeomorph.symm e') ⁻¹' e.source
⊢ y ∈ ↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')) ⁻¹' (↑(LocalHomeomorph.symm e) ⁻¹' s) ↔
    y ∈ ↑(LocalHomeomorph.symm e') ⁻¹' s
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ ↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')) ⁻¹' (↑(LocalHomeomorph.symm e) ⁻¹' s) =ᶠ[𝓝 (↑e' x)]
    ↑(LocalHomeomorph.symm e') ⁻¹' s
refine' (eventually_of_mem _ fun y (hy : y ∈ e'.symm ⁻¹' e.source) ↦ _).set_eq
no goals
case refine'_2
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
y : H
hy : y ∈ ↑(LocalHomeomorph.symm e') ⁻¹' e.source
⊢ y ∈ ↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')) ⁻¹' (↑(LocalHomeomorph.symm e) ⁻¹' s) ↔
    y ∈ ↑(LocalHomeomorph.symm e') ⁻¹' s
simp_rw [mem_preimage, LocalHomeomorph.coe_trans_symm, LocalHomeomorph.symm_symm,
  Function.comp_apply, e.left_inv hy]
case refine'_1
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ ↑(LocalHomeomorph.symm e') (↑e' x) ∈ e.source
case refine'_1
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ ↑(LocalHomeomorph.symm e') ⁻¹' e.source ∈ 𝓝 (↑e' x)
refine' (e'.symm.continuousAt <| e'.mapsTo xe').preimage_mem_nhds (e.open_source.mem_nhds _)
no goals
case refine'_1
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ ↑(LocalHomeomorph.symm e') (↑e' x) ∈ e.source
simp_rw [e'.left_inv xe', xe]
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
y : H
hy : ↑(LocalHomeomorph.symm e) (↑e (↑(LocalHomeomorph.symm e') y)) = ↑(LocalHomeomorph.symm e') y
⊢ ((g ∘ ↑(LocalHomeomorph.symm e)) ∘ ↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e'))) y =
    (g ∘ ↑(LocalHomeomorph.symm e')) y
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ (g ∘ ↑(LocalHomeomorph.symm e)) ∘ ↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e')) =ᶠ[𝓝 (↑e' x)]
    g ∘ ↑(LocalHomeomorph.symm e')
refine' ((e'.eventually_nhds' _ xe').mpr <| e.eventually_left_inverse xe).mono fun y hy ↦ _
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
y : H
hy : ↑(LocalHomeomorph.symm e) (↑e (↑(LocalHomeomorph.symm e') y)) = ↑(LocalHomeomorph.symm e') y
⊢ g (↑(LocalHomeomorph.symm e) (↑e (↑(LocalHomeomorph.symm e') y))) = g (↑(LocalHomeomorph.symm e') y)
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
y : H
hy : ↑(LocalHomeomorph.symm e) (↑e (↑(LocalHomeomorph.symm e') y)) = ↑(LocalHomeomorph.symm e') y
⊢ ((g ∘ ↑(LocalHomeomorph.symm e)) ∘ ↑(LocalHomeomorph.symm (LocalHomeomorph.symm e ≫ₕ e'))) y =
    (g ∘ ↑(LocalHomeomorph.symm e')) y
simp only [mfld_simps]
no goals
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type ?u.16176
X : Type ?u.16179
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g✝ g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
y : H
hy : ↑(LocalHomeomorph.symm e) (↑e (↑(LocalHomeomorph.symm e') y)) = ↑(LocalHomeomorph.symm e') y
⊢ g (↑(LocalHomeomorph.symm e) (↑e (↑(LocalHomeomorph.symm e') y))) = g (↑(LocalHomeomorph.symm e') y)
rw [hy]