have := ih _ ?_ (s.image (↑) : Finset (α ⧸ stabilizer α (s * t))) (t.image (↑)) rfl
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
case h.inr.inr.inl.refine_2
α : 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
this :
  (image QuotientGroup.mk s * (image QuotientGroup.mk s * image QuotientGroup.mk t).mulStab).card +
      (image QuotientGroup.mk t * (image QuotientGroup.mk s * image QuotientGroup.mk t).mulStab).card ≤
    (image QuotientGroup.mk s * image QuotientGroup.mk t).card +
      (image QuotientGroup.mk s * image QuotientGroup.mk t).mulStab.card
⊢ (image QuotientGroup.mk s).card + (image QuotientGroup.mk t).card - 1 ≤ (image QuotientGroup.mk (s * t)).card

case h.inr.inr.inl.refine_1
α : 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 * image QuotientGroup.mk t).card + (image QuotientGroup.mk s).card < (s * t).card + s.card