α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
⊢ a✝ ∈ support f \ {x, y} → a✝ ∈ support (swap x y * f)
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y : α
⊢ support f \ {x, y} ≤ support (swap x y * f)
intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
⊢ ¬↑f a✝ = a✝ → ¬(a✝ = x ∨ a✝ = y) → ¬↑(swap x y) (↑f a✝) = a✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
⊢ a✝ ∈ support f \ {x, y} → a✝ ∈ support (swap x y * f)
simp only [and_imp, Perm.coe_mul, Function.comp_apply, Ne.def, mem_support, mem_insert, mem_sdiff,
  mem_singleton]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
⊢ ↑f a✝ ≠ a✝ → a✝ ≠ x ∧ a✝ ≠ y → ↑(swap x y) (↑f a✝) ≠ a✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
⊢ ¬↑f a✝ = a✝ → ¬(a✝ = x ∨ a✝ = y) → ¬↑(swap x y) (↑f a✝) = a✝
push_neg
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
ha : ↑f a✝ ≠ a✝
hx : a✝ ≠ x
hy : a✝ ≠ y
H : ↑(swap x y) (↑f a✝) = a✝
⊢ False
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
⊢ ↑f a✝ ≠ a✝ → a✝ ≠ x ∧ a✝ ≠ y → ↑(swap x y) (↑f a✝) ≠ a✝
rintro ha ⟨hx, hy⟩ H
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
ha : ↑f a✝ ≠ a✝
hx : a✝ ≠ x
hy : a✝ ≠ y
H : ↑f a✝ = a✝
⊢ False
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
ha : ↑f a✝ ≠ a✝
hx : a✝ ≠ x
hy : a✝ ≠ y
H : ↑(swap x y) (↑f a✝) = a✝
⊢ False
rw [swap_apply_eq_iff, swap_apply_of_ne_of_ne hx hy] at H
no goals
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
ha : ↑f a✝ ≠ a✝
hx : a✝ ≠ x
hy : a✝ ≠ y
H : ↑f a✝ = a✝
⊢ False
exact ha H