Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
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₁) x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : chartAt H y ∈ atlas H M'
hg₂ : y ∈ (chartAt H y).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ ↑(c.symm ≫ₕ f₁) ⁻¹' 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 ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G

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]

Goal state after:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
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₁) x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : chartAt H y ∈ atlas H M'
hg₂ : y ∈ (chartAt H y).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ ↑(c.symm ≫ₕ f₁) ⁻¹' 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
this : F₁ ≈ F₂
⊢ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G