awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
U V : Opens M
hUV : U ≤ V
f : ↥V → M'
x : ↥U
⊢ (↑(chartAt H' (f (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) : M' → H') ∘
      f ∘
        (↑(OpenPartialHomeomorph.symm (chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) :
          H →
            ↥V) =ᶠ[𝓝
      ((↑(chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x)) : ↥V → H)
        (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))]
    (↑(chartAt H' ((f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) x)) : M' → H') ∘
      (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) ∘
        (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U)

Tactic:
exact (TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq hUV).fun_comp
      (chartAt H' (f (Set.inclusion hUV x)) ∘ f)

Premises used: chartAt, TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq, Function.comp, OpenPartialHomeomorph.toFun', Set.inclusion, Filter.EventuallyEq.fun_comp
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U : Opens M
x : ↥U
change : LiftPropAt Q (id ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x
⊢ LiftPropAt Q (Subtype.val (p := fun (x : M) ↦ x ∈ U)) x

Tactic:
change LiftPropAt Q (id ∘ Subtype.val) x

Premises used: Function.comp, id, Subtype.val, ChartedSpace.LiftPropAt
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U : Opens M
x : ↥U
rw : LiftPropAt Q id (↑x : M)
⊢ LiftPropAt Q (id ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x

Tactic:
rw [← hG.liftPropAt_iff_comp_subtype_val]

Premises used: StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_subtype_val
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U : Opens M
x : ↥U
⊢ LiftPropAt Q id (↑x : M)

Tactic:
apply hG.liftProp_id hQ

Premises used: StructureGroupoid.LocalInvariantProp.liftProp_id
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U V : Opens M
hUV : U ≤ V
x : ↥U
rw : LiftPropAt Q id (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x)
⊢ LiftPropAt Q (id ∘ Opens.inclusion hUV) x

Tactic:
rw [← hG.liftPropAt_iff_comp_inclusion hUV]

Premises used: StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_inclusion
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U V : Opens M
hUV : U ≤ V
x : ↥U
⊢ LiftPropAt Q id (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x)

Tactic:
apply hG.liftProp_id hQ

Premises used: StructureGroupoid.LocalInvariantProp.liftProp_id
-- 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
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
mp : G.IsLocalStructomorphWithinAt f s x → G.IsLocalStructomorphWithinAt f (s ∩ u) x
mpr : G.IsLocalStructomorphWithinAt f (s ∩ u) x → G.IsLocalStructomorphWithinAt f s x
⊢ G.IsLocalStructomorphWithinAt f s x ↔ G.IsLocalStructomorphWithinAt f (s ∩ u) x

Tactic:
constructor
-- 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
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s ∩ u
mp :
  ∀ (e : OpenPartialHomeomorph H H) (heG : e ∈ G) (hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source))
    (hex : x ∈ e.source), ∃ e ∈ G, EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source) ∧ x ∈ e.source
⊢ ∃ e ∈ G, EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source) ∧ x ∈ e.source

Tactic:
rcases h hx.1 with ⟨e, heG, hef, hex⟩

Premises used: And.left
-- 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
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s ∩ u
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
mfld_set_tac mfld_set_tac₁ mfld_set_tac₂ : ∀ ⦃my_y : H⦄, my_y ∈ s ∩ u ∩ e.source → my_y ∈ s ∩ e.source
mfld_set_tac₃ mfld_set_tac₄ : ∀ ⦃my_y : H⦄, (my_y ∈ s ∧ my_y ∈ u) ∧ my_y ∈ e.source → my_y ∈ s ∩ e.source
⊢ s ∩ u ∩ e.source ⊆ s ∩ e.source

Tactic:
mfld_set_tac
-- 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
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s ∩ u
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
⊢ s ∩ u ∩ e.source ⊆ s ∩ e.source

Tactic:
have : s ∩ u ∩ e.source ⊆ s ∩ e.source := by mfld_set_tac
-- 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
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s ∩ u
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
this : s ∩ u ∩ e.source ⊆ s ∩ e.source
⊢ ∃ e ∈ G, EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source) ∧ x ∈ e.source

Tactic:
⟨e, heG, hef.mono this, hex⟩

Premises used: And.intro, Exists.intro, Set.EqOn.mono
-- 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
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s ∩ u
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
this : s ∩ u ∩ e.source ⊆ s ∩ e.source
⊢ ∃ e ∈ G, EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source) ∧ x ∈ e.source

Tactic:
exact ⟨e, heG, hef.mono this, hex⟩
-- 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
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
mpr :
  ∀ (e : OpenPartialHomeomorph H H) (heG : e ∈ G) (hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source))
    (hex : x ∈ e.source), ∃ e ∈ G, EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
⊢ ∃ e ∈ G, EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
rcases h ⟨hx, hux⟩ with ⟨e, heG, hef, hex⟩

Premises used: 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
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source)
hex : x ∈ e.source
⊢ ∃ e ∈ G, EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
⟨e.restr (interior u), ?_, ?_, ?_⟩

Premises used: And.intro, interior, Exists.intro, OpenPartialHomeomorph.restr
-- 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
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source)
hex : x ∈ e.source
mpr : e.restr (interior u) ∈ G
mpr₁ : EqOn f (↑(e.restr (interior u)).toPartialEquiv : H → H) (s ∩ (e.restr (interior u)).source)
mpr₂ : x ∈ (e.restr (interior u)).source
⊢ ∃ e ∈ G, EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
refine ⟨e.restr (interior u), ?_, ?_, ?_⟩
-- 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
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source)
hex : x ∈ e.source
⊢ e.restr (interior u) ∈ G

Tactic:
closedUnderRestriction' heG isOpen_interior

Premises used: isOpen_interior, closedUnderRestriction'
-- 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
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source)
hex : x ∈ e.source
⊢ e.restr (interior u) ∈ G

Tactic:
exact closedUnderRestriction' heG isOpen_interior

Premises used: isOpen_interior, closedUnderRestriction'
-- 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
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source)
hex : x ∈ e.source
h₁ h₂ h₃ h₄ : ∀ (my_y : H), my_y ∈ s ∩ u ∩ e.source ↔ my_y ∈ s ∩ (e.source ∩ u)
⊢ s ∩ u ∩ e.source = s ∩ (e.source ∩ u)

Tactic:
mfld_set_tac
-- 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
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source)
hex : x ∈ e.source
⊢ s ∩ u ∩ e.source = s ∩ (e.source ∩ u)

Tactic:
have : s ∩ u ∩ e.source = s ∩ (e.source ∩ u) := by mfld_set_tac
-- 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
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source)
hex : x ∈ e.source
this : s ∩ u ∩ e.source = s ∩ (e.source ∩ u)
⊢ EqOn f (↑(e.restr (interior u)).toPartialEquiv : H → H) (s ∩ (e.restr (interior u)).source)

Tactic:
simpa only [this, interior_interior, hu.interior_eq, mfld_simps] using hef

Premises used: interior_interior, IsOpen.interior_eq
-- 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
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source)
hex : x ∈ e.source
⊢ x ∈ (e.restr (interior u)).source

Tactic:
simp only [*, hu.interior_eq, mfld_simps]

Premises used: IsOpen.interior_eq
-- 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
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : (↑e' : H → H) x ∈ (↑e'.symm : H → H) ⁻¹' s
⊢ x ∈ s

Tactic:
simpa only [e'.left_inv he'x, mfld_simps] using hx

Premises used: OpenPartialHomeomorph.left_inv
-- 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
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : (↑e' : H → H) x ∈ (↑e'.symm : H → H) ⁻¹' s
⊢ x ∈ s

Tactic:
have hxs : x ∈ s := by simpa only [e'.left_inv he'x, mfld_simps] using hx
-- 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
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : (↑e' : H → H) x ∈ (↑e'.symm : H → H) ⁻¹' s
hxs : x ∈ s
rcases :
  ∀ (e : OpenPartialHomeomorph H H) (heG : e ∈ G) (hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source))
    (hex : x ∈ e.source),
    ∃ e ∈ G,
      EqOn (f ∘ (↑e'.symm : H → H)) (↑e.toPartialEquiv : H → H) ((↑e'.symm : H → H) ⁻¹' s ∩ e.source) ∧
        (↑e' : H → H) x ∈ e.source
⊢ ∃ e ∈ G,
    EqOn (f ∘ (↑e'.symm : H → H)) (↑e.toPartialEquiv : H → H) ((↑e'.symm : H → H) ⁻¹' s ∩ e.source) ∧
      (↑e' : H → H) x ∈ e.source

Tactic:
rcases h hxs with ⟨e, heG, hef, hex⟩
-- 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
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : (↑e' : H → H) x ∈ (↑e'.symm : H → H) ⁻¹' s
hxs : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
⊢ ∃ e ∈ G,
    EqOn (f ∘ (↑e'.symm : H → H)) (↑e.toPartialEquiv : H → H) ((↑e'.symm : H → H) ⁻¹' s ∩ e.source) ∧
      (↑e' : H → H) x ∈ e.source

Tactic:
⟨e'.symm.trans e, G.trans (G.symm he'G) heG, ?_, ?_⟩

Premises used: OpenPartialHomeomorph.trans, And.intro, Exists.intro, StructureGroupoid.trans, StructureGroupoid.symm, OpenPartialHomeomorph.symm
-- 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
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : (↑e' : H → H) x ∈ (↑e'.symm : H → H) ⁻¹' s
hxs : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
refine_1 :
  EqOn (f ∘ (↑e'.symm : H → H)) (↑(e'.symm ≫ₕ e).toPartialEquiv : H → H)
    ((↑e'.symm : H → H) ⁻¹' s ∩ (e'.symm ≫ₕ e).source)
refine_2 : (↑e' : H → H) x ∈ (e'.symm ≫ₕ e).source
⊢ ∃ e ∈ G,
    EqOn (f ∘ (↑e'.symm : H → H)) (↑e.toPartialEquiv : H → H) ((↑e'.symm : H → H) ⁻¹' s ∩ e.source) ∧
      (↑e' : H → H) x ∈ e.source

Tactic:
refine ⟨e'.symm.trans e, G.trans (G.symm he'G) heG, ?_, ?_⟩
-- 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
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : (↑e' : H → H) x ∈ (↑e'.symm : H → H) ⁻¹' s
hxs : 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 ∈ (↑e'.symm : H → H) ⁻¹' s ∩ (e'.symm ≫ₕ e).source
⊢ (↑e'.symm : H → H) y ∈ s ∧ y ∈ e'.target ∧ (↑e'.symm : H → H) y ∈ e.source

Tactic:
simp only [mfld_simps] at hy
-- 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
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : (↑e' : H → H) x ∈ (↑e'.symm : H → H) ⁻¹' s
hxs : 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 : (↑e'.symm : H → H) y ∈ s ∧ y ∈ e'.target ∧ (↑e'.symm : H → H) y ∈ e.source
⊢ (f ∘ (↑e'.symm : H → H)) y = (↑(e'.symm ≫ₕ e).toPartialEquiv : H → H) y

Tactic:
simp only [hef ⟨hy.1, hy.2.2⟩, 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
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : (↑e' : H → H) x ∈ (↑e'.symm : H → H) ⁻¹' s
hxs : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
⊢ (↑e' : H → H) x ∈ (e'.symm ≫ₕ e).source

Tactic:
simp only [hex, he'x, mfld_simps]
-- 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 g : H → H
hfgs : ∀ y ∈ s, f y = g y
_ : f x = g x → G.IsLocalStructomorphWithinAt f s x → G.IsLocalStructomorphWithinAt g s x
⊢ f x = g x → G.IsLocalStructomorphWithinAt f s x → G.IsLocalStructomorphWithinAt g s x

Tactic:
_
-- 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 g : H → H
hfgs : ∀ y ∈ s, f y = g y
h_1 : f x = g x
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
rcases :
  ∀ (e : OpenPartialHomeomorph H H) (heG : e ∈ G) (hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source))
    (hex : x ∈ e.source), ∃ e ∈ G, EqOn g (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
⊢ ∃ e ∈ G, EqOn g (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
rcases h hx with ⟨e, heG, hef, hex⟩
-- 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 g : H → H
hfgs : ∀ y ∈ s, f y = g y
h_1 : f x = g x
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
⊢ ∃ e ∈ G, EqOn g (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
⟨e, heG, ?_, hex⟩

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
s : Set H
x : H
f g : H → H
hfgs : ∀ y ∈ s, f y = g y
h_1 : f x = g x
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
refine : EqOn g (↑e.toPartialEquiv : H → H) (s ∩ e.source)
⊢ ∃ e ∈ G, EqOn g (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
refine ⟨e, heG, ?_, hex⟩
-- 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 g : H → H
hfgs : ∀ y ∈ s, f y = g y
h_1 : f x = g x
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 ∩ e.source
rw : g y = f y
rw₁ rw₂ : g y = g y
⊢ g y = (↑e.toPartialEquiv : H → H) y

Tactic:
rw [← hef hy, hfgs y hy.1]

Premises used: And.left
-- 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
_ :
  s ⊆ f ⁻¹' e'.source →
    f x ∈ e'.source → G.IsLocalStructomorphWithinAt f s x → G.IsLocalStructomorphWithinAt ((↑e' : H → H) ∘ f) s x
⊢ s ⊆ f ⁻¹' e'.source →
    f x ∈ e'.source → G.IsLocalStructomorphWithinAt f s x → G.IsLocalStructomorphWithinAt ((↑e' : H → H) ∘ f) s x

Tactic:
_
-- 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
rcases :
  ∀ (e : OpenPartialHomeomorph H H) (heG : e ∈ G) (hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source))
    (hex : x ∈ e.source), ∃ e ∈ G, EqOn ((↑e' : H → H) ∘ f) (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
⊢ ∃ e ∈ G, EqOn ((↑e' : H → H) ∘ f) (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
rcases h hx with ⟨e, heG, hef, hex⟩
-- 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
⊢ ∃ e ∈ G, EqOn ((↑e' : H → H) ∘ f) (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
⟨e.trans e', G.trans heG he'G, ?_, ?_⟩

Premises used: OpenPartialHomeomorph.trans, And.intro, Exists.intro, StructureGroupoid.trans
-- 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
refine_1 : EqOn ((↑e' : H → H) ∘ f) (↑(e ≫ₕ e').toPartialEquiv : H → H) (s ∩ (e ≫ₕ e').source)
refine_2 : x ∈ (e ≫ₕ e').source
⊢ ∃ e ∈ G, EqOn ((↑e' : H → H) ∘ f) (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
refine ⟨e.trans e', G.trans heG he'G, ?_, ?_⟩
-- 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 ∩ (e ≫ₕ e').source
⊢ y ∈ s ∧ y ∈ e.source ∧ (↑e : H → H) y ∈ e'.source

Tactic:
simp only [mfld_simps] at hy