no goals
C : Type u
inst✝ : Category C
X₁ Y₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ Y₃
f : X₁ ⟶ Y₁
⊢ ↑(homCongr (α₁ ≪≫ α₂) (β₁ ≪≫ β₂)) f = ↑((homCongr α₁ β₁).trans (homCongr α₂ β₂)) f
simp