-- 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.inr.inr.intro
α : 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
m : ℕ
hn✝ : k.succ + m + 1 < (insertIdx k x s).length
hn : (k + m).succ < s.length
hn' : k.succ + m + 1 < (insertIdx (k + 1) x s).length
H : k < k.succ + m + 1
H' : k.succ < k.succ + m + 1
⊢ (insertIdx k x s).get ⟨k.succ + m + 1, hn✝⟩ = s.get ⟨k + 1 + m, ?intro.mk.a.inr.inr.inr.intro.hk'⟩

Tactic:
convert get_insertIdx_add_succ s x k m.succ (by simpa using hn) using 2

Result:
case h.e'_2.h.e'_3
α : 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
m : ℕ
hn✝ : k.succ + m + 1 < (insertIdx k x s).length
hn : (k + m).succ < s.length
hn' : k.succ + m + 1 < (insertIdx (k + 1) x s).length
H : k < k.succ + m + 1
H' : k.succ < k.succ + m + 1
⊢ ⟨k.succ + m + 1, hn✝⟩ = ⟨k + m.succ + 1, ⋯⟩

case h.e'_3.h.e'_3
α : 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
m : ℕ
hn✝ : k.succ + m + 1 < (insertIdx k x s).length
hn : (k + m).succ < s.length
hn' : k.succ + m + 1 < (insertIdx (k + 1) x s).length
H : k < k.succ + m + 1
H' : k.succ < k.succ + m + 1
⊢ ⟨k + 1 + m, ?intro.mk.a.inr.inr.inr.intro.hk'⟩ = ⟨k + m.succ, ⋯⟩

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
⊢ k < (permutations'Aux x s).length

Tactic:
simpa [Nat.lt_succ_iff] using hk.le

Result:
no goals

Proof state:
case intro.mk.a.inr.inr.inr.intro
α : 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
m : ℕ
hn✝ : k.succ + m + 1 < (insertIdx k x s).length
hn : (k + m).succ < s.length
hn' : k.succ + m + 1 < (insertIdx (k + 1) x s).length
H : k < k.succ + m + 1
H' : k.succ < k.succ + m + 1
⊢ (insertIdx k x s).get ⟨k.succ + m + 1, hn✝⟩ = (insertIdx (k + 1) x s).get ⟨k.succ + m + 1, hn'⟩

Tactic:
rw [get_insertIdx_add_succ]

Result:
case intro.mk.a.inr.inr.inr.intro
α : 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
m : ℕ
hn✝ : k.succ + m + 1 < (insertIdx k x s).length
hn : (k + m).succ < s.length
hn' : k.succ + m + 1 < (insertIdx (k + 1) x s).length
H : k < k.succ + m + 1
H' : k.succ < k.succ + m + 1
⊢ (insertIdx k x s).get ⟨k.succ + m + 1, hn✝⟩ = s.get ⟨k + 1 + m, ?intro.mk.a.inr.inr.inr.intro.hk'⟩

case intro.mk.a.inr.inr.inr.intro.hk'
α : 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
m : ℕ
hn✝ : k.succ + m + 1 < (insertIdx k x s).length
hn : (k + m).succ < s.length
hn' : k.succ + m + 1 < (insertIdx (k + 1) x s).length
H : k < k.succ + m + 1
H' : k.succ < k.succ + m + 1
⊢ k + 1 + m < s.length

Proof state:
case h.e'_2.h.e'_3
α : 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
m : ℕ
hn✝ : k.succ + m + 1 < (insertIdx k x s).length
hn : (k + m).succ < s.length
hn' : k.succ + m + 1 < (insertIdx (k + 1) x s).length
H : k < k.succ + m + 1
H' : k.succ < k.succ + m + 1
⊢ ⟨k.succ + m + 1, hn✝⟩ = ⟨k + m.succ + 1, ⋯⟩

Tactic:
simp [Nat.add_assoc, Nat.add_left_comm]

Result:
no goals

Proof state:
case intro.mk.a.inr.inr.inr.intro.hk'
α : 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
m : ℕ
hn✝ : k.succ + m + 1 < (insertIdx k x s).length
hn : (k + m).succ < s.length
hn' : k.succ + m + 1 < (insertIdx (k + 1) x s).length
H : k < k.succ + m + 1
H' : k.succ < k.succ + m + 1
⊢ k + 1 + m < s.length

Tactic:
simpa [Nat.succ_add] using hn

Result:
no goals

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
⊢ k = k.succ

Tactic:
have k1l : k + 1 < (permutations'Aux x s).length := by simpa using hk

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
k1l : k + 1 < (permutations'Aux x s).length
⊢ k = k.succ

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
⊢ False

Tactic:
apply k.succ_ne_self.symm

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
⊢ k = k.succ

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
⊢ (permutations'Aux x s).get ⟨k, kl⟩ = (permutations'Aux x s).get ⟨k + 1, k1l⟩

Tactic:
rw [get_permutations'Aux, get_permutations'Aux]

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
⊢ insertIdx k x s = insertIdx (k + 1) x s

Proof state:
case intro.mk.a.inr.inr.inr.intro
α : 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
m : ℕ
hn : k.succ + m + 1 < (insertIdx k x s).length
hn' : k.succ + m + 1 < (insertIdx (k + 1) x s).length
H : k < k.succ + m + 1
H' : k.succ < k.succ + m + 1
⊢ (insertIdx k x s).get ⟨k.succ + m + 1, hn⟩ = (insertIdx (k + 1) x s).get ⟨k.succ + m + 1, hn'⟩

Tactic:
rw [length_insertIdx_of_le_length hk.le, Nat.succ_lt_succ_iff, Nat.succ_add] at hn

Result:
case intro.mk.a.inr.inr.inr.intro
α : 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
m : ℕ
hn✝ : k.succ + m + 1 < (insertIdx k x s).length
hn : (k + m).succ < s.length
hn' : k.succ + m + 1 < (insertIdx (k + 1) x s).length
H : k < k.succ + m + 1
H' : k.succ < k.succ + m + 1
⊢ (insertIdx k x s).get ⟨k.succ + m + 1, hn✝⟩ = (insertIdx (k + 1) x s).get ⟨k.succ + m + 1, hn'⟩