α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : support (swap x y) = {x, y}
⊢ x ≠ y
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
⊢ support (swap x y) = {x, y} ↔ x ≠ y
refine' ⟨fun h => _, fun h => support_swap h⟩
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : support (swap x y) = {x, y}
this : x = y
⊢ False
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : support (swap x y) = {x, y}
⊢ x ≠ y
by_contra'
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : support (swap x x) = {x, x}
this : x = y
⊢ False
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : support (swap x y) = {x, y}
this : x = y
⊢ False
rw [← this] at h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this : x = y
h : ∅ = {x}
⊢ False
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : support (swap x x) = {x, x}
this : x = y
⊢ False
simp only [swap_self, support_refl, pair_eq_singleton] at h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this✝ : x = y
h : ∅ = {x}
this : x ∈ ∅
⊢ False
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this : x = y
h : ∅ = {x}
⊢ False
have : x ∈ ∅ := by
  rw [h]
  exact mem_singleton.mpr rfl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this✝¹ : x = y
h : ∅ = {x}
this✝ : x ∈ ∅
this : ∅ ≠ ∅
⊢ False
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this✝ : x = y
h : ∅ = {x}
this : x ∈ ∅
⊢ False
have := (Finset.ne_empty_of_mem this)
no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this✝¹ : x = y
h : ∅ = {x}
this✝ : x ∈ ∅
this : ∅ ≠ ∅
⊢ False
exact this rfl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this : x = y
h : ∅ = {x}
⊢ x ∈ {x}

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this : x = y
h : ∅ = {x}
⊢ Membership α (Finset α)
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this : x = y
h : ∅ = {x}
⊢ x ∈ ∅
rw [h]
no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this : x = y
h : ∅ = {x}
⊢ x ∈ {x}

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this : x = y
h : ∅ = {x}
⊢ Membership α (Finset α)
exact mem_singleton.mpr rfl