α : Type u_1
p q : Perm α
x : α
⊢ x ∈ {x | ↑(p * q) x ≠ x} → x ∈ {x | ↑p x ≠ x} ∪ {x | ↑q x ≠ x}
α : Type u_1
p q : Perm α
⊢ {x | ↑(p * q) x ≠ x} ⊆ {x | ↑p x ≠ x} ∪ {x | ↑q x ≠ x}
intro x
α : Type u_1
p q : Perm α
x : α
⊢ ¬↑p (↑q x) = x → ¬↑p x = x ∨ ¬↑q x = x
α : Type u_1
p q : Perm α
x : α
⊢ x ∈ {x | ↑(p * q) x ≠ x} → x ∈ {x | ↑p x ≠ x} ∪ {x | ↑q x ≠ x}
simp only [Perm.coe_mul, Function.comp_apply, Ne.def, Set.mem_union, Set.mem_setOf_eq]
no goals
α : Type u_1
p q : Perm α
x : α
⊢ ¬↑p (↑q x) = x → ¬↑p x = x ∨ ¬↑q x = x
by_cases hq : q x = x <;> simp [hq]