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
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
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)
⊢ 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₁ : (↑e : M → H) x ∈ (e.symm ≫ₕ e').source
Tactic: rw [← hG.right_invariance (compatible_of_mem_maximalAtlas he he')]
-- 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 ≫ₕ 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)
have simp_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' : M → H) x) ↔
  P (g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)
Tactic: simp_rw [OpenPartialHomeomorph.trans_apply, e.left_inv xe]
-- 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 ≫ₕ e').symm : H → H))
      ((↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑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 : H → M) ⁻¹' s) ((↑e' : M → H) x) ↔
  P (g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)
Tactic: rw [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
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
rw :
  P (g ∘ (↑e'.symm : H → M)) ((↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s) ((↑e' : M → H) x) ↔
    P (g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)
⊢ P ((g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H))
      ((↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑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₁ : (g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H) =ᶠ[𝓝 ((↑e' : M → H) x)] g ∘ (↑e'.symm : H → M)
Tactic: rw [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
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
rw :
  P (g ∘ (↑e'.symm : H → M)) ((↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s) ((↑e' : M → H) x) ↔
    P (g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)
rw₁ : (g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H) =ᶠ[𝓝 ((↑e' : M → H) x)] g ∘ (↑e'.symm : H → M)
⊢ P ((g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H))
      ((↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑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₂ : H → H'
Tactic: rw [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
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 ≫ₕ e').symm : H → H) ⁻¹' (↑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 refine : (↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s =ᶠ[𝓝 ((↑e' : M → H) x)] (↑e'.symm : H → M) ⁻¹' s
Tactic: refine 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
⊢ (↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s =ᶠ[𝓝 ((↑e' : M → H) x)] (↑e'.symm : H → M) ⁻¹' s
have refine_1 : (↑e'.symm : H → M) ⁻¹' e.source ∈ 𝓝 ((↑e' : M → H) x)
Tactic: refine (eventually_of_mem ?_ fun y (hy : y ∈ e'.symm ⁻¹' e.source) ↦ ?_).set_eq
-- 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
refine_1 : (↑e'.symm : H → M) ⁻¹' e.source ∈ 𝓝 ((↑e' : M → H) x)
⊢ (↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s =ᶠ[𝓝 ((↑e' : M → H) x)] (↑e'.symm : H → M) ⁻¹' s
have refine_2 : ∀ (y : H) (hy : y ∈ (↑e'.symm : H → M) ⁻¹' e.source),
  y ∈ (↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s ↔ y ∈ (↑e'.symm : H → M) ⁻¹' s
Tactic: refine (eventually_of_mem ?_ fun y (hy : y ∈ e'.symm ⁻¹' e.source) ↦ ?_).set_eq
-- 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
⊢ (↑e'.symm : H → M) ⁻¹' e.source ∈ 𝓝 ((↑e' : M → H) x)
have refine_1 : (↑e'.symm : H → M) ((↑e' : M → H) x) ∈ e.source
Tactic: refine (e'.symm.continuousAt <| e'.mapsTo xe').preimage_mem_nhds (e.open_source.mem_nhds ?_)
-- 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
y : H
hy : y ∈ (↑e'.symm : H → M) ⁻¹' e.source
⊢ y ∈ (↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s ↔ y ∈ (↑e'.symm : H → M) ⁻¹' s
have refine_2 : (↑e.symm : H → M) ((↑(e.symm ≫ₕ e').symm : H → H) y) ∈ s ↔ (↑e'.symm : H → M) y ∈ s
Tactic: simp_rw [mem_preimage, OpenPartialHomeomorph.coe_trans_symm, OpenPartialHomeomorph.symm_symm,
      Function.comp_apply, e.left_inv hy]
-- 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
y : H
hy : y ∈ (↑e'.symm : H → M) ⁻¹' e.source
refine_2 : (↑e.symm : H → M) ((↑(e.symm ≫ₕ e').symm : H → H) y) ∈ s ↔ (↑e'.symm : H → M) y ∈ s
⊢ y ∈ (↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s ↔ y ∈ (↑e'.symm : H → M) ⁻¹' s
have refine_2₁ : (↑e.symm : H → M) (((↑e.symm.symm : M → H) ∘ (↑e'.symm : H → M)) y) ∈ s ↔ (↑e'.symm : H → M) y ∈ s
Tactic: simp_rw [mem_preimage, OpenPartialHomeomorph.coe_trans_symm, OpenPartialHomeomorph.symm_symm,
      Function.comp_apply, e.left_inv hy]
-- 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
y : H
hy : y ∈ (↑e'.symm : H → M) ⁻¹' e.source
refine_2 : (↑e.symm : H → M) ((↑(e.symm ≫ₕ e').symm : H → H) y) ∈ s ↔ (↑e'.symm : H → M) y ∈ s
refine_2₁ : (↑e.symm : H → M) (((↑e.symm.symm : M → H) ∘ (↑e'.symm : H → M)) y) ∈ s ↔ (↑e'.symm : H → M) y ∈ s
⊢ y ∈ (↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s ↔ y ∈ (↑e'.symm : H → M) ⁻¹' s
have refine_2₂ : (↑e.symm : H → M) (((↑e : M → H) ∘ (↑e'.symm : H → M)) y) ∈ s ↔ (↑e'.symm : H → M) y ∈ s
Tactic: simp_rw [mem_preimage, OpenPartialHomeomorph.coe_trans_symm, OpenPartialHomeomorph.symm_symm,
      Function.comp_apply, e.left_inv hy]
-- 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
y : H
hy : y ∈ (↑e'.symm : H → M) ⁻¹' e.source
refine_2 : (↑e.symm : H → M) ((↑(e.symm ≫ₕ e').symm : H → H) y) ∈ s ↔ (↑e'.symm : H → M) y ∈ s
refine_2₁ : (↑e.symm : H → M) (((↑e.symm.symm : M → H) ∘ (↑e'.symm : H → M)) y) ∈ s ↔ (↑e'.symm : H → M) y ∈ s
refine_2₂ : (↑e.symm : H → M) (((↑e : M → H) ∘ (↑e'.symm : H → M)) y) ∈ s ↔ (↑e'.symm : H → M) y ∈ s
⊢ y ∈ (↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s ↔ y ∈ (↑e'.symm : H → M) ⁻¹' s
have refine_2₃ : (↑e.symm : H → M) ((↑e : M → H) ((↑e'.symm : H → M) y)) ∈ s ↔ (↑e'.symm : H → M) y ∈ s
Tactic: simp_rw [mem_preimage, OpenPartialHomeomorph.coe_trans_symm, OpenPartialHomeomorph.symm_symm,
      Function.comp_apply, e.left_inv hy]
-- 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
⊢ (g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H) =ᶠ[𝓝 ((↑e' : M → H) x)] g ∘ (↑e'.symm : H → M)
have refine : ∀ (y : H) (hy : (↑e.symm : H → M) ((↑e : M → H) ((↑e'.symm : H → M) y)) = (↑e'.symm : H → M) y),
  ((g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H)) y = (g ∘ (↑e'.symm : H → M)) y
Tactic: refine ((e'.eventually_nhds' _ xe').mpr <| e.eventually_left_inverse xe).mono fun y hy ↦ ?_
-- 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
y : H
hy : (↑e.symm : H → M) ((↑e : M → H) ((↑e'.symm : H → M) y)) = (↑e'.symm : H → M) y
⊢ ((g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H)) y = (g ∘ (↑e'.symm : H → M)) y
have simp : g ((↑e.symm : H → M) ((↑e : M → H) ((↑e'.symm : H → M) y))) = g ((↑e'.symm : H → M) y)
Tactic: simp only [mfld_simps]
-- 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
y : H
hy : (↑e.symm : H → M) ((↑e : M → H) ((↑e'.symm : H → M) y)) = (↑e'.symm : H → M) y
⊢ g ((↑e.symm : H → M) ((↑e : M → H) ((↑e'.symm : H → M) y))) = g ((↑e'.symm : H → M) y)
have rw : g ((↑e'.symm : H → M) y) = g ((↑e'.symm : H → M) y)
Tactic: rw [hy]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : H → M'
x : H
s : Set H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
⊢ P ((↑f : M' → H') ∘ g) s x ↔ P ((↑f' : M' → H') ∘ g) s x
have hcont : ContinuousWithinAt ((↑f : M' → H') ∘ g) s x
Tactic: have hcont : ContinuousWithinAt (f ∘ g) s x := (f.continuousAt xf).comp_continuousWithinAt hgs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : H → M'
x : H
s : Set H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
hcont : ContinuousWithinAt ((↑f : M' → H') ∘ g) s x
⊢ P ((↑f : M' → H') ∘ g) s x ↔ P ((↑f' : M' → H') ∘ g) s x
have rw : P ((↑(f.symm ≫ₕ f') : H' → H') ∘ (↑f : M' → H') ∘ g) s x ↔ P ((↑f' : M' → H') ∘ g) s x
Tactic: rw [← hG.left_invariance (compatible_of_mem_maximalAtlas hf hf') hcont
      (by simp only [xf, xf', mfld_simps])]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : H → M'
x : H
s : Set H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
hcont : ContinuousWithinAt ((↑f : M' → H') ∘ g) s x
⊢ P ((↑(f.symm ≫ₕ f') : H' → H') ∘ (↑f : M' → H') ∘ g) s x ↔ P ((↑f' : M' → H') ∘ g) s x
have refine : (↑(f.symm ≫ₕ f') : H' → H') ∘ (↑f : M' → H') ∘ g =ᶠ[𝓝[s] x] (↑f' : M' → H') ∘ g
Tactic: refine hG.congr_iff_nhdsWithin ?_ (by simp only [xf, mfld_simps])
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
inst_4 : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : OpenPartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
⊢ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → X)) ((↑e.symm : H → X) ⁻¹' s) ((↑e : X → H) x) ↔
    P ((↑f' : M' → H') ∘ g ∘ (↑e.symm : H → X)) ((↑e.symm : H → X) ⁻¹' s) ((↑e : X → H) x)
have xf₁ : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f.source
Tactic: rw [← e.left_inv xe] at xf xf' hgs
Cleared hypotheses: xf, hf', xf', hgs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
inst_4 : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : OpenPartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
xf₁ : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f.source
hf'₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
⊢ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → X)) ((↑e.symm : H → X) ⁻¹' s) ((↑e : X → H) x) ↔
    P ((↑f' : M' → H') ∘ g ∘ (↑e.symm : H → X)) ((↑e.symm : H → X) ⁻¹' s) ((↑e : X → H) x)
have xf'₁ : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f'.source
Tactic: rw [← e.left_inv xe] at xf xf' hgs
Cleared hypotheses: xf, hf', xf', hgs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
inst_4 : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : OpenPartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
xf₁ : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f.source
hf'₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf'₁ : g ((↑e.symm : H → X) ((↑e : X → H) x)) ∈ f'.source
⊢ P ((↑f : M' → H') ∘ g ∘ (↑e.symm : H → X)) ((↑e.symm : H → X) ⁻¹' s) ((↑e : X → H) x) ↔
    P ((↑f' : M' → H') ∘ g ∘ (↑e.symm : H → X)) ((↑e.symm : H → X) ⁻¹' s) ((↑e : X → H) x)
have hgs₁ : ContinuousWithinAt g s ((↑e.symm : H → X) ((↑e : X → H) x))
Tactic: rw [← e.left_inv xe] at xf xf' hgs
Cleared hypotheses: xf, hf', xf', hgs