∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C}
  (i : 𝒜),
  (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).inj i =
    { f := fun x => ⟨i, x⟩, φ := fun x => CategoryTheory.CategoryStruct.id ((f i).obj x) }