simp only [mul_smul_comm, smul_mul_assoc, mulStab_smul, card_smul_finset] at *
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
t : Finset α
ht : t.Nonempty
hstab : (s * (a / c)⁻¹ • t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * (a / c)⁻¹ • t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
hc : a ∈ t
hbac : b ∉ t
⊢ s.card + ((a / c)⁻¹ • t).card ≤ (s * (a / c)⁻¹ • t).card + 1
case h.inr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
t : Finset α
ht : t.Nonempty
hc : a ∈ t
hbac : b ∉ t
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
⊢ s.card + t.card ≤ (s * t).card + 1