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

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s.mulStab.card = 1 ↔ s.mulStab = 1
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [h, card_one]⟩
State after:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
h : s.mulStab.card = 1
⊢ s.mulStab = 1

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
h : s.mulStab.card = 1
⊢ s.mulStab = 1
Tactic:
obtain ⟨a, ha⟩ := card_eq_one.1 h
State after:
case intro
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
h : s.mulStab.card = 1
a : α
ha : s.mulStab = {a}
⊢ s.mulStab = 1

State before:
case intro
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
h : s.mulStab.card = 1
a : α
ha : s.mulStab = {a}
⊢ s.mulStab = 1
Tactic:
rw [ha]
State after:
case intro
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
h : s.mulStab.card = 1
a : α
ha : s.mulStab = {a}
⊢ {a} = 1

State before:
case intro
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
h : s.mulStab.card = 1
a : α
ha : s.mulStab = {a}
⊢ {a} = 1
Tactic:
rw [eq_singleton_iff_nonempty_unique_mem, mulStab_nonempty, ← one_mem_mulStab] at ha
State after:
case intro
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
h : s.mulStab.card = 1
a : α
ha : 1 ∈ s.mulStab ∧ ∀ x ∈ s.mulStab, x = a
⊢ {a} = 1

State before:
case intro
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
h : s.mulStab.card = 1
a : α
ha : 1 ∈ s.mulStab ∧ ∀ x ∈ s.mulStab, x = a
⊢ {a} = 1
Tactic:
rw [← ha.2 _ ha.1, singleton_one]
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
h : s.mulStab = 1
⊢ s.mulStab.card = 1
Tactic:
rw [h, card_one]
State after:
no goals