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

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
⊢ s.mulStab * s = s
Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
State after:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ∅.mulStab * ∅ = ∅

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ s.mulStab * s = s

State before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ∅.mulStab * ∅ = ∅
Tactic:
exact mul_empty _
State after:
no goals

State before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ s.mulStab * s = s
Tactic:
simp only [← coe_inj, hs, coe_mul, coe_mulStab, ← stabilizer_coe_finset, stabilizer_mul_self]
State after:
no goals