∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} {G : Type u_4} [inst_1 : (i : ι) → VAdd G (R i)] [∀ (i : ι), VAddMemClass (S i) G (R i)] (g : G)
  (x : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕), ∀ᶠ (x_1 : ι) in 𝓕, g +ᵥ x x_1 ∈ ↑(B x_1)