case a
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
⊢ {x | ↑(formPerm l) x ≠ x} ≤ ↑(toFinset l)

case a
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
⊢ ↑(toFinset l) ≤ {x | ↑(formPerm l) x ≠ x}
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
⊢ {x | ↑(formPerm l) x ≠ x} = ↑(toFinset l)
apply _root_.le_antisymm
no goals
case a
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
⊢ {x | ↑(formPerm l) x ≠ x} ≤ ↑(toFinset l)
exact support_formPerm_le' l
case a
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
x : α
hx : x ∈ ↑(toFinset l)
⊢ x ∈ {x | ↑(formPerm l) x ≠ x}
case a
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
⊢ ↑(toFinset l) ≤ {x | ↑(formPerm l) x ≠ x}
intro x hx
case a
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
x : α
hx : x ∈ l
⊢ x ∈ {x | ↑(formPerm l) x ≠ x}
case a
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
x : α
hx : x ∈ ↑(toFinset l)
⊢ x ∈ {x | ↑(formPerm l) x ≠ x}
simp only [Finset.mem_coe, mem_toFinset] at hx
case a.intro.intro
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
⊢ nthLe l n hn ∈ {x | ↑(formPerm l) x ≠ x}
case a
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
x : α
hx : x ∈ l
⊢ x ∈ {x | ↑(formPerm l) x ≠ x}
obtain ⟨n, hn, rfl⟩ := nthLe_of_mem hx
case a.intro.intro
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
⊢ nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) ≠ nthLe l n hn
case a.intro.intro
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
⊢ nthLe l n hn ∈ {x | ↑(formPerm l) x ≠ x}
rw [Set.mem_setOf_eq, formPerm_apply_nthLe _ h]
case a.intro.intro
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
⊢ False
case a.intro.intro
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
⊢ nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) ≠ nthLe l n hn
intro H
case a.intro.intro
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : ∀ (i j : ℕ) (h₁ : i < length l) (h₂ : j < length l), nthLe l i h₁ = nthLe l j h₂ → i = j
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
⊢ False
case a.intro.intro
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
⊢ False
rw [nodup_iff_nthLe_inj] at h
case a.intro.intro
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
h : (n + 1) % length l = n
⊢ False
case a.intro.intro
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : ∀ (i j : ℕ) (h₁ : i < length l) (h₂ : j < length l), nthLe l i h₁ = nthLe l j h₂ → i = j
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
⊢ False
specialize h _ _ _ _ H
case a.intro.intro.inl
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
h : (n + 1) % length l = n
hn' : Nat.succ n = length l
⊢ False

case a.intro.intro.inr
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
h : (n + 1) % length l = n
hn' : Nat.succ n < length l
⊢ False
case a.intro.intro
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
h : (n + 1) % length l = n
⊢ False
cases' (Nat.succ_le_of_lt hn).eq_or_lt with hn' hn'
case a.intro.intro.inl
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
hn' : Nat.succ n = length l
h : 0 = n
⊢ False
case a.intro.intro.inl
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
h : (n + 1) % length l = n
hn' : Nat.succ n = length l
⊢ False
simp only [← hn', Nat.mod_self] at h
case a.intro.intro.inl
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
hn' : Nat.succ n = length l
h : 0 = n
⊢ ∃ x, l = [x]
case a.intro.intro.inl
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
hn' : Nat.succ n = length l
h : 0 = n
⊢ False
refine' not_exists.mpr h' _
case a.intro.intro.inl
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
hn' : Nat.succ n = length l
h : 0 = n
⊢ length l = 1
case a.intro.intro.inl
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
hn' : Nat.succ n = length l
h : 0 = n
⊢ ∃ x, l = [x]
rw [← length_eq_one]
no goals
case a.intro.intro.inl
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
hn' : Nat.succ n = length l
h : 0 = n
⊢ length l = 1
simpa [← h, eq_comm] using hn'
no goals
case a.intro.intro.inr
α : Type u_1
β : Type ?u.764613
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
h : (n + 1) % length l = n
hn' : Nat.succ n < length l
⊢ False
simp [Nat.mod_eq_of_lt hn'] at h