Theorem: Groupoid.Functor.map_inv (Complexes/Structures/Groupoid.lean)

State before:
R : Sort ?u.16958
S : Sort u_1
T : Sort u_4
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X Y : S
g : X ⟶ Y
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ⁻¹ = (Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g) ⁻¹
Tactic:
apply (Groupoid.left_cancel (Φ.map g) _ _).mp
State after:
R : Sort ?u.16958
S : Sort u_1
T : Sort u_4
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X Y : S
g : X ⟶ Y
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ≫ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ⁻¹ =
    Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ≫ (Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g) ⁻¹

State before:
R : Sort ?u.16958
S : Sort u_1
T : Sort u_4
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X Y : S
g : X ⟶ Y
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ≫ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ⁻¹ =
    Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ≫ (Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g) ⁻¹
Tactic:
rw [← Φ.map_comp]
State after:
R : Sort ?u.16958
S : Sort u_1
T : Sort u_4
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X Y : S
g : X ⟶ Y
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (g ≫ g ⁻¹ ) =
    Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ≫ (Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g) ⁻¹

State before:
R : Sort ?u.16958
S : Sort u_1
T : Sort u_4
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X Y : S
g : X ⟶ Y
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (g ≫ g ⁻¹ ) =
    Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ≫ (Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g) ⁻¹
Tactic:
simp
State after:
no goals