refine' fun h => hab (Eq.symm (eq_of_div_eq_one _))
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
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
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
⊢ b / a ∉ t.mulStab
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
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
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
h : b / a ∈ t.mulStab
⊢ b / a = 1