Theorem: MulAction.smul_compl_set_eq (Jordan/PermIwasawa.lean)

State before:
α✝ : Type ?u.17129
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
⊢ (g • s)ᶜ = g • sᶜ
Tactic:
ext k
State after:
case h
α✝ : Type ?u.17129
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
k : α
⊢ k ∈ (g • s)ᶜ ↔ k ∈ g • sᶜ

State before:
case h
α✝ : Type ?u.17129
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
k : α
⊢ k ∈ (g • s)ᶜ ↔ k ∈ g • sᶜ
Tactic:
simp only [Set.mem_compl_iff, smul_compl_set]
State after:
no goals