rw [card_sdiff, Int.ofNat_sub (card_le_card _), card_smul_finset]
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card -
      ↑(t ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card ≤
    ↑(a • C.mulStab \
          ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)).card
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card -
      ↑(t ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card ≤
    ↑C.mulStab.card -
      ↑((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card

α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ a • C.mulStab

α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ s' t✝ t' C✝ : Finset α
a✝ b a : α
s t C : Finset α
has : a ∈ s
hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab
hC : C.Nonempty
⊢ (s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ a • C.mulStab