case h
α : Type u_1
p q : Perm α
x : α
⊢ x ∈ {x | ↑p⁻¹ x ≠ x} ↔ x ∈ {x | ↑p x ≠ x}
α : Type u_1
p q : Perm α
⊢ {x | ↑p⁻¹ x ≠ x} = {x | ↑p x ≠ x}
ext x
case h
α : Type u_1
p q : Perm α
x : α
⊢ ¬↑p⁻¹ x = x ↔ ¬↑p x = x
case h
α : Type u_1
p q : Perm α
x : α
⊢ x ∈ {x | ↑p⁻¹ x ≠ x} ↔ x ∈ {x | ↑p x ≠ x}
simp only [Set.mem_setOf_eq, Ne.def]
no goals
case h
α : Type u_1
p q : Perm α
x : α
⊢ ¬↑p⁻¹ x = x ↔ ¬↑p x = x
rw [inv_def, symm_apply_eq, eq_comm]