refine' (Finset.ssubset_iff_of_subset hsubset).mpr ⟨w, hw, _⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hab : ¬(a * c * (b * d)) • C.mulStab ⊆ s * t
hd : d ∈ C.mulStab
had : b • d = y
hsubset : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
this : (a * b) • C.mulStab = (a * c * (b * d)) • C.mulStab
hsub : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * c * (b * d)) • C.mulStab
hxy : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
z : α
hz : z ∈ (a * c * (b * d)) • C.mulStab
hzst : z ∉ s * t
w : α
hw : w ∈ C.mulStab
hwz : (a * c * (b * d)) • w = z
⊢ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hCne : C.Nonempty
x : α
hx : x ∈ s ∩ a • C.mulStab
y : α
hy : y ∈ t ∩ b • C.mulStab
c : α
hc : c ∈ C.mulStab
hac : a • c = x
d : α
hab : ¬(a * c * (b * d)) • C.mulStab ⊆ s * t
hd : d ∈ C.mulStab
had : b • d = y
hsubset : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
this : (a * b) • C.mulStab = (a * c * (b * d)) • C.mulStab
hsub : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * c * (b * d)) • C.mulStab
hxy : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
z : α
hz : z ∈ (a * c * (b * d)) • C.mulStab
hzst : z ∉ s * t
w : α
hw : w ∈ C.mulStab
hwz : (a * c * (b * d)) • w = z
⊢ w ∉ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab