awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
open_s : IsOpen[inst] s
this : x ∈ s
F₁ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f₁ ≫ₕ g) ≫ₕ g.symm ≫ₕ f₂ ≫ₕ c'
A : F₁ ∈ G
F₂ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f ≫ₕ c').restr s
⊢ F₁ ≈ F₂

Tactic:
have : F₁ ≈ F₂ := calc
        F₁ ≈ c.symm ≫ₕ f₁ ≫ₕ (g ≫ₕ g.symm) ≫ₕ f₂ ≫ₕ c' := by
            simp only [F₁, trans_assoc, _root_.refl]
        _ ≈ c.symm ≫ₕ f₁ ≫ₕ ofSet g.source g.open_source ≫ₕ f₂ ≫ₕ c' :=
          EqOnSource.trans' (_root_.refl _) (EqOnSource.trans' (_root_.refl _)
            (EqOnSource.trans' (self_trans_symm g) (_root_.refl _)))
        _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ ofSet g.source g.open_source) ≫ₕ f₂ ≫ₕ c' := by
          simp only [trans_assoc, _root_.refl]
        _ ≈ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c' := by rw [trans_of_set']
        _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ f₂ ≫ₕ c').restr s := by rw [restr_trans]
        _ ≈ (c.symm ≫ₕ (f₁ ≫ₕ f₂) ≫ₕ c').restr s := by
          simp only [trans_assoc, _root_.refl]
        _ ≈ F₂ := by simp only [F₂, feq, _root_.refl]
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
open_s : IsOpen[inst] s
this_1 : x ∈ s
F₁ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f₁ ≫ₕ g) ≫ₕ g.symm ≫ₕ f₂ ≫ₕ c'
A : F₁ ∈ G
F₂ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f ≫ₕ c').restr s
this : F₁ ≈ F₂
⊢ F₂ ∈ G

Tactic:
have : F₂ ∈ G := G.mem_of_eqOnSource A (Setoid.symm this)
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
open_s : IsOpen[inst] s
this_1 : x ∈ s
F₁ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f₁ ≫ₕ g) ≫ₕ g.symm ≫ₕ f₂ ≫ₕ c'
A : F₁ ∈ G
F₂ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f ≫ₕ c').restr s
this_2 : F₁ ≈ F₂
this : F₂ ∈ G
⊢ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G

Tactic:
this

Premises used: Set.Mem
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
open_s : IsOpen[inst] s
this_1 : x ∈ s
F₁ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f₁ ≫ₕ g) ≫ₕ g.symm ≫ₕ f₂ ≫ₕ c'
A : F₁ ∈ G
F₂ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f ≫ₕ c').restr s
this_2 : F₁ ≈ F₂
this : F₂ ∈ G
⊢ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G

Tactic:
exact this
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hs : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) c'
⊢ Nonempty.{u + 1} ↥t

Tactic:
have : Nonempty t := nonempty_coe_sort.mpr (e.mapsTo.nonempty (nonempty_coe_sort.mp hs))
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hs : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) c'
this : Nonempty.{u + 1} ↥t
obtain :
  ∀ (x : ↥t) (hc' : c' = subtypeRestr (chartAt H (↑x : H)) this),
    Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (maximalAtlas (↥s) G)
      (e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ c')
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (maximalAtlas (↥s) G)
    (e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ c')

Tactic:
obtain ⟨x, hc'⟩ := Opens.chart_eq this hc'

Premises used: TopologicalSpace.Opens.chart_eq
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hs : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'_1 : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) c'
this : Nonempty.{u + 1} ↥t
x : ↥t
hc' : c' = subtypeRestr (chartAt H (↑x : H)) this
rw :
  Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (maximalAtlas (↥s) G)
    (e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ subtypeRestr (OpenPartialHomeomorph.refl H) this)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (maximalAtlas (↥s) G)
    (e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ c')

Tactic:
rw [hc', (chartAt_self_eq)]

Premises used: chartAt_self_eq
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hs : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'_1 : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) c'
this : Nonempty.{u + 1} ↥t
x : ↥t
hc' : c' = subtypeRestr (chartAt H (↑x : H)) this
rw :
  Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (maximalAtlas (↥s) G)
    (e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (maximalAtlas (↥s) G)
    (e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ subtypeRestr (OpenPartialHomeomorph.refl H) this)

Tactic:
rw [OpenPartialHomeomorph.subtypeRestr_def, OpenPartialHomeomorph.trans_refl]

Premises used: OpenPartialHomeomorph.trans_refl, OpenPartialHomeomorph.subtypeRestr_def
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hs : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'_1 : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) c'
this : Nonempty.{u + 1} ↥t
x : ↥t
hc' : c' = subtypeRestr (chartAt H (↑x : H)) this
goal : OpenPartialHomeomorph.{u_2, u} (↑e.source : Type u_2) H :=
  e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this
⊢ Eq (α := Set (↑e.source : Type u_2)) univ
    (Subtype.val (p := fun (x : M) ↦ x ∈ { carrier := e.source, is_open' := ⋯ : Opens M }) ⁻¹' e.source)

Tactic:
Subtype.coe_preimage_self _ |>.symm

Premises used: Set.Mem, Subtype.coe_preimage_self, Eq.symm
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hs : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'_1 : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) c'
this : Nonempty.{u + 1} ↥t
x : ↥t
hc' : c' = subtypeRestr (chartAt H (↑x : H)) this
goal : OpenPartialHomeomorph.{u_2, u} (↑e.source : Type u_2) H :=
  e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this
⊢ Eq (α := Set (↑e.source : Type u_2)) univ
    (Subtype.val (p := fun (x : M) ↦ x ∈ { carrier := e.source, is_open' := ⋯ : Opens M }) ⁻¹' e.source)

Tactic:
exact Subtype.coe_preimage_self _ |>.symm

Premises used: Subtype.coe_preimage_self, Eq.symm
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hs : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'_1 : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) c'
this : Nonempty.{u + 1} ↥t
x : ↥t
hc' : c' = subtypeRestr (chartAt H (↑x : H)) this
goal : OpenPartialHomeomorph.{u_2, u} (↑e.source : Type u_2) H :=
  e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this
x_1 : (↑e.source : Type u_2)
_ :
  x_1 ∈ goal.source →
    (↑goal.toPartialEquiv : (↑e.source : Type u_2) → H) x_1 =
      (↑(toPartialEquiv (e.subtypeRestr hs)) : (↑e.source : Type u_2) → H) x_1
⊢ x_1 ∈ goal.source →
    (↑goal.toPartialEquiv : (↑e.source : Type u_2) → H) x_1 =
      (↑(toPartialEquiv (e.subtypeRestr hs)) : (↑e.source : Type u_2) → H) x_1

Tactic:
_
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hs : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'_1 : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) c'
this : Nonempty.{u + 1} ↥t
x : ↥t
hc' : c' = subtypeRestr (chartAt H (↑x : H)) this
goal : OpenPartialHomeomorph.{u_2, u} (↑e.source : Type u_2) H :=
  e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this
x_1 : (↑e.source : Type u_2)
h : x_1 ∈ goal.source
⊢ (↑goal.toPartialEquiv : (↑e.source : Type u_2) → H) x_1 =
    (↑(toPartialEquiv (e.subtypeRestr hs)) : (↑e.source : Type u_2) → H) x_1

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hs : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'_1 : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) c'
this : Nonempty.{u + 1} ↥t
x : ↥t
hc' : c' = subtypeRestr (chartAt H (↑x : H)) this
goal : OpenPartialHomeomorph.{u_2, u} (↑e.source : Type u_2) H :=
  e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this
⊢ goal ≈ e.subtypeRestr hs

Tactic:
have : goal ≈ e.subtypeRestr (s := s) hs :=
    (goal.eqOnSource_iff (e.subtypeRestr (s := s) hs)).mpr
      ⟨by
        simp only [trans_toPartialEquiv, PartialEquiv.trans_source,
          Homeomorph.toOpenPartialHomeomorph_source, toFun_eq_coe,
          Homeomorph.toOpenPartialHomeomorph_apply, Opens.openPartialHomeomorphSubtypeCoe_source,
          preimage_univ, inter_self, subtypeRestr_source, goal, s]
        exact Subtype.coe_preimage_self _ |>.symm, by intro _ _; rfl⟩
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hs : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'_1 : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) c'
this_1 : Nonempty.{u + 1} ↥t
x : ↥t
hc' : c' = subtypeRestr (chartAt H (↑x : H)) this_1
goal : OpenPartialHomeomorph.{u_2, u} (↑e.source : Type u_2) H :=
  e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this_1
this : goal ≈ e.subtypeRestr hs
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (maximalAtlas (↥s) G)
    (e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this_1)

Tactic:
G.mem_maximalAtlas_of_eqOnSource (M := s) this (G.subtypeRestr_mem_maximalAtlas he hs)

Premises used: StructureGroupoid.mem_maximalAtlas_of_eqOnSource, StructureGroupoid.subtypeRestr_mem_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hs : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'_1 : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) c'
this_1 : Nonempty.{u + 1} ↥t
x : ↥t
hc' : c' = subtypeRestr (chartAt H (↑x : H)) this_1
goal : OpenPartialHomeomorph.{u_2, u} (↑e.source : Type u_2) H :=
  e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this_1
this : goal ≈ e.subtypeRestr hs
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (maximalAtlas (↥s) G)
    (e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this_1)

Tactic:
exact G.mem_maximalAtlas_of_eqOnSource (M := s) this (G.subtypeRestr_mem_maximalAtlas he hs)

Premises used: StructureGroupoid.mem_maximalAtlas_of_eqOnSource, StructureGroupoid.subtypeRestr_mem_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
inst_7 : HasGroupoid M G
inst_8 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
pos : (h : Nonempty.{u_2 + 1} (↑e.source : Type u_2)) → Structomorph.{u, u_2, u} G ↥s ↥t
neg : (h : IsEmpty.{u_2 + 1} (↑e.source : Type u_2)) → Structomorph.{u, u_2, u} G ↥s ↥t
⊢ Structomorph.{u, u_2, u} G ↥s ↥t

Tactic:
by_cases! h : Nonempty e.source

Premises used: Set.Elem, Nonempty, PartialEquiv.source, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
inst_7 : HasGroupoid M G
inst_8 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
h : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
⊢ Structomorph.{u, u_2, u} G ↥s ↥t

Tactic:
exact { e.toHomeomorphSourceTarget with
      mem_groupoid :=
        -- The atlas of H on itself has only one chart, hence c' is the inclusion.
        -- Then, compatibility of `G` *almost* yields our claim --- except that `e` is a chart
        -- on `M` and `c` is one on `s`: we need to show that restricting `e` to `s` and composing
        -- with `c'` yields a chart in the maximal atlas of `s`.
        fun c c' hc hc' ↦ G.compatible_of_mem_maximalAtlas (G.subset_maximalAtlas hc)
          (G.restriction_mem_maximalAtlas_subtype he h c' hc') }

Premises used: OpenPartialHomeomorph.toHomeomorphSourceTarget
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
inst_7 : HasGroupoid M G
inst_8 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
h : IsEmpty.{u_2 + 1} (↑e.source : Type u_2)
⊢ (↑t : Set H) = ∅

Tactic:
convert! e.image_source_eq_target ▸ image_eq_empty.mpr (isEmpty_coe_sort.mp h)
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
inst_7 : HasGroupoid M G
inst_8 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
h : IsEmpty.{u_2 + 1} (↑e.source : Type u_2)
⊢ IsEmpty.{u + 1} ↥t

Tactic:
have : IsEmpty t := isEmpty_coe_sort.mpr
      (by convert! e.image_source_eq_target ▸ image_eq_empty.mpr (isEmpty_coe_sort.mp h))
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
inst_7 : HasGroupoid M G
inst_8 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
h : IsEmpty.{u_2 + 1} (↑e.source : Type u_2)
this : IsEmpty.{u + 1} ↥t
⊢ Structomorph.{u, u_2, u} G ↥s ↥t

Tactic:
exact { Homeomorph.empty with
      -- `c'` cannot exist: it would be the restriction of `chartAt H x` at some `x ∈ t`.
      mem_groupoid := fun _ c' _ ⟨_, ⟨x, _⟩, _⟩ ↦ (this.false x).elim }

Premises used: Homeomorph.empty