awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ PG.property (↑e' : H → H) e.source

Tactic:
PG.congr e.open_source he'.eqOn.symm he

Premises used: OpenPartialHomeomorph.EqOnSource.eqOn, OpenPartialHomeomorph.open_source, Pregroupoid.congr, Set.EqOn.symm
-- 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
⊢ PG.property (↑e' : H → H) e.source

Tactic:
exact PG.congr e.open_source he'.eqOn.symm he

Premises used: OpenPartialHomeomorph.EqOnSource.eqOn, OpenPartialHomeomorph.open_source, Pregroupoid.congr, Set.EqOn.symm
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
⊢ ∀ (s : Set (StructureGroupoid H)), IsGLB s (sInf s)

Tactic:
fun s =>
      ⟨fun S Ss F hF => mem_iInter₂.mp hF S Ss,
      fun T Tl F fT => mem_iInter₂.mpr (fun i his => Tl his fT)⟩

Premises used: Iff.mpr, Set.mem_iInter₂, IsGreatest, IsGLB, And.intro, Iff.mp
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
⊢ ∀ (s : Set (StructureGroupoid H)), IsGLB s (sInf s)

Tactic:
exact fun s =>
      ⟨fun S Ss F hF => mem_iInter₂.mp hF S Ss,
      fun T Tl F fT => mem_iInter₂.mpr (fun i his => Tl his fT)⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen[inst] s
⊢ e.restr s ∈ G

Tactic:
ClosedUnderRestriction.closedUnderRestriction he s hs

Premises used: ClosedUnderRestriction.closedUnderRestriction
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hse : e ≈ ofSet s hs
s' : Set H
hs' : IsOpen[inst] s'
hse' : e' ≈ ofSet s' hs'
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e ≫ₕ e')

Tactic:
⟨s ∩ s', hs.inter hs', ?_⟩

Premises used: Set.Mem, setOf, Inter.inter, IsOpen.inter, Exists.intro
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hse : e ≈ ofSet s hs
s' : Set H
hs' : IsOpen[inst] s'
hse' : e' ≈ ofSet s' hs'
refine : e ≫ₕ e' ≈ ofSet (s ∩ s') ⋯
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e ≫ₕ e')

Tactic:
refine ⟨s ∩ s', hs.inter hs', ?_⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hse : e ≈ ofSet s hs
s' : Set H
hs' : IsOpen[inst] s'
hse' : e' ≈ ofSet s' hs'
⊢ e ≫ₕ e' ≈ ofSet s hs ≫ₕ ofSet s' hs'

Tactic:
have := OpenPartialHomeomorph.EqOnSource.trans' hse hse'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hse : e ≈ ofSet s hs
s' : Set H
hs' : IsOpen[inst] s'
hse' : e' ≈ ofSet s' hs'
this : e ≫ₕ e' ≈ ofSet s hs ≫ₕ ofSet s' hs'
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : e ≫ₕ e' ≈ ofSet (s ∩ s') ⋯), e ≫ₕ e' ≈ ofSet (s ∩ s') ⋯
⊢ e ≫ₕ e' ≈ ofSet (s ∩ s') ⋯

Tactic:
rwa [OpenPartialHomeomorph.ofSet_trans_ofSet] at this

Premises used: OpenPartialHomeomorph.ofSet_trans_ofSet
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hse : e ≈ ofSet s hs
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} e.symm

Tactic:
⟨s, hs, ?_⟩

Premises used: Set.Mem, setOf, Exists.intro
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hse : e ≈ ofSet s hs
refine : e.symm ≈ ofSet s hs
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} e.symm

Tactic:
refine ⟨s, hs, ?_⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hse : e ≈ ofSet s hs
rw : e.symm ≈ (ofSet s hs).symm
⊢ e.symm ≈ ofSet s hs

Tactic:
rw [← ofSet_symm]

Premises used: OpenPartialHomeomorph.ofSet_symm
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hse : e ≈ ofSet s hs
⊢ e.symm ≈ (ofSet s hs).symm

Tactic:
OpenPartialHomeomorph.EqOnSource.symm' hse

Premises used: OpenPartialHomeomorph.EqOnSource.symm'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hse : e ≈ ofSet s hs
⊢ e.symm ≈ (ofSet s hs).symm

Tactic:
exact OpenPartialHomeomorph.EqOnSource.symm' hse

Premises used: OpenPartialHomeomorph.EqOnSource.symm'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
⊢ HasEquiv.Equiv (α := OpenPartialHomeomorph H H) (OpenPartialHomeomorph.refl H) (ofSet univ ⋯)

Tactic:
simp only [mfld_simps, refl]

Premises used: refl
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
h :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e.restr s)
⊢ e.source = (ofSet e.source ⋯).source

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
h :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e.restr s)
refine : EqOn (↑e : H → H) (↑(ofSet e.source ⋯) : H → H) e.source
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} e

Tactic:
refine ⟨e.source, e.open_source, by simp only [mfld_simps], ?_⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
h :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e.restr s)
x : H
hx : x ∈ e.source
rcases :
  ∀ (s : Set H) (hs : IsOpen[inst] s) (hxs : x ∈ s) (s' : Set H) (hs' : IsOpen[inst] s')
    (hes' : e.restr s ≈ ofSet s' hs'), (↑e : H → H) x = (↑(ofSet e.source ⋯) : H → H) x
⊢ (↑e : H → H) x = (↑(ofSet e.source ⋯) : H → H) x

Tactic:
rcases h x hx with ⟨s, hs, hxs, s', hs', hes'⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
h :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
hs : IsOpen[inst] s
hxs : x ∈ s
s' : Set H
hs' : IsOpen[inst] s'
hes' : e.restr s ≈ ofSet s' hs'
⊢ x ∈ e.source ∩ interior s

Tactic:
⟨hx, ?_⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
h :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
hs : IsOpen[inst] s
hxs : x ∈ s
s' : Set H
hs' : IsOpen[inst] s'
hes' : e.restr s ≈ ofSet s' hs'
refine : x ∈ interior s
⊢ x ∈ e.source ∩ interior s

Tactic:
refine ⟨hx, ?_⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
h :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
hs : IsOpen[inst] s
hxs : x ∈ s
s' : Set H
hs' : IsOpen[inst] s'
hes' : e.restr s ≈ ofSet s' hs'
rw : x ∈ s
⊢ x ∈ interior s

Tactic:
rw [hs.interior_eq]

Premises used: IsOpen.interior_eq
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
h :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
hs : IsOpen[inst] s
hxs : x ∈ s
s' : Set H
hs' : IsOpen[inst] s'
hes' : e.restr s ≈ ofSet s' hs'
⊢ x ∈ s

Tactic:
hxs
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
h :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
hs : IsOpen[inst] s
hxs : x ∈ s
s' : Set H
hs' : IsOpen[inst] s'
hes' : e.restr s ≈ ofSet s' hs'
⊢ x ∈ s

Tactic:
exact hxs
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
h :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
hs : IsOpen[inst] s
hxs : x ∈ s
s' : Set H
hs' : IsOpen[inst] s'
hes' : e.restr s ≈ ofSet s' hs'
⊢ x ∈ (e.restr s).source

Tactic:
have hes : x ∈ (e.restr s).source := by
      rw [e.restr_source]
      refine ⟨hx, ?_⟩
      rw [hs.interior_eq]
      exact hxs
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
h :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
hs : IsOpen[inst] s
hxs : x ∈ s
s' : Set H
hs' : IsOpen[inst] s'
hes' : e.restr s ≈ ofSet s' hs'
hes : x ∈ (e.restr s).source
⊢ (↑e : H → H) x = (↑(ofSet e.source ⋯) : H → H) x

Tactic:
simpa only [mfld_simps] using OpenPartialHomeomorph.EqOnSource.eqOn hes' hes

Premises used: OpenPartialHomeomorph.EqOnSource.eqOn
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hse : e ≈ ofSet s hs
hee' : e' ≈ e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} e'

Tactic:
⟨s, hs, Setoid.trans hee' hse⟩

Premises used: Set.Mem, setOf, Exists.intro, Setoid.trans
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hse : e ≈ ofSet s hs
hee' : e' ≈ e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} e'

Tactic:
exact ⟨s, hs, Setoid.trans hee' hse⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
s : Set H
hs : IsOpen[inst] s
⊢ Membership.mem (γ := StructureGroupoid H) idRestrGroupoid (ofSet s hs)

Tactic:
⟨s, hs, refl _⟩

Premises used: Set.Mem, setOf, Exists.intro, refl
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
s' : Set H
hs' : IsOpen[inst] s'
he : e ≈ ofSet s' hs'
s : Set H
hs : IsOpen[inst] s
h : e.restr s ≈ ofSet (s' ∩ s) ⋯
⊢ Membership.mem (γ := StructureGroupoid H) idRestrGroupoid (e.restr s)

Tactic:
use s' ∩ s, hs'.inter hs

Premises used: IsOpen.inter
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
s' : Set H
hs' : IsOpen[inst] s'
he : e ≈ ofSet s' hs'
s : Set H
hs : IsOpen[inst] s
⊢ e.restr s ≈ ofSet (s' ∩ s) ⋯

Tactic:
Setoid.trans (OpenPartialHomeomorph.EqOnSource.restr he s) ?_

Premises used: OpenPartialHomeomorph.EqOnSource.restr, Setoid.trans
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
s' : Set H
hs' : IsOpen[inst] s'
he : e ≈ ofSet s' hs'
s : Set H
hs : IsOpen[inst] s
h : (ofSet s' hs').restr s ≈ ofSet (s' ∩ s) ⋯
⊢ e.restr s ≈ ofSet (s' ∩ s) ⋯

Tactic:
refine Setoid.trans (OpenPartialHomeomorph.EqOnSource.restr he s) ?_

Premises used: OpenPartialHomeomorph.EqOnSource.restr, Setoid.trans
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
s' : Set H
hs' : IsOpen[inst] s'
he : e ≈ ofSet s' hs'
s : Set H
hs : IsOpen[inst] s
⊢ ((ofSet s' hs').restr s).source = (ofSet (s' ∩ s) ⋯).source

Tactic:
simp only [hs.interior_eq, mfld_simps]

Premises used: IsOpen.interior_eq
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
s' : Set H
hs' : IsOpen[inst] s'
he : e ≈ ofSet s' hs'
s : Set H
hs : IsOpen[inst] s
⊢ EqOn (↑((ofSet s' hs').restr s) : H → H) (↑(ofSet (s' ∩ s) ⋯) : H → H) ((ofSet s' hs').restr s).source

Tactic:
simp only [mfld_simps, eqOn_refl]

Premises used: Set.eqOn_refl
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
s' : Set H
hs' : IsOpen[inst] s'
he : e ≈ ofSet s' hs'
s : Set H
hs : IsOpen[inst] s
⊢ (ofSet s' hs').restr s ≈ ofSet (s' ∩ s) ⋯

Tactic:
exact ⟨by simp only [hs.interior_eq, mfld_simps], by simp only [mfld_simps, eqOn_refl]⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
mp : ClosedUnderRestriction G → idRestrGroupoid ≤ G
mpr : idRestrGroupoid ≤ G → ClosedUnderRestriction G
⊢ ClosedUnderRestriction G ↔ idRestrGroupoid ≤ G

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hes : e ≈ ofSet s hs
⊢ e ∈ G

Tactic:
G.mem_of_eqOnSource ?_ hes

Premises used: StructureGroupoid.mem_of_eqOnSource
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hes : e ≈ ofSet s hs
mp : ofSet s hs ∈ G
⊢ e ∈ G

Tactic:
refine G.mem_of_eqOnSource ?_ hes

Premises used: StructureGroupoid.mem_of_eqOnSource
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hes : e ≈ ofSet s hs
⊢ OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s ∈ G

Tactic:
closedUnderRestriction' G.id_mem hs

Premises used: StructureGroupoid.id_mem, closedUnderRestriction'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hes : e ≈ ofSet s hs
h : ofSet s hs = OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s
⊢ ofSet s hs ∈ G

Tactic:
convert! closedUnderRestriction' G.id_mem hs

Premises used: StructureGroupoid.id_mem, closedUnderRestriction'
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hes : e ≈ ofSet s hs
h : ∀ (x : H), (↑(ofSet s hs) : H → H) x = (↑(OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s) : H → H) x
h₁ :
  ∀ (x : H),
    (↑(ofSet s hs).symm : H → H) x =
      (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s)) : H → H) x
h₂ :
  ∀ (x : H),
    x ∈ (ofSet s hs).source ↔ x ∈ (toPartialEquiv (OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s)).source
⊢ ofSet s hs = OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s

Tactic:
ext
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hes : e ≈ ofSet s hs
x : H
⊢ (↑(ofSet s hs) : H → H) x = (↑(OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s) : H → H) x

Tactic:
simp [hs.interior_eq]

Premises used: IsOpen.interior_eq
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hes : e ≈ ofSet s hs
x : H
⊢ (↑(ofSet s hs).symm : H → H) x =
    (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s)) : H → H) x

Tactic:
simp [hs.interior_eq]

Premises used: IsOpen.interior_eq
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hes : e ≈ ofSet s hs
x : H
⊢ x ∈ (ofSet s hs).source ↔ x ∈ (toPartialEquiv (OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s)).source

Tactic:
simp [hs.interior_eq]

Premises used: IsOpen.interior_eq
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
mpr : ∀ {e : OpenPartialHomeomorph H H}, e ∈ G → ∀ (s : Set H), IsOpen[inst] s → e.restr s ∈ G
⊢ ClosedUnderRestriction G

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : OpenPartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen[inst] s
mpr : ofSet s hs ≫ₕ e ∈ G
⊢ e.restr s ∈ G

Tactic:
rw [← ofSet_trans (e : OpenPartialHomeomorph H H) hs]

Premises used: OpenPartialHomeomorph.ofSet_trans
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : OpenPartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen[inst] s
⊢ ofSet s hs ≫ₕ e ∈ G

Tactic:
G.trans ?_ he

Premises used: StructureGroupoid.trans
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : OpenPartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen[inst] s
mpr : ofSet s hs ∈ G
⊢ ofSet s hs ≫ₕ e ∈ G

Tactic:
refine G.trans ?_ he

Premises used: StructureGroupoid.trans
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : OpenPartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen[inst] s
mpr : Membership.mem (γ := StructureGroupoid H) idRestrGroupoid (ofSet s hs)
⊢ ofSet s hs ∈ G

Tactic:
apply StructureGroupoid.le_iff.mp h

Premises used: StructureGroupoid.le_iff, Iff.mp
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : OpenPartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen[inst] s
⊢ Membership.mem (γ := StructureGroupoid H) idRestrGroupoid (ofSet s hs)

Tactic:
idRestrGroupoid_mem hs

Premises used: idRestrGroupoid_mem
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : OpenPartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen[inst] s
⊢ Membership.mem (γ := StructureGroupoid H) idRestrGroupoid (ofSet s hs)

Tactic:
exact idRestrGroupoid_mem hs

Premises used: idRestrGroupoid_mem
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H : Type u_1
inst : TopologicalSpace H
⊢ ClosedUnderRestriction (continuousGroupoid H)

Tactic:
(closedUnderRestriction_iff_id_le _).mpr le_top

Premises used: Iff.mpr, closedUnderRestriction_iff_id_le, le_top
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace F
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : TopologicalSpace B
inst_4 : FiberBundle F E
x : TotalSpace F E
⊢ Eq (α := OpenPartialHomeomorph (TotalSpace F E) (B × F)) (chartAt (B × F) x)
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace F
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst_3 : TopologicalSpace HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : FiberBundle F E
x : TotalSpace F E
dsimp :
  Eq (α := OpenPartialHomeomorph (TotalSpace F E) (ModelProd HB F))
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
      OpenPartialHomeomorph.prod
        (chartAt HB
          ((↑(Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) : TotalSpace F E → B × F)
              x).1)
        (OpenPartialHomeomorph.refl F))
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
      OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))
⊢ Eq (α := OpenPartialHomeomorph (TotalSpace F E) (ModelProd HB F)) (chartAt (ModelProd HB F) x)
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
      OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))

Tactic:
dsimp only [chartAt_comp, prodChartedSpace_chartAt, FiberBundle.chartedSpace'_chartAt,
    chartAt_self_eq]

Premises used: prodChartedSpace_chartAt, FiberBundle.chartedSpace'_chartAt, chartAt_comp, chartAt_self_eq