Theorem: Equiv.Perm.conj_support_eq (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ a ∈ support (k • g) ↔ (ConjAct.ofConjAct k⁻¹) a ∈ support g
Tactic:
simp only [Equiv.Perm.mem_support, ConjAct.smul_def]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ (ConjAct.ofConjAct k * g * (ConjAct.ofConjAct k)⁻¹) a ≠ a ↔ g ((ConjAct.ofConjAct k⁻¹) a) ≠ (ConjAct.ofConjAct k⁻¹) a

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ (ConjAct.ofConjAct k * g * (ConjAct.ofConjAct k)⁻¹) a ≠ a ↔ g ((ConjAct.ofConjAct k⁻¹) a) ≠ (ConjAct.ofConjAct k⁻¹) a
Tactic:
rw [not_iff_not]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ (ConjAct.ofConjAct k * g * (ConjAct.ofConjAct k)⁻¹) a = a ↔ g ((ConjAct.ofConjAct k⁻¹) a) = (ConjAct.ofConjAct k⁻¹) a

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ (ConjAct.ofConjAct k * g * (ConjAct.ofConjAct k)⁻¹) a = a ↔ g ((ConjAct.ofConjAct k⁻¹) a) = (ConjAct.ofConjAct k⁻¹) a
Tactic:
simp only [Equiv.Perm.coe_mul, Function.comp_apply, ConjAct.ofConjAct_inv]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ (ConjAct.ofConjAct k) (g ((ConjAct.ofConjAct k)⁻¹ a)) = a ↔ g ((ConjAct.ofConjAct k)⁻¹ a) = (ConjAct.ofConjAct k)⁻¹ a

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ (ConjAct.ofConjAct k) (g ((ConjAct.ofConjAct k)⁻¹ a)) = a ↔ g ((ConjAct.ofConjAct k)⁻¹ a) = (ConjAct.ofConjAct k)⁻¹ a
Tactic:
apply Equiv.apply_eq_iff_eq_symm_apply
State after:
no goals