∀ {ι : Type u_5} {α : ι → Type u_6} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → Div (α i)] (s t : (i : ι) → Finset (α i)),
  (Fintype.piFinset fun i => s i / t i) = Fintype.piFinset s / Fintype.piFinset t