awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M_1 : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M_1
inst_2 : ChartedSpace H M_1
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : HasGroupoid M G
c 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'
⊢ c.symm ≫ₕ c' ∈ G

Tactic:
exact G.compatible hc hc'

Premises used: StructureGroupoid.compatible
-- 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'
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'
⊢ (c'.symm ≫ₕ e.toOpenPartialHomeomorph ≫ₕ c).symm ∈ G

Tactic:
have : (c'.symm ≫ₕ e.toHomeomorph.toOpenPartialHomeomorph ≫ₕ c).symm ∈ G :=
        G.symm (e.mem_groupoid c' c hc' 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'
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'
this : (c'.symm ≫ₕ e.toOpenPartialHomeomorph ≫ₕ c).symm ∈ G
rwa :
  ∀ (this : (e.toOpenPartialHomeomorph ≫ₕ c).symm ≫ₕ c'.symm.symm ∈ G),
    c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
rwa₁ :
  ∀ (this : (c.symm ≫ₕ e.toOpenPartialHomeomorph.symm) ≫ₕ c'.symm.symm ∈ G),
    c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
rwa₂ :
  ∀ (this : (c.symm ≫ₕ e.toOpenPartialHomeomorph.symm) ≫ₕ c' ∈ G), c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (this : c.symm ≫ₕ e.toOpenPartialHomeomorph.symm ≫ₕ c' ∈ G), c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
⊢ c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G

Tactic:
rwa [trans_symm_eq_symm_trans_symm, trans_symm_eq_symm_trans_symm, symm_symm, trans_assoc]
        at this

Premises used: OpenPartialHomeomorph.trans_assoc, OpenPartialHomeomorph.trans_symm_eq_symm_trans_symm, OpenPartialHomeomorph.symm_symm
-- 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'
⊢ c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c' ∈ G

Tactic:
G.locality fun x hx ↦ ?_

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

Tactic:
refine G.locality fun x hx ↦ ?_

Premises used: StructureGroupoid.locality
-- 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
⊢ f = f₁ ≫ₕ f₂

Tactic:
have feq : f = f₁ ≫ₕ f₂ := Homeomorph.trans_toOpenPartialHomeomorph _ _
-- 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
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)

Tactic:
have hg₁ := chart_mem_atlas (H := H) y
-- 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)
⊢ y ∈ (toPartialEquiv (chartAt H y)).source

Tactic:
have hg₂ := mem_chart_source (H := H) y
-- 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
hs : IsOpen[inst] (c.symm ≫ₕ f₁).source
ht : IsOpen[inst_3] g.source
⊢ IsOpen[inst] s

Tactic:
apply (c.symm ≫ₕ f₁).continuousOn_toFun.isOpen_inter_preimage

Premises used: OpenPartialHomeomorph.trans, ContinuousOn.isOpen_inter_preimage, OpenPartialHomeomorph.continuousOn_toFun, OpenPartialHomeomorph.symm
-- 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
⊢ IsOpen[inst] (c.symm ≫ₕ f₁).source

Tactic:
apply open_source

Premises used: OpenPartialHomeomorph.open_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 ≫ₕ (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
⊢ IsOpen[inst_3] g.source

Tactic:
apply open_source

Premises used: OpenPartialHomeomorph.open_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 ≫ₕ (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
⊢ IsOpen[inst] s

Tactic:
have open_s : IsOpen s := by
        apply (c.symm ≫ₕ f₁).continuousOn_toFun.isOpen_inter_preimage <;> apply open_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 ≫ₕ (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
left : x ∈ (c.symm ≫ₕ f₁).source
right : x ∈ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
⊢ x ∈ s

Tactic:
constructor
-- 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
left : x ∈ c.symm.source
⊢ x ∈ (c.symm ≫ₕ f₁).source

Tactic:
simp only [f₁, trans_source, preimage_univ, inter_univ,
            Homeomorph.toOpenPartialHomeomorph_source]

Premises used: Set.inter_univ, OpenPartialHomeomorph.trans_source, Set.preimage_univ, Homeomorph.toOpenPartialHomeomorph_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 ≫ₕ (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 ∩ (↑c.symm : H → M) ⁻¹' ((e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source

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 ≫ₕ (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
⊢ let f₁ := e.toOpenPartialHomeomorph;
  let f₂ := e'.toOpenPartialHomeomorph;
  let f := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph;
  f = f₁ ≫ₕ f₂

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 ≫ₕ (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₂
⊢ let f₁ := e.toOpenPartialHomeomorph;
  let y := (↑(c.symm ≫ₕ f₁) : H → M') x;
  Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)

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 ≫ₕ (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)
⊢ let f₁ := e.toOpenPartialHomeomorph;
  let y := (↑(c.symm ≫ₕ f₁) : H → M') x;
  y ∈ (toPartialEquiv (chartAt H y)).source

Tactic:
rw [trans_source] at hx

Premises used: OpenPartialHomeomorph.trans_source