case h
C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category D
X Y Z : C
P✝ : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h✝ : Factors P✝ g
P : MonoOver Z
h : Factors (Quotient.mk'' P) g
⊢ Factors (Quotient.mk'' P) (f ≫ g)
C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category D
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : Factors P g
⊢ Factors P (f ≫ g)
induction' P using Quotient.ind' with P
case h.intro
C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category D
X Y Z : C
P✝ : Subobject Z
f : X ⟶ Y
P : MonoOver Z
g : Y ⟶ P.obj.left
h : Factors P✝ (g ≫ MonoOver.arrow P)
⊢ Factors (Quotient.mk'' P) (f ≫ g ≫ MonoOver.arrow P)
case h
C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category D
X Y Z : C
P✝ : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h✝ : Factors P✝ g
P : MonoOver Z
h : Factors (Quotient.mk'' P) g
⊢ Factors (Quotient.mk'' P) (f ≫ g)
obtain ⟨g, rfl⟩ := h
no goals
case h.intro
C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category D
X Y Z : C
P✝ : Subobject Z
f : X ⟶ Y
P : MonoOver Z
g : Y ⟶ P.obj.left
h : Factors P✝ (g ≫ MonoOver.arrow P)
⊢ Factors (Quotient.mk'' P) (f ≫ g ≫ MonoOver.arrow P)
exact ⟨f ≫ g, by simp⟩
no goals
C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category D
X Y Z : C
P✝ : Subobject Z
f : X ⟶ Y
P : MonoOver Z
g : Y ⟶ P.obj.left
h : Factors P✝ (g ≫ MonoOver.arrow P)
⊢ (f ≫ g) ≫ MonoOver.arrow P = f ≫ g ≫ MonoOver.arrow P
simp