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

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s.mulStab ∩ t.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 : α
⊢ ∅.mulStab ∩ t.mulStab ⊆ (∅ ∪ t).mulStab

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

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

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

State before:
case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
ht : t.Nonempty
⊢ s.mulStab ∩ t.mulStab ⊆ (s ∪ t).mulStab
Tactic:
intro x hx
State after:
case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
ht : t.Nonempty
x : α
hx : x ∈ s.mulStab ∩ t.mulStab
⊢ x ∈ (s ∪ t).mulStab

State before:
case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
ht : t.Nonempty
x : α
hx : x ∈ s.mulStab ∩ t.mulStab
⊢ x ∈ (s ∪ t).mulStab
Tactic:
rw [mem_mulStab (hs.mono subset_union_left), smul_finset_union,
  (mem_mulStab hs).mp (mem_of_mem_inter_left hx),
  (mem_mulStab ht).mp (mem_of_mem_inter_right hx)]
State after:
no goals

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

State before:
case inr.inl
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s : Finset α
a : α
hs : s.Nonempty
⊢ s.mulStab ∩ ∅.mulStab ⊆ (s ∪ ∅).mulStab
Tactic:
simp
State after:
no goals