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

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ t.mulStab ⊆ (s * t).mulStab
Tactic:
rw [mul_comm]
State after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ t.mulStab ⊆ (t * s).mulStab

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ t.mulStab ⊆ (t * s).mulStab
Tactic:
exact subset_mulStab_mul_left hs
State after:
no goals