awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
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 s x
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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
have refine_1 : (f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H) =ᶠ[𝓝 x] f
Tactic: refine hG.congr ?_ ((hG.congr_set ?_).mp this)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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
⊢ P f s x
have refine_2 : (↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s =ᶠ[𝓝 x] s
Tactic: refine hG.congr ?_ ((hG.congr_set ?_).mp this)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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
have refine_1 : ∀ (x' : H) (hx' : x' ∈ e.source), ((f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H)) x' = f x'
Tactic: refine eventually_of_mem (e.open_source.mem_nhds hxe) fun x' hx' ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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
⊢ ((f ∘ (↑e.symm : H → H)) ∘ (↑e : H → H)) x' = f x'
have refine_1 : f ((↑e.symm : H → H) ((↑e : H → H) x')) = f x'
Tactic: simp_rw [Function.comp_apply, e.left_inv hx']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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
⊢ (↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s =ᶠ[𝓝 x] s
have refine_2 : ∀ᶠ (x : H) in 𝓝 x, x ∈ (↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ↔ x ∈ s
Tactic: rw [eventuallyEq_set]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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
have refine_2 : ∀ (x' : H) (hx' : x' ∈ e.source), 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' ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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
⊢ x' ∈ (↑e : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ↔ x' ∈ s
have refine_2 : (↑e.symm : H → H) ((↑e : H → H) x') ∈ s ↔ x' ∈ s
Tactic: simp_rw [mem_preimage, e.left_inv hx']
-- 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'
P : (H → H') → Set H → H → Prop
f : M → M'
x : M
⊢ 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)
have 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)
Tactic: rw [LiftPropAt, liftPropWithinAt_iff', continuousWithinAt_univ, preimage_univ]
-- 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'
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)
⊢ 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)
have 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)
Tactic: rw [LiftPropAt, liftPropWithinAt_iff', continuousWithinAt_univ, preimage_univ]
-- 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'
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)
⊢ 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)
have 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)
Tactic: rw [LiftPropAt, liftPropWithinAt_iff', continuousWithinAt_univ, preimage_univ]
-- 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'
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)
⊢ 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)
have 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)
Tactic: rw [LiftPropAt, liftPropWithinAt_iff', continuousWithinAt_univ, preimage_univ]
-- 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'
P : (H → H') → Set H → H → Prop
f : M → M'
⊢ 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)
have 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)
Tactic: simp_rw [LiftProp, liftPropAt_iff, forall_and, continuous_iff_continuousAt]
-- 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'
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)
⊢ 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)
have 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)
Tactic: simp_rw [LiftProp, liftPropAt_iff, forall_and, continuous_iff_continuousAt]
-- 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'
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)
⊢ 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)
have 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)
Tactic: simp_rw [LiftProp, liftPropAt_iff, forall_and, continuous_iff_continuousAt]
-- 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'
P : (H → H') → Set H → H → Prop
U : Opens M'
f : M → ↥U
s : Set M
x : M
⊢ LiftPropWithinAt P (Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) s x ↔ LiftPropWithinAt P f s x
have 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)
Tactic: simp only [ChartedSpace.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'
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 ∧
      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)
have a : ContinuousWithinAt (Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) s x ↔ ContinuousWithinAt f s x
Tactic: congrm ?_ ∧ ?_
-- 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'
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
⊢ 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)
have 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)
Tactic: congrm ?_ ∧ ?_
-- 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'
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
f : M → M'
⊢ 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)
have 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)
Tactic: rw [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'
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
f : M → M'
⊢ 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)
have refine : ∀ (hf : ContinuousWithinAt f s x),
  (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s =ᶠ[𝓝 ((↑(chartAt H x) : M → H) x)]
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
        (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source)
Tactic: refine and_congr_right fun hf ↦ hG.congr_set ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
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'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
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
⊢ P (g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x) ↔
    P (g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)
have rw : P ((g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H))
    ((↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s) ((↑(e.symm ≫ₕ e') : H → H) ((↑e : M → H) x)) ↔
  P (g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)
Tactic: rw [← hG.right_invariance (compatible_of_mem_maximalAtlas he he')]