obtain ⟨c, hc, hcx⟩ := mem_smul_finset.mp (mem_sdiff.mp hx).1
case a.refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
hxyd : y * d = x
⊢ x ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
case a.refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
x : α
hx : x ∈ a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)
hx' : x ∈ (s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
y : α
hyst : y ∈ s ∪ t
d : α
hd : d ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
hxyd : y * d = x
c : α
hc : c ∈ C.mulStab
hcx : a • c = x
⊢ x ∈ s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab