calc
min (card s + card Hs) (card t + card Ht) =
  min (Nat.card N * card (s.image (QuotientGroup.mk (s := N))) +
  Nat.card N * card (Hs.image (QuotientGroup.mk (s := N))))
  (Nat.card N * card (t.image (QuotientGroup.mk (s := N))) +
  Nat.card N * card (Ht.image (QuotientGroup.mk (s := N)))) := by
    rw [← subgroup_mul_card_eq_mul_of_mul_stab_subset N s,
    ← subgroup_mul_card_eq_mul_of_mul_stab_subset N t,
    ← subgroup_mul_card_eq_mul_of_mul_stab_subset N Hs,
    ← subgroup_mul_card_eq_mul_of_mul_stab_subset N Ht]
    all_goals { aesop }
_ = Nat.card N * min (card (s.image (QuotientGroup.mk (s := N))) +
  card (Hs.image (QuotientGroup.mk (s := N)))) (card (t.image (QuotientGroup.mk (s := N))) +
  card (Ht.image (QuotientGroup.mk (s := N)))) := by
    rw [← mul_add, ← mul_add, Nat.mul_min_mul_left]
_ = Nat.card N * min (card (image (QuotientGroup.mk (s := N)) s) +
  card (mulStab (image (QuotientGroup.mk (s := N)) s)))
  (card (image (QuotientGroup.mk (s := N)) t) +
  card (mulStab (image (QuotientGroup.mk (s := N)) t))) := by
    rw [mulStab_quotient_commute_subgroup N t, mulStab_quotient_commute_subgroup N s]
    all_goals simp [*]
_ ≤ Nat.card N * (card (image (QuotientGroup.mk (s := N)) s ∪
  image (QuotientGroup.mk (s := N)) t) +
  card (mulStab (image (QuotientGroup.mk (s := N)) s ∪
  image (QuotientGroup.mk (s := N)) t))) := Nat.mul_le_mul_left _ this
_ ≤ card (s ∪ t) + card (s ∪ t).mulStab := by
  rw [mul_add, ← image_union, subgroup_mul_card_eq_mul_of_mul_stab_subset N (s ∪ t),
      ← mulStab_quotient_commute_subgroup N (s ∪ t),
      subgroup_mul_card_eq_mul_of_mul_stab_subset N (s ∪ t).mulStab]
  all_goals
  { simp only [hNmulstab, mulStab_idem]; norm_cast; exact inter_mulStab_subset_mulStab_union }
case inr.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
hHs : Hs.Nonempty
hHt : Ht.Nonempty
hH : H.Nonempty
N : Subgroup α := stabilizer α s ⊓ stabilizer α t
hN : N = stabilizer α s ⊓ stabilizer α t
hNmulstab : ↑N = ↑(Hs ∩ Ht)
h1 : (image QuotientGroup.mk s).mulStab ∩ (image QuotientGroup.mk t).mulStab = 1
this :
  min ((image QuotientGroup.mk s).card + (image QuotientGroup.mk s).mulStab.card)
      ((image QuotientGroup.mk t).card + (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
⊢ min (s.card + Hs.card) (t.card + Ht.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
no goals