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

State before:
α : Type u_1
β : Type u_2
γ : Type ?u.76228
δ : Type ?u.76231
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F G : α ⥤ β
η : NatTrans F G
⊢ comp (id G) η = η
Tactic:
ext
State after:
case app.h
α : Type u_1
β : Type u_2
γ : Type ?u.76228
δ : Type ?u.76231
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F G : α ⥤ β
η : NatTrans F G
x✝ : α
⊢ app (comp (id G) η) x✝ = app η x✝

State before:
case app.h
α : Type u_1
β : Type u_2
γ : Type ?u.76228
δ : Type ?u.76231
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F G : α ⥤ β
η : NatTrans F G
x✝ : α
⊢ app (comp (id G) η) x✝ = app η x✝
Tactic:
simp
State after:
no goals