C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
a : Pseudoelement P
x : Over P
⊢ Over.mk (x.hom ≫ f ≫ g) ≈ Over.mk ((Over.mk (x.hom ≫ f)).hom ≫ g)
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
a : Pseudoelement P
x : Over P
⊢ (fun g_1 => app (f ≫ g) g_1) x ≈ (fun g_1 => app g g_1) ((fun g => app f g) x)
simp only [app]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
a : Pseudoelement P
x : Over P
⊢ Over.mk (x.hom ≫ f ≫ g) ≈ Over.mk ((Over.mk (x.hom ≫ f)).hom ≫ g)
rw [← Category.assoc, Over.coe_hom]