awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
s : Opens M
inst_4 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
he : e ∈ w
x : ↥s
hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w
w_1 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
he' : e' ∈ w_1
x' : ↥s
hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1
⊢ e.symm ≫ₕ e' ∈ G
have rw : ∀ (he : e = subtypeRestr (chartAt H (↑x : M)) sorry)
  (hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) sorry} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w)
  (w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (he' : e' ∈ w) (x' : ↥s)
  (hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) sorry} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w),
  e.symm ≫ₕ e' ∈ G
Tactic: rw [hc.symm, mem_singleton_iff] at he
Cleared hypotheses: he, hc, w_1, he', x', hc'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
s : Opens M
inst_4 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x : ↥s
he : e = subtypeRestr (chartAt H (↑x : M)) ⋯
hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w
w_1 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
he' : e' ∈ w_1
x' : ↥s
hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1
⊢ e.symm ≫ₕ e' ∈ G
have he'₁ : e' = subtypeRestr (chartAt H (↑x' : M)) sorry
Tactic: rw [hc'.symm, mem_singleton_iff] at he'
Cleared hypotheses: he', hc'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
s : Opens M
inst_4 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x : ↥s
he : e = subtypeRestr (chartAt H (↑x : M)) ⋯
hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w
w_1 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x' : ↥s
he' : e' = subtypeRestr (chartAt H (↑x' : M)) ⋯
hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1
⊢ e.symm ≫ₕ e' ∈ G
have rw : OpenPartialHomeomorph.symm (subtypeRestr (chartAt H (↑x : M)) sorry) ≫ₕ subtypeRestr (chartAt H (↑x' : M)) sorry ∈ G
Tactic: rw [he, he']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
s : Opens M
inst_4 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x : ↥s
he : e = subtypeRestr (chartAt H (↑x : M)) ⋯
hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w
w_1 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x' : ↥s
he' : e' = subtypeRestr (chartAt H (↑x' : M)) ⋯
hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1
⊢ OpenPartialHomeomorph.symm (subtypeRestr (chartAt H (↑x : M)) ⋯) ≫ₕ subtypeRestr (chartAt H (↑x' : M)) ⋯ ∈ G
have refine : OpenPartialHomeomorph.restr (OpenPartialHomeomorph.symm (chartAt H (↑x : M)) ≫ₕ chartAt H (↑x' : M))
    ((toPartialEquiv (chartAt H (↑x : M))).target ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) ⁻¹' (↑s : Set M)) ∈
  G
Tactic: refine G.mem_of_eqOnSource ?_
      (subtypeRestr_symm_trans_subtypeRestr (s := s) _ (chartAt H x) (chartAt H x'))
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
s : Opens M
inst_4 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x : ↥s
he : e = subtypeRestr (chartAt H (↑x : M)) ⋯
hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w
w_1 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x' : ↥s
he' : e' = subtypeRestr (chartAt H (↑x' : M)) ⋯
hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1
⊢ OpenPartialHomeomorph.restr (OpenPartialHomeomorph.symm (chartAt H (↑x : M)) ≫ₕ chartAt H (↑x' : M))
      ((toPartialEquiv (chartAt H (↑x : M))).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) ⁻¹' (↑s : Set M)) ∈
    G
have he₁ : OpenPartialHomeomorph.symm (chartAt H (↑x : M)) ≫ₕ chartAt H (↑x' : M) ∈ G
Tactic: apply closedUnderRestriction'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
s : Opens M
inst_4 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x : ↥s
he : e = subtypeRestr (chartAt H (↑x : M)) ⋯
hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w
w_1 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x' : ↥s
he' : e' = subtypeRestr (chartAt H (↑x' : M)) ⋯
hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1
he₁ : OpenPartialHomeomorph.symm (chartAt H (↑x : M)) ≫ₕ chartAt H (↑x' : M) ∈ G
⊢ OpenPartialHomeomorph.restr (OpenPartialHomeomorph.symm (chartAt H (↑x : M)) ≫ₕ chartAt H (↑x' : M))
      ((toPartialEquiv (chartAt H (↑x : M))).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) ⁻¹' (↑s : Set M)) ∈
    G
have hs : IsOpen[inst]
  ((toPartialEquiv (chartAt H (↑x : M))).target ∩
    (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) ⁻¹' (↑s : Set M))
Tactic: apply closedUnderRestriction'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U : Opens M
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H (↑x : M)
⊢ (e.subtypeRestr ⋯).target ∈ 𝓝 ((↑e : M → H) (↑x : M))
have apply : (↑e : M → H) (↑x : M) ∈ (e.subtypeRestr sorry).target
Tactic: apply (e.subtypeRestr ⟨x⟩).open_target.mem_nhds
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U : Opens M
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H (↑x : M)
⊢ (↑e.symm : H → M) =ᶠ[𝓝 ((↑e : M → H) (↑x : M))]
    Subtype.val (p := fun (x : M) ↦ x ∈ U) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U)
have heUx_nhds : (e.subtypeRestr sorry).target ∈ 𝓝 ((↑e : M → H) (↑x : M))
Tactic: have heUx_nhds : (e.subtypeRestr ⟨x⟩).target ∈ 𝓝 (e x) := by
    apply (e.subtypeRestr ⟨x⟩).open_target.mem_nhds
    exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U V : Opens M
hUV : U ≤ V
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H (↑x : M)
⊢ (e.subtypeRestr ⋯).target ∈ 𝓝 ((↑e : M → H) (↑x : M))
have apply : (↑e : M → H) (↑x : M) ∈ (e.subtypeRestr sorry).target
Tactic: apply (e.subtypeRestr ⟨x⟩).open_target.mem_nhds
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U V : Opens M
hUV : U ≤ V
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H (↑x : M)
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H (inclusion hUV x))) :
      H →
        ↥V) =ᶠ[𝓝
      ((↑(chartAt H (inclusion hUV x)) : ↥V → H) (Set.inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))]
    inclusion hUV ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U)
have heUx_nhds : (e.subtypeRestr sorry).target ∈ 𝓝 ((↑e : M → H) (↑x : M))
Tactic: have heUx_nhds : (e.subtypeRestr ⟨x⟩).target ∈ 𝓝 (e x) := by
    apply (e.subtypeRestr ⟨x⟩).open_target.mem_nhds
    exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
s : Opens M
hs : Nonempty.{u_2 + 1} ↥s
G : StructureGroupoid H
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (atlas H ↥s) e'
⊢ (e.subtypeRestr hs).symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e.subtypeRestr hs ∈ G
have obtain : ∀ (x : ↥s) (this : e' = subtypeRestr (chartAt H (↑x : M)) hs),
  (e.subtypeRestr hs).symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e.subtypeRestr hs ∈ G
Tactic: obtain ⟨x, this⟩ := Opens.chart_eq hs he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
s : Opens M
hs : Nonempty.{u_2 + 1} ↥s
G : StructureGroupoid H
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (atlas H ↥s) e'
x : ↥s
this : e' = subtypeRestr (chartAt H (↑x : M)) hs
⊢ (e.subtypeRestr hs).symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e.subtypeRestr hs ∈ G
have rw : (e.subtypeRestr hs).symm ≫ₕ subtypeRestr (chartAt H (↑x : M)) hs ∈ G ∧
  OpenPartialHomeomorph.symm (subtypeRestr (chartAt H (↑x : M)) hs) ≫ₕ e.subtypeRestr hs ∈ G
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
H' : Type u_1
M_1 : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M_1
inst_2 : ChartedSpace H M_1
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : HasGroupoid M G
c c' : OpenPartialHomeomorph M H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c'
⊢ c.symm ≫ₕ Homeomorph.toOpenPartialHomeomorph (Homeomorph.refl M) ≫ₕ c' ∈ G
have change : c.symm ≫ₕ OpenPartialHomeomorph.refl M ≫ₕ c' ∈ G
Tactic: change OpenPartialHomeomorph.symm c ≫ₕ OpenPartialHomeomorph.refl M ≫ₕ c' ∈ G
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
H' : Type u_1
M_1 : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M_1
inst_2 : ChartedSpace H M_1
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : HasGroupoid M G
c c' : OpenPartialHomeomorph M H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c'
⊢ c.symm ≫ₕ OpenPartialHomeomorph.refl M ≫ₕ c' ∈ G
have rw : c.symm ≫ₕ c' ∈ G
Tactic: rw [OpenPartialHomeomorph.refl_trans]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
c : OpenPartialHomeomorph M' H
c' : OpenPartialHomeomorph M H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c'
⊢ c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
have this : (c'.symm ≫ₕ e.toOpenPartialHomeomorph ≫ₕ c).symm ∈ G
Tactic: have : (c'.symm ≫ₕ e.toHomeomorph.toOpenPartialHomeomorph ≫ₕ c).symm ∈ G :=
        G.symm (e.mem_groupoid c' c hc' hc)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
c : OpenPartialHomeomorph M' H
c' : OpenPartialHomeomorph M H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c'
this : (c'.symm ≫ₕ e.toOpenPartialHomeomorph ≫ₕ c).symm ∈ G
⊢ c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
have rwa : ∀ (this : (e.toOpenPartialHomeomorph ≫ₕ c).symm ≫ₕ c'.symm.symm ∈ G), c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
Tactic: rwa [trans_symm_eq_symm_trans_symm, trans_symm_eq_symm_trans_symm, symm_symm, trans_assoc]
        at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
c : OpenPartialHomeomorph M' H
c' : OpenPartialHomeomorph M H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c'
this : (c'.symm ≫ₕ e.toOpenPartialHomeomorph ≫ₕ c).symm ∈ G
rwa :
  ∀ (this : (e.toOpenPartialHomeomorph ≫ₕ c).symm ≫ₕ c'.symm.symm ∈ G),
    c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
⊢ c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
have rwa₁ : ∀ (this : (c.symm ≫ₕ e.toOpenPartialHomeomorph.symm) ≫ₕ c'.symm.symm ∈ G),
  c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
Tactic: rwa [trans_symm_eq_symm_trans_symm, trans_symm_eq_symm_trans_symm, symm_symm, trans_assoc]
        at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
c : OpenPartialHomeomorph M' H
c' : OpenPartialHomeomorph M H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c'
this : (c'.symm ≫ₕ e.toOpenPartialHomeomorph ≫ₕ c).symm ∈ G
rwa :
  ∀ (this : (e.toOpenPartialHomeomorph ≫ₕ c).symm ≫ₕ c'.symm.symm ∈ G),
    c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
rwa₁ :
  ∀ (this : (c.symm ≫ₕ e.toOpenPartialHomeomorph.symm) ≫ₕ c'.symm.symm ∈ G),
    c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
⊢ c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
have rwa₂ : ∀ (this : (c.symm ≫ₕ e.toOpenPartialHomeomorph.symm) ≫ₕ c' ∈ G), c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
Tactic: rwa [trans_symm_eq_symm_trans_symm, trans_symm_eq_symm_trans_symm, symm_symm, trans_assoc]
        at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
c : OpenPartialHomeomorph M' H
c' : OpenPartialHomeomorph M H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c'
this : (c'.symm ≫ₕ e.toOpenPartialHomeomorph ≫ₕ c).symm ∈ G
rwa :
  ∀ (this : (e.toOpenPartialHomeomorph ≫ₕ c).symm ≫ₕ c'.symm.symm ∈ G),
    c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
rwa₁ :
  ∀ (this : (c.symm ≫ₕ e.toOpenPartialHomeomorph.symm) ≫ₕ c'.symm.symm ∈ G),
    c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
rwa₂ :
  ∀ (this : (c.symm ≫ₕ e.toOpenPartialHomeomorph.symm) ≫ₕ c' ∈ G), c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
⊢ c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
have rwa₃ : ∀ (this : c.symm ≫ₕ e.toOpenPartialHomeomorph.symm ≫ₕ c' ∈ G), c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
Tactic: rwa [trans_symm_eq_symm_trans_symm, trans_symm_eq_symm_trans_symm, symm_symm, trans_assoc]
        at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
⊢ c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c' ∈ G
have refine : ∀ (x : H) (hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source),
  ∃ (s : Set H),
    IsOpen[inst] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G
Tactic: refine G.locality fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
⊢ ∃ (s : Set H),
    IsOpen[inst] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G
have feq : f = f₁ ≫ₕ f₂
Tactic: have feq : f = f₁ ≫ₕ f₂ := Homeomorph.trans_toOpenPartialHomeomorph _ _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
⊢ ∃ (s : Set H),
    IsOpen[inst] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G
have hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
Tactic: have hg₁ := chart_mem_atlas (H := H) y
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
⊢ ∃ (s : Set H),
    IsOpen[inst] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G
have hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
Tactic: have hg₂ := mem_chart_source (H := H) y
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
⊢ IsOpen[inst] s
have hs : IsOpen[inst] (c.symm ≫ₕ f₁).source
Tactic: apply (c.symm ≫ₕ f₁).continuousOn_toFun.isOpen_inter_preimage