suffices hineq :
  (s * t).mulStab.card *
      ((s.image (↑) : Finset (α ⧸ stabilizer α (s * t))).card +
          (t.image (↑) : Finset (α ⧸ stabilizer α (s * t))).card -
        1) ≤
    (s * t).card by
rw [mul_tsub, mul_one, mul_add, tsub_le_iff_left, card_mulStab_mul_card_image_coe',
    card_mulStab_mul_card_image_coe'] at hineq
  convert hineq using 1
  exact add_comm _ _
case h.inr.inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ih :
  ∀ m < (s * t).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
hs : s.Nonempty
ht : t.Nonempty
hstab : (s * t).mulStab ≠ 1
image_coe_mul : image QuotientGroup.mk (s * t) = image QuotientGroup.mk s * image QuotientGroup.mk t
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
case h.inr.inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ih :
  ∀ m < (s * t).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
hs : s.Nonempty
ht : t.Nonempty
hstab : (s * t).mulStab ≠ 1
image_coe_mul : image QuotientGroup.mk (s * t) = image QuotientGroup.mk s * image QuotientGroup.mk t
⊢ (s * t).mulStab.card * ((image QuotientGroup.mk s).card + (image QuotientGroup.mk t).card - 1) ≤ (s * t).card