refine'
  ((subset_inter (mulStab_mul_ssubset_mulStab hs₁ ht₁ hab).subset Subset.rfl).trans
        inter_mulStab_subset_mulStab_union).antisymm'
    fun x hx => _
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
⊢ (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab = (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : ¬(a * b) • C.mulStab ⊆ s * t
hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))
hCne : C.Nonempty
x : α
hx : x ∈ (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab