α : Type u_1
p q : Perm α
n : ℤ
x : α
⊢ x ∈ {x | ↑(p ^ n) x ≠ x} → x ∈ {x | ↑p x ≠ x}
α : Type u_1
p q : Perm α
n : ℤ
⊢ {x | ↑(p ^ n) x ≠ x} ⊆ {x | ↑p x ≠ x}
intro x
α : Type u_1
p q : Perm α
n : ℤ
x : α
⊢ ¬↑(p ^ n) x = x → ¬↑p x = x
α : Type u_1
p q : Perm α
n : ℤ
x : α
⊢ x ∈ {x | ↑(p ^ n) x ≠ x} → x ∈ {x | ↑p x ≠ x}
simp only [Set.mem_setOf_eq, Ne.def]
α : Type u_1
p q : Perm α
n : ℤ
x : α
hx : ¬↑(p ^ n) x = x
H : ↑p x = x
⊢ False
α : Type u_1
p q : Perm α
n : ℤ
x : α
⊢ ¬↑(p ^ n) x = x → ¬↑p x = x
intro hx H
no goals
α : Type u_1
p q : Perm α
n : ℤ
x : α
hx : ¬↑(p ^ n) x = x
H : ↑p x = x
⊢ False
simp [zpow_apply_eq_self_of_apply_eq_self H] at hx