∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Div (f i)] (s : Set I) [inst_1 : (i : I) → Decidable (i ∈ s)]
  (f₁ f₂ g₁ g₂ : (i : I) → f i), s.piecewise (f₁ / f₂) (g₁ / g₂) = s.piecewise f₁ g₁ / s.piecewise f₂ g₂