awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
left : PG.property (↑e : H → H) e.source
right : PG.property (↑e.symm : H → H) 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

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
⊢ PG.property (↑e : H → H) e.source

Tactic:
PG.locality e.open_source fun x xu ↦ ?_

Premises used: OpenPartialHomeomorph.open_source, Pregroupoid.locality
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
left : ∀ (x : H) (xu : x ∈ e.source), ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e : H → H) (e.source ∩ v)
⊢ PG.property (↑e : H → H) e.source

Tactic:
refine PG.locality e.open_source fun x xu ↦ ?_

Premises used: OpenPartialHomeomorph.open_source, Pregroupoid.locality
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
x : H
xu : x ∈ e.source
left :
  ∀ (s : Set H) (s_open : IsOpen[inst] s) (xs : x ∈ s)
    (hs :
      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.restr s)),
    ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e : H → H) (e.source ∩ v)
⊢ ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e : H → H) (e.source ∩ v)

Tactic:
rcases he x xu with ⟨s, s_open, xs, hs⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
x : H
xu : x ∈ e.source
s : Set H
s_open : IsOpen[inst] s
xs : x ∈ s
hs :
  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.restr s)
⊢ ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e : H → H) (e.source ∩ v)

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

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
x : H
xu : x ∈ e.source
s : Set H
s_open : IsOpen[inst] s
xs : x ∈ s
hs :
  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.restr s)
left : PG.property (↑e : H → H) (e.source ∩ s)
⊢ ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e : H → H) (e.source ∩ v)

Tactic:
refine ⟨s, s_open, xs, ?_⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
x : H
xu : x ∈ e.source
s : Set H
s_open : IsOpen[inst] s
xs : x ∈ s
hs :
  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.restr s)
⊢ PG.property (↑(e.restr s) : H → H) (e.restr s).source

Tactic:
hs.1

Premises used: And.left
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
x : H
xu : x ∈ e.source
s : Set H
s_open : IsOpen[inst] s
xs : x ∈ s
hs :
  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.restr s)
h : e.source ∩ s = (e.restr s).source
⊢ PG.property (↑e : H → H) (e.source ∩ s)

Tactic:
convert! hs.1 using 1

Premises used: And.left
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
x : H
xu : x ∈ e.source
s : Set H
s_open : IsOpen[inst] s
xs : x ∈ s
hs :
  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.restr s)
h h₁ : e.source ∩ s = e.source ∩ s
⊢ e.source ∩ s = e.source ∩ interior s

Tactic:
rw [s_open.interior_eq]

Premises used: IsOpen.interior_eq
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
⊢ PG.property (↑e.symm : H → H) e.target

Tactic:
PG.locality e.open_target fun x xu ↦ ?_

Premises used: Pregroupoid.locality, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
right :
  ∀ (x : H) (xu : x ∈ e.target), ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e.symm : H → H) (e.target ∩ v)
⊢ PG.property (↑e.symm : H → H) e.target

Tactic:
refine PG.locality e.open_target fun x xu ↦ ?_

Premises used: Pregroupoid.locality, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
x : H
xu : x ∈ e.target
right :
  ∀ (s : Set H) (s_open : IsOpen[inst] s) (xs : (↑e.symm : H → H) x ∈ s)
    (hs :
      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.restr s)),
    ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e.symm : H → H) (e.target ∩ v)
⊢ ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e.symm : H → H) (e.target ∩ v)

Tactic:
rcases he (e.symm x) (e.map_target xu) with ⟨s, s_open, xs, hs⟩

Premises used: OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.map_target, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst] s
xs : (↑e.symm : H → H) x ∈ s
hs :
  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.restr s)
⊢ ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e.symm : H → H) (e.target ∩ v)

Tactic:
⟨e.target ∩ e.symm ⁻¹' s, ?_, ⟨xu, xs⟩, ?_⟩

Premises used: PartialEquiv.target, OpenPartialHomeomorph.toFun', Inter.inter, Set.preimage, And.intro, Exists.intro, OpenPartialHomeomorph.toPartialEquiv, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst] s
xs : (↑e.symm : H → H) x ∈ s
hs :
  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.restr s)
right : IsOpen[inst] (e.target ∩ (↑e.symm : H → H) ⁻¹' s)
right₁ : PG.property (↑e.symm : H → H) (e.target ∩ (e.target ∩ (↑e.symm : H → H) ⁻¹' s))
⊢ ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e.symm : H → H) (e.target ∩ v)

Tactic:
refine ⟨e.target ∩ e.symm ⁻¹' s, ?_, ⟨xu, xs⟩, ?_⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst] s
xs : (↑e.symm : H → H) x ∈ s
hs :
  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.restr s)
⊢ IsOpen[inst] (e.target ∩ (↑e.symm : H → H) ⁻¹' s)

Tactic:
ContinuousOn.isOpen_inter_preimage e.continuousOn_invFun e.open_target s_open

Premises used: ContinuousOn.isOpen_inter_preimage, OpenPartialHomeomorph.continuousOn_invFun, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst] s
xs : (↑e.symm : H → H) x ∈ s
hs :
  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.restr s)
⊢ IsOpen[inst] (e.target ∩ (↑e.symm : H → H) ⁻¹' s)

Tactic:
exact ContinuousOn.isOpen_inter_preimage e.continuousOn_invFun e.open_target s_open

Premises used: ContinuousOn.isOpen_inter_preimage, OpenPartialHomeomorph.continuousOn_invFun, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst] s
xs : (↑e.symm : H → H) x ∈ s
hs :
  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.restr s)
right : PG.property (↑e.symm : H → H) (e.target ∩ (↑e.symm : H → H) ⁻¹' s)
⊢ PG.property (↑e.symm : H → H) (e.target ∩ (e.target ∩ (↑e.symm : H → H) ⁻¹' s))

Tactic:
rw [← inter_assoc, inter_self]

Premises used: Set.inter_self, Set.inter_assoc
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst] s
xs : (↑e.symm : H → H) x ∈ s
hs :
  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.restr s)
⊢ PG.property (↑(e.restr s).symm : H → H) (e.restr s).target

Tactic:
hs.2

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst] s
xs : (↑e.symm : H → H) x ∈ s
hs :
  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.restr s)
h : e.target ∩ (↑e.symm : H → H) ⁻¹' s = (e.restr s).target
⊢ PG.property (↑e.symm : H → H) (e.target ∩ (↑e.symm : H → H) ⁻¹' s)

Tactic:
convert! hs.2 using 1

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          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.restr s)
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst] s
xs : (↑e.symm : H → H) x ∈ s
hs :
  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.restr s)
h h₁ : e.target ∩ (↑e.symm : H → H) ⁻¹' s = e.target ∩ (↑e.symm : H → H) ⁻¹' s
⊢ e.target ∩ (↑e.symm : H → H) ⁻¹' s = e.target ∩ (↑e.symm : H → H) ⁻¹' interior s

Tactic:
rw [s_open.interior_eq]

Premises used: IsOpen.interior_eq
-- 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
ee' : e' ≈ e
left : PG.property (↑e' : H → H) e'.source
right : PG.property (↑e'.symm : H → H) 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'

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
ee' : e' ≈ e
left : PG.property (↑e : H → H) e'.source
⊢ PG.property (↑e' : H → H) e'.source

Tactic:
apply PG.congr e'.open_source ee'.2

Premises used: OpenPartialHomeomorph.open_source, And.right, Pregroupoid.congr
-- 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
ee' : e' ≈ e
⊢ PG.property (↑e : H → H) e'.source

Tactic:
simp only [ee'.1, he.1]

Premises used: 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
ee' : e' ≈ e
⊢ e'.symm ≈ e.symm

Tactic:
have A := EqOnSource.symm' ee'
-- 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
ee' : e' ≈ e
A : e'.symm ≈ e.symm
right : PG.property (↑e.symm : H → H) e'.symm.source
⊢ PG.property (↑e'.symm : H → H) e'.target

Tactic:
apply PG.congr e'.symm.open_source A.2

Premises used: OpenPartialHomeomorph.open_source, And.right, Pregroupoid.congr, OpenPartialHomeomorph.symm
-- 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
ee' : e' ≈ e
A : e'.symm ≈ e.symm
⊢ PG.property (↑e.symm : H → H) e.target

Tactic:
he.2

Premises used: And.right
-- 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
ee' : e' ≈ e
A : e'.symm ≈ e.symm
h : e'.symm.source = e.target
⊢ PG.property (↑e.symm : H → H) e'.symm.source

Tactic:
convert! he.2 using 1

Premises used: And.right
-- 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
ee' : e' ≈ e
A : e'.symm ≈ e.symm
h : e.symm.source = e.target
h₁ : e.symm.source = e.target
h₂ h₃ : e.target = e.target
⊢ e'.symm.source = e.target

Tactic:
rw [A.1, symm_toPartialEquiv, PartialEquiv.symm_source]

Premises used: OpenPartialHomeomorph.symm_toPartialEquiv, PartialEquiv.symm_source, And.left
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
⊢ e ∈ PG.groupoid ↔ PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s
⊢ PG₁.groupoid ≤ PG₂.groupoid

Tactic:
StructureGroupoid.le_iff.2 fun e he ↦ ?_

Premises used: Iff.mpr, StructureGroupoid.le_iff
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s
refine : ∀ (e : OpenPartialHomeomorph H H) (he : e ∈ PG₁.groupoid), e ∈ PG₂.groupoid
⊢ PG₁.groupoid ≤ PG₂.groupoid

Tactic:
refine StructureGroupoid.le_iff.2 fun e he ↦ ?_

Premises used: Iff.mpr, StructureGroupoid.le_iff
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s
e : OpenPartialHomeomorph H H
he : e ∈ PG₁.groupoid
⊢ PG₁.property (↑e : H → H) e.source ∧ PG₁.property (↑e.symm : H → H) e.target

Tactic:
rw [mem_groupoid_of_pregroupoid] at he ⊢

Premises used: mem_groupoid_of_pregroupoid
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s
e : OpenPartialHomeomorph H H
he : PG₁.property (↑e : H → H) e.source ∧ PG₁.property (↑e.symm : H → H) e.target
⊢ PG₂.property (↑e : H → H) e.source ∧ PG₂.property (↑e.symm : H → H) e.target

Tactic:
⟨h _ _ he.1, h _ _ he.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s
e : OpenPartialHomeomorph H H
he : PG₁.property (↑e : H → H) e.source ∧ PG₁.property (↑e.symm : H → H) e.target
⊢ PG₂.property (↑e : H → H) e.source ∧ PG₂.property (↑e.symm : H → H) e.target

Tactic:
exact ⟨h _ _ he.1, h _ _ he.2⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he' : e ≈ e'
he : PG.property (↑e : H → H) e.source
rw : PG.property (↑e' : H → H) e.source
⊢ PG.property (↑e' : H → H) e'.source

Tactic:
rw [← he'.1]

Premises used: And.left