Theorem: Finset.mul_subset_right_iff (LeanCamCombi/Kneser/MulStab.lean)

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ht : t.Nonempty
⊢ s * t ⊆ t ↔ s ⊆ t.mulStab
Tactic:
simp_rw [← smul_eq_mul, ← biUnion_smul_finset, biUnion_subset,
  ← mem_mulStab_iff_smul_finset_subset ht, subset_iff]
State after:
no goals