rw [smul_eq_iff_eq_inv_smul, ← smul_assoc, smul_eq_mul, mul_assoc, mul_comm c _, ← mul_assoc, ←
  mul_assoc, ← mul_assoc, mul_assoc _ a b, inv_mul_self (a * b), one_mul, ← smul_eq_mul,
  smul_assoc, smul_mulStab hc, smul_mulStab hd]
α : 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
hsubset : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
⊢ (a * b) • C.mulStab = (a * c * (b * d)) • C.mulStab
no goals