awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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)
have refine : ContinuousWithinAt (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' ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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
⊢ 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)
have 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)
Tactic: simp only [liftPropWithinAt_iff']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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
⊢ LiftPropWithinAt P g s x ↔ LiftPropWithinAt P (g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
have 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)
Tactic: rw [liftPropWithinAt_self_source, liftPropWithinAt_iff',
    e.symm.continuousWithinAt_iff_continuousWithinAt_comp_right xe, e.symm_symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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)
have 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)
Tactic: refine and_congr Iff.rfl ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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)
⊢ 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)
have 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)
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]