awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
members : Set (OpenPartialHomeomorph H H)
trans' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e ≫ₕ e' ∈ members
symm' : ∀ e ∈ members, e.symm ∈ members
id_mem' : OpenPartialHomeomorph.refl H ∈ members
locality' :
  ∀ (e : OpenPartialHomeomorph H H),
    (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst_1] s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members
mem_of_eqOnSource' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members
members_1 : Set (OpenPartialHomeomorph H H)
trans'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members_1 → e' ∈ members_1 → e ≫ₕ e' ∈ members_1
symm'_1 : ∀ e ∈ members_1, e.symm ∈ members_1
id_mem'_1 : OpenPartialHomeomorph.refl H ∈ members_1
locality'_1 :
  ∀ (e : OpenPartialHomeomorph H H),
    (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst_1] s ∧ x ∈ s ∧ e.restr s ∈ members_1) → e ∈ members_1
mem_of_eqOnSource'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members_1 → e' ≈ e → e' ∈ members_1
h :
  Eq.{u_2 + 1} (α := Set (OpenPartialHomeomorph H H))
    ((fun (s : StructureGroupoid H) ↦ s.members)
      { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
        mem_of_eqOnSource' := mem_of_eqOnSource' })
    ((fun (s : StructureGroupoid H) ↦ s.members)
      { members := members_1, trans' := trans'_1, symm' := symm'_1, id_mem' := id_mem'_1, locality' := locality'_1,
        mem_of_eqOnSource' := mem_of_eqOnSource'_1 })
⊢ { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
      mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
    { members := members_1, trans' := trans'_1, symm' := symm'_1, id_mem' := id_mem'_1, locality' := locality'_1,
      mem_of_eqOnSource' := mem_of_eqOnSource'_1 }

Tactic:
congr
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ e ∈ G.members ∧ e ∈ G'.members

Tactic:
And.intro (G.locality' e ?_) (G'.locality' e ?_)

Premises used: And.intro, StructureGroupoid.locality'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
refine_1 : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members
refine_2 : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G'.members
⊢ e ∈ G.members ∧ e ∈ G'.members

Tactic:
refine And.intro (G.locality' e ?_) (G'.locality' e ?_)

Premises used: And.intro, StructureGroupoid.locality'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
refine_1 :
  ∀ (s : Set H) (hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members),
    ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members

Tactic:
rcases hx x hex with ⟨s, hs⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
h : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members

Tactic:
use s
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members

Tactic:
And.intro hs.left (And.intro hs.right.left ?_)

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
h : e.restr s ∈ G.members
⊢ IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members

Tactic:
refine And.intro hs.left (And.intro hs.right.left ?_)

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
refine_2 :
  ∀ (s : Set H) (hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members),
    ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G'.members
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G'.members

Tactic:
rcases hx x hex with ⟨s, hs⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
h : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G'.members
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G'.members

Tactic:
use s
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G'.members

Tactic:
And.intro hs.left (And.intro hs.right.left ?_)

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
h : e.restr s ∈ G'.members
⊢ IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G'.members

Tactic:
refine And.intro hs.left (And.intro hs.right.left ?_)

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ e.restr s ∈ G.members

Tactic:
hs.right.right.left

Premises used: And.right, And.left
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ e.restr s ∈ G.members

Tactic:
exact hs.right.right.left

Premises used: And.right, And.left
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ e.restr s ∈ G'.members

Tactic:
hs.right.right.right

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ e.restr s ∈ G'.members

Tactic:
exact hs.right.right.right

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
simp :
  ∀ (e e' : OpenPartialHomeomorph H H),
    (∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e ∈ i.members) →
      (∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e' ∈ i.members) →
        ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e ≫ₕ e' ∈ i.members
⊢ ∀ (e e' : OpenPartialHomeomorph H H),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) e →
      Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) e' →
        Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) (e ≫ₕ e')

Tactic:
simp only [mem_iInter]

Premises used: Set.mem_iInter
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
e e' : OpenPartialHomeomorph H H
he : ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e ∈ i.members
he' : ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e' ∈ i.members
i : StructureGroupoid H
hi : i ∈ S
⊢ e ≫ₕ e' ∈ i.members

Tactic:
i.trans' e e' (he i hi) (he' i hi)

Premises used: StructureGroupoid.trans'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
e e' : OpenPartialHomeomorph H H
he : ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e ∈ i.members
he' : ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e' ∈ i.members
i : StructureGroupoid H
hi : i ∈ S
⊢ e ≫ₕ e' ∈ i.members

Tactic:
exact i.trans' e e' (he i hi) (he' i hi)

Premises used: StructureGroupoid.trans'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
simp :
  ∀ (e : OpenPartialHomeomorph H H),
    (∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e ∈ i.members) →
      ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e.symm ∈ i.members
⊢ ∀ (e : OpenPartialHomeomorph H H),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) e →
      Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) e.symm

Tactic:
simp only [mem_iInter]

Premises used: Set.mem_iInter
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
e : OpenPartialHomeomorph H H
he : ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e ∈ i.members
i : StructureGroupoid H
hi : i ∈ S
⊢ e.symm ∈ i.members

Tactic:
i.symm' e (he i hi)

Premises used: StructureGroupoid.symm'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
e : OpenPartialHomeomorph H H
he : ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e ∈ i.members
i : StructureGroupoid H
hi : i ∈ S
⊢ e.symm ∈ i.members

Tactic:
exact i.symm' e (he i hi)

Premises used: StructureGroupoid.symm'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
simp : ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), OpenPartialHomeomorph.refl H ∈ i.members
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) (OpenPartialHomeomorph.refl H)

Tactic:
simp only [mem_iInter]

Premises used: Set.mem_iInter
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
i : StructureGroupoid H
_ : i ∈ S → OpenPartialHomeomorph.refl H ∈ i.members
⊢ ∀ (i_1 : i ∈ S), OpenPartialHomeomorph.refl H ∈ i.members

Tactic:
_
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
i : StructureGroupoid H
i_1 : i ∈ S
⊢ OpenPartialHomeomorph.refl H ∈ i.members

Tactic:
i.id_mem'

Premises used: StructureGroupoid.id_mem'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
i : StructureGroupoid H
i_1 : i ∈ S
⊢ OpenPartialHomeomorph.refl H ∈ i.members

Tactic:
exact i.id_mem'

Premises used: StructureGroupoid.id_mem'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
simp :
  ∀ (e : OpenPartialHomeomorph H H),
    (∀ x ∈ e.source,
        ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e.restr s ∈ i.members) →
      ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e ∈ i.members
⊢ ∀ (e : OpenPartialHomeomorph H H),
    (∀ x ∈ e.source,
        ∃ (s : Set H),
          IsOpen[inst] s ∧
            x ∈ s ∧ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) (e.restr s)) →
      Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) e

Tactic:
simp only [mem_iInter]

Premises used: Set.mem_iInter
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e.restr s ∈ i.members
i : StructureGroupoid H
hi : i ∈ S
⊢ e ∈ i.members

Tactic:
i.locality' e ?_

Premises used: StructureGroupoid.locality'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e.restr s ∈ i.members
i : StructureGroupoid H
hi : i ∈ S
refine : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ i.members
⊢ e ∈ i.members

Tactic:
refine i.locality' e ?_

Premises used: StructureGroupoid.locality'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e.restr s ∈ i.members
i : StructureGroupoid H
hi : i ∈ S
x : H
hex : x ∈ e.source
rcases :
  ∀ (s : Set H) (hs : IsOpen[inst] s ∧ x ∈ s ∧ ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e.restr s ∈ i.members),
    ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ i.members
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ i.members

Tactic:
rcases he x hex with ⟨s, hs⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e.restr s ∈ i.members
i : StructureGroupoid H
hi : i ∈ S
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst] s ∧ x ∈ s ∧ ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e.restr s ∈ i.members
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ i.members

Tactic:
⟨s, ⟨hs.left, ⟨hs.right.left, hs.right.right i hi⟩⟩⟩

Premises used: And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e.restr s ∈ i.members
i : StructureGroupoid H
hi : i ∈ S
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst] s ∧ x ∈ s ∧ ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e.restr s ∈ i.members
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ i.members

Tactic:
exact ⟨s, ⟨hs.left, ⟨hs.right.left, hs.right.right i hi⟩⟩⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
simp :
  ∀ (e e' : OpenPartialHomeomorph H H),
    (∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e ∈ i.members) →
      e' ≈ e → ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e' ∈ i.members
⊢ ∀ (e e' : OpenPartialHomeomorph H H),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) e →
      e' ≈ e → Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) e'

Tactic:
simp only [mem_iInter]

Premises used: Set.mem_iInter
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
e e' : OpenPartialHomeomorph H H
he : ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e ∈ i.members
he'e : e' ≈ e
⊢ ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e' ∈ i.members

Tactic:
fun i hi => i.mem_of_eqOnSource' e e' (he i hi) he'e

Premises used: StructureGroupoid.mem_of_eqOnSource'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
e e' : OpenPartialHomeomorph H H
he : ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e ∈ i.members
he'e : e' ≈ e
⊢ ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e' ∈ i.members

Tactic:
exact fun i hi => i.mem_of_eqOnSource' e e' (he i hi) he'e
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ G
he' : e' ∈ G
⊢ e ≫ₕ e' ∈ G

Tactic:
G.trans' e e' he he'

Premises used: StructureGroupoid.trans'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
e : OpenPartialHomeomorph H H
he : e ∈ G
⊢ e.symm ∈ G

Tactic:
G.symm' e he

Premises used: StructureGroupoid.symm'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
⊢ OpenPartialHomeomorph.refl H ∈ G

Tactic:
G.id_mem'

Premises used: StructureGroupoid.id_mem'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
e : OpenPartialHomeomorph H H
h : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G
⊢ e ∈ G

Tactic:
G.locality' e h

Premises used: StructureGroupoid.locality'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ G
h : e' ≈ e
⊢ e' ∈ G

Tactic:
G.mem_of_eqOnSource' e e' he h

Premises used: StructureGroupoid.mem_of_eqOnSource'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
e e' : OpenPartialHomeomorph H H
h : e ≈ e'
⊢ e ∈ G ↔ e' ∈ G

Tactic:
⟨fun he ↦ G.mem_of_eqOnSource he (Setoid.symm h), fun he' ↦ G.mem_of_eqOnSource he' h⟩

Premises used: StructureGroupoid.mem_of_eqOnSource, Setoid.symm, Iff.intro
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
a b : StructureGroupoid H
h : a.members = b.members
mk :
  ∀ (members : Set (OpenPartialHomeomorph H H))
    (trans' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e ≫ₕ e' ∈ members)
    (symm' : ∀ e ∈ members, e.symm ∈ members) (id_mem' : OpenPartialHomeomorph.refl H ∈ members)
    (locality' :
      ∀ (e : OpenPartialHomeomorph H H),
        (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members)
    (mem_of_eqOnSource' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members)
    (h :
      { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
            mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H }.members =
        b.members),
    { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
        mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
      b
⊢ a = b

Tactic:
cases a
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
b : StructureGroupoid H
members : Set (OpenPartialHomeomorph H H)
trans' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e ≫ₕ e' ∈ members
symm' : ∀ e ∈ members, e.symm ∈ members
id_mem' : OpenPartialHomeomorph.refl H ∈ members
locality' :
  ∀ (e : OpenPartialHomeomorph H H),
    (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members
mem_of_eqOnSource' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members
h :
  { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
        mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H }.members =
    b.members
mk :
  ∀ (members_1 : Set (OpenPartialHomeomorph H H))
    (trans'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members_1 → e' ∈ members_1 → e ≫ₕ e' ∈ members_1)
    (symm'_1 : ∀ e ∈ members_1, e.symm ∈ members_1) (id_mem'_1 : OpenPartialHomeomorph.refl H ∈ members_1)
    (locality'_1 :
      ∀ (e : OpenPartialHomeomorph H H),
        (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ members_1) → e ∈ members_1)
    (mem_of_eqOnSource'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members_1 → e' ≈ e → e' ∈ members_1)
    (h :
      { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
            mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H }.members =
        { members := members_1, trans' := trans'_1, symm' := symm'_1, id_mem' := id_mem'_1, locality' := locality'_1,
            mem_of_eqOnSource' := mem_of_eqOnSource'_1 }.members),
    { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
        mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
      { members := members_1, trans' := trans'_1, symm' := symm'_1, id_mem' := id_mem'_1, locality' := locality'_1,
        mem_of_eqOnSource' := mem_of_eqOnSource'_1 }
⊢ { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
      mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
    b

Tactic:
cases b