C : Type u₁
inst✝³ : Category C
X✝ Y Z : C
D : Type u₂
inst✝² : Category D
B A₁ A₂ : C
X : Subobject B
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
h₁ : X ≤ mk f
h₂ : mk f ≤ mk g
⊢ underlying.map (LE.le.hom h₁ ≫ LE.le.hom h₂) ≫ (underlyingIso g).hom =
    underlying.map (LE.le.hom (_ : X ≤ mk g)) ≫ (underlyingIso g).hom
C : Type u₁
inst✝³ : Category C
X✝ Y Z : C
D : Type u₂
inst✝² : Category D
B A₁ A₂ : C
X : Subobject B
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
h₁ : X ≤ mk f
h₂ : mk f ≤ mk g
⊢ ofLEMk X f h₁ ≫ ofMkLEMk f g h₂ = ofLEMk X g (_ : X ≤ mk g)
simp only [ofMkLE, ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp_assoc 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₁ A₂ : C
X : Subobject B
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
h₁ : X ≤ mk f
h₂ : mk f ≤ mk g
⊢ underlying.map (LE.le.hom h₁ ≫ LE.le.hom h₂) ≫ (underlyingIso g).hom =
    underlying.map (LE.le.hom (_ : X ≤ mk g)) ≫ (underlyingIso g).hom
congr 1