set H' := (s' * t').mulStab
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
ih : (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hnotconv : (C ∪ s' * t').card + (C ∪ s' * t').mulStab.card < (s ∩ t).card + ((s ∪ t) * (C ∪ s' * t').mulStab).card
hCun : (C ∪ s' * t').mulStab = (s' * t').mulStab
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
hconv : (s ∩ t).card + ((s ∪ t) * H).card ≤ C.card + H.card
hsub : (s' * t').mulStab ⊆ H
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * (s' * t').mulStab).card <
    ↑H.card - ↑(s' * (s' * t').mulStab).card - ↑(t' * (s' * t').mulStab).card
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hnotconv : (C ∪ s' * t').card + (C ∪ s' * t').mulStab.card < (s ∩ t).card + ((s ∪ t) * (C ∪ s' * t').mulStab).card
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
hconv : (s ∩ t).card + ((s ∪ t) * H).card ≤ C.card + H.card
H' : Finset α := (s' * t').mulStab
ih : (s' * H').card + (t' * H').card ≤ (s' * t').card + H'.card
hCun : (C ∪ s' * t').mulStab = H'
hsub : H' ⊆ H
⊢ ↑((s ∪ t) * H).card - ↑((s ∪ t) * H').card < ↑H.card - ↑(s' * H').card - ↑(t' * H').card