awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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_1] f.source

Tactic:
apply open_source

Premises used: OpenPartialHomeomorph.open_source
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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

Tactic:
have hs : IsOpen s := by
    apply e.symm.continuousOn_toFun.isOpen_inter_preimage <;> apply open_source
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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
simp : x ∈ e.target
⊢ x ∈ s

Tactic:
simp only [s, f, mem_inter_iff, mem_preimage, mem_chart_source, and_true]

Premises used: mem_chart_source, and_true, Set.mem_inter_iff, Set.mem_preimage
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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 ∈ e.target

Tactic:
((mem_inter_iff _ _ _).1 hx).1

Premises used: Set.Mem, Set.mem_inter_iff, And.left, Iff.mp
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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 ∈ e.target

Tactic:
exact ((mem_inter_iff _ _ _).1 hx).1

Premises used: Set.mem_inter_iff, And.left, Iff.mp
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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

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
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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

Tactic:
⟨s, hs, xs, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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
refine : (e.symm ≫ₕ e').restr s ∈ G
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ (e.symm ≫ₕ e').restr s ∈ G

Tactic:
refine ⟨s, hs, xs, ?_⟩
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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 ≫ₕ f ∈ G

Tactic:
have A : e.symm ≫ₕ f ∈ G := (mem_maximalAtlas_iff.1 he f (chart_mem_atlas _ _)).1
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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
⊢ f.symm ≫ₕ e' ∈ G

Tactic:
have B : f.symm ≫ₕ e' ∈ G := (mem_maximalAtlas_iff.1 he' f (chart_mem_atlas _ _)).2
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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 ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G

Tactic:
have C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G := G.trans A B
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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 ≫ₕ f) ≫ₕ f.symm ≫ₕ e' = e.symm ≫ₕ (f ≫ₕ f.symm) ≫ₕ e'

Tactic:
simp only [trans_assoc]

Premises used: OpenPartialHomeomorph.trans_assoc
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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
rw rw₁ :
  (eqOnSourceSetoid : OpenPartialHomeomorph H H → OpenPartialHomeomorph H H → Prop) (e.symm ≫ₕ ofSet f.source ⋯ ≫ₕ e')
    (e.symm ≫ₕ ofSet f.source ⋯ ≫ₕ e')
⊢ e.symm ≫ₕ ofSet f.source ⋯ ≫ₕ e' ≈ (e.symm ≫ₕ ofSet f.source ⋯) ≫ₕ e'

Tactic:
rw [trans_assoc]

Premises used: OpenPartialHomeomorph.trans_assoc
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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
rw : e.symm.restr (e.symm.source ∩ (↑e.symm : H → M) ⁻¹' f.source) ≫ₕ e' ≈ e.symm.restr s ≫ₕ e'
⊢ (e.symm ≫ₕ ofSet f.source ⋯) ≫ₕ e' ≈ e.symm.restr s ≫ₕ e'

Tactic:
rw [trans_of_set']

Premises used: OpenPartialHomeomorph.trans_of_set'
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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 (e.symm.source ∩ (↑e.symm : H → M) ⁻¹' f.source) ≫ₕ e' ≈ e.symm.restr s ≫ₕ e'

Tactic:
apply refl

Premises used: refl
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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
rw rw₁ :
  (eqOnSourceSetoid : OpenPartialHomeomorph H H → OpenPartialHomeomorph H H → Prop) ((e.symm ≫ₕ e').restr s)
    ((e.symm ≫ₕ e').restr s)
⊢ e.symm.restr s ≫ₕ e' ≈ (e.symm ≫ₕ e').restr s

Tactic:
rw [restr_trans]

Premises used: OpenPartialHomeomorph.restr_trans
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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 ≫ₕ 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]
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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
D : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ≈ (e.symm ≫ₕ e').restr s
⊢ (e.symm ≫ₕ e').restr s ∈ G

Tactic:
G.mem_of_eqOnSource C (Setoid.symm D)

Premises used: StructureGroupoid.mem_of_eqOnSource, Setoid.symm
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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
D : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ≈ (e.symm ≫ₕ e').restr s
⊢ (e.symm ≫ₕ e').restr s ∈ G

Tactic:
exact G.mem_of_eqOnSource C (Setoid.symm D)

Premises used: StructureGroupoid.mem_of_eqOnSource, Setoid.symm
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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

Tactic:
obtain ⟨l, r⟩ := mem_maximalAtlas_iff.mp he e'' he''

Premises used: Iff.mp, mem_maximalAtlas_iff
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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

Tactic:
obtain ⟨l, r⟩ := mem_maximalAtlas_iff.mp he e'' he''

Premises used: Iff.mp, mem_maximalAtlas_iff
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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
r : e''.symm ≫ₕ e ∈ G
⊢ e'.symm ≫ₕ e'' ∈ G ∧ e''.symm ≫ₕ e' ∈ G

Tactic:
⟨G.mem_of_eqOnSource l (EqOnSource.trans' (EqOnSource.symm' h) (e''.eqOnSource_refl)),
         G.mem_of_eqOnSource r (EqOnSource.trans' (e''.symm).eqOnSource_refl h)⟩

Premises used: StructureGroupoid.mem_of_eqOnSource, OpenPartialHomeomorph.EqOnSource.trans', OpenPartialHomeomorph.eqOnSource_refl, And.intro, OpenPartialHomeomorph.EqOnSource.symm', OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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
r : e''.symm ≫ₕ e ∈ G
⊢ e'.symm ≫ₕ e'' ∈ G ∧ e''.symm ≫ₕ e' ∈ G

Tactic:
exact ⟨G.mem_of_eqOnSource l (EqOnSource.trans' (EqOnSource.symm' h) (e''.eqOnSource_refl)),
         G.mem_of_eqOnSource r (EqOnSource.trans' (e''.symm).eqOnSource_refl h)⟩
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
inst : TopologicalSpace H
G : StructureGroupoid H
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (atlas H H) (OpenPartialHomeomorph.refl H)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
inst : TopologicalSpace H
G : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf : f ∈ G
⊢ f.symm ≫ₕ OpenPartialHomeomorph.refl H ∈ G ∧ OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H) ≫ₕ f ∈ G

Tactic:
⟨G.trans (G.symm hf) G.id_mem, G.trans (G.symm G.id_mem) hf⟩

Premises used: And.intro, StructureGroupoid.trans, StructureGroupoid.symm, StructureGroupoid.id_mem
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
inst : TopologicalSpace H
G : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf : f ∈ G
⊢ f.symm ≫ₕ OpenPartialHomeomorph.refl H ∈ G ∧ OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl H) ≫ₕ f ∈ G

Tactic:
exact ⟨G.trans (G.symm hf) G.id_mem, G.trans (G.symm G.id_mem) hf⟩
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G G' : StructureGroupoid H
h : G ≤ G'
⊢ Subset (α := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) (maximalAtlas M G')

Tactic:
fun _ he e' he' ↦ ⟨h (he e' he').1, h (he e' he').2⟩

Premises used: Set.Mem, setOf, Set.Subset, And.right, And.left, And.intro, StructureGroupoid.maximalAtlas
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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
rw : IsOpen[inst_1] (e.source ∩ s)
⊢ IsOpen[inst] ((↑e : M → H) '' (e.source ∩ s))

Tactic:
rw [isOpen_image_iff_of_subset_source _ inter_subset_left]

Premises used: OpenPartialHomeomorph.isOpen_image_iff_of_subset_source, Set.inter_subset_left
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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_1] (e.source ∩ s)

Tactic:
e.open_source.inter hs

Premises used: OpenPartialHomeomorph.open_source, IsOpen.inter
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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_1] (e.source ∩ s)

Tactic:
exact e.open_source.inter hs

Premises used: OpenPartialHomeomorph.open_source, IsOpen.inter
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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))

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
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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))
apply : (e.restr (e.source ∩ s)).symm ≫ₕ e' ≈ (e.symm ≫ₕ e').restr ((↑e : M → H) '' (e.source ∩ s))
⊢ (e.restr (e.source ∩ s)).symm ≫ₕ e' ∈ G

Tactic:
apply G.mem_of_eqOnSource (closedUnderRestriction' (he e' he').1 hs'')

Premises used: StructureGroupoid.mem_of_eqOnSource, And.left, closedUnderRestriction'
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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' ≈ (e.symm ≫ₕ e').restr ((↑e : M → H) '' (e.source ∩ s))

Tactic:
e.restr_symm_trans (e.open_source.inter hs) hs'' inter_subset_left

Premises used: OpenPartialHomeomorph.open_source, Set.inter_subset_left, IsOpen.inter, OpenPartialHomeomorph.restr_symm_trans
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
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' ≈ (e.symm ≫ₕ e').restr ((↑e : M → H) '' (e.source ∩ s))

Tactic:
exact e.restr_symm_trans (e.open_source.inter hs) hs'' inter_subset_left

Premises used: OpenPartialHomeomorph.open_source, Set.inter_subset_left, IsOpen.inter, OpenPartialHomeomorph.restr_symm_trans