refine' fun x hx => mem_sdiff.mpr ⟨_, _⟩
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab) ⊆
    ((s ∪ t) * C.mulStab) \ ((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
case a.refine'_1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
⊢ x ∈ (s ∪ t) * C.mulStab

case a.refine'_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)
⊢ x ∉ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab