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
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
⊢ (toPartialEquiv (OpenPartialHomeomorph.refl H)).source = univ

Tactic:
simp
-- 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
⊢ (e.restr s).source = univ

Tactic:
have : (e.restr s).source = univ := by
          rw [hs]
          simp
-- 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
this : (e.restr s).source = univ
⊢ e.source ∩ interior s = univ

Tactic:
have : e.toPartialEquiv.source ∩ interior s = univ := 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 : 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
this_1 : (e.restr s).source = univ
this : e.source ∩ interior s = univ
rw : e.source ∩ interior s ⊆ interior s
⊢ univ ⊆ interior s

Tactic:
rw [← 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 : 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
this_1 : (e.restr s).source = univ
this : e.source ∩ interior s = univ
⊢ e.source ∩ interior s ⊆ interior s

Tactic:
inter_subset_right

Premises used: Set.inter_subset_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)
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
this_1 : (e.restr s).source = univ
this : e.source ∩ interior s = univ
⊢ e.source ∩ interior s ⊆ interior s

Tactic:
exact inter_subset_right

Premises used: Set.inter_subset_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)
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
this_1 : (e.restr s).source = univ
this : e.source ∩ interior s = univ
⊢ univ ⊆ interior s

Tactic:
have : univ ⊆ interior s := by
          rw [← this]
          exact inter_subset_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)
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
this_1 : (e.restr s).source = univ
this_2 : e.source ∩ interior s = univ
this : univ ⊆ interior s
rwa : ∀ (this : univ ⊆ s), s = univ
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : s = univ), s = univ
⊢ s = univ

Tactic:
rwa [open_s.interior_eq, univ_subset_iff] at this

Premises used: Set.univ_subset_iff, 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
x's : x ∈ (e.restr s).source
hs : e.restr s = OpenPartialHomeomorph.refl H
this_1 : (e.restr s).source = univ
this_2 : e.source ∩ interior s = univ
this : univ ⊆ interior s
⊢ s = univ

Tactic:
have : s = univ := by rwa [open_s.interior_eq, univ_subset_iff] 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 : 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
this_1 : (e.restr s).source = univ
this_2 : e.source ∩ interior s = univ
this_3 : univ ⊆ interior s
this : s = univ
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e

Tactic:
simpa only [this, restr_univ] using hs

Premises used: OpenPartialHomeomorph.restr_univ
-- 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)) {e : OpenPartialHomeomorph H H | e.source = ∅} (e.restr s)
inr : False
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e

Tactic:
exfalso
-- 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)) {e : OpenPartialHomeomorph H H | e.source = ∅} (e.restr s)
⊢ (e.restr s).source = ∅

Tactic:
rw [mem_setOf_eq] at hs

Premises used: Set.mem_setOf_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
x's : x ∈ (e.restr s).source
hs : (e.restr s).source = ∅
inr inr₁ inr₂ inr₃ : ∀ (x's : Membership.mem (γ := Set H) ∅ x) (hs : (e.restr s).source = ∅), False
⊢ False

Tactic:
rwa [hs] at x's
-- 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'e : e' ≈ 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'
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'
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) 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'e : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
inl : 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 e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
⊢ e = e'

Tactic:
eq_of_eqOnSource_univ (Setoid.symm he'e) ?_ ?_

Premises used: Setoid.symm, OpenPartialHomeomorph.eq_of_eqOnSource_univ
-- 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'e : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
refine_1 : e.source = univ
refine_2 : e.target = univ
⊢ e = e'

Tactic:
refine eq_of_eqOnSource_univ (Setoid.symm he'e) ?_ ?_

Premises used: Setoid.symm, OpenPartialHomeomorph.eq_of_eqOnSource_univ
-- 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'e : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
refine_1 : (toPartialEquiv (OpenPartialHomeomorph.refl H)).source = univ
⊢ e.source = univ

Tactic:
rw [Set.mem_singleton_iff.1 he]

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 e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
refine_2 : (toPartialEquiv (OpenPartialHomeomorph.refl H)).target = univ
⊢ e.target = univ

Tactic:
rw [Set.mem_singleton_iff.1 he]

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 e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
⊢ (toPartialEquiv (OpenPartialHomeomorph.refl H)).source = univ

Tactic:
rfl
-- 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'e : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
⊢ (toPartialEquiv (OpenPartialHomeomorph.refl H)).target = univ

Tactic:
rfl
-- 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'e : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
⊢ e = e'

Tactic:
have : e = e' := by
        refine eq_of_eqOnSource_univ (Setoid.symm he'e) ?_ ?_ <;>
          rw [Set.mem_singleton_iff.1 he] <;> rfl
-- 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'e : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
this : e = e'
inl inl₁ inl₂ inl₃ : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e'

Tactic:
rwa [← 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'e : e' ≈ e
he : 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'
⊢ 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 e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e
⊢ e.source = ∅

Tactic:
have he : e.toPartialEquiv.source = ∅ := 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'e : e' ≈ e
he_1 : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e
he : e.source = ∅
inr : e'.source = ∅
inr₁ inr₂ inr₃ inr₄ : e.source = ∅
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e'

Tactic:
rwa [Set.mem_setOf_eq, EqOnSource.source_eq he'e]

Premises used: OpenPartialHomeomorph.EqOnSource.source_eq, Set.mem_setOf_eq
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
u : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf_1 : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members (idGroupoid H)) f
hf :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) f
⊢ f = OpenPartialHomeomorph.refl H ∨ f.source = ∅

Tactic:
simp only [singleton_union, mem_setOf_eq, mem_insert_iff] at hf

Premises used: Set.singleton_union, Set.mem_setOf_eq, Set.mem_insert_iff
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
u : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf_1 : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members (idGroupoid H)) f
hf : f = OpenPartialHomeomorph.refl H ∨ f.source = ∅
inl : ∀ (hf : f = OpenPartialHomeomorph.refl H), f ∈ u.members
inr : ∀ (hf : f.source = ∅), f ∈ u.members
⊢ f ∈ u.members

Tactic:
rcases hf with hf | hf
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
u : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf_1 : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members (idGroupoid H)) f
hf : f = OpenPartialHomeomorph.refl H
inl : OpenPartialHomeomorph.refl H ∈ u.members
⊢ f ∈ u.members

Tactic:
rw [hf]
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
u : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf_1 : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members (idGroupoid H)) f
hf : f = OpenPartialHomeomorph.refl H
⊢ OpenPartialHomeomorph.refl H ∈ u.members

Tactic:
apply u.id_mem

Premises used: StructureGroupoid.id_mem
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
u : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf_1 : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members (idGroupoid H)) f
hf : f.source = ∅
inr : ∀ x ∈ f.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ f.restr s ∈ u
⊢ f ∈ u.members

Tactic:
apply u.locality

Premises used: StructureGroupoid.locality
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
u : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf_1 : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members (idGroupoid H)) f
hf : f.source = ∅
x : H
hx : x ∈ f.source
⊢ False

Tactic:
rw [hf, mem_empty_iff_false] at hx

Premises used: Set.mem_empty_iff_false
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
u : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf_1 : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members (idGroupoid H)) f
hf : f.source = ∅
x : H
hx : False
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ f.restr s ∈ u

Tactic:
hx.elim

Premises used: False.elim
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
u : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf_1 : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members (idGroupoid H)) f
hf : f.source = ∅
x : H
hx : False
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ f.restr s ∈ u

Tactic:
exact hx.elim

Premises used: False.elim
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e'
left : PG.property (↑(e ≫ₕ e') : H → H) (e ≫ₕ e').source
right : PG.property (↑(e ≫ₕ e').symm : H → H) (e ≫ₕ e').target
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
    (e ≫ₕ e')

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e'
left : IsOpen[inst] (e.source ∩ (↑e : H → H) ⁻¹' e'.source)
⊢ PG.property (↑(e ≫ₕ e') : H → H) (e ≫ₕ e').source

Tactic:
apply PG.comp he.1 he'.1 e.open_source e'.open_source

Premises used: OpenPartialHomeomorph.open_source, Pregroupoid.comp, And.left
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e'
⊢ IsOpen[inst] (e.source ∩ (↑e : H → H) ⁻¹' e'.source)

Tactic:
apply e.continuousOn_toFun.isOpen_inter_preimage e.open_source e'.open_source

Premises used: OpenPartialHomeomorph.open_source, ContinuousOn.isOpen_inter_preimage, OpenPartialHomeomorph.continuousOn_toFun
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e'
right : IsOpen[inst] (e'.target ∩ (↑e'.symm : H → H) ⁻¹' e.target)
⊢ PG.property (↑(e ≫ₕ e').symm : H → H) (e ≫ₕ e').target

Tactic:
apply PG.comp he'.2 he.2 e'.open_target e.open_target

Premises used: Pregroupoid.comp, And.right, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e'
⊢ IsOpen[inst] (e'.target ∩ (↑e'.symm : H → H) ⁻¹' e.target)

Tactic:
apply e'.continuousOn_invFun.isOpen_inter_preimage e'.open_target e.open_target

Premises used: ContinuousOn.isOpen_inter_preimage, OpenPartialHomeomorph.continuousOn_invFun, OpenPartialHomeomorph.open_target