rw [mem_mulStab_iff_subset_smul_finset (hs₁.mul ht₁)]
α : 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 : C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
hxC : x ∈ C.mulStab
⊢ x ∈ (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
α : 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 : C ∪ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)) = C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
hxC : x ∈ C.mulStab
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ x • (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))