Theorem: Category.Functor.id_comp (CategoryTheory/Basic.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type ?u.59997
δ : Type ?u.60000
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
⊢ 𝟭 β ◌ F = F
Tactic:
aesop
State after:
no goals