-- Mathlib/GroupTheory/Perm/List.lean
theorem support_formPerm_of_nodup' (l : List α) (h : Nodup l) (h' : ∀ x : α, l ≠ [x]) :
    { x | formPerm l x ≠ x } = l.toFinset

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ {x | l.formPerm x ≠ x} = ↑l.toFinset

Tactic:
apply _root_.le_antisymm

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

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

Proof state:
case a.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : ∀ ⦃a₁ a₂ : Fin l.length⦄, l.get a₁ = l.get a₂ → a₁ = a₂
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
⊢ False

Tactic:
specialize h H

Result:
case a.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
h : ⟨(n + 1) % l.length, ⋯⟩ = ⟨n, hn⟩
⊢ False

Proof state:
case a.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
⊢ False

Tactic:
rw [nodup_iff_injective_get, Function.Injective] at h

Result:
case a.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : ∀ ⦃a₁ a₂ : Fin l.length⦄, l.get a₁ = l.get a₂ → a₁ = a₂
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
⊢ False

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

Tactic:
intro x hx

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
x : α
hx : x ∈ ↑l.toFinset
⊢ x ∈ {x | l.formPerm x ≠ x}

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
x : α
hx : x ∈ l
⊢ x ∈ {x | l.formPerm x ≠ x}

Tactic:
obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx

Result:
case a.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
⊢ l[n] ∈ {x | l.formPerm x ≠ x}

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
x : α
hx : x ∈ ↑l.toFinset
⊢ x ∈ {x | l.formPerm x ≠ x}

Tactic:
simp only [Finset.mem_coe, mem_toFinset] at hx

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
x : α
hx : x ∈ l
⊢ x ∈ {x | l.formPerm x ≠ x}

Proof state:
case a.intro.intro.inr
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
h : ⟨(n + 1) % l.length, ⋯⟩ = ⟨n, hn⟩
hn' : n.succ < l.length
⊢ False

Tactic:
simp [Nat.mod_eq_of_lt hn'] at h

Result:
no goals

Proof state:
case a.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
⊢ l[n] ∈ {x | l.formPerm x ≠ x}

Tactic:
rw [Set.mem_setOf_eq, formPerm_apply_getElem _ h]

Result:
case a.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
⊢ l[(n + 1) % l.length] ≠ l[n]

Proof state:
case a.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
⊢ l[(n + 1) % l.length] ≠ l[n]

Tactic:
intro H

Result:
case a.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
⊢ False

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

Tactic:
exact support_formPerm_le' l

Result:
no goals

Proof state:
case a.intro.intro.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ = l.length
h : ⟨0, ⋯⟩ = ⟨n, hn⟩
⊢ ∃ x, l = [x]

Tactic:
rw [← length_eq_one, ← hn', (Fin.mk.inj_iff.mp h).symm]

Result:
no goals

Proof state:
case a.intro.intro.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ = l.length
h : ⟨0, ⋯⟩ = ⟨n, hn⟩
⊢ False

Tactic:
refine not_exists.mpr h' ?_

Result:
case a.intro.intro.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ = l.length
h : ⟨0, ⋯⟩ = ⟨n, hn⟩
⊢ ∃ x, l = [x]

Proof state:
case a.intro.intro.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
h : ⟨(n + 1) % l.length, ⋯⟩ = ⟨n, hn⟩
hn' : n.succ = l.length
⊢ False

Tactic:
simp only [← hn', Nat.mod_self] at h

Result:
case a.intro.intro.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ = l.length
h : ⟨0, ⋯⟩ = ⟨n, hn⟩
⊢ False

Proof state:
case a.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
h : ⟨(n + 1) % l.length, ⋯⟩ = ⟨n, hn⟩
⊢ False

Tactic:
rcases (Nat.succ_le_of_lt hn).eq_or_lt with hn' | hn'

Result:
case a.intro.intro.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
h : ⟨(n + 1) % l.length, ⋯⟩ = ⟨n, hn⟩
hn' : n.succ = l.length
⊢ False

case a.intro.intro.inr
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
h : ⟨(n + 1) % l.length, ⋯⟩ = ⟨n, hn⟩
hn' : n.succ < l.length
⊢ False