case intro.intro
C : Type u_1
inst✝ : Category C
h : ∀ (A B : C), ∃ c x, Mono (BinaryCofan.inl c)
A B : C
c' : BinaryCofan A B
hc' : IsColimit c'
c : BinaryCofan A B
hc₁ : IsColimit c
hc₂ : Mono (BinaryCofan.inl c)
⊢ Mono (BinaryCofan.inl c')
C : Type u_1
inst✝ : Category C
h : ∀ (A B : C), ∃ c x, Mono (BinaryCofan.inl c)
A B : C
c' : BinaryCofan A B
hc' : IsColimit c'
⊢ Mono (BinaryCofan.inl c')
obtain ⟨c, hc₁, hc₂⟩ := h A B
no goals
case intro.intro
C : Type u_1
inst✝ : Category C
h : ∀ (A B : C), ∃ c x, Mono (BinaryCofan.inl c)
A B : C
c' : BinaryCofan A B
hc' : IsColimit c'
c : BinaryCofan A B
hc₁ : IsColimit c
hc₂ : Mono (BinaryCofan.inl c)
⊢ Mono (BinaryCofan.inl c')
simpa only [mono_inl_iff hc' hc₁] using hc₂