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'
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'
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 ∧ LiftPropWithinAt P ((↑f : M' → H') ∘ g) s x
have rw : 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 ((↑f : M' → H') ∘ g) s x ∧
      P (((↑f : M' → H') ∘ g) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x))
Tactic: rw [liftPropWithinAt_self_target, liftPropWithinAt_iff', and_congr_right_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'
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'
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hg : 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 ((↑f : M' → H') ∘ g) s x ∧
      P (((↑f : 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 simp_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 (((↑f : M' → H') ∘ g) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
Tactic: simp_rw [(f.continuousAt xf).comp_continuousWithinAt hg, 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'
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 ∧
      LiftPropWithinAt P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
have rw : ContinuousWithinAt g s x ∧ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x) →
  ContinuousWithinAt ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
Tactic: rw [hG.liftPropWithinAt_indep_chart he xe hf xf, liftPropWithinAt_self, and_left_comm,
    Iff.comm, and_iff_right_iff_imp]
-- 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'
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
h : ContinuousWithinAt g s x ∧ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
⊢ ContinuousWithinAt ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
have h1 : ContinuousWithinAt (g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e.symm.symm : M → H) x)
Tactic: have h1 := (e.symm.continuousWithinAt_iff_continuousWithinAt_comp_right xe).mp h.1
-- 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
h : ContinuousWithinAt g s x ∧ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
h1 : ContinuousWithinAt (g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e.symm.symm : M → H) x)
⊢ ContinuousAt (↑f : M' → H') ((g ∘ (↑e.symm : H → M)) ((↑e : M → H) x))
have simp_rw : ContinuousAt (↑f : M' → H') (g ((↑e.symm : H → M) ((↑e : M → H) x)))
Tactic: simp_rw [Function.comp, e.left_inv xe, f.continuousAt 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 : 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
h : ContinuousWithinAt g s x ∧ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
h1 : ContinuousWithinAt (g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e.symm.symm : M → H) x)
simp_rw : ContinuousAt (↑f : M' → H') (g ((↑e.symm : H → M) ((↑e : M → H) x)))
⊢ ContinuousAt (↑f : M' → H') ((g ∘ (↑e.symm : H → M)) ((↑e : M → H) x))
have simp_rw₁ : ContinuousAt (↑f : M' → H') (g x)
Tactic: simp_rw [Function.comp, e.left_inv xe, f.continuousAt xf]
-- 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'
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
h : ContinuousWithinAt g s x ∧ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
h1 : ContinuousWithinAt (g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e.symm.symm : M → H) x)
⊢ ContinuousWithinAt ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x)
have this : ContinuousAt (↑f : M' → H') ((g ∘ (↑e.symm : H → M)) ((↑e : M → H) x))
Tactic: have : ContinuousAt f ((g ∘ e.symm) (e x)) := by
    simp_rw [Function.comp, e.left_inv xe, f.continuousAt 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 : OpenPartialHomeomorph M H
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set 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
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
h : LiftPropOn P g s
y : H
hy : y ∈ e.target ∩ (↑e.symm : H → M) ⁻¹' (s ∩ g ⁻¹' f.source)
⊢ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) y
have h₁ : y = (↑e : M → H) ((↑e.symm : H → M) y)
Tactic: convert! ((hG.liftPropWithinAt_indep_chart he (e.symm_mapsTo hy.1) hf hy.2.2).1 (h _ hy.2.1)).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'
e : OpenPartialHomeomorph M H
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set 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
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
h : LiftPropOn P g s
y : H
hy : y ∈ e.target ∩ (↑e.symm : H → M) ⁻¹' (s ∩ g ⁻¹' f.source)
⊢ y = (↑e : M → H) ((↑e.symm : H → M) y)
have h₁ : y = y
Tactic: rw [e.right_inv hy.1]
-- 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 : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
ht : t ∈ 𝓝[s] x
⊢ LiftPropWithinAt P g (s ∩ t) x ↔ LiftPropWithinAt P g s x
have rw : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' (s ∩ t) =ᶠ[𝓝 ((↑(chartAt H x) : M → H) x)]
  (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s
Tactic: rw [liftPropWithinAt_iff', liftPropWithinAt_iff', continuousWithinAt_inter' ht, 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
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 : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
ht : t ∈ 𝓝[s] x
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' (s ∩ t) =ᶠ[𝓝 ((↑(chartAt H x) : M → H) x)]
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s
have simp_rw : ∀ᶠ (x : M) in 𝓝 x, x ∈ s ∩ t ↔ x ∈ s
Tactic: simp_rw [eventuallyEq_set, mem_preimage,
    (chartAt _ x).eventually_nhds' (fun x ↦ x ∈ s ∩ t ↔ x ∈ s) (mem_chart_source _ 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 : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
hu : s =ᶠ[𝓝 x] t
⊢ LiftPropWithinAt P g s x ↔ LiftPropWithinAt P g t x
have rw : LiftPropWithinAt P g (s ∩ {x : M | (fun (x : M) ↦ s x = t x) x}) x =
  LiftPropWithinAt P g (t ∩ {x : M | (fun (x : M) ↦ s x = t x) x}) x
Tactic: rw [← hG.liftPropWithinAt_inter (s := s) hu, ← hG.liftPropWithinAt_inter (s := t) hu,
    ← eq_iff_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
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
hu : s =ᶠ[𝓝 x] t
⊢ LiftPropWithinAt P g (s ∩ {x : M | (fun (x : M) ↦ s x = t x) x}) x =
    LiftPropWithinAt P g (t ∩ {x : M | (fun (x : M) ↦ s x = t x) x}) x
have e_s : s ∩ {x : M | (fun (x : M) ↦ s x = t x) x} = t ∩ {x : M | (fun (x : M) ↦ s x = t x) x}
Tactic: congr 1
-- 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 : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
hs : s ∈ 𝓝 x
⊢ LiftPropAt P g x
have rwa : ∀ (h : LiftPropWithinAt P g (univ ∩ s) x) (hs : s ∈ 𝓝 x), LiftPropAt P g x
Tactic: rwa [← univ_inter s, hG.liftPropWithinAt_inter hs] at h
Cleared hypotheses: h, hs
-- 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 : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
hs : s ∈ 𝓝 x
rwa : ∀ (h : LiftPropWithinAt P g (univ ∩ s) x) (hs : s ∈ 𝓝 x), LiftPropAt P g x
⊢ LiftPropAt P g x
have rwa₁ : ∀ (h : LiftPropWithinAt P g univ x) (hs : s ∈ 𝓝 x), LiftPropAt P g x
Tactic: rwa [← univ_inter s, hG.liftPropWithinAt_inter hs] at h
Cleared hypotheses: h, hs
-- 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 : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropAt P g x
hs : s ∈ 𝓝 x
⊢ LiftPropWithinAt P g s x
have rwa : LiftPropWithinAt P g (univ ∩ s) x
Tactic: rwa [← univ_inter s, hG.liftPropWithinAt_inter hs]
-- 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 : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropAt P g x
hs : s ∈ 𝓝 x
rwa : LiftPropWithinAt P g (univ ∩ s) x
⊢ LiftPropWithinAt P g s x
have rwa₁ : LiftPropWithinAt P g univ x
Tactic: rwa [← univ_inter s, hG.liftPropWithinAt_inter hs]
-- 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 : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
h : ∀ x ∈ s, ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g (s ∩ u)
x : M
hx : x ∈ s
⊢ LiftPropWithinAt P g s x
have rcases : ∀ (u : Set M) (u_open : IsOpen[inst_1] u) (xu : x ∈ u) (hu : LiftPropOn P g (s ∩ u)), LiftPropWithinAt P g s x
Tactic: rcases h x hx with ⟨u, u_open, xu, hu⟩
-- 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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
h : ∀ x ∈ s, ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g (s ∩ u)
x : M
hx : x ∈ s
u : Set M
u_open : IsOpen[inst_1] u
xu : x ∈ u
hu : LiftPropOn P g (s ∩ u)
⊢ LiftPropWithinAt P g s x
have this : LiftPropWithinAt P g (s ∩ u) x
Tactic: have := hu x ⟨hx, xu⟩
-- 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 : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
h : ∀ x ∈ s, ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g (s ∩ u)
x : M
hx : x ∈ s
u : Set M
u_open : IsOpen[inst_1] u
xu : x ∈ u
hu : LiftPropOn P g (s ∩ u)
this : LiftPropWithinAt P g (s ∩ u) x
⊢ LiftPropWithinAt P g s x
have rwa : u ∈ 𝓝 x
Tactic: rwa [hG.liftPropWithinAt_inter] at this
-- 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 : M → M'
hG : G.LocalInvariantProp G' P
h : ∀ (x : M), ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g u
⊢ LiftProp P g
have rw : LiftPropOn P g univ
Tactic: rw [← liftPropOn_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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
hG : G.LocalInvariantProp G' P
h : ∀ (x : M), ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g u
⊢ LiftPropOn P g univ
have refine : ∀ (x : M), Membership.mem (γ := Set M) univ x → ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g (univ ∩ u)
Tactic: refine hG.liftPropOn_of_locally_liftPropOn fun 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
⊢ LiftPropWithinAt P g' s 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)
Tactic: refine ⟨h.1.congr_of_eventuallyEq h₁ 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'
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))
      ((↑(chartAt H x) : M → H) x) =
    ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(chartAt H x) : M → H) x)
have simp_rw : (↑(chartAt H' (g' x)) : M' → H')
    (g' ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑(chartAt H x) : M → H) x))) =
  (↑(chartAt H' (g x)) : M' → H')
    (g ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑(chartAt H x) : M → H) x)))
Tactic: simp_rw [Function.comp_apply, (chartAt H x).left_inv (mem_chart_source H x), 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'
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
simp_rw :
  (↑(chartAt H' (g' x)) : M' → H')
      (g' ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑(chartAt H x) : M → H) x))) =
    (↑(chartAt H' (g x)) : M' → H')
      (g ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑(chartAt H x) : M → H) x)))
⊢ ((↑(chartAt H' (g' x)) : M' → H') ∘ g' ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(chartAt H x) : M → H) x) =
    ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(chartAt H x) : M → H) x)
have simp_rw₁ : (↑(chartAt H' (g' x)) : M' → H') (g' x) = (↑(chartAt H' (g x)) : M' → H') (g x)
Tactic: simp_rw [Function.comp_apply, (chartAt H x).left_inv (mem_chart_source H x), hx]