case intro.intro
α : Type u_1
β : Type ?u.813892
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ ↑(formPerm l) (nthLe l k hk) = nthLe l k hk ↔ length l ≤ 1
α : Type u_1
β : Type ?u.813892
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : x ∈ l
⊢ ↑(formPerm l) x = x ↔ length l ≤ 1
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem hx
case intro.intro
α : Type u_1
β : Type ?u.813892
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ (k + 1) % length l = k ↔ length l ≤ 1
case intro.intro
α : Type u_1
β : Type ?u.813892
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ ↑(formPerm l) (nthLe l k hk) = nthLe l k hk ↔ length l ≤ 1
rw [formPerm_apply_nthLe _ hl, hl.nthLe_inj_iff]
case intro.intro.zero
α : Type u_1
β : Type ?u.813892
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
hn : length l = Nat.zero
⊢ (k + 1) % Nat.zero = k ↔ Nat.zero ≤ 1

case intro.intro.succ
α : Type u_1
β : Type ?u.813892
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
n✝ : ℕ
hn : length l = Nat.succ n✝
⊢ (k + 1) % Nat.succ n✝ = k ↔ Nat.succ n✝ ≤ 1
case intro.intro
α : Type u_1
β : Type ?u.813892
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ (k + 1) % length l = k ↔ length l ≤ 1
cases hn : l.length
no goals
case intro.intro.zero
α : Type u_1
β : Type ?u.813892
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
hn : length l = Nat.zero
⊢ (k + 1) % Nat.zero = k ↔ Nat.zero ≤ 1
exact absurd k.zero_le (hk.trans_le hn.le).not_le
case intro.intro.succ
α : Type u_1
β : Type ?u.813892
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk✝ : k < length l
hx : nthLe l k hk✝ ∈ l
n✝ : ℕ
hk : k < Nat.succ n✝
hn : length l = Nat.succ n✝
⊢ (k + 1) % Nat.succ n✝ = k ↔ Nat.succ n✝ ≤ 1
case intro.intro.succ
α : Type u_1
β : Type ?u.813892
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
n✝ : ℕ
hn : length l = Nat.succ n✝
⊢ (k + 1) % Nat.succ n✝ = k ↔ Nat.succ n✝ ≤ 1
rw [hn] at hk
case intro.intro.succ.inl
α : Type u_1
β : Type ?u.813892
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk✝ : k < length l
hx : nthLe l k hk✝ ∈ l
n✝ : ℕ
hk : k < Nat.succ n✝
hn : length l = Nat.succ n✝
hk' : k = n✝
⊢ (k + 1) % Nat.succ n✝ = k ↔ Nat.succ n✝ ≤ 1

case intro.intro.succ.inr
α : Type u_1
β : Type ?u.813892
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk✝ : k < length l
hx : nthLe l k hk✝ ∈ l
n✝ : ℕ
hk : k < Nat.succ n✝
hn : length l = Nat.succ n✝
hk' : k < n✝
⊢ (k + 1) % Nat.succ n✝ = k ↔ Nat.succ n✝ ≤ 1
case intro.intro.succ
α : Type u_1
β : Type ?u.813892
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk✝ : k < length l
hx : nthLe l k hk✝ ∈ l
n✝ : ℕ
hk : k < Nat.succ n✝
hn : length l = Nat.succ n✝
⊢ (k + 1) % Nat.succ n✝ = k ↔ Nat.succ n✝ ≤ 1
cases' (Nat.le_of_lt_succ hk).eq_or_lt with hk' hk'
no goals
case intro.intro.succ.inl
α : Type u_1
β : Type ?u.813892
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk✝ : k < length l
hx : nthLe l k hk✝ ∈ l
n✝ : ℕ
hk : k < Nat.succ n✝
hn : length l = Nat.succ n✝
hk' : k = n✝
⊢ (k + 1) % Nat.succ n✝ = k ↔ Nat.succ n✝ ≤ 1
simp [← hk', Nat.succ_le_succ_iff, eq_comm]
no goals
case intro.intro.succ.inr
α : Type u_1
β : Type ?u.813892
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk✝ : k < length l
hx : nthLe l k hk✝ ∈ l
n✝ : ℕ
hk : k < Nat.succ n✝
hn : length l = Nat.succ n✝
hk' : k < n✝
⊢ (k + 1) % Nat.succ n✝ = k ↔ Nat.succ n✝ ≤ 1
simpa [Nat.mod_eq_of_lt (Nat.succ_lt_succ hk'), Nat.succ_lt_succ_iff] using
  k.zero_le.trans_lt hk'