case nil
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
n✝ : ℕ
hn✝ : n✝ < length (permutations'Aux x s)
n : ℕ
hn : n < length (permutations'Aux x [])
⊢ nthLe (permutations'Aux x []) n hn = insertNth n x []

case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
n✝ : ℕ
hn✝ : n✝ < length (permutations'Aux x s✝)
y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < length (permutations'Aux x s)), nthLe (permutations'Aux x s) n hn = insertNth n x s
n : ℕ
hn : n < length (permutations'Aux x (y :: s))
⊢ nthLe (permutations'Aux x (y :: s)) n hn = insertNth n x (y :: s)
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
n : ℕ
hn : n < length (permutations'Aux x s)
⊢ nthLe (permutations'Aux x s) n hn = insertNth n x s
induction' s with y s IH generalizing n
case nil
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
n✝ : ℕ
hn✝¹ : n✝ < length (permutations'Aux x s)
n : ℕ
hn✝ : n < length (permutations'Aux x [])
hn : n = 0
⊢ nthLe (permutations'Aux x []) n hn✝ = insertNth n x []
case nil
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
n✝ : ℕ
hn✝ : n✝ < length (permutations'Aux x s)
n : ℕ
hn : n < length (permutations'Aux x [])
⊢ nthLe (permutations'Aux x []) n hn = insertNth n x []
simp only [length, zero_add, lt_one_iff] at hn
no goals
case nil
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
n✝ : ℕ
hn✝¹ : n✝ < length (permutations'Aux x s)
n : ℕ
hn✝ : n < length (permutations'Aux x [])
hn : n = 0
⊢ nthLe (permutations'Aux x []) n hn✝ = insertNth n x []
simp [hn]
case cons.zero
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
n : ℕ
hn✝ : n < length (permutations'Aux x s✝)
y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < length (permutations'Aux x s)), nthLe (permutations'Aux x s) n hn = insertNth n x s
hn : zero < length (permutations'Aux x (y :: s))
⊢ nthLe (permutations'Aux x (y :: s)) zero hn = insertNth zero x (y :: s)

case cons.succ
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
n : ℕ
hn✝ : n < length (permutations'Aux x s✝)
y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < length (permutations'Aux x s)), nthLe (permutations'Aux x s) n hn = insertNth n x s
n✝ : ℕ
hn : succ n✝ < length (permutations'Aux x (y :: s))
⊢ nthLe (permutations'Aux x (y :: s)) (succ n✝) hn = insertNth (succ n✝) x (y :: s)
case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
n✝ : ℕ
hn✝ : n✝ < length (permutations'Aux x s✝)
y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < length (permutations'Aux x s)), nthLe (permutations'Aux x s) n hn = insertNth n x s
n : ℕ
hn : n < length (permutations'Aux x (y :: s))
⊢ nthLe (permutations'Aux x (y :: s)) n hn = insertNth n x (y :: s)
cases n
no goals
case cons.zero
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
n : ℕ
hn✝ : n < length (permutations'Aux x s✝)
y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < length (permutations'Aux x s)), nthLe (permutations'Aux x s) n hn = insertNth n x s
hn : zero < length (permutations'Aux x (y :: s))
⊢ nthLe (permutations'Aux x (y :: s)) zero hn = insertNth zero x (y :: s)
simp [nthLe]
no goals
case cons.succ
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
n : ℕ
hn✝ : n < length (permutations'Aux x s✝)
y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < length (permutations'Aux x s)), nthLe (permutations'Aux x s) n hn = insertNth n x s
n✝ : ℕ
hn : succ n✝ < length (permutations'Aux x (y :: s))
⊢ nthLe (permutations'Aux x (y :: s)) (succ n✝) hn = insertNth (succ n✝) x (y :: s)
simpa [nthLe] using IH _ _