∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C)
  (t : CategoryTheory.Limits.FormalCoproduct C) (m : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt ⟶ t) (i : 𝒜)
  (a : (f i).I),
  ((CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv 𝒜 f t) m i).f a =
    m.f (((CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).inj i).f a)