∀ {G : Type u_1} [inst : CommGroup G] (sets : Set (Set G)) (nonempty : sets.Nonempty)
  (inter_sets : ∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y) (one : ∀ U ∈ sets, 1 ∈ U)
  (mul : ∀ U ∈ sets, ∃ V ∈ sets, V * V ⊆ U) (inv : ∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (fun x => x⁻¹) ⁻¹' U),
  groupFilterBasisOfComm sets nonempty inter_sets one mul inv =
    { sets := sets, nonempty := nonempty, inter_sets := ⋯, one' := ⋯, mul' := ⋯, inv' := ⋯, conj' := ⋯ }