refine le_of_le_of_eq (mul_le_mul_left' ?_ _) (card_mul_card_eq_mulStab_card_mul_coe s t).symm
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
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
⊢ (image QuotientGroup.mk s).card + (image QuotientGroup.mk t).card - 1 ≤ (image QuotientGroup.mk (s * t)).card