[GOAL]
C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
γ : c ⟶ c
⊢ (fun δ => f ≫ δ ≫ inv f) ((fun γ => inv f ≫ γ ≫ f) γ) = γ
[PROOFSTEP]
simp_rw [Category.assoc, comp_inv, Category.comp_id, ← Category.assoc, comp_inv, Category.id_comp]
[GOAL]
C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
δ : d ⟶ d
⊢ (fun γ => inv f ≫ γ ≫ f) ((fun δ => f ≫ δ ≫ inv f) δ) = δ
[PROOFSTEP]
simp_rw [Category.assoc, inv_comp, ← Category.assoc, inv_comp, Category.id_comp, Category.comp_id]
[GOAL]
C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
γ₁ γ₂ : c ⟶ c
⊢ Equiv.toFun
      { toFun := fun γ => inv f ≫ γ ≫ f, invFun := fun δ => f ≫ δ ≫ inv f,
        left_inv := (_ : ∀ (γ : c ⟶ c), (fun δ => f ≫ δ ≫ inv f) ((fun γ => inv f ≫ γ ≫ f) γ) = γ),
        right_inv := (_ : ∀ (δ : d ⟶ d), (fun γ => inv f ≫ γ ≫ f) ((fun δ => f ≫ δ ≫ inv f) δ) = δ) }
      (γ₁ * γ₂) =
    Equiv.toFun
        { toFun := fun γ => inv f ≫ γ ≫ f, invFun := fun δ => f ≫ δ ≫ inv f,
          left_inv := (_ : ∀ (γ : c ⟶ c), (fun δ => f ≫ δ ≫ inv f) ((fun γ => inv f ≫ γ ≫ f) γ) = γ),
          right_inv := (_ : ∀ (δ : d ⟶ d), (fun γ => inv f ≫ γ ≫ f) ((fun δ => f ≫ δ ≫ inv f) δ) = δ) }
        γ₁ *
      Equiv.toFun
        { toFun := fun γ => inv f ≫ γ ≫ f, invFun := fun δ => f ≫ δ ≫ inv f,
          left_inv := (_ : ∀ (γ : c ⟶ c), (fun δ => f ≫ δ ≫ inv f) ((fun γ => inv f ≫ γ ≫ f) γ) = γ),
          right_inv := (_ : ∀ (δ : d ⟶ d), (fun γ => inv f ≫ γ ≫ f) ((fun δ => f ≫ δ ≫ inv f) δ) = δ) }
        γ₂
[PROOFSTEP]
simp only [vertexGroup_mul, inv_eq_inv, Category.assoc, IsIso.hom_inv_id_assoc]
