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

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
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 + m.succ < s.length

Tactic:
simpa using hn

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

Tactic:
refine ext_get hl fun n hn hn' => ?_

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
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'⟩

Proof state:
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'⟩

Tactic:
rw [get_insertIdx_of_lt _ _ _ _ H (H.trans hk),
  get_insertIdx_of_lt _ _ _ _ (H.trans (Nat.lt_succ_self _))]

Result:
no goals

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

Tactic:
rw [length_insertIdx_of_le_length hk.le, length_insertIdx_of_le_length (Nat.succ_le_of_lt hk)]

Result:
no goals

Proof state:
α : Type u_1
s : List α
x : α
⊢ (permutations'Aux x s).Nodup ↔ x ∉ s

Tactic:
refine ⟨fun h H ↦ ?_, nodup_permutations'Aux_of_not_mem _ _⟩

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

Proof state:
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'⟩

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

Result:
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⟩ = (insertIdx (k + 1) x s).get ⟨k.succ, hn'⟩

case intro.mk.a.inr.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
H' : k.succ < 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 = k.succ

Tactic:
rw [← @Fin.mk.inj_iff _ _ _ kl k1l]

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, kl⟩ = ⟨k + 1, k1l⟩

Proof state:
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⟩

Tactic:
exact get_insertIdx_add_succ _ _ _ 0 _

Result:
no goals

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⟩ = (insertIdx (k + 1) x s).get ⟨k.succ, hn'⟩

Tactic:
rw [get_insertIdx_self _ _ _ (Nat.succ_le_of_lt hk)]

Result:
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

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

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_lt H'

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.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'⟩