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'
e : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
inst_6 : HasGroupoid M G
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
rw :
  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) ↔
    P ((↑(chartAt H' (g ((↑e.symm : H → M) ((↑e : M → H) x)))) : M' → H') ∘ g ∘ (↑e.symm : H → M))
      ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
rw₁ :
  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) ↔
    P ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
rw₂ :
  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) ↔
    P ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
rw₃ :
  P (((↑(chartAt H' (g x)) : M' → H') ∘ g) ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x) ↔
    P ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
rw₄ rw₅ :
  P ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x) ↔
    P ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) 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) ↔
    P ((↑(chartAt H' ((g ∘ (↑e.symm : H → M)) ((↑e : M → H) x))) : M' → H') ∘ g ∘ (↑e.symm : H → M))
      ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)

Tactic:
rw [Function.comp_apply, e.left_inv xe, ← Function.comp_assoc,
    hG.liftPropWithinAt_indep_chart_source_aux (chartAt _ (g x) ∘ g) (chart_mem_maximalAtlas G x)
      (mem_chart_source _ x) he xe, Function.comp_assoc]

Premises used: mem_chart_source, chartAt, StructureGroupoid.chart_mem_maximalAtlas, Function.comp, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source_aux, OpenPartialHomeomorph.left_inv, OpenPartialHomeomorph.toFun', Function.comp_apply, Function.comp_assoc
-- 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'
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
inst_6 : HasGroupoid M' G'
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
rw :
  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 ((↑f : M' → H') ∘ g) s x ∧
        P (((↑f : M' → H') ∘ g) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
          ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x))
⊢ LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ LiftPropWithinAt P ((↑f : M' → H') ∘ g) s x

Tactic:
rw [liftPropWithinAt_self_target, liftPropWithinAt_iff', and_congr_right_iff]

Premises used: and_congr_right_iff, StructureGroupoid.liftPropWithinAt_self_target, 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'
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
inst_6 : HasGroupoid M' G'
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hg : ContinuousWithinAt g s x
simp_rw :
  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) ↔
    P (((↑f : M' → H') ∘ g) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) 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 ((↑f : M' → H') ∘ g) s x ∧
      P (((↑f : M' → H') ∘ g) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)

Tactic:
simp_rw [(f.continuousAt xf).comp_continuousWithinAt hg, true_and]

Premises used: OpenPartialHomeomorph.continuousAt, ContinuousAt.comp_continuousWithinAt, true_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'
G : StructureGroupoid H
G' : StructureGroupoid H'
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
inst_6 : HasGroupoid M' G'
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hg : 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) ↔
    P (((↑f : M' → H') ∘ g) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)

Tactic:
hG.liftPropWithinAt_indep_chart_target_aux (mem_chart_source _ _)
    (chart_mem_maximalAtlas _ _) (mem_chart_source _ _) hf xf hg

Premises used: mem_chart_source, StructureGroupoid.chart_mem_maximalAtlas, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target_aux
-- 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'
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
inst_6 : HasGroupoid M' G'
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hg : 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) ↔
    P (((↑f : M' → H') ∘ g) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)

Tactic:
exact hG.liftPropWithinAt_indep_chart_target_aux (mem_chart_source _ _)
    (chart_mem_maximalAtlas _ _) (mem_chart_source _ _) hf xf hg

Premises used: mem_chart_source, StructureGroupoid.chart_mem_maximalAtlas, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target_aux
-- 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'
e : OpenPartialHomeomorph M H
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
inst_6 : HasGroupoid M G
inst_7 : HasGroupoid M' G'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
rw :
  ContinuousWithinAt g s x ∧ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x) →
    ContinuousWithinAt ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
⊢ LiftPropWithinAt P g s x ↔
    ContinuousWithinAt g s x ∧
      LiftPropWithinAt P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)

Tactic:
rw [hG.liftPropWithinAt_indep_chart he xe hf xf, liftPropWithinAt_self, and_left_comm,
    Iff.comm, and_iff_right_iff_imp]

Premises used: and_left_comm, StructureGroupoid.liftPropWithinAt_self, and_iff_right_iff_imp, Iff.comm, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart
-- 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'
e : OpenPartialHomeomorph M H
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
inst_6 : HasGroupoid M G
inst_7 : HasGroupoid M' G'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
h : ContinuousWithinAt g s x ∧ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
⊢ ContinuousWithinAt (g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e.symm.symm : M → H) x)

Tactic:
have h1 := (e.symm.continuousWithinAt_iff_continuousWithinAt_comp_right xe).mp h.1
-- 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'
e : OpenPartialHomeomorph M H
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
inst_6 : HasGroupoid M G
inst_7 : HasGroupoid M' G'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
h : ContinuousWithinAt g s x ∧ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
h1 : ContinuousWithinAt (g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e.symm.symm : M → H) x)
simp_rw : ContinuousAt (↑f : M' → H') (g ((↑e.symm : H → M) ((↑e : M → H) x)))
simp_rw₁ : ContinuousAt (↑f : M' → H') (g x)
⊢ ContinuousAt (↑f : M' → H') ((g ∘ (↑e.symm : H → M)) ((↑e : M → H) x))

Tactic:
simp_rw [Function.comp, e.left_inv xe, f.continuousAt xf]

Premises used: OpenPartialHomeomorph.continuousAt, Function.comp, OpenPartialHomeomorph.left_inv
-- 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'
e : OpenPartialHomeomorph M H
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
inst_6 : HasGroupoid M G
inst_7 : HasGroupoid M' G'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
h : ContinuousWithinAt g s x ∧ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
h1 : ContinuousWithinAt (g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e.symm.symm : M → H) x)
⊢ ContinuousAt (↑f : M' → H') ((g ∘ (↑e.symm : H → M)) ((↑e : M → H) x))

Tactic:
have : ContinuousAt f ((g ∘ e.symm) (e x)) := by
    simp_rw [Function.comp, e.left_inv xe, f.continuousAt xf]
-- 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'
e : OpenPartialHomeomorph M H
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
inst_6 : HasGroupoid M G
inst_7 : HasGroupoid M' G'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
h : ContinuousWithinAt g s x ∧ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
h1 : ContinuousWithinAt (g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e.symm.symm : M → H) x)
this : ContinuousAt (↑f : M' → H') ((g ∘ (↑e.symm : H → M)) ((↑e : M → H) x))
⊢ ContinuousWithinAt ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)

Tactic:
this.comp_continuousWithinAt h1

Premises used: ContinuousAt.comp_continuousWithinAt
-- 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'
e : OpenPartialHomeomorph M H
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
inst_6 : HasGroupoid M G
inst_7 : HasGroupoid M' G'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
h : ContinuousWithinAt g s x ∧ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
h1 : ContinuousWithinAt (g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e.symm.symm : M → H) x)
this : ContinuousAt (↑f : M' → H') ((g ∘ (↑e.symm : H → M)) ((↑e : M → H) x))
⊢ ContinuousWithinAt ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)

Tactic:
exact this.comp_continuousWithinAt h1

Premises used: ContinuousAt.comp_continuousWithinAt
-- 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'
e : OpenPartialHomeomorph M H
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
inst_6 : HasGroupoid M G
inst_7 : HasGroupoid M' G'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
h : LiftPropOn P g s
y : H
hy : y ∈ e.target ∩ (↑e.symm : H → M) ⁻¹' (s ∩ g ⁻¹' f.source)
⊢ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) ((↑e.symm : H → M) y))

Tactic:
((hG.liftPropWithinAt_indep_chart he (e.symm_mapsTo hy.1) hf hy.2.2).1 (h _ hy.2.1)).2

Premises used: OpenPartialHomeomorph.symm_mapsTo, And.right, And.left, Iff.mp, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart
-- 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'
e : OpenPartialHomeomorph M H
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
inst_6 : HasGroupoid M G
inst_7 : HasGroupoid M' G'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
h : LiftPropOn P g s
y : H
hy : y ∈ e.target ∩ (↑e.symm : H → M) ⁻¹' (s ∩ g ⁻¹' f.source)
h₁ : y = (↑e : M → H) ((↑e.symm : H → M) y)
⊢ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) y

Tactic:
convert! ((hG.liftPropWithinAt_indep_chart he (e.symm_mapsTo hy.1) hf hy.2.2).1 (h _ hy.2.1)).2

Premises used: OpenPartialHomeomorph.symm_mapsTo, And.right, And.left, Iff.mp, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart
-- 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'
e : OpenPartialHomeomorph M H
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
inst_6 : HasGroupoid M G
inst_7 : HasGroupoid M' G'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
h : LiftPropOn P g s
y : H
hy : y ∈ e.target ∩ (↑e.symm : H → M) ⁻¹' (s ∩ g ⁻¹' f.source)
h₁ h₂ : y = y
⊢ y = (↑e : M → H) ((↑e.symm : H → M) y)

Tactic:
rw [e.right_inv hy.1]

Premises used: And.left, OpenPartialHomeomorph.right_inv
-- 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
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
ht : t ∈ 𝓝[s] x
rw :
  (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' (s ∩ t) =ᶠ[𝓝 ((↑(chartAt H x) : M → H) x)]
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s
⊢ LiftPropWithinAt P g (s ∩ t) x ↔ LiftPropWithinAt P g s x

Tactic:
rw [liftPropWithinAt_iff', liftPropWithinAt_iff', continuousWithinAt_inter' ht, hG.congr_set]

Premises used: StructureGroupoid.LocalInvariantProp.congr_set, continuousWithinAt_inter', 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
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
ht : t ∈ 𝓝[s] x
simp_rw : ∀ᶠ (x : M) in 𝓝 x, x ∈ s ∩ t ↔ x ∈ s
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' (s ∩ t) =ᶠ[𝓝 ((↑(chartAt H x) : M → H) x)]
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s

Tactic:
simp_rw [eventuallyEq_set, mem_preimage,
    (chartAt _ x).eventually_nhds' (fun x ↦ x ∈ s ∩ t ↔ x ∈ s) (mem_chart_source _ x)]

Premises used: mem_chart_source, chartAt, Membership.mem, Filter.eventuallyEq_set, Inter.inter, Iff, OpenPartialHomeomorph.eventually_nhds', 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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
ht : t ∈ 𝓝[s] x
⊢ ∀ᶠ (x : M) in 𝓝 x, x ∈ s ∩ t ↔ x ∈ s

Tactic:
(mem_nhdsWithin_iff_eventuallyEq.mp ht).symm.mem_iff

Premises used: Filter.EventuallyEq.mem_iff, mem_nhdsWithin_iff_eventuallyEq, Iff.mp, Filter.EventuallyEq.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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
ht : t ∈ 𝓝[s] x
⊢ ∀ᶠ (x : M) in 𝓝 x, x ∈ s ∩ t ↔ x ∈ s

Tactic:
exact (mem_nhdsWithin_iff_eventuallyEq.mp ht).symm.mem_iff

Premises used: Filter.EventuallyEq.mem_iff, mem_nhdsWithin_iff_eventuallyEq, Iff.mp, Filter.EventuallyEq.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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
ht : t ∈ 𝓝 x
⊢ LiftPropWithinAt P g (s ∩ t) x ↔ LiftPropWithinAt P g s x

Tactic:
hG.liftPropWithinAt_inter' (mem_nhdsWithin_of_mem_nhds ht)

Premises used: mem_nhdsWithin_of_mem_nhds, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter'
-- 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
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
hu : s =ᶠ[𝓝 x] t
rw :
  LiftPropWithinAt P g (s ∩ {x : M | (fun (x : M) ↦ s x = t x) x}) x =
    LiftPropWithinAt P g (t ∩ {x : M | (fun (x : M) ↦ s x = t x) x}) x
⊢ LiftPropWithinAt P g s x ↔ LiftPropWithinAt P g t x

Tactic:
rw [← hG.liftPropWithinAt_inter (s := s) hu, ← hG.liftPropWithinAt_inter (s := t) hu,
    ← eq_iff_iff]

Premises used: StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter, eq_iff_iff