set H := Hs * Ht with hH
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs : Hs = s.mulStab
Ht : Finset α := t.mulStab
hHt : Ht = t.mulStab
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
Hs : Finset α := s.mulStab
hHs : Hs = s.mulStab
Ht : Finset α := t.mulStab
hHt : Ht = t.mulStab
H : Finset α := Hs * Ht
hH : H = Hs * Ht
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card