awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : H
hx : x ∈ e.target
apply : e.target ∈ 𝓝 x
⊢ LiftPropWithinAt Q (↑e.symm : H → M) e.target x

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

Premises used: StructureGroupoid.LocalInvariantProp.liftPropWithinAt_of_liftPropAt_of_mem_nhds, StructureGroupoid.LocalInvariantProp.liftPropAt_symm_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 : H
hx : x ∈ e.target
⊢ e.target ∈ 𝓝 x

Tactic:
e.open_target.mem_nhds hx

Premises used: IsOpen.mem_nhds, OpenPartialHomeomorph.open_target
-- 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 : H
hx : x ∈ e.target
⊢ e.target ∈ 𝓝 x

Tactic:
exact e.open_target.mem_nhds hx

Premises used: IsOpen.mem_nhds, OpenPartialHomeomorph.open_target
-- 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
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
⊢ LiftPropAt Q (↑(chartAt H x) : M → H) x

Tactic:
hG.liftPropAt_of_mem_maximalAtlas hQ (chart_mem_maximalAtlas G x) (mem_chart_source H x)

Premises used: mem_chart_source, StructureGroupoid.chart_mem_maximalAtlas, 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
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
⊢ LiftPropOn Q (↑(chartAt H x) : M → H) (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
hG.liftPropOn_of_mem_maximalAtlas hQ (chart_mem_maximalAtlas G x)

Premises used: StructureGroupoid.chart_mem_maximalAtlas, StructureGroupoid.LocalInvariantProp.liftPropOn_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
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
⊢ (↑(chartAt H x) : M → H) x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target

Tactic:
simp
-- 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
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
⊢ LiftPropOn Q (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target

Tactic:
hG.liftPropOn_symm_of_mem_maximalAtlas hQ (chart_mem_maximalAtlas G x)

Premises used: StructureGroupoid.chart_mem_maximalAtlas, StructureGroupoid.LocalInvariantProp.liftPropOn_symm_of_mem_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
f : OpenPartialHomeomorph H H
hf : f ∈ G
x : H
hx : x ∈ f.source
⊢ LiftPropAt Q (↑f : H → H) x

Tactic:
liftPropAt_of_mem_maximalAtlas hG hQ (G.mem_maximalAtlas_of_mem_groupoid hf) hx

Premises used: StructureGroupoid.mem_maximalAtlas_of_mem_groupoid, StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
f : OpenPartialHomeomorph H H
hf : f ∈ G
⊢ LiftPropOn Q (↑f : H → H) f.source

Tactic:
liftPropOn_of_mem_maximalAtlas hG hQ (G.mem_maximalAtlas_of_mem_groupoid hf)

Premises used: StructureGroupoid.mem_maximalAtlas_of_mem_groupoid, StructureGroupoid.LocalInvariantProp.liftPropOn_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
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
simp_rw :
  ∀ (x : M),
    Q ((↑(chartAt H (id x)) : M → H) ∘ id ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
      ((↑(chartAt H x) : M → H) x)
⊢ LiftProp.{u_1, u_2, u_1, u_2} (M := M) Q id

Tactic:
simp_rw [liftProp_iff, continuous_id, true_and]

Premises used: ChartedSpace.liftProp_iff, continuous_id, true_and
-- 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
⊢ ∀ (x : M),
    Q ((↑(chartAt H (id x)) : M → H) ∘ id ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
      ((↑(chartAt H x) : M → H) x)

Tactic:
fun x ↦ hG.congr' ((chartAt H x).eventually_right_inverse <| mem_chart_target H x) (hQ _)

Premises used: chartAt, OpenPartialHomeomorph.eventually_right_inverse, OpenPartialHomeomorph.toFun', mem_chart_target, 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
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
⊢ ∀ (x : M),
    Q ((↑(chartAt H (id x)) : M → H) ∘ id ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
      ((↑(chartAt H x) : M → H) x)

Tactic:
exact fun x ↦ hG.congr' ((chartAt H x).eventually_right_inverse <| mem_chart_target H x) (hQ _)

Premises used: chartAt, OpenPartialHomeomorph.eventually_right_inverse, OpenPartialHomeomorph.toFun', mem_chart_target, StructureGroupoid.LocalInvariantProp.congr'
-- 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 : Opens M
f : M → M'
x : ↥U
simp :
  ContinuousWithinAt f univ (↑x : M) ∧
      P ((↑(chartAt H' (f (↑x : M))) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) ⁻¹' univ)
        ((↑(chartAt H (↑x : M)) : M → H) (↑x : M)) ↔
    ContinuousWithinAt (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) univ x ∧
      P
        ((↑(chartAt H' ((f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x)) : M' → H') ∘
          (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U) ⁻¹' univ) ((↑(chartAt H x) : ↥U → H) x)
⊢ LiftPropAt P f (↑x : M) ↔ LiftPropAt P (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x

Tactic:
simp only [LiftPropAt, liftPropWithinAt_iff']

Premises used: ChartedSpace.LiftPropAt, 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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
U : Opens M
f : M → M'
x : ↥U
a : ContinuousWithinAt f univ (↑x : M) ↔ ContinuousWithinAt (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) univ x
a₁ :
  P ((↑(chartAt H' (f (↑x : M))) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) ⁻¹' univ)
      ((↑(chartAt H (↑x : M)) : M → H) (↑x : M)) ↔
    P
      ((↑(chartAt H' ((f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x)) : M' → H') ∘
        (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U) ⁻¹' univ) ((↑(chartAt H x) : ↥U → H) x)
⊢ ContinuousWithinAt f univ (↑x : M) ∧
      P ((↑(chartAt H' (f (↑x : M))) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) ⁻¹' univ)
        ((↑(chartAt H (↑x : M)) : M → H) (↑x : M)) ↔
    ContinuousWithinAt (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) univ x ∧
      P
        ((↑(chartAt H' ((f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x)) : M' → H') ∘
          (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U) ⁻¹' univ) ((↑(chartAt H x) : ↥U → H) x)

Tactic:
congrm ?_ ∧ ?_
-- 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 : Opens M
f : M → M'
x : ↥U
a : ContinuousAt f (↑x : M) ↔ ContinuousAt (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x
⊢ ContinuousWithinAt f univ (↑x : M) ↔ ContinuousWithinAt (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) univ x

Tactic:
simp_rw [continuousWithinAt_univ, U.isOpenEmbedding'.continuousAt_iff]

Premises used: continuousWithinAt_univ, TopologicalSpace.Opens.isOpenEmbedding', Topology.IsOpenEmbedding.continuousAt_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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
U : Opens M
f : M → M'
x : ↥U
a :
  (↑(chartAt H' (f (↑x : M))) : M' → H') ∘
      f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) =ᶠ[𝓝 ((↑(chartAt H (↑x : M)) : M → H) (↑x : M))]
    (↑(chartAt H' ((f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x)) : M' → H') ∘
      (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U)
⊢ P ((↑(chartAt H' (f (↑x : M))) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) ⁻¹' univ)
      ((↑(chartAt H (↑x : M)) : M → H) (↑x : M)) ↔
    P
      ((↑(chartAt H' ((f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x)) : M' → H') ∘
        (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U) ⁻¹' univ) ((↑(chartAt H x) : ↥U → H) x)

Tactic:
apply hG.congr_iff

Premises used: StructureGroupoid.LocalInvariantProp.congr_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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
U : Opens M
f : M → M'
x : ↥U
⊢ (↑(chartAt H' (f (↑x : M))) : M' → H') ∘
      f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) =ᶠ[𝓝 ((↑(chartAt H (↑x : M)) : M → H) (↑x : M))]
    (↑(chartAt H' ((f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x)) : M' → H') ∘
      (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U)

Tactic:
(U.chartAt_subtype_val_symm_eventuallyEq).fun_comp (chartAt H' (f x) ∘ f)

Premises used: TopologicalSpace.Opens.chartAt_subtype_val_symm_eventuallyEq, chartAt, Function.comp, OpenPartialHomeomorph.toFun', Filter.EventuallyEq.fun_comp, Subtype.val
-- 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 : Opens M
f : M → M'
x : ↥U
⊢ (↑(chartAt H' (f (↑x : M))) : M' → H') ∘
      f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) =ᶠ[𝓝 ((↑(chartAt H (↑x : M)) : M → H) (↑x : M))]
    (↑(chartAt H' ((f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x)) : M' → H') ∘
      (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U)

Tactic:
exact (U.chartAt_subtype_val_symm_eventuallyEq).fun_comp (chartAt H' (f x) ∘ f)

Premises used: TopologicalSpace.Opens.chartAt_subtype_val_symm_eventuallyEq, chartAt, Function.comp, OpenPartialHomeomorph.toFun', Filter.EventuallyEq.fun_comp, Subtype.val
-- 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
simp :
  ContinuousWithinAt f univ (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x) ∧
      P
        ((↑(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))
        ((↑(OpenPartialHomeomorph.symm (chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) :
            H → ↥V) ⁻¹'
          univ)
        ((↑(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)) ↔
    ContinuousWithinAt (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) univ x ∧
      P
        ((↑(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))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U) ⁻¹' univ) ((↑(chartAt H x) : ↥U → H) x)
⊢ LiftPropAt P f (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x) ↔
    LiftPropAt P (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) x

Tactic:
simp only [LiftPropAt, liftPropWithinAt_iff']

Premises used: ChartedSpace.LiftPropAt, 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'
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
a :
  ContinuousWithinAt f univ (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x) ↔
    ContinuousWithinAt (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) univ x
a₁ :
  P
      ((↑(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))
      ((↑(OpenPartialHomeomorph.symm (chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) :
          H → ↥V) ⁻¹'
        univ)
      ((↑(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)) ↔
    P
      ((↑(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))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U) ⁻¹' univ) ((↑(chartAt H x) : ↥U → H) x)
⊢ ContinuousWithinAt f univ (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x) ∧
      P
        ((↑(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))
        ((↑(OpenPartialHomeomorph.symm (chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) :
            H → ↥V) ⁻¹'
          univ)
        ((↑(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)) ↔
    ContinuousWithinAt (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) univ x ∧
      P
        ((↑(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))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U) ⁻¹' univ) ((↑(chartAt H x) : ↥U → H) x)

Tactic:
congrm ?_ ∧ ?_
-- 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
a :
  ContinuousAt f (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x) ↔
    ContinuousAt (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) x
⊢ ContinuousWithinAt f univ (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x) ↔
    ContinuousWithinAt (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) univ x

Tactic:
simp_rw [continuousWithinAt_univ,
      (TopologicalSpace.Opens.isOpenEmbedding_of_le hUV).continuousAt_iff]

Premises used: continuousWithinAt_univ, Topology.IsOpenEmbedding.continuousAt_iff, TopologicalSpace.Opens.isOpenEmbedding_of_le
-- 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
a :
  (↑(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)
⊢ P
      ((↑(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))
      ((↑(OpenPartialHomeomorph.symm (chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) :
          H → ↥V) ⁻¹'
        univ)
      ((↑(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)) ↔
    P
      ((↑(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))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U) ⁻¹' univ) ((↑(chartAt H x) : ↥U → H) x)

Tactic:
apply hG.congr_iff

Premises used: StructureGroupoid.LocalInvariantProp.congr_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'
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:
(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