-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_apply_mem_eq_self_iff (hl : Nodup l) (x : α) (hx : x ∈ l) :
    formPerm l x = x ↔ length l ≤ 1

Proof state:
case intro.intro.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
hn : l.length = 0
⊢ (k + 1) % 0 = k ↔ 0 ≤ 1

Tactic:
exact absurd k.zero_le (hk.trans_le hn.le).not_le

Result:
no goals

Proof state:
case intro.intro.succ.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk✝ : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hk : k < n✝ + 1
hn : l.length = n✝ + 1
hk' : k = n✝
⊢ (k + 1) % (n✝ + 1) = k ↔ n✝ + 1 ≤ 1

Tactic:
simp [← hk', Nat.succ_le_succ_iff, eq_comm]

Result:
no goals

Proof state:
case intro.intro.succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk✝ : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hk : k < n✝ + 1
hn : l.length = n✝ + 1
⊢ (k + 1) % (n✝ + 1) = k ↔ n✝ + 1 ≤ 1

Tactic:
rcases (Nat.le_of_lt_succ hk).eq_or_lt with hk' | hk'

Result:
case intro.intro.succ.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk✝ : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hk : k < n✝ + 1
hn : l.length = n✝ + 1
hk' : k = n✝
⊢ (k + 1) % (n✝ + 1) = k ↔ n✝ + 1 ≤ 1

case intro.intro.succ.inr
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk✝ : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hk : k < n✝ + 1
hn : l.length = n✝ + 1
hk' : k < n✝
⊢ (k + 1) % (n✝ + 1) = k ↔ n✝ + 1 ≤ 1

Proof state:
case intro.intro.succ.inr
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk✝ : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hk : k < n✝ + 1
hn : l.length = n✝ + 1
hk' : k < n✝
⊢ (k + 1) % (n✝ + 1) = k ↔ n✝ + 1 ≤ 1

Tactic:
simpa [Nat.mod_eq_of_lt (Nat.succ_lt_succ hk'), Nat.succ_lt_succ_iff] using
  (k.zero_le.trans_lt hk').ne.symm

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ (k + 1) % l.length = k ↔ l.length ≤ 1

Tactic:
cases hn : l.length

Result:
case intro.intro.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
hn : l.length = 0
⊢ (k + 1) % 0 = k ↔ 0 ≤ 1

case intro.intro.succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hn : l.length = n✝ + 1
⊢ (k + 1) % (n✝ + 1) = k ↔ n✝ + 1 ≤ 1

Proof state:
case intro.intro.succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hn : l.length = n✝ + 1
⊢ (k + 1) % (n✝ + 1) = k ↔ n✝ + 1 ≤ 1

Tactic:
rw [hn] at hk

Result:
case intro.intro.succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk✝ : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hk : k < n✝ + 1
hn : l.length = n✝ + 1
⊢ (k + 1) % (n✝ + 1) = k ↔ n✝ + 1 ≤ 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ l.formPerm x = x ↔ l.length ≤ 1

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l.formPerm l[k] = l[k] ↔ l.length ≤ 1

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l.formPerm l[k] = l[k] ↔ l.length ≤ 1

Tactic:
rw [formPerm_apply_getElem _ hl k hk, hl.getElem_inj_iff]

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ (k + 1) % l.length = k ↔ l.length ≤ 1