case h
C : Type u₁
inst✝¹ : Category C
X✝ Y Z : C
D : Type u₂
inst✝ : Category D
X : C
p : Subobject X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)
P : Subobject X
⊢ ∀ (a : MonoOver X), p (Quotient.mk'' a)
C : Type u₁
inst✝¹ : Category C
X✝ Y Z : C
D : Type u₂
inst✝ : Category D
X : C
p : Subobject X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)
P : Subobject X
⊢ p P
apply Quotient.inductionOn'
case h
C : Type u₁
inst✝¹ : Category C
X✝ Y Z : C
D : Type u₂
inst✝ : Category D
X : C
p : Subobject X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)
P : Subobject X
a : MonoOver X
⊢ p (Quotient.mk'' a)
case h
C : Type u₁
inst✝¹ : Category C
X✝ Y Z : C
D : Type u₂
inst✝ : Category D
X : C
p : Subobject X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)
P : Subobject X
⊢ ∀ (a : MonoOver X), p (Quotient.mk'' a)
intro a
no goals
case h
C : Type u₁
inst✝¹ : Category C
X✝ Y Z : C
D : Type u₂
inst✝ : Category D
X : C
p : Subobject X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)
P : Subobject X
a : MonoOver X
⊢ p (Quotient.mk'' a)
exact h a.arrow