C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category D
B : C
X Y Z : Subobject B
h₁ : X ≤ Y
h₂ : Y ≤ Z
⊢ underlying.map (LE.le.hom h₁ ≫ LE.le.hom h₂) = underlying.map (LE.le.hom (_ : X ≤ Z))
C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category D
B : C
X Y Z : Subobject B
h₁ : X ≤ Y
h₂ : Y ≤ Z
⊢ ofLE X Y h₁ ≫ ofLE Y Z h₂ = ofLE X Z (_ : X ≤ Z)
simp only [ofLE, ← Functor.map_comp underlying]
no goals
C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category D
B : C
X Y Z : Subobject B
h₁ : X ≤ Y
h₂ : Y ≤ Z
⊢ underlying.map (LE.le.hom h₁ ≫ LE.le.hom h₂) = underlying.map (LE.le.hom (_ : X ≤ Z))
congr 1