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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
⊢ ∀ (x : α), x ∈ support c ↔ g x ∈ support c
Tactic:
intro x
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ x ∈ support c ↔ g x ∈ support c

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ x ∈ support c ↔ g x ∈ support c
Tactic:
simp only [Equiv.Perm.mem_support, not_iff_not, ← Equiv.Perm.mul_apply]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ c x = x ↔ (c * g) x = g x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ c x = x ↔ (c * g) x = g x
Tactic:
rw [← hgc, Equiv.Perm.mul_apply]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ c x = x ↔ g (c x) = g x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ c x = x ↔ g (c x) = g x
Tactic:
exact (Equiv.apply_eq_iff_eq g).symm
State after:
no goals