[GOAL]
C : Type u
inst✝ : Groupoid C
X Y : C
f : X ⟶ Y
⊢ inv (inv f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Groupoid C
X Y : C
f : Y ⟶ X
⊢ inv (inv f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Groupoid C
X Y a✝ b✝ : C
f : a✝ ⟶ b✝
⊢ Quiver.reverse (Quiver.reverse f) = f
[PROOFSTEP]
dsimp [Quiver.reverse]
[GOAL]
C : Type u
inst✝ : Groupoid C
X Y a✝ b✝ : C
f : a✝ ⟶ b✝
⊢ Groupoid.inv (Groupoid.inv f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Groupoid C
X Y : C
D : Type u_1
inst✝ : Groupoid D
F : C ⥤ D
u✝ v✝ : C
f : u✝ ⟶ v✝
⊢ F.map (Quiver.reverse f) = Quiver.reverse (F.map f)
[PROOFSTEP]
simp only [Quiver.reverse, Quiver.HasReverse.reverse', Groupoid.inv_eq_inv, Functor.map_inv]
[GOAL]
C : Type u
inst✝ : Groupoid C
X Y : C
f : X ⟶ Y
⊢ f ≫ inv f = 𝟙 X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Groupoid C
X Y : C
f : X ⟶ Y
⊢ inv f ≫ f = 𝟙 Y
[PROOFSTEP]
aesop_cat
[GOAL]
I : Type u
J : I → Type u₂
inst✝ : (i : I) → Groupoid (J i)
X✝ Y✝ : (i : I) → J i
f : X✝ ⟶ Y✝
⊢ (fun {X Y} f i => Groupoid.inv (f i)) f ≫ f = 𝟙 Y✝
[PROOFSTEP]
funext i
[GOAL]
case h
I : Type u
J : I → Type u₂
inst✝ : (i : I) → Groupoid (J i)
X✝ Y✝ : (i : I) → J i
f : X✝ ⟶ Y✝
i : I
⊢ ((fun {X Y} f i => Groupoid.inv (f i)) f ≫ f) i = 𝟙 Y✝ i
[PROOFSTEP]
apply Groupoid.inv_comp
[GOAL]
I : Type u
J : I → Type u₂
inst✝ : (i : I) → Groupoid (J i)
X✝ Y✝ : (i : I) → J i
f : X✝ ⟶ Y✝
⊢ f ≫ (fun {X Y} f i => Groupoid.inv (f i)) f = 𝟙 X✝
[PROOFSTEP]
funext i
[GOAL]
case h
I : Type u
J : I → Type u₂
inst✝ : (i : I) → Groupoid (J i)
X✝ Y✝ : (i : I) → J i
f : X✝ ⟶ Y✝
i : I
⊢ (f ≫ (fun {X Y} f i => Groupoid.inv (f i)) f) i = 𝟙 X✝ i
[PROOFSTEP]
apply Groupoid.comp_inv
