-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
ι : Type u_1
f : ι → Type u_2
g : (i : ι) → f i → C
inst_1 : ∀ (i : ι), HasCoproduct.{u_2, v, u} (g i)
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (i : ι) ↦ sigmaObj.{u_2, v, u} (g i)
s : Cofan (C := C) fun (p : (i : ι) × f i) ↦ g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i))
fun :
  ∀ (m : (sigmaObj.{u_1, v, u} fun (i : ι) ↦ sigmaObj.{u_2, v, u} (g i)) ⟶ s.pt),
    (∀ (j : (i : ι) × f i),
        Cofan.inj (C := C) (f := fun (p : (i : ι) × f i) ↦
              g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i)))
              (Cofan.mk (sigmaObj.{u_1, v, u} fun (i : ι) ↦ sigmaObj.{u_2, v, u} (g i)) fun (X : (i : ι) × f i) ↦
                CategoryStruct.comp (Y :=
                  sigmaObj.{u_2, v, u} (β := f (X.fst (β := fun (i : ι) ↦ f i))) (g (X.fst (β := fun (i : ι) ↦ f i))))
                  (Sigma.ι (g (X.fst (β := fun (i : ι) ↦ f i))) (X.snd (β := fun (i : ι) ↦ f i)))
                  (Sigma.ι.{u_1, v, u} (C := C) (fun (i : ι) ↦ sigmaObj.{u_2, v, u} (g i))
                    (X.fst (β := fun (i : ι) ↦ f i))))
              j ≫
            m =
          s.inj j) →
      m =
        (fun
              (s :
                Cofan (C := C) fun (p : (i : ι) × f i) ↦
                  g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i))) ↦
            (Sigma.desc fun (b : ι) ↦ Sigma.desc fun (c : f b) ↦ s.inj (Sigma.mk (β := fun (i : ι) ↦ f i) b c) :
              (sigmaObj.{u_1, v, u} fun (b : ι) ↦
                  sigmaObj.{u_2, v, u} fun (c : f b) ↦
                    g ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).fst (β := fun (i : ι) ↦ f i))
                      ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).snd (β := fun (i : ι) ↦ f i))) ⟶
                s.pt))
          s
⊢ ∀
    (m :
      Cocone.pt (J := Discrete ((i : ι) × f i)) (F :=
          Discrete.functor fun (p : (i : ι) × f i) ↦
            g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i)))
          (Cofan.mk (sigmaObj.{u_1, v, u} fun (i : ι) ↦ sigmaObj.{u_2, v, u} (g i)) fun (X : (i : ι) × f i) ↦
            CategoryStruct.comp (Y :=
              sigmaObj.{u_2, v, u} (β := f (X.fst (β := fun (i : ι) ↦ f i))) (g (X.fst (β := fun (i : ι) ↦ f i))))
              (Sigma.ι (g (X.fst (β := fun (i : ι) ↦ f i))) (X.snd (β := fun (i : ι) ↦ f i)))
              (Sigma.ι.{u_1, v, u} (C := C) (fun (i : ι) ↦ sigmaObj.{u_2, v, u} (g i))
                (X.fst (β := fun (i : ι) ↦ f i)))) ⟶
        s.pt),
    (∀ (j : (i : ι) × f i),
        Cofan.inj (C := C) (f := fun (p : (i : ι) × f i) ↦
              g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i)))
              (Cofan.mk (sigmaObj.{u_1, v, u} fun (i : ι) ↦ sigmaObj.{u_2, v, u} (g i)) fun (X : (i : ι) × f i) ↦
                CategoryStruct.comp (Y :=
                  sigmaObj.{u_2, v, u} (β := f (X.fst (β := fun (i : ι) ↦ f i))) (g (X.fst (β := fun (i : ι) ↦ f i))))
                  (Sigma.ι (g (X.fst (β := fun (i : ι) ↦ f i))) (X.snd (β := fun (i : ι) ↦ f i)))
                  (Sigma.ι.{u_1, v, u} (C := C) (fun (i : ι) ↦ sigmaObj.{u_2, v, u} (g i))
                    (X.fst (β := fun (i : ι) ↦ f i))))
              j ≫
            m =
          s.inj j) →
      m =
        (fun
              (s :
                Cofan (C := C) fun (p : (i : ι) × f i) ↦
                  g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i))) ↦
            (Sigma.desc fun (b : ι) ↦ Sigma.desc fun (c : f b) ↦ s.inj (Sigma.mk (β := fun (i : ι) ↦ f i) b c) :
              (sigmaObj.{u_1, v, u} fun (b : ι) ↦
                  sigmaObj.{u_2, v, u} fun (c : f b) ↦
                    g ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).fst (β := fun (i : ι) ↦ f i))
                      ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).snd (β := fun (i : ι) ↦ f i))) ⟶
                s.pt))
          s

Tactic:
(m : (∐ fun i ↦ ∐ g i) ⟶ _)