awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hG : G.LocalInvariantProp G' P
U : Opens M
f : M → M'
x : ↥U
⊢ P ((↑(chartAt H' (f (↑x : M))) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) ⁻¹' univ)
      ((↑(chartAt H (↑x : M)) : M → H) (↑x : M)) ↔
    P
      ((↑(chartAt H' ((f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x)) : M' → H') ∘
        (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U) ⁻¹' univ) ((↑(chartAt H x) : ↥U → H) x)
have a : (↑(chartAt H' (f (↑x : M))) : M' → H') ∘
    f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) =ᶠ[𝓝 ((↑(chartAt H (↑x : M)) : M → H) (↑x : M))]
  (↑(chartAt H' ((f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x)) : M' → H') ∘
    (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U)
Tactic: apply hG.congr_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
hG : G.LocalInvariantProp G' P
U V : Opens M
hUV : U ≤ V
f : ↥V → M'
x : ↥U
⊢ LiftPropAt P f (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x) ↔
    LiftPropAt P (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) x
have simp : ContinuousWithinAt f univ (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x) ∧
    P
      ((↑(chartAt H' (f (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) : M' → H') ∘
        f ∘
          (↑(OpenPartialHomeomorph.symm (chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) :
            H → ↥V))
      ((↑(OpenPartialHomeomorph.symm (chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) :
          H → ↥V) ⁻¹'
        univ)
      ((↑(chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x)) : ↥V → H)
        (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x)) ↔
  ContinuousWithinAt (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) univ x ∧
    P
      ((↑(chartAt H' ((f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) x)) : M' → H') ∘
        (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) ∘
          (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U) ⁻¹' univ) ((↑(chartAt H x) : ↥U → H) x)
Tactic: simp only [LiftPropAt, 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
hG : G.LocalInvariantProp G' P
U V : Opens M
hUV : U ≤ V
f : ↥V → M'
x : ↥U
⊢ ContinuousWithinAt f univ (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x) ∧
      P
        ((↑(chartAt H' (f (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) : M' → H') ∘
          f ∘
            (↑(OpenPartialHomeomorph.symm (chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) :
              H → ↥V))
        ((↑(OpenPartialHomeomorph.symm (chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) :
            H → ↥V) ⁻¹'
          univ)
        ((↑(chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x)) : ↥V → H)
          (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x)) ↔
    ContinuousWithinAt (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) univ x ∧
      P
        ((↑(chartAt H' ((f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) x)) : M' → H') ∘
          (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) ∘
            (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U) ⁻¹' univ) ((↑(chartAt H x) : ↥U → H) x)
have a : ContinuousWithinAt f univ (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x) ↔
  ContinuousWithinAt (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) univ 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
hG : G.LocalInvariantProp G' P
U V : Opens M
hUV : U ≤ V
f : ↥V → M'
x : ↥U
a :
  ContinuousWithinAt f univ (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x) ↔
    ContinuousWithinAt (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) univ x
⊢ ContinuousWithinAt f univ (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x) ∧
      P
        ((↑(chartAt H' (f (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) : M' → H') ∘
          f ∘
            (↑(OpenPartialHomeomorph.symm (chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) :
              H → ↥V))
        ((↑(OpenPartialHomeomorph.symm (chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) :
            H → ↥V) ⁻¹'
          univ)
        ((↑(chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x)) : ↥V → H)
          (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x)) ↔
    ContinuousWithinAt (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) univ x ∧
      P
        ((↑(chartAt H' ((f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) x)) : M' → H') ∘
          (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) ∘
            (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U) ⁻¹' univ) ((↑(chartAt H x) : ↥U → H) x)
have a₁ : P
    ((↑(chartAt H' (f (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) : M' → H') ∘
      f ∘
        (↑(OpenPartialHomeomorph.symm (chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) : H → ↥V))
    ((↑(OpenPartialHomeomorph.symm (chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) : H → ↥V) ⁻¹'
      univ)
    ((↑(chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x)) : ↥V → H)
      (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x)) ↔
  P
    ((↑(chartAt H' ((f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) x)) : M' → H') ∘
      (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) ∘
        (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U) ⁻¹' univ) ((↑(chartAt H x) : ↥U → 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
hG : G.LocalInvariantProp G' P
U V : Opens M
hUV : U ≤ V
f : ↥V → M'
x : ↥U
⊢ ContinuousWithinAt f univ (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x) ↔
    ContinuousWithinAt (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) univ x
have a : ContinuousAt f (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x) ↔
  ContinuousAt (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) x
Tactic: simp_rw [continuousWithinAt_univ,
      (TopologicalSpace.Opens.isOpenEmbedding_of_le hUV).continuousAt_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
hG : G.LocalInvariantProp G' P
U V : Opens M
hUV : U ≤ V
f : ↥V → M'
x : ↥U
⊢ P
      ((↑(chartAt H' (f (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) : M' → H') ∘
        f ∘
          (↑(OpenPartialHomeomorph.symm (chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) :
            H → ↥V))
      ((↑(OpenPartialHomeomorph.symm (chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) :
          H → ↥V) ⁻¹'
        univ)
      ((↑(chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x)) : ↥V → H)
        (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x)) ↔
    P
      ((↑(chartAt H' ((f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) x)) : M' → H') ∘
        (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) ∘
          (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U) ⁻¹' univ) ((↑(chartAt H x) : ↥U → H) x)
have a : (↑(chartAt H' (f (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) : M' → H') ∘
    f ∘
      (↑(OpenPartialHomeomorph.symm (chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))) :
        H →
          ↥V) =ᶠ[𝓝
    ((↑(chartAt H (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x)) : ↥V → H)
      (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))]
  (↑(chartAt H' ((f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) x)) : M' → H') ∘
    (f ∘ inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U)
Tactic: apply hG.congr_iff
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U : Opens M
x : ↥U
⊢ LiftPropAt Q (Subtype.val (p := fun (x : M) ↦ x ∈ U)) x
have change : LiftPropAt Q (id ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x
Tactic: change LiftPropAt Q (id ∘ Subtype.val) x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U : Opens M
x : ↥U
⊢ LiftPropAt Q (id ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x
have rw : LiftPropAt Q id (↑x : M)
Tactic: rw [← hG.liftPropAt_iff_comp_subtype_val]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U V : Opens M
hUV : U ≤ V
x : ↥U
⊢ LiftPropAt Q (id ∘ Opens.inclusion hUV) x
have rw : LiftPropAt Q id (inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x)
Tactic: rw [← hG.liftPropAt_iff_comp_inclusion hUV]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
⊢ G.IsLocalStructomorphWithinAt f s x ↔ G.IsLocalStructomorphWithinAt f (s ∩ u) x
have mp : G.IsLocalStructomorphWithinAt f s x → G.IsLocalStructomorphWithinAt f (s ∩ u) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
mp : G.IsLocalStructomorphWithinAt f s x → G.IsLocalStructomorphWithinAt f (s ∩ u) x
⊢ G.IsLocalStructomorphWithinAt f s x ↔ G.IsLocalStructomorphWithinAt f (s ∩ u) x
have mpr : G.IsLocalStructomorphWithinAt f (s ∩ u) x → G.IsLocalStructomorphWithinAt f s x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s ∩ u
⊢ ∃ e ∈ G, EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source) ∧ x ∈ e.source
have mp : ∀ (e : OpenPartialHomeomorph H H) (heG : e ∈ G) (hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source))
  (hex : x ∈ e.source), ∃ e ∈ G, EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source) ∧ x ∈ e.source
Tactic: rcases h hx.1 with ⟨e, heG, hef, hex⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s ∩ u
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
⊢ s ∩ u ∩ e.source ⊆ s ∩ e.source
have mfld_set_tac : ∀ ⦃my_y : H⦄, my_y ∈ s ∩ u ∩ e.source → my_y ∈ s ∩ e.source
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s ∩ u
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
mfld_set_tac mfld_set_tac₁ mfld_set_tac₂ : ∀ ⦃my_y : H⦄, my_y ∈ s ∩ u ∩ e.source → my_y ∈ s ∩ e.source
⊢ s ∩ u ∩ e.source ⊆ s ∩ e.source
have mfld_set_tac₃ : ∀ ⦃my_y : H⦄, (my_y ∈ s ∧ my_y ∈ u) ∧ my_y ∈ e.source → my_y ∈ s ∩ e.source
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s ∩ u
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
⊢ ∃ e ∈ G, EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source) ∧ x ∈ e.source
have this : s ∩ u ∩ e.source ⊆ s ∩ e.source
Tactic: have : s ∩ u ∩ e.source ⊆ s ∩ e.source := by mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
⊢ ∃ e ∈ G, EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
have mpr : ∀ (e : OpenPartialHomeomorph H H) (heG : e ∈ G) (hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source))
  (hex : x ∈ e.source), ∃ e ∈ G, EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
Tactic: rcases h ⟨hx, hux⟩ with ⟨e, heG, hef, hex⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source)
hex : x ∈ e.source
⊢ ∃ e ∈ G, EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
have mpr : e.restr (interior u) ∈ G
Tactic: refine ⟨e.restr (interior u), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source)
hex : x ∈ e.source
mpr : e.restr (interior u) ∈ G
⊢ ∃ e ∈ G, EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
have mpr₁ : EqOn f (↑(e.restr (interior u)).toPartialEquiv : H → H) (s ∩ (e.restr (interior u)).source)
Tactic: refine ⟨e.restr (interior u), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source)
hex : x ∈ e.source
mpr : e.restr (interior u) ∈ G
mpr₁ : EqOn f (↑(e.restr (interior u)).toPartialEquiv : H → H) (s ∩ (e.restr (interior u)).source)
⊢ ∃ e ∈ G, EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
have mpr₂ : x ∈ (e.restr (interior u)).source
Tactic: refine ⟨e.restr (interior u), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source)
hex : x ∈ e.source
⊢ s ∩ u ∩ e.source = s ∩ (e.source ∩ u)
have h₁ : ∀ (x : H), x ∈ s ∩ u ∩ e.source ↔ x ∈ s ∩ (e.source ∩ u)
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ u ∩ e.source)
hex : x ∈ e.source
⊢ EqOn f (↑(e.restr (interior u)).toPartialEquiv : H → H) (s ∩ (e.restr (interior u)).source)
have this : s ∩ u ∩ e.source = s ∩ (e.source ∩ u)
Tactic: have : s ∩ u ∩ e.source = s ∩ (e.source ∩ u) := by mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : (↑e' : H → H) x ∈ (↑e'.symm : H → H) ⁻¹' s
⊢ ∃ e ∈ G,
    EqOn (f ∘ (↑e'.symm : H → H)) (↑e.toPartialEquiv : H → H) ((↑e'.symm : H → H) ⁻¹' s ∩ e.source) ∧
      (↑e' : H → H) x ∈ e.source
have hxs : x ∈ s
Tactic: have hxs : x ∈ s := by simpa only [e'.left_inv he'x, mfld_simps] using hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : (↑e' : H → H) x ∈ (↑e'.symm : H → H) ⁻¹' s
hxs : x ∈ s
⊢ ∃ e ∈ G,
    EqOn (f ∘ (↑e'.symm : H → H)) (↑e.toPartialEquiv : H → H) ((↑e'.symm : H → H) ⁻¹' s ∩ e.source) ∧
      (↑e' : H → H) x ∈ e.source
have rcases : ∀ (e : OpenPartialHomeomorph H H) (heG : e ∈ G) (hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source))
  (hex : x ∈ e.source),
  ∃ e ∈ G,
    EqOn (f ∘ (↑e'.symm : H → H)) (↑e.toPartialEquiv : H → H) ((↑e'.symm : H → H) ⁻¹' s ∩ e.source) ∧
      (↑e' : H → H) x ∈ e.source
Tactic: rcases h hxs with ⟨e, heG, hef, hex⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : (↑e' : H → H) x ∈ (↑e'.symm : H → H) ⁻¹' s
hxs : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
⊢ ∃ e ∈ G,
    EqOn (f ∘ (↑e'.symm : H → H)) (↑e.toPartialEquiv : H → H) ((↑e'.symm : H → H) ⁻¹' s ∩ e.source) ∧
      (↑e' : H → H) x ∈ e.source
have refine_1 : EqOn (f ∘ (↑e'.symm : H → H)) (↑(e'.symm ≫ₕ e).toPartialEquiv : H → H)
  ((↑e'.symm : H → H) ⁻¹' s ∩ (e'.symm ≫ₕ e).source)
Tactic: refine ⟨e'.symm.trans e, G.trans (G.symm he'G) heG, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : (↑e' : H → H) x ∈ (↑e'.symm : H → H) ⁻¹' s
hxs : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
refine_1 :
  EqOn (f ∘ (↑e'.symm : H → H)) (↑(e'.symm ≫ₕ e).toPartialEquiv : H → H)
    ((↑e'.symm : H → H) ⁻¹' s ∩ (e'.symm ≫ₕ e).source)
⊢ ∃ e ∈ G,
    EqOn (f ∘ (↑e'.symm : H → H)) (↑e.toPartialEquiv : H → H) ((↑e'.symm : H → H) ⁻¹' s ∩ e.source) ∧
      (↑e' : H → H) x ∈ e.source
have refine_2 : (↑e' : H → H) x ∈ (e'.symm ≫ₕ e).source
Tactic: refine ⟨e'.symm.trans e, G.trans (G.symm he'G) heG, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : (↑e' : H → H) x ∈ (↑e'.symm : H → H) ⁻¹' s
hxs : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
y : H
hy : y ∈ (↑e'.symm : H → H) ⁻¹' s ∩ (e'.symm ≫ₕ e).source
⊢ (f ∘ (↑e'.symm : H → H)) y = (↑(e'.symm ≫ₕ e).toPartialEquiv : H → H) y
have hy₁ : (↑e'.symm : H → H) y ∈ s ∧ y ∈ e'.target ∧ (↑e'.symm : H → H) y ∈ e.source
Tactic: simp only [mfld_simps] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
f g : H → H
hfgs : ∀ y ∈ s, f y = g y
h_1 : f x = g x
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
⊢ ∃ e ∈ G, EqOn g (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
have rcases : ∀ (e : OpenPartialHomeomorph H H) (heG : e ∈ G) (hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source))
  (hex : x ∈ e.source), ∃ e ∈ G, EqOn g (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
Tactic: rcases h hx with ⟨e, heG, hef, hex⟩