case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ↑f x = x
⊢ support (swap x (↑f x) * f) = support f \ {x}

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

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

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
hzf : ¬z = ↑f x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
by_cases hzf : z = f x
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
hzf : ¬z = ↑f x
hzfx : ↑f z = x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
hzf : ¬z = ↑f x
hzfx : ¬↑f z = x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
hzf : ¬z = ↑f x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
by_cases hzfx : f z = x
no goals
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ↑f x = x
⊢ support (swap x (↑f x) * f) = support f \ {x}
simp [hx, sdiff_singleton_eq_erase, not_mem_support.mpr hx, erase_eq_of_not_mem]
no goals
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : z = x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
simp [hzx]
no goals
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
hzf : z = ↑f x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
simp [hzf, hx, h, swap_apply_of_ne_of_ne]
no goals
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
hzf : ¬z = ↑f x
hzfx : ↑f z = x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
simp [Ne.symm hzx, hzx, Ne.symm hzf, hzfx]
no goals
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
hzf : ¬z = ↑f x
hzfx : ¬↑f z = x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
simp [Ne.symm hzx, hzx, Ne.symm hzf, hzfx, f.injective.ne hzx, swap_apply_of_ne_of_ne]