Theorem: Groupoid.Functor.map_id' (Complexes/Structures/Groupoid.lean)

State before:
R : Sort ?u.16460
S : Sort u_3
T : Sort u_2
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X : S
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X) = 𝟙 (Quiver.PreFunctor.obj Φ.toFunctor.toPreFunctor X)
Tactic:
have := Φ.map_comp (𝟙 X) (𝟙 X)
State after:
R : Sort ?u.16460
S : Sort u_3
T : Sort u_2
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X : S
this :
  Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X ≫ 𝟙 X) =
    Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X) ≫ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X)
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X) = 𝟙 (Quiver.PreFunctor.obj Φ.toFunctor.toPreFunctor X)

State before:
R : Sort ?u.16460
S : Sort u_3
T : Sort u_2
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X : S
this :
  Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X ≫ 𝟙 X) =
    Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X) ≫ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X)
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X) = 𝟙 (Quiver.PreFunctor.obj Φ.toFunctor.toPreFunctor X)
Tactic:
rw [Category.comp_id, right_cancel_id] at this
State after:
R : Sort ?u.16460
S : Sort u_3
T : Sort u_2
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X : S
this : 𝟙 (Quiver.PreFunctor.obj Φ.toFunctor.toPreFunctor X) = Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X)
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X) = 𝟙 (Quiver.PreFunctor.obj Φ.toFunctor.toPreFunctor X)

State before:
R : Sort ?u.16460
S : Sort u_3
T : Sort u_2
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X : S
this : 𝟙 (Quiver.PreFunctor.obj Φ.toFunctor.toPreFunctor X) = Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X)
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X) = 𝟙 (Quiver.PreFunctor.obj Φ.toFunctor.toPreFunctor X)
Tactic:
exact this.symm
State after:
no goals