case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
⊢ support (swap x y) = {x, y}
ext z
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : z = x
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
by_cases hx : z = x
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : z = x
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
any_goals simpa [hx] using h.symm
no goals
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
simpa [hx] using h.symm
no goals
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
hy : ¬z = y
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
simp [swap_apply_of_ne_of_ne, hx, hy] <;>
exact h