[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.549, u_1} C
inst✝ : HasZeroMorphisms C
A B : C
c : BinaryCofan A B
hc : IsColimit c
⊢ Mono (BinaryCofan.inl c)
[PROOFSTEP]
haveI : IsSplitMono c.inl := IsSplitMono.mk' (SplitMono.mk (hc.desc (BinaryCofan.mk (𝟙 A) 0)) (IsColimit.fac _ _ _))
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.549, u_1} C
inst✝ : HasZeroMorphisms C
A B : C
c : BinaryCofan A B
hc : IsColimit c
this : IsSplitMono (BinaryCofan.inl c)
⊢ Mono (BinaryCofan.inl c)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
⊢ Mono (BinaryCofan.inr c)
[PROOFSTEP]
haveI hc' : IsColimit (BinaryCofan.mk c.inr c.inl) :=
  BinaryCofan.IsColimit.mk _ (fun f₁ f₂ => hc.desc (BinaryCofan.mk f₂ f₁)) (by aesop_cat) (by aesop_cat)
    (fun f₁ f₂ m h₁ h₂ => BinaryCofan.IsColimit.hom_ext hc (by aesop_cat) (by aesop_cat))
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
⊢ ∀ {T : C} (f : (pair A B).obj { as := WalkingPair.right } ⟶ T) (g : (pair A B).obj { as := WalkingPair.left } ⟶ T),
    BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c)) ≫
        (fun {T} f₁ f₂ => IsColimit.desc hc (BinaryCofan.mk f₂ f₁)) f g =
      f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
⊢ ∀ {T : C} (f : (pair A B).obj { as := WalkingPair.right } ⟶ T) (g : (pair A B).obj { as := WalkingPair.left } ⟶ T),
    BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c)) ≫
        (fun {T} f₁ f₂ => IsColimit.desc hc (BinaryCofan.mk f₂ f₁)) f g =
      g
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
T✝ : C
f₁ : (pair A B).obj { as := WalkingPair.right } ⟶ T✝
f₂ : (pair A B).obj { as := WalkingPair.left } ⟶ T✝
m : (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c)).pt ⟶ T✝
h₁ : BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c)) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c)) ≫ m = f₂
⊢ BinaryCofan.inl c ≫ m = BinaryCofan.inl c ≫ (fun {T} f₁ f₂ => IsColimit.desc hc (BinaryCofan.mk f₂ f₁)) f₁ f₂
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
T✝ : C
f₁ : (pair A B).obj { as := WalkingPair.right } ⟶ T✝
f₂ : (pair A B).obj { as := WalkingPair.left } ⟶ T✝
m : (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c)).pt ⟶ T✝
h₁ : BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c)) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c)) ≫ m = f₂
⊢ BinaryCofan.inr c ≫ m = BinaryCofan.inr c ≫ (fun {T} f₁ f₂ => IsColimit.desc hc (BinaryCofan.mk f₂ f₁)) f₁ f₂
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
hc' : IsColimit (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c))
⊢ Mono (BinaryCofan.inr c)
[PROOFSTEP]
exact binaryCofan_inl _ hc'
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B : C
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Mono (BinaryCofan.inl c₁) ↔ Mono (BinaryCofan.inl c₂)
[PROOFSTEP]
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₂⟩
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} 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₂)
[PROOFSTEP]
exact ⟨fun h₁ => this _ _ hc₁ hc₂ h₁, fun h₂ => this _ _ hc₂ hc₁ h₂⟩
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} 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₂)
[PROOFSTEP]
intro c₁ c₂ hc₁ hc₂
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} 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₂)
[PROOFSTEP]
intro
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} 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₂)
[PROOFSTEP]
simpa only [IsColimit.comp_coconePointUniqueUpToIso_hom] using mono_comp c₁.inl (hc₁.coconePointUniqueUpToIso hc₂).hom
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} 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')
[PROOFSTEP]
obtain ⟨c, hc₁, hc₂⟩ := h A B
[GOAL]
case intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} 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')
[PROOFSTEP]
simpa only [mono_inl_iff hc' hc₁] using hc₂
[GOAL]
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B : Type u
⊢ ∃ c x, Mono (BinaryCofan.inl c)
[PROOFSTEP]
refine' ⟨BinaryCofan.mk (Sum.inl : A ⟶ Sum A B) Sum.inr, _, _⟩
[GOAL]
case refine'_1
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B : Type u
⊢ IsColimit (BinaryCofan.mk Sum.inl Sum.inr)
[PROOFSTEP]
exact
  BinaryCofan.IsColimit.mk _
    (fun f₁ f₂ x => by
      rcases x with x | x
      exacts [f₁ x, f₂ x])
    (fun f₁ f₂ => by rfl) (fun f₁ f₂ => by rfl)
    (fun f₁ f₂ m h₁ h₂ => by
      funext x
      rcases x with x | x
      · exact congr_fun h₁ x
      · exact congr_fun h₂ x)
[GOAL]
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
x : (BinaryCofan.mk Sum.inl Sum.inr).pt
⊢ T✝
[PROOFSTEP]
rcases x with x | x
[GOAL]
case inl
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
x : A
⊢ T✝
case inr C : Type u_1 inst✝ : Category.{?u.12890, u_1} C A B T✝ : Type u f₁ : A ⟶ T✝ f₂ : B ⟶ T✝ x : B ⊢ T✝
[PROOFSTEP]
exacts [f₁ x, f₂ x]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
⊢ BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr) ≫
      (fun {T} f₁ f₂ x => Sum.casesOn x (fun x => f₁ x) fun x => f₂ x) f₁ f₂ =
    f₁
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
⊢ BinaryCofan.inr (BinaryCofan.mk Sum.inl Sum.inr) ≫
      (fun {T} f₁ f₂ x => Sum.casesOn x (fun x => f₁ x) fun x => f₂ x) f₁ f₂ =
    f₂
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
m : (BinaryCofan.mk Sum.inl Sum.inr).pt ⟶ T✝
h₁ : BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk Sum.inl Sum.inr) ≫ m = f₂
⊢ m = (fun {T} f₁ f₂ x => Sum.casesOn x (fun x => f₁ x) fun x => f₂ x) f₁ f₂
[PROOFSTEP]
funext x
[GOAL]
case h
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
m : (BinaryCofan.mk Sum.inl Sum.inr).pt ⟶ T✝
h₁ : BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk Sum.inl Sum.inr) ≫ m = f₂
x : (BinaryCofan.mk Sum.inl Sum.inr).pt
⊢ m x = (fun {T} f₁ f₂ x => Sum.casesOn x (fun x => f₁ x) fun x => f₂ x) f₁ f₂ x
[PROOFSTEP]
rcases x with x | x
[GOAL]
case h.inl
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
m : (BinaryCofan.mk Sum.inl Sum.inr).pt ⟶ T✝
h₁ : BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk Sum.inl Sum.inr) ≫ m = f₂
x : A
⊢ m (Sum.inl x) = (fun {T} f₁ f₂ x => Sum.casesOn x (fun x => f₁ x) fun x => f₂ x) f₁ f₂ (Sum.inl x)
[PROOFSTEP]
exact congr_fun h₁ x
[GOAL]
case h.inr
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
m : (BinaryCofan.mk Sum.inl Sum.inr).pt ⟶ T✝
h₁ : BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk Sum.inl Sum.inr) ≫ m = f₂
x : B
⊢ m (Sum.inr x) = (fun {T} f₁ f₂ x => Sum.casesOn x (fun x => f₁ x) fun x => f₂ x) f₁ f₂ (Sum.inr x)
[PROOFSTEP]
exact congr_fun h₂ x
[GOAL]
case refine'_2
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B : Type u
⊢ Mono (BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr))
[PROOFSTEP]
rw [mono_iff_injective]
[GOAL]
case refine'_2
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B : Type u
⊢ Function.Injective (BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr))
[PROOFSTEP]
intro a₁ a₂ h
[GOAL]
case refine'_2
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B : Type u
a₁ a₂ : (pair A B).obj { as := WalkingPair.left }
h : BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr) a₁ = BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr) a₂
⊢ a₁ = a₂
[PROOFSTEP]
simpa using h
