awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
h_1 : s ⊆ f ⁻¹' e'.source
hfx : f x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
y : H
hy : y ∈ s ∧ y ∈ e.source ∧ (↑e : H → H) y ∈ e'.source
⊢ ((↑e' : H → H) ∘ f) y = (↑(e ≫ₕ e').toPartialEquiv : H → H) y

Tactic:
simp only [hef ⟨hy.1, hy.2.1⟩, mfld_simps]

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
h_1 : s ⊆ f ⁻¹' e'.source
hfx : f x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
⊢ x ∈ (e ≫ₕ e').source

Tactic:
simpa only [hex, hef ⟨hx, hex⟩, mfld_simps] using hfx

Premises used: And.intro
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
mp :
  G.IsLocalStructomorphWithinAt (↑f : H → H) s x →
    x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source
mpr :
  (x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source) →
    G.IsLocalStructomorphWithinAt (↑f : H → H) s x
⊢ G.IsLocalStructomorphWithinAt (↑f : H → H) s x ↔
    x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f : H → H) s x
h2x : x ∈ s
mp :
  ∀ (e : OpenPartialHomeomorph H H) (he : e ∈ G) (hfe : EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source))
    (hxe : x ∈ e.source), ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source
⊢ ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
obtain ⟨e, he, hfe, hxe⟩ := hf h2x
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f : H → H) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hxe : x ∈ e.source
⊢ ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
⟨e.restr f.source, closedUnderRestriction' he f.open_source, ?_, ?_, hxe, ?_⟩

Premises used: OpenPartialHomeomorph.open_source, And.intro, Exists.intro, PartialEquiv.source, OpenPartialHomeomorph.toPartialEquiv, closedUnderRestriction', OpenPartialHomeomorph.restr
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f : H → H) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hxe : x ∈ e.source
mp : (e.restr f.source).source ⊆ f.source
mp₁ : EqOn (↑f : H → H) (↑(e.restr f.source) : H → H) (s ∩ (e.restr f.source).source)
mp₂ : x ∈ interior f.source
⊢ ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
refine ⟨e.restr f.source, closedUnderRestriction' he f.open_source, ?_, ?_, hxe, ?_⟩
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f : H → H) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hxe : x ∈ e.source
⊢ e.source ∩ interior f.source ⊆ f.source

Tactic:
inter_subset_right.trans interior_subset

Premises used: interior_subset, HasSubset.Subset.trans, Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f : H → H) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hxe : x ∈ e.source
⊢ e.source ∩ interior f.source ⊆ f.source

Tactic:
exact inter_subset_right.trans interior_subset

Premises used: interior_subset, HasSubset.Subset.trans, Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f : H → H) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hxe : x ∈ e.source
x' : H
hx' : x' ∈ s ∩ (e.restr f.source).source
⊢ (↑f : H → H) x' = (↑(e.restr f.source) : H → H) x'

Tactic:
hfe ⟨hx'.1, hx'.2.1⟩

Premises used: OpenPartialHomeomorph.toFun', And.right, And.left, And.intro
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f : H → H) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hxe : x ∈ e.source
x' : H
hx' : x' ∈ s ∩ (e.restr f.source).source
⊢ (↑f : H → H) x' = (↑(e.restr f.source) : H → H) x'

Tactic:
exact hfe ⟨hx'.1, hx'.2.1⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f : H → H) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hxe : x ∈ e.source
mp : x ∈ f.source
⊢ x ∈ interior f.source

Tactic:
rw [f.open_source.interior_eq]

Premises used: OpenPartialHomeomorph.open_source, IsOpen.interior_eq
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f : H → H) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hxe : x ∈ e.source
⊢ x ∈ f.source

Tactic:
Or.resolve_right hx (not_not.mpr h2x)

Premises used: Iff.mpr, Classical.not_not, Or.resolve_right
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f : H → H) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hxe : x ∈ e.source
⊢ x ∈ f.source

Tactic:
exact Or.resolve_right hx (not_not.mpr h2x)

Premises used: Iff.mpr, Classical.not_not, Or.resolve_right
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx_1 : x ∈ f.source ∪ sᶜ
hf : x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source
hx : x ∈ s
mpr :
  ∀ (e : OpenPartialHomeomorph H H) (he : e ∈ G),
    e.source ⊆ f.source →
      ∀ (hfe : EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source)) (hxe : x ∈ e.source),
        ∃ e ∈ G, EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
⊢ ∃ e ∈ G, EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
obtain ⟨e, he, _, hfe, hxe⟩ := hf hx
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx_1 : x ∈ f.source ∪ sᶜ
hf : x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source
hx : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
left : e.source ⊆ f.source
hfe : EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source)
hxe : x ∈ e.source
⊢ ∃ e ∈ G, EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
⟨e, he, hfe, hxe⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx_1 : x ∈ f.source ∪ sᶜ
hf : x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source
hx : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
left : e.source ⊆ f.source
hfe : EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source)
hxe : x ∈ e.source
⊢ ∃ e ∈ G, EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
exact ⟨e, he, hfe, hxe⟩
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hs : f.source ⊆ s
hx : x ∈ f.source ∪ sᶜ
rw :
  (x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source) ↔
    x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source
⊢ G.IsLocalStructomorphWithinAt (↑f : H → H) s x ↔
    x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source

Tactic:
rw [f.isLocalStructomorphWithinAt_iff hx]

Premises used: OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hs : f.source ⊆ s
hx : x ∈ f.source ∪ sᶜ
⊢ (x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source) ↔
    x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source

Tactic:
imp_congr_right fun _ ↦ exists_congr fun e ↦ and_congr_right fun _ ↦ ?_

Premises used: imp_congr_right, and_congr_right, exists_congr
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hs : f.source ⊆ s
hx : x ∈ f.source ∪ sᶜ
refine :
  x ∈ s →
    ∀ e ∈ G,
      e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source ↔
        e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source
⊢ (x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source) ↔
    x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source

Tactic:
refine imp_congr_right fun _ ↦ exists_congr fun e ↦ and_congr_right fun _ ↦ ?_

Premises used: imp_congr_right, and_congr_right, exists_congr
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hs : f.source ⊆ s
hx : x ∈ f.source ∪ sᶜ
h : x ∈ s
e : OpenPartialHomeomorph H H
h_1 : e ∈ G
⊢ e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source ↔
    e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source

Tactic:
and_congr_right fun h2e ↦ ?_

Premises used: and_congr_right
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hs : f.source ⊆ s
hx : x ∈ f.source ∪ sᶜ
h : x ∈ s
e : OpenPartialHomeomorph H H
h_1 : e ∈ G
refine :
  ∀ (h2e : e.source ⊆ f.source),
    EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source ↔
      EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source
⊢ e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source ↔
    e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source

Tactic:
refine and_congr_right fun h2e ↦ ?_

Premises used: and_congr_right
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hs : f.source ⊆ s
hx : x ∈ f.source ∪ sᶜ
h : x ∈ s
e : OpenPartialHomeomorph H H
h_1 : e ∈ G
h2e : e.source ⊆ f.source
rw rw₁ : EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source ↔ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source
⊢ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source ↔ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source

Tactic:
rw [inter_eq_right.mpr (h2e.trans hs)]

Premises used: Iff.mpr, HasSubset.Subset.trans, Set.inter_eq_right
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
x : H
simp_rw : Membership.mem (γ := Set H) univ x
⊢ x ∈ f.source ∪ f.sourceᶜ

Tactic:
simp_rw [union_compl_self, mem_univ]

Premises used: Set.union_compl_self, Set.mem_univ
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
apply :
  ∀ x ∈ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').source,
    ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
⊢ (e ≫ₕ f).symm ≫ₕ e' ≫ₕ f' ∈ G₁

Tactic:
apply G₁.locality

Premises used: StructureGroupoid.locality
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx : x ∈ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').source
⊢ (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source

Tactic:
simp only [mfld_simps] at hx
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
⊢ x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source

Tactic:
simp only [hx, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
⊢ x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source

Tactic:
have hxs : x ∈ f.symm ⁻¹' (e.symm ≫ₕ e').source := by simp only [hx, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
⊢ x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)

Tactic:
simp only [hx, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
⊢ x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)

Tactic:
have hxs' : x ∈ f.target ∩
          f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ e.symm ≫ₕ e' ⁻¹' f'.source) := by
        simp only [hx, mfld_simps]