awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
Goal:
H_1 : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H_1
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H_1 M
H : Type u_5
inst_3 : TopologicalSpace H
G : StructureGroupoid H
e e' : OpenPartialHomeomorph H H
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (atlas H H) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (atlas H H) e'
⊢ e.symm ≫ₕ e' ∈ G
have he₁ : e = OpenPartialHomeomorph.refl H
Tactic: rw [chartedSpaceSelf_atlas] at he he'
Cleared hypotheses: he, he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
Goal:
H_1 : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H_1
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H_1 M
H : Type u_5
inst_3 : TopologicalSpace H
G : StructureGroupoid H
e e' : OpenPartialHomeomorph H H
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (atlas H H) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (atlas H H) e'
he₁ : e = OpenPartialHomeomorph.refl H
⊢ e.symm ≫ₕ e' ∈ G
have he'₁ : e' = OpenPartialHomeomorph.refl H
Tactic: rw [chartedSpaceSelf_atlas] at he he'
Cleared hypotheses: 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
⊢ HasGroupoid M (continuousGroupoid H)
have refine : ∀ {e e' : OpenPartialHomeomorph M H},
  Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e →
    Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e' →
      Membership.mem (γ := StructureGroupoid H) (continuousGroupoid H) (e.symm ≫ₕ e')
Tactic: refine ⟨fun _ _ ↦ ?_⟩
-- 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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
⊢ e.symm ≫ₕ e' ∈ G
have refine : ∀ (x : H) (hx : x ∈ (e.symm ≫ₕ e').source), ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ (e.symm ≫ₕ e').restr s ∈ G
Tactic: refine G.locality fun x hx ↦ ?_
-- 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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H ((↑e.symm : H → M) x)
s : Set H := e.target ∩ (↑e.symm : H → M) ⁻¹' f.source
⊢ IsOpen[inst] s
have hs : IsOpen[inst] e.symm.source
Tactic: apply e.symm.continuousOn_toFun.isOpen_inter_preimage
-- 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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H ((↑e.symm : H → M) x)
s : Set H := e.target ∩ (↑e.symm : H → M) ⁻¹' f.source
hs : IsOpen[inst] e.symm.source
⊢ IsOpen[inst] s
have ht : IsOpen[inst_1] f.source
Tactic: apply e.symm.continuousOn_toFun.isOpen_inter_preimage
-- 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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H ((↑e.symm : H → M) x)
s : Set H := e.target ∩ (↑e.symm : H → M) ⁻¹' f.source
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ (e.symm ≫ₕ e').restr s ∈ G
have hs : IsOpen[inst] s
Tactic: have hs : IsOpen s := by
    apply e.symm.continuousOn_toFun.isOpen_inter_preimage <;> apply open_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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H ((↑e.symm : H → M) x)
s : Set H := e.target ∩ (↑e.symm : H → M) ⁻¹' f.source
hs : IsOpen[inst] s
⊢ x ∈ s
have simp : x ∈ e.target
Tactic: simp only [s, f, mem_inter_iff, mem_preimage, mem_chart_source, and_true]
-- 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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H ((↑e.symm : H → M) x)
s : Set H := e.target ∩ (↑e.symm : H → M) ⁻¹' f.source
hs : IsOpen[inst] s
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ (e.symm ≫ₕ e').restr s ∈ G
have xs : x ∈ s
Tactic: have xs : x ∈ s := by
    simp only [s, f, mem_inter_iff, mem_preimage, mem_chart_source, and_true]
    exact ((mem_inter_iff _ _ _).1 hx).1
-- 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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H ((↑e.symm : H → M) x)
s : Set H := e.target ∩ (↑e.symm : H → M) ⁻¹' f.source
hs : IsOpen[inst] s
xs : x ∈ s
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ (e.symm ≫ₕ e').restr s ∈ G
have refine : (e.symm ≫ₕ e').restr s ∈ G
Tactic: refine ⟨s, hs, xs, ?_⟩
-- 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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H ((↑e.symm : H → M) x)
s : Set H := e.target ∩ (↑e.symm : H → M) ⁻¹' f.source
hs : IsOpen[inst] s
xs : x ∈ s
⊢ (e.symm ≫ₕ e').restr s ∈ G
have A : e.symm ≫ₕ f ∈ G
Tactic: have A : e.symm ≫ₕ f ∈ G := (mem_maximalAtlas_iff.1 he f (chart_mem_atlas _ _)).1
-- 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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H ((↑e.symm : H → M) x)
s : Set H := e.target ∩ (↑e.symm : H → M) ⁻¹' f.source
hs : IsOpen[inst] s
xs : x ∈ s
A : e.symm ≫ₕ f ∈ G
⊢ (e.symm ≫ₕ e').restr s ∈ G
have B : f.symm ≫ₕ e' ∈ G
Tactic: have B : f.symm ≫ₕ e' ∈ G := (mem_maximalAtlas_iff.1 he' f (chart_mem_atlas _ _)).2
-- 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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H ((↑e.symm : H → M) x)
s : Set H := e.target ∩ (↑e.symm : H → M) ⁻¹' f.source
hs : IsOpen[inst] s
xs : x ∈ s
A : e.symm ≫ₕ f ∈ G
B : f.symm ≫ₕ e' ∈ G
⊢ (e.symm ≫ₕ e').restr s ∈ G
have C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G
Tactic: have C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G := G.trans A B
-- 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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H ((↑e.symm : H → M) x)
s : Set H := e.target ∩ (↑e.symm : H → M) ⁻¹' f.source
hs : IsOpen[inst] s
xs : x ∈ s
A : e.symm ≫ₕ f ∈ G
B : f.symm ≫ₕ e' ∈ G
C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G
⊢ e.symm ≫ₕ ofSet f.source ⋯ ≫ₕ e' ≈ (e.symm ≫ₕ ofSet f.source ⋯) ≫ₕ e'
have rw : (eqOnSourceSetoid : OpenPartialHomeomorph H H → OpenPartialHomeomorph H H → Prop) (e.symm ≫ₕ ofSet f.source sorry ≫ₕ e')
  (e.symm ≫ₕ ofSet f.source sorry ≫ₕ e')
Tactic: rw [trans_assoc]
-- 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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H ((↑e.symm : H → M) x)
s : Set H := e.target ∩ (↑e.symm : H → M) ⁻¹' f.source
hs : IsOpen[inst] s
xs : x ∈ s
A : e.symm ≫ₕ f ∈ G
B : f.symm ≫ₕ e' ∈ G
C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G
⊢ (e.symm ≫ₕ ofSet f.source ⋯) ≫ₕ e' ≈ e.symm.restr s ≫ₕ e'
have rw : e.symm.restr (e.symm.source ∩ (↑e.symm : H → M) ⁻¹' f.source) ≫ₕ e' ≈ e.symm.restr s ≫ₕ e'
Tactic: rw [trans_of_set']
-- 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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H ((↑e.symm : H → M) x)
s : Set H := e.target ∩ (↑e.symm : H → M) ⁻¹' f.source
hs : IsOpen[inst] s
xs : x ∈ s
A : e.symm ≫ₕ f ∈ G
B : f.symm ≫ₕ e' ∈ G
C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G
⊢ e.symm.restr s ≫ₕ e' ≈ (e.symm ≫ₕ e').restr s
have rw : (eqOnSourceSetoid : OpenPartialHomeomorph H H → OpenPartialHomeomorph H H → Prop) ((e.symm ≫ₕ e').restr s)
  ((e.symm ≫ₕ e').restr s)
Tactic: rw [restr_trans]
-- 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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H ((↑e.symm : H → M) x)
s : Set H := e.target ∩ (↑e.symm : H → M) ⁻¹' f.source
hs : IsOpen[inst] s
xs : x ∈ s
A : e.symm ≫ₕ f ∈ G
B : f.symm ≫ₕ e' ∈ G
C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G
⊢ (e.symm ≫ₕ e').restr s ∈ G
have D : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ≈ (e.symm ≫ₕ e').restr s
Tactic: have D : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ≈ (e.symm ≫ₕ e').restr s := calc
    (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' = e.symm ≫ₕ (f ≫ₕ f.symm) ≫ₕ e' := by simp only [trans_assoc]
    _ ≈ e.symm ≫ₕ ofSet f.source f.open_source ≫ₕ e' :=
      EqOnSource.trans' (refl _) (EqOnSource.trans' (self_trans_symm _) (refl _))
    _ ≈ (e.symm ≫ₕ ofSet f.source f.open_source) ≫ₕ e' := by rw [trans_assoc]
    _ ≈ e.symm.restr s ≫ₕ e' := by rw [trans_of_set']; apply refl
    _ ≈ (e.symm ≫ₕ e').restr s := by rw [restr_trans]
-- 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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
h : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
e'' : OpenPartialHomeomorph M H
he'' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e''
⊢ e'.symm ≫ₕ e'' ∈ G ∧ e''.symm ≫ₕ e' ∈ G
have l : e.symm ≫ₕ e'' ∈ G
Tactic: obtain ⟨l, r⟩ := mem_maximalAtlas_iff.mp he e'' he''
-- 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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
h : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
e'' : OpenPartialHomeomorph M H
he'' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e''
l : e.symm ≫ₕ e'' ∈ G
⊢ e'.symm ≫ₕ e'' ∈ G ∧ e''.symm ≫ₕ e' ∈ G
have r : e''.symm ≫ₕ e ∈ G
Tactic: obtain ⟨l, r⟩ := mem_maximalAtlas_iff.mp he e'' 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
⊢ IsOpen[inst] ((↑e : M → H) '' (e.source ∩ s))
have rw : IsOpen[inst_1] (e.source ∩ s)
Tactic: rw [isOpen_image_iff_of_subset_source _ inter_subset_left]
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
⊢ (e.restr s).symm ≫ₕ e' ∈ G
have hs'' : IsOpen[inst] ((↑e : M → H) '' (e.source ∩ s))
Tactic: have hs'' : IsOpen (e '' (e.source ∩ s)) := by
    rw [isOpen_image_iff_of_subset_source _ inter_subset_left]
    exact e.open_source.inter hs
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
hs'' : IsOpen[inst] ((↑e : M → H) '' (e.source ∩ s))
⊢ (e.restr (e.source ∩ s)).symm ≫ₕ e' ∈ G
have apply : (e.restr (e.source ∩ s)).symm ≫ₕ e' ≈ (e.symm ≫ₕ e').restr ((↑e : M → H) '' (e.source ∩ s))
Tactic: apply G.mem_of_eqOnSource (closedUnderRestriction' (he e' he').1 hs'')
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
hs'' : IsOpen[inst] ((↑e : M → H) '' (e.source ∩ s))
⊢ (e.restr s).symm ≫ₕ e' ∈ G
have this : (e.restr (e.source ∩ s)).symm ≫ₕ e' ∈ G
Tactic: have : (e.restr (e.source ∩ s)).symm ≫ₕ e' ∈ G := by
    apply G.mem_of_eqOnSource (closedUnderRestriction' (he e' he').1 hs'')
    exact e.restr_symm_trans (e.open_source.inter hs) hs'' inter_subset_left
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
hs'' : IsOpen[inst] ((↑e : M → H) '' (e.source ∩ s))
this : (e.restr (e.source ∩ s)).symm ≫ₕ e' ∈ G
⊢ (e.restr s).symm ≫ₕ e' ∈ G
have refine : (e.restr s).symm ≫ₕ e' ≈ (e.restr (e.source ∩ s)).symm ≫ₕ e'
Tactic: refine G.mem_of_eqOnSource this ?_
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
⊢ IsOpen[inst] ((↑e' : M → H) '' (e'.source ∩ s))
have rw : IsOpen[inst_1] (e'.source ∩ s)
Tactic: rw [isOpen_image_iff_of_subset_source e' inter_subset_left]
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
⊢ e'.symm ≫ₕ e.restr s ∈ G
have hs'' : IsOpen[inst] ((↑e' : M → H) '' (e'.source ∩ s))
Tactic: have hs'' : IsOpen (e' '' (e'.source ∩ s)) := by
    rw [isOpen_image_iff_of_subset_source e' inter_subset_left]
    exact e'.open_source.inter hs
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
hs'' : IsOpen[inst] ((↑e' : M → H) '' (e'.source ∩ s))
⊢ e'.symm ≫ₕ e.restr s ∈ G
have ht : IsOpen[inst] (e'.target ∩ (↑e'.symm : H → M) ⁻¹' s)
Tactic: have ht : IsOpen (e'.target ∩ e'.symm ⁻¹' s) := by
    rw [← image_source_inter_eq']
    exact isOpen_image_source_inter e' hs
-- 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
α : Type u_5
inst_3 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
x : α
⊢ x ∈ e.source
have rw : Membership.mem (γ := Set α) univ x
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
inst : TopologicalSpace H
α : Type u_5
inst_1 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst_2 : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e'
he'' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e''
⊢ e'.symm ≫ₕ e'' ∈ G
have rw : e.symm ≫ₕ e ∈ G
Tactic: rw [e.singletonChartedSpace_mem_atlas_eq h e' he',
        e.singletonChartedSpace_mem_atlas_eq h e'' he'']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
inst : TopologicalSpace H
α : Type u_5
inst_1 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst_2 : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e'
he'' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e''
⊢ e.symm ≫ₕ e ∈ G
have refine : ofSet e.target sorry ∈ G
Tactic: refine G.mem_of_eqOnSource ?_ e.symm_trans_self
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
Goal:
H : Type u
inst : TopologicalSpace H
α : Type u_5
inst_1 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst_2 : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e'
he'' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e''
⊢ ofSet e.target ⋯ ∈ G
have hle : idRestrGroupoid ≤ G
Tactic: have hle : idRestrGroupoid ≤ G := (closedUnderRestriction_iff_id_le G).mp (by assumption)
-- 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
x : ↥s
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (⋃ (x : ↥s), {subtypeRestr (chartAt H (↑x : M)) ⋯})
    (subtypeRestr (chartAt H (↑x : M)) ⋯)
have simp : ∃ (i : ↥s),
  Eq (α := OpenPartialHomeomorph.{u_2, u} (↥s) H) (subtypeRestr (chartAt H (↑x : M)) sorry)
    (subtypeRestr (chartAt H (↑i : M)) sorry)
Tactic: simp only [mem_iUnion, mem_singleton_iff]
-- 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
x w : ↥s
⊢ ∃ (i : ↥s),
    Eq (α := OpenPartialHomeomorph.{u_2, u} (↥s) H) (subtypeRestr (chartAt H (↑x : M)) ⋯)
      (subtypeRestr (chartAt H (↑i : M)) ⋯)
have h : Eq (α := OpenPartialHomeomorph.{u_2, u} (↥s) H) (subtypeRestr (chartAt H (↑x : M)) sorry)
  (subtypeRestr (chartAt H (↑x : M)) sorry)
Tactic: use x
-- 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
s : Opens M
hs : Nonempty.{u_2 + 1} ↥s
e : OpenPartialHomeomorph.{u_2, u} (↥s) H
he : Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (atlas H ↥s) e
⊢ ∃ (x : ↥s), e = subtypeRestr (chartAt H (↑x : M)) hs
have rcases : ∀ (xset : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (he : e ∈ xset) (x : ↥s)
  (hx :
    (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) sorry} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = xset),
  ∃ (x : ↥s), e = subtypeRestr (chartAt H (↑x : M)) hs
Tactic: rcases he with ⟨xset, ⟨x, hx⟩, he⟩
Cleared hypotheses: he