obtain rfl | hC := C.eq_empty_or_nonempty
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
⊢ ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card ≤
    ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C : Finset α
a✝ b✝ a b : α
s t : Finset α
has : a ∈ s
hsC : Disjoint t (a • ∅.mulStab)
hst : (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab ⊆ ∅.mulStab
⊢ ↑∅.mulStab.card - ↑(s ∩ a • ∅.mulStab * (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab).card ≤
    ↑((s ∪ t) * ∅.mulStab).card - ↑((s ∪ t) * (s ∩ a • ∅.mulStab * (t ∩ b • ∅.mulStab)).mulStab).card

case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b✝ a b : α
s t C : Finset α
has : a ∈ s
hsC : Disjoint t (a • C.mulStab)
hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card ≤
    ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card