rw [card_sdiff
    (subset_trans (mul_subset_mul_left hst)
      (subset_trans (mul_subset_mul_right inter_subset_right) _)),
  card_smul_finset, Int.ofNat_sub]
α : 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 =
    ↑(a • C.mulStab \ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)).card
α : 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
⊢ (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card ≤ C.mulStab.card

α : 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
⊢ a • C.mulStab * C.mulStab ⊆ a • C.mulStab