case h
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
t : MonoOver X
⊢ (map (f ≫ g)).obj (Quotient.mk'' t) = (map g).obj ((map f).obj (Quotient.mk'' t))
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
x : Subobject X
⊢ (map (f ≫ g)).obj x = (map g).obj ((map f).obj x)
induction' x using Quotient.inductionOn' with t
no goals
case h
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
t : MonoOver X
⊢ (map (f ≫ g)).obj (Quotient.mk'' t) = (map g).obj ((map f).obj (Quotient.mk'' t))
exact Quotient.sound ⟨(MonoOver.mapComp _ _).app t⟩