C : Type u_2
inst✝ : Category C
A B : C
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ ∀ (c₁ c₂ : BinaryCofan A B), IsColimit c₁ → IsColimit c₂ → Mono (BinaryCofan.inl c₁) → Mono (BinaryCofan.inl c₂)
C : Type u_2
inst✝ : Category C
A B : C
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Mono (BinaryCofan.inl c₁) ↔ Mono (BinaryCofan.inl c₂)
suffices
  ∀ (c₁ c₂ : BinaryCofan A B) (_ : IsColimit c₁) (_ : IsColimit c₂) (_ : Mono c₁.inl),
    Mono c₂.inl
  by exact ⟨fun h₁ => this _ _ hc₁ hc₂ h₁, fun h₂ => this _ _ hc₂ hc₁ h₂⟩
C : Type u_2
inst✝ : Category C
A B : C
c₁✝ c₂✝ : BinaryCofan A B
hc₁✝ : IsColimit c₁✝
hc₂✝ : IsColimit c₂✝
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Mono (BinaryCofan.inl c₁) → Mono (BinaryCofan.inl c₂)
C : Type u_2
inst✝ : Category C
A B : C
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ ∀ (c₁ c₂ : BinaryCofan A B), IsColimit c₁ → IsColimit c₂ → Mono (BinaryCofan.inl c₁) → Mono (BinaryCofan.inl c₂)
intro c₁ c₂ hc₁ hc₂
C : Type u_2
inst✝ : Category C
A B : C
c₁✝ c₂✝ : BinaryCofan A B
hc₁✝ : IsColimit c₁✝
hc₂✝ : IsColimit c₂✝
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
x✝ : Mono (BinaryCofan.inl c₁)
⊢ Mono (BinaryCofan.inl c₂)
C : Type u_2
inst✝ : Category C
A B : C
c₁✝ c₂✝ : BinaryCofan A B
hc₁✝ : IsColimit c₁✝
hc₂✝ : IsColimit c₂✝
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Mono (BinaryCofan.inl c₁) → Mono (BinaryCofan.inl c₂)
intro
no goals
C : Type u_2
inst✝ : Category C
A B : C
c₁✝ c₂✝ : BinaryCofan A B
hc₁✝ : IsColimit c₁✝
hc₂✝ : IsColimit c₂✝
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
x✝ : Mono (BinaryCofan.inl c₁)
⊢ Mono (BinaryCofan.inl c₂)
simpa only [IsColimit.comp_coconePointUniqueUpToIso_hom] using
  mono_comp c₁.inl (hc₁.coconePointUniqueUpToIso hc₂).hom
no goals
C : Type u_2
inst✝ : Category C
A B : C
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
this : ∀ (c₁ c₂ : BinaryCofan A B), IsColimit c₁ → IsColimit c₂ → Mono (BinaryCofan.inl c₁) → Mono (BinaryCofan.inl c₂)
⊢ Mono (BinaryCofan.inl c₁) ↔ Mono (BinaryCofan.inl c₂)
exact ⟨fun h₁ => this _ _ hc₁ hc₂ h₁, fun h₂ => this _ _ hc₂ hc₁ h₂⟩