Theorem: MulAction.mem_stabilizer_of_finite_iff_smul_le (Jordan/Mathlib/Stabilizer.lean)

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
⊢ g ∈ stabilizer G s ↔ g • s ⊆ s
Tactic:
haveI : Fintype s := Set.Finite.fintype hs
State after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this : Fintype ↑s
⊢ g ∈ stabilizer G s ↔ g • s ⊆ s

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this : Fintype ↑s
⊢ g ∈ stabilizer G s ↔ g • s ⊆ s
Tactic:
haveI : Fintype (g • s : Set α) := Fintype.ofFinite _
State after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g ∈ stabilizer G s ↔ g • s ⊆ s

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g ∈ stabilizer G s ↔ g • s ⊆ s
Tactic:
rw [mem_stabilizer_iff]
State after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g • s = s ↔ g • s ⊆ s

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g • s = s ↔ g • s ⊆ s
Tactic:
constructor
State after:
case mp
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g • s = s → g • s ⊆ s

case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g • s ⊆ s → g • s = s

State before:
case mp
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g • s = s → g • s ⊆ s

case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g • s ⊆ s → g • s = s
Tactic:
exact Eq.subset
State after:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g • s ⊆ s → g • s = s

State before:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g • s ⊆ s → g • s = s
Tactic:
rw [← Set.toFinset_inj, ← Set.toFinset_subset_toFinset]
State after:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ Set.toFinset (g • s) ⊆ Set.toFinset s → Set.toFinset (g • s) = Set.toFinset s

State before:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ Set.toFinset (g • s) ⊆ Set.toFinset s → Set.toFinset (g • s) = Set.toFinset s
Tactic:
intro h
State after:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ Set.toFinset (g • s) = Set.toFinset s

State before:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ Set.toFinset (g • s) = Set.toFinset s
Tactic:
apply Finset.eq_of_subset_of_card_le h
State after:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ (Set.toFinset s).card ≤ (Set.toFinset (g • s)).card

State before:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ (Set.toFinset s).card ≤ (Set.toFinset (g • s)).card
Tactic:
apply le_of_eq
State after:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ (Set.toFinset s).card = (Set.toFinset (g • s)).card

State before:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ (Set.toFinset s).card = (Set.toFinset (g • s)).card
Tactic:
suffices (g • s).toFinset = Finset.map ⟨_, MulAction.injective g⟩ hs.toFinset by
  rw [this, Finset.card_map, Set.toFinite_toFinset]
State after:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ Set.toFinset (g • s) = Finset.map { toFun := fun x => g • x, inj' := ⋯ } (Set.Finite.toFinset hs)

State before:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ Set.toFinset (g • s) = Finset.map { toFun := fun x => g • x, inj' := ⋯ } (Set.Finite.toFinset hs)
Tactic:
rw [← Finset.coe_inj]
State after:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ ↑(Set.toFinset (g • s)) = ↑(Finset.map { toFun := fun x => g • x, inj' := ⋯ } (Set.Finite.toFinset hs))

State before:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ ↑(Set.toFinset (g • s)) = ↑(Finset.map { toFun := fun x => g • x, inj' := ⋯ } (Set.Finite.toFinset hs))
Tactic:
simp only [Set.coe_toFinset, Set.toFinite_toFinset, Finset.coe_map, Function.Embedding.coeFn_mk, Set.image_smul]
State after:
no goals

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝¹ : Fintype ↑s
this✝ : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
this : Set.toFinset (g • s) = Finset.map { toFun := fun x => g • x, inj' := ⋯ } (Set.Finite.toFinset hs)
⊢ (Set.toFinset s).card = (Set.toFinset (g • s)).card
Tactic:
rw [this, Finset.card_map, Set.toFinite_toFinset]
State after:
no goals