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
hx₁ : x ∈ c.symm.source ∩ (↑c.symm : H → M) ⁻¹' ((e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
feq₁ :
  let f₁ := e.toOpenPartialHomeomorph;
  let f₂ := e'.toOpenPartialHomeomorph;
  let f := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph;
  f = f₁ ≫ₕ f₂
hg₃ :
  let f₁ := e.toOpenPartialHomeomorph;
  let y := (↑(c.symm ≫ₕ f₁) : H → M') x;
  Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₄ :
  let f₁ := e.toOpenPartialHomeomorph;
  let y := (↑(c.symm ≫ₕ f₁) : H → M') x;
  y ∈ (toPartialEquiv (chartAt H y)).source
⊢ let f₁ := e.toOpenPartialHomeomorph;
  let y := (↑(c.symm ≫ₕ f₁) : H → M') x;
  let g : OpenPartialHomeomorph M' H := chartAt H y;
  let s := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source;
  IsOpen[inst] s

Tactic:
rw [trans_source] at hx

Premises used: OpenPartialHomeomorph.trans_source
-- 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.source ∩ (↑c.symm : H → M) ⁻¹' ((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
⊢ x ∈ c.symm.source

Tactic:
hx.1

Premises used: And.left
-- 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.source ∩ (↑c.symm : H → M) ⁻¹' ((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
⊢ x ∈ c.symm.source

Tactic:
exact hx.1

Premises used: And.left
-- 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
⊢ x ∈ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source

Tactic:
hg₂

Premises used: Set.Mem, setOf, Set.preimage
-- 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
⊢ x ∈ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source

Tactic:
exact hg₂
-- 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
⊢ x ∈ s

Tactic:
have : x ∈ s := by
        constructor
        · simp only [f₁, trans_source, preimage_univ, inter_univ,
            Homeomorph.toOpenPartialHomeomorph_source]
          rw [trans_source] at hx
          exact hx.1
        · exact hg₂
-- 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
⊢ ∃ (s : Set H),
    IsOpen[inst] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G

Tactic:
⟨s, open_s, this, ?_⟩

Premises used: And.intro, Exists.intro
-- 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
refine : (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G
⊢ ∃ (s : Set H),
    IsOpen[inst] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G

Tactic:
refine ⟨s, open_s, 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 : x ∈ s
F₁ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f₁ ≫ₕ g) ≫ₕ g.symm ≫ₕ f₂ ≫ₕ c'
⊢ F₁ ∈ G

Tactic:
have A : F₁ ∈ G := G.trans (e.mem_groupoid c g hc hg₁) (e'.mem_groupoid g c' hg₁ hc')
-- 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₁ ≈ c.symm ≫ₕ f₁ ≫ₕ (g ≫ₕ g.symm) ≫ₕ f₂ ≫ₕ c'

Tactic:
simp only [F₁, trans_assoc, _root_.refl]

Premises used: OpenPartialHomeomorph.trans_assoc, 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 : 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
⊢ c.symm ≫ₕ f₁ ≫ₕ ofSet g.source ⋯ ≫ₕ f₂ ≫ₕ c' ≈ ((c.symm ≫ₕ f₁) ≫ₕ ofSet g.source ⋯) ≫ₕ f₂ ≫ₕ c'

Tactic:
simp only [trans_assoc, _root_.refl]

Premises used: OpenPartialHomeomorph.trans_assoc, 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 : 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
rw rw₁ :
  (eqOnSourceSetoid : OpenPartialHomeomorph H H → OpenPartialHomeomorph H H → Prop)
    ((c.symm ≫ₕ f₁).restr ((c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source) ≫ₕ f₂ ≫ₕ c')
    ((c.symm ≫ₕ f₁).restr ((c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source) ≫ₕ f₂ ≫ₕ c')
⊢ ((c.symm ≫ₕ f₁) ≫ₕ ofSet g.source ⋯) ≫ₕ f₂ ≫ₕ c' ≈ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c'

Tactic:
rw [trans_of_set']

Premises used: OpenPartialHomeomorph.trans_of_set'
-- 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
rw rw₁ :
  (eqOnSourceSetoid : OpenPartialHomeomorph H H → OpenPartialHomeomorph H H → Prop)
    (((c.symm ≫ₕ f₁) ≫ₕ f₂ ≫ₕ c').restr s) (((c.symm ≫ₕ f₁) ≫ₕ f₂ ≫ₕ c').restr s)
⊢ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c' ≈ ((c.symm ≫ₕ f₁) ≫ₕ f₂ ≫ₕ c').restr s

Tactic:
rw [restr_trans]

Premises used: OpenPartialHomeomorph.restr_trans
-- 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
⊢ ((c.symm ≫ₕ f₁) ≫ₕ f₂ ≫ₕ c').restr s ≈ (c.symm ≫ₕ (f₁ ≫ₕ f₂) ≫ₕ c').restr s

Tactic:
simp only [trans_assoc, _root_.refl]

Premises used: OpenPartialHomeomorph.trans_assoc, 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 : 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
⊢ (c.symm ≫ₕ (f₁ ≫ₕ f₂) ≫ₕ c').restr s ≈ F₂

Tactic:
simp only [F₂, feq, _root_.refl]

Premises used: refl