Theorem: Equiv.Perm.support'_swap (Bruhat/Perm.lean)

State before:
α : Type u_1
x y : α
f : Perm α
inst✝ : DecidableEq α
hxy : x ≠ y
⊢ support' (swap x y) = {x, y}
Tactic:
ext z
State after:
case h
α : Type u_1
x y : α
f : Perm α
inst✝ : DecidableEq α
hxy : x ≠ y
z : α
⊢ z ∈ support' (swap x y) ↔ z ∈ {x, y}

State before:
case h
α : Type u_1
x y : α
f : Perm α
inst✝ : DecidableEq α
hxy : x ≠ y
z : α
⊢ z ∈ support' (swap x y) ↔ z ∈ {x, y}
Tactic:
simp only [support', ne_eq, mem_setOf_eq, mem_insert_iff, mem_singleton_iff]
State after:
case h
α : Type u_1
x y : α
f : Perm α
inst✝ : DecidableEq α
hxy : x ≠ y
z : α
⊢ ¬(swap x y) z = z ↔ z = x ∨ z = y

State before:
case h
α : Type u_1
x y : α
f : Perm α
inst✝ : DecidableEq α
hxy : x ≠ y
z : α
⊢ ¬(swap x y) z = z ↔ z = x ∨ z = y
Tactic:
rw [← Ne.def, Equiv.swap_apply_ne_self_iff, and_iff_right hxy]
State after:
no goals