Theorem: Equiv.Perm.stabilizer_univ_eq_top (Jordan/PermMaximal.lean)

State before:
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
⊢ stabilizer G _root_.Set.univ = ⊤
Tactic:
rw [eq_top_iff]
State after:
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
⊢ ⊤ ≤ stabilizer G _root_.Set.univ

State before:
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
⊢ ⊤ ≤ stabilizer G _root_.Set.univ
Tactic:
intro g
State after:
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g ∈ ⊤ → g ∈ stabilizer G _root_.Set.univ

State before:
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g ∈ ⊤ → g ∈ stabilizer G _root_.Set.univ
Tactic:
apply imp_intro
State after:
case h
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g ∈ stabilizer G _root_.Set.univ

State before:
case h
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g ∈ stabilizer G _root_.Set.univ
Tactic:
rw [mem_stabilizer_iff]
State after:
case h
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g • _root_.Set.univ = _root_.Set.univ

State before:
case h
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g • _root_.Set.univ = _root_.Set.univ
Tactic:
simp only [Set.smul_set_univ]
State after:
no goals