no goals
α : Type u_1
β : Type ?u.337374
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set α
⊢ (∀ (i : Set α),
      i ∈ 𝓝 1 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ {x | x.snd⁻¹ * x.fst ∈ id i}}) ↔
    ∀ (U : Set α), U ∈ 𝓝 1 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), y • U
simp [← preimage_smul_inv, preimage]