-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma IsStableUnderCoproductsOfShape.mk (J : Type*) [W.RespectsIso]
    (hW : ∀ (X₁ X₂ : J → C) [HasCoproduct X₁] [HasCoproduct X₂]
      (f : ∀ j, X₁ j ⟶ X₂ j) (_ : ∀ (j : J), W (f j)),
      W (Limits.Sigma.map f)) : W.IsStableUnderCoproductsOfShape J

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Sigma.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }
this✝¹ : HasColimit X₁
this✝ : HasColimit X₂
this : HasCoproduct fun j => X₁.obj { as := j }
⊢ W (hc₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
have : HasCoproduct fun j ↦ X₂.obj (Discrete.mk j) :=
  hasColimitOfIso (Discrete.natIso (fun j ↦ Iso.refl (X₂.obj j)))

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Sigma.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }
this✝² : HasColimit X₁
this✝¹ : HasColimit X₂
this✝ : HasCoproduct fun j => X₁.obj { as := j }
this : HasCoproduct fun j => X₂.obj { as := j }
⊢ W (hc₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Sigma.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }
this✝² : HasColimit X₁
this✝¹ : HasColimit X₂
this✝ : HasCoproduct fun j => X₁.obj { as := j }
this : HasCoproduct fun j => X₂.obj { as := j }
hf' : W (Limits.Sigma.map φ)
⊢ (Sigma.isoColimit X₁ ≪≫ (colimit.isColimit X₁).coconePointUniqueUpToIso hc₁).hom ≫
      (Arrow.mk (hc₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })).hom =
    (Arrow.mk (Limits.Sigma.map φ)).hom ≫
      (Sigma.isoColimit X₂ ≪≫ (colimit.isColimit X₂).coconePointUniqueUpToIso hc₂).hom

Tactic:
apply colimit.hom_ext

Result:
case w
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Sigma.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }
this✝² : HasColimit X₁
this✝¹ : HasColimit X₂
this✝ : HasCoproduct fun j => X₁.obj { as := j }
this : HasCoproduct fun j => X₂.obj { as := j }
hf' : W (Limits.Sigma.map φ)
⊢ ∀ (j : Discrete J),
    colimit.ι (Discrete.functor fun j => X₁.obj { as := j }) j ≫
        (Sigma.isoColimit X₁ ≪≫ (colimit.isColimit X₁).coconePointUniqueUpToIso hc₁).hom ≫
          (Arrow.mk (hc₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })).hom =
      colimit.ι (Discrete.functor fun j => X₁.obj { as := j }) j ≫
        (Arrow.mk (Limits.Sigma.map φ)).hom ≫
          (Sigma.isoColimit X₂ ≪≫ (colimit.isColimit X₂).coconePointUniqueUpToIso hc₂).hom