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'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono_of_mem_nhdsWithin : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x
h : LiftPropWithinAt P g s x
hst : s ∈ 𝓝[t] x
simp :
  ∀
    (h :
      ContinuousWithinAt g s x ∧
        P ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
          ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)),
    ContinuousWithinAt g t x ∧
      P ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t) ((↑(chartAt H x) : M → H) x)
⊢ LiftPropWithinAt P g t x

Tactic:
simp only [liftPropWithinAt_iff'] at h ⊢

Premises used: ChartedSpace.liftPropWithinAt_iff'
-- 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'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono_of_mem_nhdsWithin : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x
hst : s ∈ 𝓝[t] x
h :
  ContinuousWithinAt g s x ∧
    P ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
⊢ ContinuousWithinAt g t x ∧
    P ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t) ((↑(chartAt H x) : M → H) x)

Tactic:
⟨h.1.mono_of_mem_nhdsWithin hst, mono_of_mem_nhdsWithin ?_ h.2⟩

Premises used: ContinuousWithinAt.mono_of_mem_nhdsWithin, And.right, And.left, And.intro
-- 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'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono_of_mem_nhdsWithin : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x
hst : s ∈ 𝓝[t] x
h :
  ContinuousWithinAt g s x ∧
    P ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
refine :
  (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∈
    𝓝[(↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t] (↑(chartAt H x) : M → H) x
⊢ ContinuousWithinAt g t x ∧
    P ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t) ((↑(chartAt H x) : M → H) x)

Tactic:
refine ⟨h.1.mono_of_mem_nhdsWithin hst, mono_of_mem_nhdsWithin ?_ h.2⟩
-- 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'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono_of_mem_nhdsWithin : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x
hst : s ∈ 𝓝[t] x
h :
  ContinuousWithinAt g s x ∧
    P ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
simp_rw :
  s ∈
    map (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)
      (𝓝[(↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t] (↑(chartAt H x) : M → H) x)
simp_rw₁ : s ∈ 𝓝[t] (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑(chartAt H x) : M → H) x)
simp_rw₂ : s ∈ 𝓝[t] x
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∈
    𝓝[(↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t] (↑(chartAt H x) : M → H) x

Tactic:
simp_rw [← mem_map, (chartAt H x).symm.map_nhdsWithin_preimage_eq (mem_chart_target H x),
    (chartAt H x).left_inv (mem_chart_source H x), hst]

Premises used: mem_chart_source, chartAt, OpenPartialHomeomorph.left_inv, OpenPartialHomeomorph.map_nhdsWithin_preimage_eq, mem_chart_target, Filter.mem_map, OpenPartialHomeomorph.symm
-- 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'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
⊢ LiftPropWithinAt P g t x

Tactic:
⟨h.1.mono hts, mono (fun y hy ↦ ?_) h.2⟩

Premises used: ChartedSpace.LiftPropWithinAt.prop, ChartedSpace.LiftPropWithinAt.continuousWithinAt, ContinuousWithinAt.mono, ChartedSpace.LiftPropWithinAt.mk
-- 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'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
refine :
  ∀ (y : H) (hy : y ∈ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t),
    y ∈ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s
⊢ LiftPropWithinAt P g t x

Tactic:
refine ⟨h.1.mono hts, mono (fun y hy ↦ ?_) h.2⟩
-- 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'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
y : H
hy : y ∈ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) y ∈ t

Tactic:
simp only [mfld_simps] at hy
-- 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'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
y : H
hy : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) y ∈ t
⊢ y ∈ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s

Tactic:
simp only [hy, hts _, mfld_simps]
-- 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'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropAt P g x
⊢ LiftPropWithinAt P g univ x

Tactic:
rw [← liftPropWithinAt_univ] at h

Premises used: StructureGroupoid.liftPropWithinAt_univ
-- 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'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g univ x
⊢ LiftPropWithinAt P g s x

Tactic:
liftPropWithinAt_mono mono h (subset_univ _)

Premises used: StructureGroupoid.LocalInvariantProp.liftPropWithinAt_mono, Set.subset_univ
-- 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'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g univ x
⊢ LiftPropWithinAt P g s x

Tactic:
exact liftPropWithinAt_mono mono h (subset_univ _)

Premises used: StructureGroupoid.LocalInvariantProp.liftPropWithinAt_mono, Set.subset_univ
-- 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'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropOn P g t
hst : s ⊆ t
⊢ LiftPropOn P g s

Tactic:
fun x hx ↦ liftPropWithinAt_mono mono (h x (hst hx)) hst

Premises used: StructureGroupoid.LocalInvariantProp.liftPropWithinAt_mono, ChartedSpace.LiftPropOn
-- 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'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftProp P g
⊢ LiftPropOn P g univ

Tactic:
rw [← liftPropOn_univ] at h

Premises used: StructureGroupoid.liftPropOn_univ
-- 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'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropOn P g univ
⊢ LiftPropOn P g s

Tactic:
liftPropOn_mono mono h (subset_univ _)

Premises used: Set.subset_univ, StructureGroupoid.LocalInvariantProp.liftPropOn_mono
-- 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'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropOn P g univ
⊢ LiftPropOn P g s

Tactic:
exact liftPropOn_mono mono h (subset_univ _)

Premises used: Set.subset_univ, StructureGroupoid.LocalInvariantProp.liftPropOn_mono
-- 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
e : OpenPartialHomeomorph M H
x : M
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.source
simp_rw :
  Q ((↑(OpenPartialHomeomorph.refl H) : H → H) ∘ (↑e : M → H) ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' univ)
    ((↑e : M → H) x)
⊢ LiftPropAt Q (↑e : M → H) x

Tactic:
simp_rw [LiftPropAt, hG.liftPropWithinAt_indep_chart he hx G.id_mem_maximalAtlas (mem_univ _),
    (e.continuousAt hx).continuousWithinAt, true_and]

Premises used: OpenPartialHomeomorph.continuousAt, ContinuousAt.continuousWithinAt, Set.mem_univ, StructureGroupoid.id_mem_maximalAtlas, ChartedSpace.LiftPropAt, true_and, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart
-- 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
e : OpenPartialHomeomorph M H
x : M
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.source
⊢ Q ((↑(OpenPartialHomeomorph.refl H) : H → H) ∘ (↑e : M → H) ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' univ)
    ((↑e : M → H) x)

Tactic:
hG.congr' (e.eventually_right_inverse' hx) (hQ _)

Premises used: OpenPartialHomeomorph.eventually_right_inverse', StructureGroupoid.LocalInvariantProp.congr'
-- 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
e : OpenPartialHomeomorph M H
x : M
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.source
⊢ Q ((↑(OpenPartialHomeomorph.refl H) : H → H) ∘ (↑e : M → H) ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' univ)
    ((↑e : M → H) x)

Tactic:
exact hG.congr' (e.eventually_right_inverse' hx) (hQ _)

Premises used: OpenPartialHomeomorph.eventually_right_inverse', StructureGroupoid.LocalInvariantProp.congr'
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
x : M
hx : x ∈ e.source
apply : e.source ∈ 𝓝 x
⊢ LiftPropWithinAt Q (↑e : M → H) e.source x

Tactic:
apply hG.liftPropWithinAt_of_liftPropAt_of_mem_nhds (hG.liftPropAt_of_mem_maximalAtlas hQ he hx)

Premises used: StructureGroupoid.LocalInvariantProp.liftPropWithinAt_of_liftPropAt_of_mem_nhds, StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_maximalAtlas
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
x : M
hx : x ∈ e.source
⊢ e.source ∈ 𝓝 x

Tactic:
e.open_source.mem_nhds hx

Premises used: OpenPartialHomeomorph.open_source, IsOpen.mem_nhds
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
x : M
hx : x ∈ e.source
⊢ e.source ∈ 𝓝 x

Tactic:
exact e.open_source.mem_nhds hx

Premises used: OpenPartialHomeomorph.open_source, IsOpen.mem_nhds
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.target
h : Q ((↑e : M → H) ∘ (↑e.symm : H → M)) univ x
⊢ (↑e.symm : H → M) x ∈ e.source

Tactic:
simp only [hx, mfld_simps]
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.target
h : Q ((↑e : M → H) ∘ (↑e.symm : H → M)) univ x
⊢ (↑e.symm : H → M) x ∈ e.source

Tactic:
have : e.symm x ∈ e.source := by simp only [hx, mfld_simps]
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.target
h : Q ((↑e : M → H) ∘ (↑e.symm : H → M)) univ x
this : (↑e.symm : H → M) x ∈ e.source
rw :
  ContinuousWithinAt (↑e.symm : H → M) univ x ∧
    Q ((↑e : M → H) ∘ (↑e.symm : H → M) ∘ (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H)) : H → H))
      ((↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H)) : H → H) ⁻¹' univ)
      ((↑(OpenPartialHomeomorph.refl H) : H → H) x)
⊢ LiftPropAt Q (↑e.symm : H → M) x

Tactic:
rw [LiftPropAt, hG.liftPropWithinAt_indep_chart G.id_mem_maximalAtlas (mem_univ _) he this]

Premises used: Set.mem_univ, StructureGroupoid.id_mem_maximalAtlas, ChartedSpace.LiftPropAt, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.target
h : Q ((↑e : M → H) ∘ (↑e.symm : H → M)) univ x
this : (↑e.symm : H → M) x ∈ e.source
⊢ ContinuousWithinAt (↑e.symm : H → M) univ x ∧
    Q ((↑e : M → H) ∘ (↑e.symm : H → M) ∘ (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H)) : H → H))
      ((↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H)) : H → H) ⁻¹' univ)
      ((↑(OpenPartialHomeomorph.refl H) : H → H) x)

Tactic:
⟨(e.symm.continuousAt hx).continuousWithinAt, ?_⟩

Premises used: OpenPartialHomeomorph.continuousAt, ContinuousAt.continuousWithinAt, And.intro, OpenPartialHomeomorph.symm
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.target
h : Q ((↑e : M → H) ∘ (↑e.symm : H → M)) univ x
this : (↑e.symm : H → M) x ∈ e.source
refine :
  Q ((↑e : M → H) ∘ (↑e.symm : H → M) ∘ (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H)) : H → H))
    ((↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H)) : H → H) ⁻¹' univ)
    ((↑(OpenPartialHomeomorph.refl H) : H → H) x)
⊢ ContinuousWithinAt (↑e.symm : H → M) univ x ∧
    Q ((↑e : M → H) ∘ (↑e.symm : H → M) ∘ (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H)) : H → H))
      ((↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H)) : H → H) ⁻¹' univ)
      ((↑(OpenPartialHomeomorph.refl H) : H → H) x)

Tactic:
refine ⟨(e.symm.continuousAt hx).continuousWithinAt, ?_⟩
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.target
h : Q ((↑e : M → H) ∘ (↑e.symm : H → M)) univ x
this : (↑e.symm : H → M) x ∈ e.source
⊢ Q ((↑e : M → H) ∘ (↑e.symm : H → M) ∘ (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H)) : H → H))
    ((↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H)) : H → H) ⁻¹' univ)
    ((↑(OpenPartialHomeomorph.refl H) : H → H) x)

Tactic:
simp only [h, mfld_simps]
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.target
suffices : Q ((↑e : M → H) ∘ (↑e.symm : H → M)) univ x
⊢ LiftPropAt Q (↑e.symm : H → M) x

Tactic:
suffices h : Q (e ∘ e.symm) univ x by
    have : e.symm x ∈ e.source := by simp only [hx, mfld_simps]
    rw [LiftPropAt, hG.liftPropWithinAt_indep_chart G.id_mem_maximalAtlas (mem_univ _) he this]
    refine ⟨(e.symm.continuousAt hx).continuousWithinAt, ?_⟩
    simp only [h, mfld_simps]
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.target
⊢ Q ((↑e : M → H) ∘ (↑e.symm : H → M)) univ x

Tactic:
hG.congr' (e.eventually_right_inverse hx) (hQ x)

Premises used: OpenPartialHomeomorph.eventually_right_inverse, StructureGroupoid.LocalInvariantProp.congr'
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.target
⊢ Q ((↑e : M → H) ∘ (↑e.symm : H → M)) univ x

Tactic:
exact hG.congr' (e.eventually_right_inverse hx) (hQ x)

Premises used: OpenPartialHomeomorph.eventually_right_inverse, StructureGroupoid.LocalInvariantProp.congr'