-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
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))
⊢ ∀
    (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
have 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
Tactic: (m : (∐ fun i ↦ ∐ g i) ⟶ _)