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

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
⊢ s.mulStab ⊆ s / {a}
Tactic:
refine fun b hb ↦ mem_div.2 ⟨_, ?_, _, mem_singleton_self _, mul_div_cancel_right _ _⟩
State after:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ s.mulStab
⊢ b * a ∈ s

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ s.mulStab
⊢ b * a ∈ s
Tactic:
rw [mem_mulStab ⟨a, ha⟩] at hb
State after:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b • s = s
⊢ b * a ∈ s

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b • s = s
⊢ b * a ∈ s
Tactic:
rw [← hb]
State after:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b • s = s
⊢ b * a ∈ b • s

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b • s = s
⊢ b * a ∈ b • s
Tactic:
exact smul_mem_smul_finset ha
State after:
no goals