awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
⊢ P f (s ∩ f ⁻¹' e'.source) x → P ((↑e' : H' → H') ∘ f) (s ∩ f ⁻¹' e'.source) x

Tactic:
exact hG.left_invariance' he' inter_subset_right hxe'

Premises used: StructureGroupoid.LocalInvariantProp.left_invariance', Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
⊢ P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x) ↔ P f s x

Tactic:
⟨fun h ↦ ?_, hG.right_invariance' he hxe⟩

Premises used: StructureGroupoid.LocalInvariantProp.right_invariance', Iff.intro
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
refine : ∀ (h : P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x)), P f s x
⊢ P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x) ↔ P f s x

Tactic:
refine ⟨fun h ↦ ?_, hG.right_invariance' he hxe⟩
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
h : P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x)
have :
  ∀
    (this :
      P ((f ∘ (↑e.symm : H → H)) ∘ (↑e.symm.symm : H → H)) ((↑e.symm.symm : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s)
        ((↑e.symm : H → H) ((↑e : H → H) x))),
    P f s x
⊢ P f s x

Tactic:
have := hG.right_invariance' (G.symm he) (e.mapsTo hxe) h
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
h : P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x)
this :
  P ((f ∘ (↑e.symm : H → H)) ∘ (↑e.symm.symm : H → H)) ((↑e.symm.symm : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s)
    ((↑e.symm : H → H) ((↑e : H → H) x))
⊢ P ((f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H)) ((↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s) x

Tactic:
rw [e.symm_symm, e.left_inv hxe] at this

Premises used: OpenPartialHomeomorph.left_inv, OpenPartialHomeomorph.symm_symm
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
h : P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x)
this : P ((f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H)) ((↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s) x
⊢ P f s x

Tactic:
hG.congr ?_ ((hG.congr_set ?_).mp this)

Premises used: Iff.mp, StructureGroupoid.LocalInvariantProp.congr_set, StructureGroupoid.LocalInvariantProp.congr
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
h : P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x)
this : P ((f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H)) ((↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s) x
refine_1 : (f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H) =ᶠ[𝓝 x] f
refine_2 : (↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s =ᶠ[𝓝 x] s
⊢ P f s x

Tactic:
refine hG.congr ?_ ((hG.congr_set ?_).mp this)

Premises used: Iff.mp, StructureGroupoid.LocalInvariantProp.congr_set, StructureGroupoid.LocalInvariantProp.congr
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
h : P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x)
this : P ((f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H)) ((↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s) x
⊢ (f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H) =ᶠ[𝓝 x] f

Tactic:
eventually_of_mem (e.open_source.mem_nhds hxe) fun x' hx' ↦ ?_

Premises used: OpenPartialHomeomorph.open_source, Filter.EventuallyEq, Filter.eventually_of_mem, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
h : P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x)
this : P ((f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H)) ((↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s) x
refine_1 : ∀ (x' : H) (hx' : x' ∈ e.source), ((f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H)) x' = f x'
⊢ (f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H) =ᶠ[𝓝 x] f

Tactic:
refine eventually_of_mem (e.open_source.mem_nhds hxe) fun x' hx' ↦ ?_

Premises used: OpenPartialHomeomorph.open_source, Filter.eventually_of_mem, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
h : P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x)
this : P ((f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H)) ((↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s) x
x' : H
hx' : x' ∈ e.source
refine_1 : f ((↑e.symm : H → H) ((↑e : H → H) x')) = f x'
⊢ ((f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H)) x' = f x'

Tactic:
simp_rw [Function.comp_apply, e.left_inv hx']

Premises used: OpenPartialHomeomorph.left_inv, Function.comp_apply
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
h : P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x)
this : P ((f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H)) ((↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s) x
refine_2 : ∀ᶠ (x : H) in 𝓝 x, x ∈ (↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ↔ x ∈ s
⊢ (↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s =ᶠ[𝓝 x] s

Tactic:
rw [eventuallyEq_set]

Premises used: Filter.eventuallyEq_set
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
h : P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x)
this : P ((f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H)) ((↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s) x
⊢ ∀ᶠ (x : H) in 𝓝 x, x ∈ (↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ↔ x ∈ s

Tactic:
eventually_of_mem (e.open_source.mem_nhds hxe) fun x' hx' ↦ ?_

Premises used: OpenPartialHomeomorph.open_source, Filter.eventually_of_mem, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
h : P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x)
this : P ((f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H)) ((↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s) x
refine_2 : ∀ (x' : H) (hx' : x' ∈ e.source), x' ∈ (↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ↔ x' ∈ s
⊢ ∀ᶠ (x : H) in 𝓝 x, x ∈ (↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ↔ x ∈ s

Tactic:
refine eventually_of_mem (e.open_source.mem_nhds hxe) fun x' hx' ↦ ?_

Premises used: OpenPartialHomeomorph.open_source, Filter.eventually_of_mem, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
h : P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x)
this : P ((f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H)) ((↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s) x
x' : H
hx' : x' ∈ e.source
refine_2 : (↑e.symm : H → H) ((↑e : H → H) x') ∈ s ↔ x' ∈ s
⊢ x' ∈ (↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ↔ x' ∈ s

Tactic:
simp_rw [mem_preimage, e.left_inv hx']

Premises used: OpenPartialHomeomorph.left_inv, Set.mem_preimage
-- 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
f : M → M'
x : M
rw :
  LiftPropWithinAt P f univ x ↔
    ContinuousAt f x ∧
      P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
        ((↑(chartAt H x) : M → H) x)
rw₁ :
  ContinuousWithinAt f univ x ∧
      P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' univ) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousAt f x ∧
      P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
        ((↑(chartAt H x) : M → H) x)
rw₂ :
  ContinuousAt f x ∧
      P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' univ) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousAt f x ∧
      P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
        ((↑(chartAt H x) : M → H) x)
rw₃ rw₄ :
  ContinuousAt f x ∧
      P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
        ((↑(chartAt H x) : M → H) x) ↔
    ContinuousAt f x ∧
      P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
        ((↑(chartAt H x) : M → H) x)
⊢ LiftPropAt P f x ↔
    ContinuousAt f x ∧
      P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
        ((↑(chartAt H x) : M → H) x)

Tactic:
rw [LiftPropAt, liftPropWithinAt_iff', continuousWithinAt_univ, preimage_univ]

Premises used: continuousWithinAt_univ, Set.preimage_univ, 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'
P : (H → H') → Set H → H → Prop
f : M → M'
simp_rw :
  (∀ (x : M), LiftPropAt P f x) ↔
    Continuous[inst_1, inst_4] f ∧
      ∀ (x : M),
        P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
          ((↑(chartAt H x) : M → H) x)
simp_rw₁ :
  (∀ (x : M),
      ContinuousAt f x ∧
        P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
          ((↑(chartAt H x) : M → H) x)) ↔
    Continuous[inst_1, inst_4] f ∧
      ∀ (x : M),
        P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
          ((↑(chartAt H x) : M → H) x)
simp_rw₂ :
  ((∀ (x : M), ContinuousAt f x) ∧
      ∀ (x : M),
        P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
          ((↑(chartAt H x) : M → H) x)) ↔
    Continuous[inst_1, inst_4] f ∧
      ∀ (x : M),
        P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
          ((↑(chartAt H x) : M → H) x)
⊢ LiftProp P f ↔
    Continuous[inst_1, inst_4] f ∧
      ∀ (x : M),
        P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
          ((↑(chartAt H x) : M → H) x)

Tactic:
simp_rw [LiftProp, liftPropAt_iff, forall_and, continuous_iff_continuousAt]

Premises used: ChartedSpace.LiftProp, ChartedSpace.liftPropAt_iff, continuous_iff_continuousAt, forall_and
-- 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
U : Opens M'
f : M → ↥U
s : Set M
x : M
simp :
  ContinuousWithinAt (Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) s x ∧
      P
        ((↑(chartAt H' ((Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) x)) : M' → H') ∘
          (Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt f s x ∧
      P ((↑(chartAt H' (f x)) : ↥U → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
⊢ LiftPropWithinAt P (Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) s x ↔ LiftPropWithinAt P f s x

Tactic:
simp only [ChartedSpace.liftPropWithinAt_iff']

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

Tactic:
Topology.IsEmbedding.subtypeVal.isInducing.continuousWithinAt_iff.symm

Premises used: Topology.IsEmbedding.isInducing, Topology.IsEmbedding.subtypeVal, Iff.symm, Topology.IsInducing.continuousWithinAt_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
U : Opens M'
f : M → ↥U
s : Set M
x : M
⊢ ContinuousWithinAt (Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) s x ↔ ContinuousWithinAt f s x

Tactic:
exact Topology.IsEmbedding.subtypeVal.isInducing.continuousWithinAt_iff.symm

Premises used: Topology.IsEmbedding.isInducing, Topology.IsEmbedding.subtypeVal, Iff.symm, Topology.IsInducing.continuousWithinAt_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
U : Opens M'
f : M → ↥U
s : Set M
x : M
⊢ P
      ((↑(chartAt H' ((Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) x)) : M' → H') ∘
        (Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    P ((↑(chartAt H' (f x)) : ↥U → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)

Tactic:
rfl
-- 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'
x : M
⊢ LiftPropWithinAt P g univ x ↔ LiftPropAt P g x

Tactic:
Iff.rfl

Premises used: Iff.rfl, ChartedSpace.LiftPropAt
-- 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'
⊢ LiftPropOn P g univ ↔ LiftProp P g

Tactic:
simp [LiftPropOn, LiftProp, LiftPropAt]

Premises used: ChartedSpace.LiftProp, ChartedSpace.LiftPropOn, ChartedSpace.LiftPropAt
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
P : (H → H') → Set H → H → Prop
f : H → H'
s : Set H
x : H
⊢ LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P f s x

Tactic:
liftPropWithinAt_iff' ..

Premises used: Set.Mem, setOf, OpenPartialHomeomorph.toFun', Set.preimage, ChartedSpace.liftPropWithinAt_iff'
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
f : H → M'
s : Set H
x : H
⊢ LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P ((↑(chartAt H' (f x)) : M' → H') ∘ f) s x

Tactic:
liftPropWithinAt_iff' ..

Premises used: Set.Mem, setOf, OpenPartialHomeomorph.toFun', Set.preimage, ChartedSpace.liftPropWithinAt_iff'
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
P : (H → H') → Set H → H → Prop
s : Set M
x : M
f : M → H'
⊢ LiftPropWithinAt P f s x ↔
    ContinuousWithinAt f s x ∧
      P (f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)

Tactic:
liftPropWithinAt_iff' ..

Premises used: OpenPartialHomeomorph.toFun', 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
s : Set M
x : M
hG : G.LocalInvariantProp G' P
f : M → M'
rw :
  ContinuousWithinAt f s x ∧
      P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt f s x ∧
      P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
          (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
            (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
        ((↑(chartAt H x) : M → H) x)
⊢ LiftPropWithinAt P f s x ↔
    ContinuousWithinAt f s x ∧
      P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
          (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
            (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
        ((↑(chartAt H x) : M → H) x)

Tactic:
rw [liftPropWithinAt_iff']

Premises used: ChartedSpace.liftPropWithinAt_iff'