-- Mathlib/Data/List/Permutation.lean
theorem nodup_permutations'Aux_iff {s : List α} {x : α} : Nodup (permutations'Aux x s) ↔ x ∉ s

Proof state:
case intro.mk.a.inr.inl
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
n : ℕ
hk : n < s.length
hk' : s.get ⟨n, hk⟩ = x
kl : n < (permutations'Aux x s).length
k1l : n + 1 < (permutations'Aux x s).length
hl : (insertIdx n x s).length = (insertIdx (n + 1) x s).length
hn : n < (insertIdx n x s).length
hn' : n < (insertIdx (n + 1) x s).length
⊢ (insertIdx n x s).get ⟨n, hn⟩ = (insertIdx (n + 1) x s).get ⟨n, hn'⟩

Tactic:
rw [get_insertIdx_self _ _ _ hk.le, get_insertIdx_of_lt _ _ _ _ (Nat.lt_succ_self _) hk, hk']

Result:
no goals

Proof state:
case intro.mk.a
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
hl : (insertIdx k x s).length = (insertIdx (k + 1) x s).length
n : ℕ
hn : n < (insertIdx k x s).length
hn' : n < (insertIdx (k + 1) x s).length
⊢ (insertIdx k x s).get ⟨n, hn⟩ = (insertIdx (k + 1) x s).get ⟨n, hn'⟩

Tactic:
rcases lt_trichotomy n k with (H | rfl | H)

Result:
case intro.mk.a.inl
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H✝ : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
hl : (insertIdx k x s).length = (insertIdx (k + 1) x s).length
n : ℕ
hn : n < (insertIdx k x s).length
hn' : n < (insertIdx (k + 1) x s).length
H : n < k
⊢ (insertIdx k x s).get ⟨n, hn⟩ = (insertIdx (k + 1) x s).get ⟨n, hn'⟩

case intro.mk.a.inr.inl
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
n : ℕ
hk : n < s.length
hk' : s.get ⟨n, hk⟩ = x
kl : n < (permutations'Aux x s).length
k1l : n + 1 < (permutations'Aux x s).length
hl : (insertIdx n x s).length = (insertIdx (n + 1) x s).length
hn : n < (insertIdx n x s).length
hn' : n < (insertIdx (n + 1) x s).length
⊢ (insertIdx n x s).get ⟨n, hn⟩ = (insertIdx (n + 1) x s).get ⟨n, hn'⟩

case intro.mk.a.inr.inr
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H✝ : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
hl : (insertIdx k x s).length = (insertIdx (k + 1) x s).length
n : ℕ
hn : n < (insertIdx k x s).length
hn' : n < (insertIdx (k + 1) x s).length
H : k < n
⊢ (insertIdx k x s).get ⟨n, hn⟩ = (insertIdx (k + 1) x s).get ⟨n, hn'⟩

Proof state:
case intro.mk
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ ⟨k, kl⟩ = ⟨k + 1, k1l⟩

Tactic:
apply h

Result:
case intro.mk.a
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ (permutations'Aux x s).get ⟨k, kl⟩ = (permutations'Aux x s).get ⟨k + 1, k1l⟩

Proof state:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
⊢ k + 1 < (permutations'Aux x s).length

Tactic:
simpa using hk

Result:
no goals

Proof state:
case intro.mk
α : Type u_1
s : List α
x : α
h : (permutations'Aux x s).Nodup
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
⊢ False

Tactic:
rw [nodup_iff_injective_get] at h

Result:
case intro.mk
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
⊢ False

Proof state:
case intro.mk.a
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ insertIdx k x s = insertIdx (k + 1) x s

Tactic:
have hl : length (insertIdx k x s) = length (insertIdx (k + 1) x s) := by
  rw [length_insertIdx_of_le_length hk.le, length_insertIdx_of_le_length (Nat.succ_le_of_lt hk)]

Result:
case intro.mk.a
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
hl : (insertIdx k x s).length = (insertIdx (k + 1) x s).length
⊢ insertIdx k x s = insertIdx (k + 1) x s

Proof state:
case intro.mk
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
⊢ k = k.succ

Tactic:
have kl : k < (permutations'Aux x s).length := by simpa [Nat.lt_succ_iff] using hk.le

Result:
case intro.mk
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
⊢ k = k.succ

Proof state:
case intro.mk.a.inr.inr.inl
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H✝ : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
hl : (insertIdx k x s).length = (insertIdx (k + 1) x s).length
hn : k.succ < (insertIdx k x s).length
hn' : k.succ < (insertIdx (k + 1) x s).length
H : k < k.succ
⊢ (insertIdx k x s).get ⟨k.succ, hn⟩ = x

Tactic:
convert hk' using 1

Result:
case h.e'_2
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H✝ : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
hl : (insertIdx k x s).length = (insertIdx (k + 1) x s).length
hn : k.succ < (insertIdx k x s).length
hn' : k.succ < (insertIdx (k + 1) x s).length
H : k < k.succ
⊢ (insertIdx k x s).get ⟨k.succ, hn⟩ = s.get ⟨k, hk⟩

Proof state:
α : Type u_1
s : List α
x : α
h : (permutations'Aux x s).Nodup
H : x ∈ s
⊢ False

Tactic:
obtain ⟨⟨k, hk⟩, hk'⟩ := get_of_mem H

Result:
case intro.mk
α : Type u_1
s : List α
x : α
h : (permutations'Aux x s).Nodup
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
⊢ False