-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
lemma Cofan.isColimit_iff_isIso_sigmaDesc {f : β → C} [HasCoproduct f] (c : Cofan f) :
    IsIso (Sigma.desc c.inj) ↔ Nonempty (IsColimit c)

Proof state:
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
c : Cofan f
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
this : IsIso (((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom ≫ hc.desc c)
⊢ IsIso (Sigma.desc c.inj)

Tactic:
convert this

Result:
case h.e'_5.h
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
c : Cofan f
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
this : IsIso (((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom ≫ hc.desc c)
e_3✝ : ∐ f = (mk (∐ f) (Sigma.ι f)).pt
⊢ Sigma.desc c.inj = ((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom ≫ hc.desc c

Proof state:
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
c : Cofan f
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
⊢ IsIso (Sigma.desc c.inj)

Tactic:
have : IsIso (((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom ≫ hc.desc c) := by
  simp; infer_instance

Result:
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
c : Cofan f
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
this : IsIso (((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom ≫ hc.desc c)
⊢ IsIso (Sigma.desc c.inj)

Proof state:
case h.e'_5.h
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
c : Cofan f
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
this : IsIso (((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom ≫ hc.desc c)
e_3✝ : ∐ f = (mk (∐ f) (Sigma.ι f)).pt
⊢ Sigma.desc c.inj = ((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom ≫ hc.desc c

Tactic:
ext

Result:
case h.e'_5.h.h
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
c : Cofan f
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
this : IsIso (((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom ≫ hc.desc c)
e_3✝ : ∐ f = (mk (∐ f) (Sigma.ι f)).pt
b✝ : β
⊢ Sigma.ι f b✝ ≫ Sigma.desc c.inj =
    Sigma.ι f b✝ ≫ ((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom ≫ hc.desc c

Proof state:
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
c : Cofan f
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
⊢ IsIso (((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom ≫ hc.desc c)

Tactic:
simp

Result:
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
c : Cofan f
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
⊢ IsIso ((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom

Proof state:
case h.e'_5.h.h
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
c : Cofan f
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
this : IsIso (((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom ≫ hc.desc c)
e_3✝ : ∐ f = (mk (∐ f) (Sigma.ι f)).pt
b✝ : β
⊢ Sigma.ι f b✝ ≫ Sigma.desc c.inj =
    Sigma.ι f b✝ ≫ ((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom ≫ hc.desc c

Tactic:
simp only [colimit.ι_desc, mk_pt, mk_ι_app, IsColimit.coconePointUniqueUpToIso,
  coproductIsCoproduct, colimit.cocone_x, Functor.mapIso_hom, IsColimit.uniqueUpToIso_hom,
  Cocones.forget_map, IsColimit.descCoconeMorphism_hom, IsColimit.ofIsoColimit_desc,
  Cocones.ext_inv_hom, Iso.refl_inv, colimit.isColimit_desc, Category.id_comp,
  IsColimit.desc_self, Category.comp_id]

Result:
case h.e'_5.h.h
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
c : Cofan f
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
this : IsIso (((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom ≫ hc.desc c)
e_3✝ : ∐ f = (mk (∐ f) (Sigma.ι f)).pt
b✝ : β
⊢ c.inj b✝ = c.ι.app { as := b✝ }

Proof state:
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
c : Cofan f
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
⊢ IsIso ((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom

Tactic:
infer_instance

Result:
no goals

Proof state:
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
c : Cofan f
⊢ IsIso (Sigma.desc c.inj) ↔ Nonempty (IsColimit c)

Tactic:
refine ⟨fun h ↦ ⟨isColimitOfIsIsoSigmaDesc c⟩, fun ⟨hc⟩ ↦ ?_⟩

Result:
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
c : Cofan f
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
⊢ IsIso (Sigma.desc c.inj)

Proof state:
case h.e'_5.h.h
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
c : Cofan f
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
this : IsIso (((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom ≫ hc.desc c)
e_3✝ : ∐ f = (mk (∐ f) (Sigma.ι f)).pt
b✝ : β
⊢ c.inj b✝ = c.ι.app { as := b✝ }

Tactic:
rfl

Result:
no goals