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
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g 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)
have refine : (↑(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]
  (↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)
Tactic: refine hG.congr_nhdsWithin' ?_
    (by simp_rw [Function.comp_apply, (chartAt H x).left_inv (mem_chart_source H x), hx]) h.2
-- 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
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ (↑(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]
    (↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)
have simp_rw : ∀ᶠ (x_1 : H) in 𝓝[(↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s] (↑(chartAt H x) : M → H) x,
  (↑(chartAt H' (g' x)) : M' → H') (g' ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) x_1)) =
    (↑(chartAt H' (g x)) : M' → H') (g ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) x_1))
Tactic: simp_rw [EventuallyEq, Function.comp_apply]
-- 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
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ ∀ᶠ (x_1 : H) in 𝓝[(↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s] (↑(chartAt H x) : M → H) x,
    (↑(chartAt H' (g' x)) : M' → H') (g' ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) x_1)) =
      (↑(chartAt H' (g x)) : M' → H') (g ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) x_1))
have rw : ∀ᶠ (x_1 : M) in 𝓝[s] x, (↑(chartAt H' (g' x)) : M' → H') (g' x_1) = (↑(chartAt H' (g x)) : M' → H') (g x_1)
Tactic: rw [(chartAt H x).eventually_nhdsWithin'
    (fun y ↦ chartAt H' (g' x) (g' y) = chartAt H' (g x) (g y)) (mem_chart_source H x)]
-- 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
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
y : M
hy : g' y = g y
⊢ (↑(chartAt H' (g' x)) : M' → H') (g' y) = (↑(chartAt H' (g x)) : M' → H') (g y)
have rw : (↑(chartAt H' (g x)) : M' → H') (g' y) = (↑(chartAt H' (g x)) : M' → H') (g y)
Tactic: rw [hx, hy]
-- 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
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
y : M
hy : g' y = g y
rw : (↑(chartAt H' (g x)) : M' → H') (g' y) = (↑(chartAt H' (g x)) : M' → H') (g y)
⊢ (↑(chartAt H' (g' x)) : M' → H') (g' y) = (↑(chartAt H' (g x)) : M' → H') (g y)
have rw₁ : (↑(chartAt H' (g x)) : M' → H') (g y) = (↑(chartAt H' (g x)) : M' → H') (g y)
Tactic: rw [hx, hy]
-- 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
g : M → M'
s t : Set M
x : M
mono_of_mem_nhdsWithin : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x
h : LiftPropWithinAt P g s x
hst : s ∈ 𝓝[t] x
⊢ LiftPropWithinAt P g t x
have simp : ∀
  (h :
    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 t x ∧
    P ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t) ((↑(chartAt H x) : M → H) x)
Tactic: simp only [liftPropWithinAt_iff'] at h ⊢
Cleared hypotheses: h
-- 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
g : M → M'
s t : Set M
x : M
mono_of_mem_nhdsWithin : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x
hst : s ∈ 𝓝[t] x
h :
  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 t x ∧
    P ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t) ((↑(chartAt H x) : M → H) x)
have refine : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∈
  𝓝[(↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t] (↑(chartAt H x) : M → H) x
Tactic: refine ⟨h.1.mono_of_mem_nhdsWithin hst, mono_of_mem_nhdsWithin ?_ h.2⟩
-- 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
g : M → M'
s t : Set M
x : M
mono_of_mem_nhdsWithin : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x
hst : s ∈ 𝓝[t] x
h :
  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)
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∈
    𝓝[(↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t] (↑(chartAt H x) : M → H) x
have simp_rw : s ∈
  map (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)
    (𝓝[(↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t] (↑(chartAt H x) : M → H) x)
Tactic: simp_rw [← mem_map, (chartAt H x).symm.map_nhdsWithin_preimage_eq (mem_chart_target H x),
    (chartAt H x).left_inv (mem_chart_source H x), hst]
-- 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
g : M → M'
s t : Set M
x : M
mono_of_mem_nhdsWithin : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x
hst : s ∈ 𝓝[t] x
h :
  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)
simp_rw :
  s ∈
    map (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)
      (𝓝[(↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t] (↑(chartAt H x) : M → H) x)
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∈
    𝓝[(↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t] (↑(chartAt H x) : M → H) x
have simp_rw₁ : s ∈ 𝓝[t] (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑(chartAt H x) : M → H) x)
Tactic: simp_rw [← mem_map, (chartAt H x).symm.map_nhdsWithin_preimage_eq (mem_chart_target H x),
    (chartAt H x).left_inv (mem_chart_source H x), hst]
-- 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
g : M → M'
s t : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
⊢ LiftPropWithinAt P g t x
have refine : ∀ (y : H) (hy : y ∈ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t),
  y ∈ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s
Tactic: refine ⟨h.1.mono hts, mono (fun y hy ↦ ?_) h.2⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
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
g : M → M'
s t : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
y : H
hy : y ∈ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' t
⊢ y ∈ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s
have hy₁ : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) y ∈ t
Tactic: simp only [mfld_simps] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
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
g : M → M'
s : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropAt P g x
⊢ LiftPropWithinAt P g s x
have h₁ : LiftPropWithinAt P g univ x
Tactic: rw [← liftPropWithinAt_univ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
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
g : M → M'
s : Set M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftProp P g
⊢ LiftPropOn P g s
have h₁ : LiftPropOn P g univ
Tactic: rw [← liftPropOn_univ] at h
Cleared hypotheses: h
-- 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
e : OpenPartialHomeomorph M H
x : M
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.source
⊢ LiftPropAt Q (↑e : M → H) x
have simp_rw : Q ((↑(OpenPartialHomeomorph.refl H) : H → H) ∘ (↑e : M → H) ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' univ)
  ((↑e : M → H) x)
Tactic: simp_rw [LiftPropAt, hG.liftPropWithinAt_indep_chart he hx G.id_mem_maximalAtlas (mem_univ _),
    (e.continuousAt hx).continuousWithinAt, true_and]
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
x : M
hx : x ∈ e.source
⊢ LiftPropWithinAt Q (↑e : M → H) e.source x
have apply : e.source ∈ 𝓝 x
Tactic: apply hG.liftPropWithinAt_of_liftPropAt_of_mem_nhds (hG.liftPropAt_of_mem_maximalAtlas hQ he hx)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
Goal:
H : Type u_1
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.target
h : Q ((↑e : M → H) ∘ (↑e.symm : H → M)) univ x
⊢ LiftPropAt Q (↑e.symm : H → M) x
have this : (↑e.symm : H → M) x ∈ e.source
Tactic: have : e.symm x ∈ e.source := by simp only [hx, mfld_simps]
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.target
h : Q ((↑e : M → H) ∘ (↑e.symm : H → M)) univ x
this : (↑e.symm : H → M) x ∈ e.source
⊢ LiftPropAt Q (↑e.symm : H → M) x
have rw : ContinuousWithinAt (↑e.symm : H → M) univ x ∧
  Q ((↑e : M → H) ∘ (↑e.symm : H → M) ∘ (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H)) : H → H))
    ((↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H)) : H → H) ⁻¹' univ)
    ((↑(OpenPartialHomeomorph.refl H) : H → H) x)
Tactic: rw [LiftPropAt, hG.liftPropWithinAt_indep_chart G.id_mem_maximalAtlas (mem_univ _) he this]
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.target
h : Q ((↑e : M → H) ∘ (↑e.symm : H → M)) univ x
this : (↑e.symm : H → M) x ∈ e.source
⊢ ContinuousWithinAt (↑e.symm : H → M) univ x ∧
    Q ((↑e : M → H) ∘ (↑e.symm : H → M) ∘ (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H)) : H → H))
      ((↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H)) : H → H) ⁻¹' univ)
      ((↑(OpenPartialHomeomorph.refl H) : H → H) x)
have refine : Q ((↑e : M → H) ∘ (↑e.symm : H → M) ∘ (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H)) : H → H))
  ((↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H)) : H → H) ⁻¹' univ)
  ((↑(OpenPartialHomeomorph.refl H) : H → H) x)
Tactic: refine ⟨(e.symm.continuousAt hx).continuousWithinAt, ?_⟩
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
hx : x ∈ e.target
⊢ LiftPropAt Q (↑e.symm : H → M) x
have suffices : Q ((↑e : M → H) ∘ (↑e.symm : H → M)) univ x
Tactic: suffices h : Q (e ∘ e.symm) univ x by
    have : e.symm x ∈ e.source := by simp only [hx, mfld_simps]
    rw [LiftPropAt, hG.liftPropWithinAt_indep_chart G.id_mem_maximalAtlas (mem_univ _) he this]
    refine ⟨(e.symm.continuousAt hx).continuousWithinAt, ?_⟩
    simp only [h, mfld_simps]
-- 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
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst_3 : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
x : H
hx : x ∈ e.target
⊢ LiftPropWithinAt Q (↑e.symm : H → M) e.target x
have apply : e.target ∈ 𝓝 x
Tactic: apply hG.liftPropWithinAt_of_liftPropAt_of_mem_nhds
    (hG.liftPropAt_symm_of_mem_maximalAtlas hQ he hx)
-- 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
⊢ LiftProp.{u_1, u_2, u_1, u_2} (M := M) Q id
have simp_rw : ∀ (x : M),
  Q ((↑(chartAt H (id x)) : M → H) ∘ id ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
    ((↑(chartAt H x) : M → H) x)
Tactic: simp_rw [liftProp_iff, continuous_id, true_and]
-- 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
⊢ LiftPropAt P f (↑x : M) ↔ LiftPropAt P (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x
have simp : ContinuousWithinAt f univ (↑x : M) ∧
    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)) ↔
  ContinuousWithinAt (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) univ x ∧
    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)
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 : Opens M
f : M → M'
x : ↥U
⊢ ContinuousWithinAt f univ (↑x : M) ∧
      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)) ↔
    ContinuousWithinAt (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) univ x ∧
      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 : ContinuousWithinAt f univ (↑x : M) ↔ ContinuousWithinAt (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) 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 : Opens M
f : M → M'
x : ↥U
a : ContinuousWithinAt f univ (↑x : M) ↔ ContinuousWithinAt (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) univ x
⊢ ContinuousWithinAt f univ (↑x : M) ∧
      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)) ↔
    ContinuousWithinAt (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) univ x ∧
      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₁ : 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)
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 : Opens M
f : M → M'
x : ↥U
⊢ ContinuousWithinAt f univ (↑x : M) ↔ ContinuousWithinAt (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) univ x
have a : ContinuousAt f (↑x : M) ↔ ContinuousAt (f ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x
Tactic: simp_rw [continuousWithinAt_univ, U.isOpenEmbedding'.continuousAt_iff]