-- 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 }
this : HasCoproduct fun j => X₂.obj { as := j }
hf' : W (Limits.Sigma.map φ)
⊢ W (hc₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
refine (W.arrow_mk_iso_iff ?_).1 hf'

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 }
hf' : W (Limits.Sigma.map φ)
⊢ Arrow.mk (Limits.Sigma.map φ) ≅ Arrow.mk (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 }
⊢ W (hc₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
have hf' := hW _ _ φ (fun j => hf (Discrete.mk 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 }
hf' : W (Limits.Sigma.map φ)
⊢ 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₁
⊢ W (hc₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
have : HasColimit X₂ := ⟨c₂, hc₂⟩

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₂
⊢ W (hc₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Proof state:
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

Tactic:
rintro ⟨j⟩

Result:
case w.mk
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 : J
⊢ colimit.ι (Discrete.functor fun j => X₁.obj { as := j }) { as := 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 }) { as := j } ≫
      (Arrow.mk (Limits.Sigma.map φ)).hom ≫
        (Sigma.isoColimit X₂ ≪≫ (colimit.isColimit X₂).coconePointUniqueUpToIso hc₂).hom

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
⊢ W (hc₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
let φ := fun j => f.app (Discrete.mk 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 }
⊢ W (hc₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })