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

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

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

State before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ht : t.Nonempty
hs : s.Nonempty
⊢ s.mulStab ⊆ (s * t).mulStab
Tactic:
simp_rw [subset_iff, mem_mulStab hs, mem_mulStab (hs.mul ht)]
State after:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ht : t.Nonempty
hs : s.Nonempty
⊢ ∀ ⦃x : α⦄, x • s = s → x • (s * t) = s * t

State before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ht : t.Nonempty
hs : s.Nonempty
⊢ ∀ ⦃x : α⦄, x • s = s → x • (s * t) = s * t
Tactic:
rintro a h
State after:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
ht : t.Nonempty
hs : s.Nonempty
a : α
h : a • s = s
⊢ a • (s * t) = s * t

State before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
ht : t.Nonempty
hs : s.Nonempty
a : α
h : a • s = s
⊢ a • (s * t) = s * t
Tactic:
rw [← smul_mul_assoc, h]
State after:
no goals

State before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
t : Finset α
a : α
ht : t.Nonempty
⊢ ∅.mulStab ⊆ (∅ * t).mulStab
Tactic:
simp
State after:
no goals