have : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (x * y) • C.mulStab := by
  apply subset_trans (mul_subset_mul inter_subset_right inter_subset_right)
  rw [smul_mul_smul]
  rw [← hac, ← had, smul_mul_smul, smul_assoc]
  apply smul_finset_subset_smul_finset
  rw [← smul_smul]
  rw [mul_subset_iff]
  intro x hx y hy
  rw [smul_mulStab hd, smul_mulStab hc, mem_mulStab hCne, ← smul_smul,
    (mem_mulStab hCne).mp hy, (mem_mulStab hCne).mp hx]
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
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 : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) / {x * y} ⊆ C.mulStab
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hab : ¬(a * b) • C.mulStab ⊆ s * t
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 : α
hd : d ∈ C.mulStab
had : b • d = y
hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)
this : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (x * y) • C.mulStab
⊢ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) / {x * y} ⊆ C.mulStab