C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
Y : Subobject B
h₁ : X ≤ mk f
h₂ : mk f ≤ Y
⊢ underlying.map (LE.le.hom h₁ ≫ LE.le.hom h₂) = underlying.map (LE.le.hom (_ : X ≤ Y))
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
Y : Subobject B
h₁ : X ≤ mk f
h₂ : mk f ≤ Y
⊢ ofLEMk X f h₁ ≫ ofMkLE f Y h₂ = ofLE X Y (_ : X ≤ Y)
simp only [ofMkLE, ofLEMk, ofLE, ← Functor.map_comp underlying, assoc, Iso.hom_inv_id_assoc]
no goals
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
Y : Subobject B
h₁ : X ≤ mk f
h₂ : mk f ≤ Y
⊢ underlying.map (LE.le.hom h₁ ≫ LE.le.hom h₂) = underlying.map (LE.le.hom (_ : X ≤ Y))
congr 1