-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem BinaryCofan.isColimit_iff_isIso_inl {X Y : C} (h : IsInitial Y) (c : BinaryCofan X Y) :
    Nonempty (IsColimit c) ↔ IsIso c.inl

Proof state:
case mp.intro.mk.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
e : (c.inl ≫ l) ≫ c.inl = 𝟙 X ≫ c.inl
⊢ c.inl ≫ l ≫ c.inl = c.inl

Tactic:
rwa [Category.assoc,Category.id_comp] at e

Result:
no goals

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) → IsIso c.inl

Tactic:
rintro ⟨H⟩

Result:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
⊢ IsIso c.inl

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
a✝ : IsIso c.inl
⊢ Nonempty (IsColimit c)

Tactic:
exact
  ⟨BinaryCofan.IsColimit.mk _ (fun f _ => inv c.inl ≫ f)
      (fun _ _ => IsIso.hom_inv_id_assoc _ _) (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ =>
      (IsIso.eq_inv_comp _).mpr e⟩

Result:
no goals

Proof state:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
⊢ IsIso c.inl

Tactic:
obtain ⟨l, hl, -⟩ := BinaryCofan.IsColimit.desc' H (𝟙 X) (h.to X)

Result:
case mp.intro.mk.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
⊢ IsIso c.inl

Proof state:
case mp.intro.mk.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
⊢ IsIso c.inl

Tactic:
refine ⟨⟨l, hl, BinaryCofan.IsColimit.hom_ext H (?_) (h.hom_ext _ _)⟩⟩

Result:
case mp.intro.mk.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
⊢ c.inl ≫ l ≫ c.inl = c.inl ≫ 𝟙 (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔ IsIso c.inl

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) → IsIso c.inl

case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ IsIso c.inl → Nonempty (IsColimit c)

Proof state:
case mp.intro.mk.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
⊢ c.inl ≫ l ≫ c.inl = c.inl ≫ 𝟙 (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })

Tactic:
rw [Category.comp_id]

Result:
case mp.intro.mk.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
⊢ c.inl ≫ l ≫ c.inl = c.inl

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ IsIso c.inl → Nonempty (IsColimit c)

Tactic:
intro

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
a✝ : IsIso c.inl
⊢ Nonempty (IsColimit c)