case mk.mk.mk
C : Type u_1
inst✝ : Category C
r : HomRel C
P : {a b : Quotient r} → (a ⟶ b) → Prop
h : ∀ {x y : C} (f : x ⟶ y), P ((functor r).map f)
x y : C
f✝ : { as := x } ⟶ { as := y }
f : { as := x }.as ⟶ { as := y }.as
⊢ P (Quot.mk (CompClosure r) f)
C : Type u_1
inst✝ : Category C
r : HomRel C
P : {a b : Quotient r} → (a ⟶ b) → Prop
h : ∀ {x y : C} (f : x ⟶ y), P ((functor r).map f)
⊢ ∀ {a b : Quotient r} (f : a ⟶ b), P f
rintro ⟨x⟩ ⟨y⟩ ⟨f⟩
no goals
case mk.mk.mk
C : Type u_1
inst✝ : Category C
r : HomRel C
P : {a b : Quotient r} → (a ⟶ b) → Prop
h : ∀ {x y : C} (f : x ⟶ y), P ((functor r).map f)
x y : C
f✝ : { as := x } ⟶ { as := y }
f : { as := x }.as ⟶ { as := y }.as
⊢ P (Quot.mk (CompClosure r) f)
exact h f