{ι : Type u_1} →
  {α : Type u_2} →
    {π : ι → Type u_4} →
      [inst : AddCommMonoid α] →
        [inst_1 : PartialOrder α] →
          [inst_2 : (i : ι) → AddCommMonoid (π i)] →
            [inst_3 : (i : ι) → PartialOrder (π i)] →
              [inst_4 : (i : ι) → SMulZeroClass α (π i)] → [(i : ι) → CeilDiv α (π i)] → CeilDiv α ((i : ι) → π i)