obtain rfl | hCne := C.eq_empty_or_nonempty
α : 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))
⊢ (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab = (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' : Finset α
a b : α
hs₁ : (s ∩ a • ∅.mulStab).Nonempty
ht₁ : (t ∩ b • ∅.mulStab).Nonempty
hab : ¬(a * b) • ∅.mulStab ⊆ s * t
hC : Disjoint ∅ (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab))
⊢ (∅ ∪ s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab = (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab

case inr
α : 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
⊢ (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab = (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab