α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h : Nodup (permutations'Aux x s)
⊢ ¬x ∈ s
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
⊢ Nodup (permutations'Aux x s) ↔ ¬x ∈ s
refine' ⟨fun h => _, nodup_permutations'Aux_of_not_mem _ _⟩
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h : Nodup (permutations'Aux x s)
H : x ∈ s
⊢ False
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h : Nodup (permutations'Aux x s)
⊢ ¬x ∈ s
intro H
case intro.intro
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h : Nodup (permutations'Aux x s)
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
⊢ False
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h : Nodup (permutations'Aux x s)
H : x ∈ s
⊢ False
obtain ⟨k, hk, hk'⟩ := nthLe_of_mem H
case intro.intro
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
⊢ False
case intro.intro
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h : Nodup (permutations'Aux x s)
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
⊢ False
rw [nodup_iff_nthLe_inj] at h
case intro.intro
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
⊢ k = k + 1
case intro.intro
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
⊢ False
suffices k = k + 1 by simp at this
case intro.intro.refine'_1
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
⊢ k < length (permutations'Aux x s)

case intro.intro.refine'_2
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
⊢ k + 1 < length (permutations'Aux x s)

case intro.intro.refine'_3
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
⊢ nthLe (permutations'Aux x s) k ?intro.intro.refine'_1 = nthLe (permutations'Aux x s) (k + 1) ?intro.intro.refine'_2
case intro.intro
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
⊢ k = k + 1
refine' h k (k + 1) _ _ _
case intro.intro.refine'_3
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
⊢ insertNth k x s = insertNth (k + 1) x s
case intro.intro.refine'_3
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
⊢ nthLe (permutations'Aux x s) k (_ : k < length (permutations'Aux x s)) =
    nthLe (permutations'Aux x s) (k + 1) (_ : k + 1 < length (permutations'Aux x s))
rw [nthLe_permutations'Aux, nthLe_permutations'Aux]
case intro.intro.refine'_3
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
⊢ insertNth k x s = insertNth (k + 1) x s
case intro.intro.refine'_3
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
⊢ insertNth k x s = insertNth (k + 1) x s
have hl : length (insertNth k x s) = length (insertNth (k + 1) x s) := by
  rw [length_insertNth _ _ hk.le, length_insertNth _ _ (Nat.succ_le_of_lt hk)]
case intro.intro.refine'_3
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
n : ℕ
hn : n < length (insertNth k x s)
hn' : n < length (insertNth (k + 1) x s)
⊢ nthLe (insertNth k x s) n hn = nthLe (insertNth (k + 1) x s) n hn'
case intro.intro.refine'_3
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
⊢ insertNth k x s = insertNth (k + 1) x s
refine' ext_nthLe hl fun n hn hn' => _
case intro.intro.refine'_3.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
n : ℕ
hn : n < length (insertNth k x s)
hn' : n < length (insertNth (k + 1) x s)
H : n < k
⊢ nthLe (insertNth k x s) n hn = nthLe (insertNth (k + 1) x s) n hn'

case intro.intro.refine'_3.inr.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
n : ℕ
hk : n < length s
hk' : nthLe s n hk = x
hl : length (insertNth n x s) = length (insertNth (n + 1) x s)
hn : n < length (insertNth n x s)
hn' : n < length (insertNth (n + 1) x s)
⊢ nthLe (insertNth n x s) n hn = nthLe (insertNth (n + 1) x s) n hn'

case intro.intro.refine'_3.inr.inr
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
n : ℕ
hn : n < length (insertNth k x s)
hn' : n < length (insertNth (k + 1) x s)
H : k < n
⊢ nthLe (insertNth k x s) n hn = nthLe (insertNth (k + 1) x s) n hn'
case intro.intro.refine'_3
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
n : ℕ
hn : n < length (insertNth k x s)
hn' : n < length (insertNth (k + 1) x s)
⊢ nthLe (insertNth k x s) n hn = nthLe (insertNth (k + 1) x s) n hn'
rcases lt_trichotomy n k with (H | rfl | H)
no goals
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
this : k = k + 1
⊢ False
simp at this
no goals
case intro.intro.refine'_1
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
⊢ k < length (permutations'Aux x s)
simpa [Nat.lt_succ_iff] using hk.le
no goals
case intro.intro.refine'_2
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
⊢ k + 1 < length (permutations'Aux x s)
simpa using hk
no goals
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
⊢ length (insertNth k x s) = length (insertNth (k + 1) x s)
rw [length_insertNth _ _ hk.le, length_insertNth _ _ (Nat.succ_le_of_lt hk)]
no goals
case intro.intro.refine'_3.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
n : ℕ
hn : n < length (insertNth k x s)
hn' : n < length (insertNth (k + 1) x s)
H : n < k
⊢ nthLe (insertNth k x s) n hn = nthLe (insertNth (k + 1) x s) n hn'
rw [nthLe_insertNth_of_lt _ _ _ _ H (H.trans hk),
  nthLe_insertNth_of_lt _ _ _ _ (H.trans (Nat.lt_succ_self _))]
no goals
case intro.intro.refine'_3.inr.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H : x ∈ s
n : ℕ
hk : n < length s
hk' : nthLe s n hk = x
hl : length (insertNth n x s) = length (insertNth (n + 1) x s)
hn : n < length (insertNth n x s)
hn' : n < length (insertNth (n + 1) x s)
⊢ nthLe (insertNth n x s) n hn = nthLe (insertNth (n + 1) x s) n hn'
rw [nthLe_insertNth_self _ _ _ hk.le, nthLe_insertNth_of_lt _ _ _ _ (Nat.lt_succ_self _) hk,
  hk']
case intro.intro.refine'_3.inr.inr.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
hn : succ k < length (insertNth k x s)
hn' : succ k < length (insertNth (k + 1) x s)
H : k < succ k
⊢ nthLe (insertNth k x s) (succ k) hn = nthLe (insertNth (k + 1) x s) (succ k) hn'

case intro.intro.refine'_3.inr.inr.inr
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
n : ℕ
hn : n < length (insertNth k x s)
hn' : n < length (insertNth (k + 1) x s)
H : k < n
H' : succ k < n
⊢ nthLe (insertNth k x s) n hn = nthLe (insertNth (k + 1) x s) n hn'
case intro.intro.refine'_3.inr.inr
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
n : ℕ
hn : n < length (insertNth k x s)
hn' : n < length (insertNth (k + 1) x s)
H : k < n
⊢ nthLe (insertNth k x s) n hn = nthLe (insertNth (k + 1) x s) n hn'
rcases(Nat.succ_le_of_lt H).eq_or_lt with (rfl | H')
case intro.intro.refine'_3.inr.inr.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
hn : succ k < length (insertNth k x s)
hn' : succ k < length (insertNth (k + 1) x s)
H : k < succ k
⊢ nthLe (insertNth k x s) (succ k) hn = x
case intro.intro.refine'_3.inr.inr.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
hn : succ k < length (insertNth k x s)
hn' : succ k < length (insertNth (k + 1) x s)
H : k < succ k
⊢ nthLe (insertNth k x s) (succ k) hn = nthLe (insertNth (k + 1) x s) (succ k) hn'
rw [nthLe_insertNth_self _ _ _ (Nat.succ_le_of_lt hk)]
case h.e'_2
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
hn : succ k < length (insertNth k x s)
hn' : succ k < length (insertNth (k + 1) x s)
H : k < succ k
⊢ nthLe (insertNth k x s) (succ k) hn = nthLe s k hk
case intro.intro.refine'_3.inr.inr.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
hn : succ k < length (insertNth k x s)
hn' : succ k < length (insertNth (k + 1) x s)
H : k < succ k
⊢ nthLe (insertNth k x s) (succ k) hn = x
convert hk' using 1
no goals
case h.e'_2
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
hn : succ k < length (insertNth k x s)
hn' : succ k < length (insertNth (k + 1) x s)
H : k < succ k
⊢ nthLe (insertNth k x s) (succ k) hn = nthLe s k hk
exact nthLe_insertNth_add_succ _ _ _ 0 _
case intro.intro.refine'_3.inr.inr.inr.intro
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
m : ℕ
hn : succ k + m + 1 < length (insertNth k x s)
hn' : succ k + m + 1 < length (insertNth (k + 1) x s)
H : k < succ k + m + 1
H' : succ k < succ k + m + 1
⊢ nthLe (insertNth k x s) (succ k + m + 1) hn = nthLe (insertNth (k + 1) x s) (succ k + m + 1) hn'
case intro.intro.refine'_3.inr.inr.inr
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
n : ℕ
hn : n < length (insertNth k x s)
hn' : n < length (insertNth (k + 1) x s)
H : k < n
H' : succ k < n
⊢ nthLe (insertNth k x s) n hn = nthLe (insertNth (k + 1) x s) n hn'
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_lt H'
case intro.intro.refine'_3.inr.inr.inr.intro
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
m : ℕ
hn✝ : succ k + m + 1 < length (insertNth k x s)
hn : succ (k + m) < length s
hn' : succ k + m + 1 < length (insertNth (k + 1) x s)
H : k < succ k + m + 1
H' : succ k < succ k + m + 1
⊢ nthLe (insertNth k x s) (succ k + m + 1) hn✝ = nthLe (insertNth (k + 1) x s) (succ k + m + 1) hn'
case intro.intro.refine'_3.inr.inr.inr.intro
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
m : ℕ
hn : succ k + m + 1 < length (insertNth k x s)
hn' : succ k + m + 1 < length (insertNth (k + 1) x s)
H : k < succ k + m + 1
H' : succ k < succ k + m + 1
⊢ nthLe (insertNth k x s) (succ k + m + 1) hn = nthLe (insertNth (k + 1) x s) (succ k + m + 1) hn'
erw [length_insertNth _ _ hk.le, Nat.succ_lt_succ_iff, Nat.succ_add] at hn
case intro.intro.refine'_3.inr.inr.inr.intro
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
m : ℕ
hn✝ : succ k + m + 1 < length (insertNth k x s)
hn : succ (k + m) < length s
hn' : succ k + m + 1 < length (insertNth (k + 1) x s)
H : k < succ k + m + 1
H' : succ k < succ k + m + 1
⊢ nthLe (insertNth k x s) (succ k + m + 1) hn✝ = nthLe s (k + 1 + m) ?intro.intro.refine'_3.inr.inr.inr.intro.hk'

case intro.intro.refine'_3.inr.inr.inr.intro.hk'
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
m : ℕ
hn✝ : succ k + m + 1 < length (insertNth k x s)
hn : succ (k + m) < length s
hn' : succ k + m + 1 < length (insertNth (k + 1) x s)
H : k < succ k + m + 1
H' : succ k < succ k + m + 1
⊢ k + 1 + m < length s
case intro.intro.refine'_3.inr.inr.inr.intro
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
m : ℕ
hn✝ : succ k + m + 1 < length (insertNth k x s)
hn : succ (k + m) < length s
hn' : succ k + m + 1 < length (insertNth (k + 1) x s)
H : k < succ k + m + 1
H' : succ k < succ k + m + 1
⊢ nthLe (insertNth k x s) (succ k + m + 1) hn✝ = nthLe (insertNth (k + 1) x s) (succ k + m + 1) hn'
rw [nthLe_insertNth_add_succ]
case h.e'_2.h.e'_3
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
m : ℕ
hn✝ : succ k + m + 1 < length (insertNth k x s)
hn : succ (k + m) < length s
hn' : succ k + m + 1 < length (insertNth (k + 1) x s)
H : k < succ k + m + 1
H' : succ k < succ k + m + 1
⊢ succ k + m + 1 = k + succ m + 1

case h.e'_3.h.e'_3
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
m : ℕ
hn✝ : succ k + m + 1 < length (insertNth k x s)
hn : succ (k + m) < length s
hn' : succ k + m + 1 < length (insertNth (k + 1) x s)
H : k < succ k + m + 1
H' : succ k < succ k + m + 1
⊢ k + 1 + m = k + succ m

case intro.intro.refine'_3.inr.inr.inr.intro.hk'
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
m : ℕ
hn✝ : succ k + m + 1 < length (insertNth k x s)
hn : succ (k + m) < length s
hn' : succ k + m + 1 < length (insertNth (k + 1) x s)
H : k < succ k + m + 1
H' : succ k < succ k + m + 1
⊢ k + 1 + m < length s
case intro.intro.refine'_3.inr.inr.inr.intro
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
m : ℕ
hn✝ : succ k + m + 1 < length (insertNth k x s)
hn : succ (k + m) < length s
hn' : succ k + m + 1 < length (insertNth (k + 1) x s)
H : k < succ k + m + 1
H' : succ k < succ k + m + 1
⊢ nthLe (insertNth k x s) (succ k + m + 1) hn✝ = nthLe s (k + 1 + m) ?intro.intro.refine'_3.inr.inr.inr.intro.hk'

case intro.intro.refine'_3.inr.inr.inr.intro.hk'
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
m : ℕ
hn✝ : succ k + m + 1 < length (insertNth k x s)
hn : succ (k + m) < length s
hn' : succ k + m + 1 < length (insertNth (k + 1) x s)
H : k < succ k + m + 1
H' : succ k < succ k + m + 1
⊢ k + 1 + m < length s
convert nthLe_insertNth_add_succ s x k m.succ (by simpa using hn) using 2
no goals
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
m : ℕ
hn✝ : succ k + m + 1 < length (insertNth k x s)
hn : succ (k + m) < length s
hn' : succ k + m + 1 < length (insertNth (k + 1) x s)
H : k < succ k + m + 1
H' : succ k < succ k + m + 1
⊢ k + succ m < length s
simpa using hn
no goals
case h.e'_2.h.e'_3
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
m : ℕ
hn✝ : succ k + m + 1 < length (insertNth k x s)
hn : succ (k + m) < length s
hn' : succ k + m + 1 < length (insertNth (k + 1) x s)
H : k < succ k + m + 1
H' : succ k < succ k + m + 1
⊢ succ k + m + 1 = k + succ m + 1
simp [Nat.add_succ, Nat.succ_add]
no goals
case h.e'_3.h.e'_3
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
m : ℕ
hn✝ : succ k + m + 1 < length (insertNth k x s)
hn : succ (k + m) < length s
hn' : succ k + m + 1 < length (insertNth (k + 1) x s)
H : k < succ k + m + 1
H' : succ k < succ k + m + 1
⊢ k + 1 + m = k + succ m
simp [add_left_comm, add_comm]
no goals
case intro.intro.refine'_3.inr.inr.inr.intro.hk'
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (permutations'Aux x s)) (h₂ : j < length (permutations'Aux x s)),
    nthLe (permutations'Aux x s) i h₁ = nthLe (permutations'Aux x s) j h₂ → i = j
H✝ : x ∈ s
k : ℕ
hk : k < length s
hk' : nthLe s k hk = x
hl : length (insertNth k x s) = length (insertNth (k + 1) x s)
m : ℕ
hn✝ : succ k + m + 1 < length (insertNth k x s)
hn : succ (k + m) < length s
hn' : succ k + m + 1 < length (insertNth (k + 1) x s)
H : k < succ k + m + 1
H' : succ k < succ k + m + 1
⊢ k + 1 + m < length s
simpa [Nat.succ_add] using hn