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

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

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

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b • s = s
⊢ a / b ∈ s
Tactic:
rwa [← hb, ← inv_smul_mem_iff, smul_eq_mul, inv_mul_eq_div] at ha
State after:
no goals