awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : H → M'
x : H
s : Set H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
hcont : ContinuousWithinAt ((↑f : M' → H') ∘ g) s x
refine : (↑(f.symm ≫ₕ f') : H' → H') ∘ (↑f : M' → H') ∘ g =ᶠ[𝓝[s] x] (↑f' : M' → H') ∘ g
⊢ P ((↑(f.symm ≫ₕ f') : H' → H') ∘ (↑f : M' → H') ∘ g) s x ↔ P ((↑f' : M' → H') ∘ g) s x

Tactic:
refine hG.congr_iff_nhdsWithin ?_ (by simp only [xf, mfld_simps])

Premises used: StructureGroupoid.LocalInvariantProp.congr_iff_nhdsWithin
-- 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'
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : H → M'
x : H
s : Set H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
hcont : ContinuousWithinAt ((↑f : M' → H') ∘ g) s x
⊢ (↑(f.symm ≫ₕ f') : H' → H') ∘ (↑f : M' → H') ∘ g =ᶠ[𝓝[s] x] (↑f' : M' → H') ∘ g

Tactic:
(hgs.eventually <| f.eventually_left_inverse xf).mono fun y ↦ congr_arg f'

Premises used: OpenPartialHomeomorph.eventually_left_inverse, Filter.EventuallyEq, OpenPartialHomeomorph.toFun', Filter.Eventually.mono, congr_arg, Filter.Tendsto.eventually
-- 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'
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : H → M'
x : H
s : Set H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
hcont : ContinuousWithinAt ((↑f : M' → H') ∘ g) s x
⊢ (↑(f.symm ≫ₕ f') : H' → H') ∘ (↑f : M' → H') ∘ g =ᶠ[𝓝[s] x] (↑f' : M' → H') ∘ g

Tactic:
exact (hgs.eventually <| f.eventually_left_inverse xf).mono fun y ↦ congr_arg f'

Premises used: OpenPartialHomeomorph.eventually_left_inverse, OpenPartialHomeomorph.toFun', Filter.Eventually.mono, congr_arg, Filter.Tendsto.eventually
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
inst_4 : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : OpenPartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
⊢ g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f.source

Tactic:
rw [← e.left_inv xe] at xf xf' hgs

Premises used: OpenPartialHomeomorph.left_inv
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
inst_4 : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : OpenPartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
xf₁ : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f.source
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'

Tactic:
rw [← e.left_inv xe] at xf xf' hgs

Premises used: OpenPartialHomeomorph.left_inv
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
inst_4 : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : OpenPartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
xf₁ : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f.source
hf'₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
⊢ g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f'.source

Tactic:
rw [← e.left_inv xe] at xf xf' hgs

Premises used: OpenPartialHomeomorph.left_inv
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
inst_4 : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : OpenPartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
xf₁ : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f.source
hf'₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf'₁ : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f'.source
⊢ ContinuousWithinAt g s ((↑e.symm : H → X) ((↑e : X → H) x))

Tactic:
rw [← e.left_inv xe] at xf xf' hgs

Premises used: OpenPartialHomeomorph.left_inv
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
inst_4 : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : OpenPartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f'.source
hgs : ContinuousWithinAt g s ((↑e.symm : H → X) ((↑e : X → H) x))
⊢ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → X)) ((↑e.symm : H → X) ⁻¹' s) ((↑e : X → H) x) ↔
    P ((↑f' : M' → H') ∘ g ∘ (↑e.symm : H → X)) ((↑e.symm : H → X) ⁻¹' s) ((↑e : X → H) x)

Tactic:
hG.liftPropWithinAt_indep_chart_target_aux2 (g ∘ e.symm) hf xf hf' xf' ?_

Premises used: Function.comp, OpenPartialHomeomorph.toFun', StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target_aux2, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
inst_4 : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : OpenPartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f'.source
hgs : ContinuousWithinAt g s ((↑e.symm : H → X) ((↑e : X → H) x))
refine : ContinuousWithinAt (g ∘ (↑e.symm : H → X)) ((↑e.symm : H → X) ⁻¹' s) ((↑e : X → H) x)
⊢ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → X)) ((↑e.symm : H → X) ⁻¹' s) ((↑e : X → H) x) ↔
    P ((↑f' : M' → H') ∘ g ∘ (↑e.symm : H → X)) ((↑e.symm : H → X) ⁻¹' s) ((↑e : X → H) x)

Tactic:
refine hG.liftPropWithinAt_indep_chart_target_aux2 (g ∘ e.symm) hf xf hf' xf' ?_

Premises used: Function.comp, OpenPartialHomeomorph.toFun', StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target_aux2, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
inst_4 : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : OpenPartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f'.source
hgs : ContinuousWithinAt g s ((↑e.symm : H → X) ((↑e : X → H) x))
⊢ ContinuousWithinAt (g ∘ (↑e.symm : H → X)) ((↑e.symm : H → X) ⁻¹' s) ((↑e : X → H) x)

Tactic:
hgs.comp (e.symm.continuousAt <| e.mapsTo xe).continuousWithinAt Subset.rfl

Premises used: OpenPartialHomeomorph.continuousAt, ContinuousAt.continuousWithinAt, Set.Subset.rfl, ContinuousWithinAt.comp, OpenPartialHomeomorph.mapsTo, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
inst_4 : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : OpenPartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f'.source
hgs : ContinuousWithinAt g s ((↑e.symm : H → X) ((↑e : X → H) x))
⊢ ContinuousWithinAt (g ∘ (↑e.symm : H → X)) ((↑e.symm : H → X) ⁻¹' s) ((↑e : X → H) x)

Tactic:
exact hgs.comp (e.symm.continuousAt <| e.mapsTo xe).continuousWithinAt Subset.rfl

Premises used: OpenPartialHomeomorph.continuousAt, ContinuousAt.continuousWithinAt, Set.Subset.rfl, ContinuousWithinAt.comp, OpenPartialHomeomorph.mapsTo, 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'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
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
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
rw :
  P (((↑f : M' → H') ∘ g) ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x) ↔
    P ((↑f' : M' → H') ∘ g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)
rw₁ :
  P (((↑f : M' → H') ∘ g) ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x) ↔
    P ((↑f' : M' → H') ∘ g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)
rw₂ :
  P ((↑f : M' → H') ∘ g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x) ↔
    P ((↑f' : M' → H') ∘ g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)
rw₃ rw₄ :
  P ((↑f' : M' → H') ∘ g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x) ↔
    P ((↑f' : M' → H') ∘ g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)
⊢ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x) ↔
    P ((↑f' : M' → H') ∘ g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)

Tactic:
rw [← Function.comp_assoc, hG.liftPropWithinAt_indep_chart_source_aux (f ∘ g) he xe he' xe',
    Function.comp_assoc, hG.liftPropWithinAt_indep_chart_target_aux xe' hf xf hf' xf' hgs]

Premises used: Function.comp, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source_aux, OpenPartialHomeomorph.toFun', StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target_aux, 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'
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
simp :
  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 s x ∧ P ((↑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 ∧ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)

Tactic:
simp only [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'
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
⊢ 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 s x ∧ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)

Tactic:
and_congr_right <|
    hG.liftPropWithinAt_indep_chart_aux (chart_mem_maximalAtlas _ _) (mem_chart_source _ _) he xe
      (chart_mem_maximalAtlas _ _) (mem_chart_source _ _) hf xf

Premises used: mem_chart_source, StructureGroupoid.chart_mem_maximalAtlas, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_aux, and_congr_right
-- 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
⊢ 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 s x ∧ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)

Tactic:
exact and_congr_right <|
    hG.liftPropWithinAt_indep_chart_aux (chart_mem_maximalAtlas _ _) (mem_chart_source _ _) he xe
      (chart_mem_maximalAtlas _ _) (mem_chart_source _ _) hf xf

Premises used: mem_chart_source, StructureGroupoid.chart_mem_maximalAtlas, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_aux, and_congr_right
-- 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 :
  ContinuousWithinAt (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) ↔
    ContinuousWithinAt (g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : 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)
⊢ LiftPropWithinAt P g s x ↔ LiftPropWithinAt P (g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)

Tactic:
rw [liftPropWithinAt_self_source, liftPropWithinAt_iff',
    e.symm.continuousWithinAt_iff_continuousWithinAt_comp_right xe, e.symm_symm]

Premises used: OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right, StructureGroupoid.liftPropWithinAt_self_source, OpenPartialHomeomorph.symm_symm, OpenPartialHomeomorph.symm, 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'
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
⊢ ContinuousWithinAt (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) ↔
    ContinuousWithinAt (g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : 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:
and_congr Iff.rfl ?_

Premises used: Iff.rfl, and_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'
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
refine :
  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)
⊢ ContinuousWithinAt (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) ↔
    ContinuousWithinAt (g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : 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:
refine and_congr Iff.rfl ?_

Premises used: Iff.rfl, and_congr