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

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ a ∈ s.mulStab ↔ a • s = s
Tactic:
rw [mulStab, mem_filter, mem_div, and_iff_right_of_imp]
State after:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ a • s = s → ∃ b ∈ s, ∃ c ∈ s, b / c = a

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ a • s = s → ∃ b ∈ s, ∃ c ∈ s, b / c = a
Tactic:
obtain ⟨b, hb⟩ := hs
State after:
case intro
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a b : α
hb : b ∈ s
⊢ a • s = s → ∃ b ∈ s, ∃ c ∈ s, b / c = a

State before:
case intro
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a b : α
hb : b ∈ s
⊢ a • s = s → ∃ b ∈ s, ∃ c ∈ s, b / c = a
Tactic:
exact fun h ↦ ⟨_, by rw [← h]; exact smul_mem_smul_finset hb, _, hb, mul_div_cancel_right _ _⟩
State after:
no goals

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

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