awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : 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] 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] 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_1
mk :
  ∀ (trans'_2 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e ≫ₕ e' ∈ members)
    (symm'_2 : ∀ e ∈ members, e.symm ∈ members) (id_mem'_2 : OpenPartialHomeomorph.refl H ∈ members)
    (locality'_2 :
      ∀ (e : OpenPartialHomeomorph H H),
        (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members)
    (mem_of_eqOnSource'_2 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members),
    { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
        mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
      { members := members, trans' := trans'_2, symm' := symm'_2, id_mem' := id_mem'_2, locality' := locality'_2,
        mem_of_eqOnSource' := mem_of_eqOnSource'_2 }
⊢ { 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:
induction h
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : 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] 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 → e' ∈ members → e ≫ₕ e' ∈ members
symm'_1 : ∀ e ∈ members, e.symm ∈ members
id_mem'_1 : OpenPartialHomeomorph.refl H ∈ members
locality'_1 :
  ∀ (e : OpenPartialHomeomorph H H),
    (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members
mem_of_eqOnSource'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members
⊢ { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
      mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
    { members := members, trans' := trans'_1, symm' := symm'_1, id_mem' := id_mem'_1, locality' := locality'_1,
      mem_of_eqOnSource' := mem_of_eqOnSource'_1 }

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G₁ G₂ : StructureGroupoid H
⊢ G₁ ≤ G₂ ↔ ∀ e ∈ G₁, e ∈ G₂

Tactic:
Iff.rfl

Premises used: Iff.rfl, Set.Subset
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e'
inl :
  ∀ (he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H))
      ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e ≫ₕ e')
inr :
  ∀ (he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H))
      ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e ≫ₕ e')
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e ≫ₕ e')

Tactic:
rcases he with he | he
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e'
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e ≫ₕ e')

Tactic:
simpa only [mem_singleton_iff.1 he, refl_trans]

Premises used: Set.mem_singleton_iff, Iff.mp, OpenPartialHomeomorph.refl_trans
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e'
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e
⊢ (e ≫ₕ e').source ⊆ e.source

Tactic:
have : (e ≫ₕ e').source ⊆ e.source := sep_subset _ _
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e'
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e
this : (e ≫ₕ e').source ⊆ e.source
⊢ (e ≫ₕ e').source ⊆ ∅

Tactic:
rw [he] at this
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e'
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e
this : (e ≫ₕ e').source ⊆ ∅
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} (e ≫ₕ e')

Tactic:
have : e ≫ₕ e' ∈ { e : OpenPartialHomeomorph H H | e.source = ∅ } := eq_bot_iff.2 this
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e'
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e
this_1 : (e ≫ₕ e').source ⊆ ∅
this : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} (e ≫ₕ e')
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e ≫ₕ e')

Tactic:
(mem_union _ _ _).2 (Or.inr this)

Premises used: Set.mem_union, Iff.mpr, Or.inr
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e'
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e
this_1 : (e ≫ₕ e').source ⊆ ∅
this : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} (e ≫ₕ e')
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e ≫ₕ e')

Tactic:
exact (mem_union _ _ _).2 (Or.inr this)

Premises used: Set.mem_union, Iff.mpr, Or.inr
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
inl :
  ∀ (E : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H))
      ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e.symm
inr :
  ∀ (E : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H))
      ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e.symm
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e.symm

Tactic:
rcases (mem_union _ _ _).1 he with E | E

Premises used: Set.mem_union, Iff.mp
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
E : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e.symm

Tactic:
simp [mem_singleton_iff.mp E]

Premises used: Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
E : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e
inr : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e.symm
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e.symm

Tactic:
right
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
E : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e.symm

Tactic:
simpa only [e.toPartialEquiv.image_source_eq_target.symm, mfld_simps] using E

Premises used: PartialEquiv.image_source_eq_target, OpenPartialHomeomorph.toPartialEquiv, Eq.symm
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
inl :
  ∀ (h : e.source = ∅),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H))
      ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
inr :
  ∀ (h : e.source.Nonempty),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H))
      ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e

Tactic:
rcases e.source.eq_empty_or_nonempty with h | h

Premises used: Set.eq_empty_or_nonempty, PartialEquiv.source, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
h : e.source = ∅
inl : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e

Tactic:
right
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
h : e.source = ∅
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e

Tactic:
h

Premises used: Set.Mem, setOf
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
h : e.source = ∅
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e

Tactic:
exact h
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
h : e.source.Nonempty
inr : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e

Tactic:
left
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
h : e.source.Nonempty
inr :
  ∀ (x : H) (hx : x ∈ e.source), Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e

Tactic:
rcases h with ⟨x, hx⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
inr :
  ∀ (s : Set H) (open_s : IsOpen[inst_1] s) (xs : x ∈ s)
    (hs :
      Membership.mem (γ := Set (OpenPartialHomeomorph H H))
        ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e

Tactic:
rcases he x hx with ⟨s, open_s, xs, hs⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
rw : x ∈ e.source ∩ s
⊢ x ∈ (e.restr s).source

Tactic:
rw [restr_source, open_s.interior_eq]

Premises used: OpenPartialHomeomorph.restr_source, IsOpen.interior_eq
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
⊢ x ∈ e.source ∩ s

Tactic:
⟨hx, xs⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
⊢ x ∈ e.source ∩ s

Tactic:
exact ⟨hx, xs⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
⊢ x ∈ (e.restr s).source

Tactic:
have x's : x ∈ (e.restr s).source := by
        rw [restr_source, open_s.interior_eq]
        exact ⟨hx, xs⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x's : x ∈ (e.restr s).source
inr :
  ∀ (hs : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} (e.restr s)),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
inr₁ :
  ∀
    (hs :
      Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} (e.restr s)),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e

Tactic:
rcases hs with hs | hs
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} (e.restr s)
⊢ e.restr s = OpenPartialHomeomorph.refl H

Tactic:
simpa only using hs
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} (e.restr s)
⊢ e.restr s = OpenPartialHomeomorph.refl H

Tactic:
replace hs : OpenPartialHomeomorph.restr e s = OpenPartialHomeomorph.refl H := by
          simpa only using hs
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : e.restr s = OpenPartialHomeomorph.refl H
rw : (toPartialEquiv (OpenPartialHomeomorph.refl H)).source = univ
⊢ (e.restr s).source = univ

Tactic:
rw [hs]