case nil
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n✝ : ℕ
h✝ : n✝ ≤ length l
n : ℕ
h : n ≤ length []
⊢ insertNth n x [] ~ [x]

case cons
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n✝ : ℕ
h✝ : n✝ ≤ length l
head✝ : α
tail✝ : List α
l_ih : ∀ {n : ℕ}, n ≤ length tail✝ → insertNth n x tail✝ ~ x :: tail✝
n : ℕ
h : n ≤ length (head✝ :: tail✝)
⊢ insertNth n x (head✝ :: tail✝) ~ x :: head✝ :: tail✝
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h : n ≤ length l
⊢ insertNth n x l ~ x :: l
induction' l with _ _ l_ih generalizing n
case cons.zero
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h✝ : n ≤ length l
head✝ : α
tail✝ : List α
l_ih : ∀ {n : ℕ}, n ≤ length tail✝ → insertNth n x tail✝ ~ x :: tail✝
h : zero ≤ length (head✝ :: tail✝)
⊢ insertNth zero x (head✝ :: tail✝) ~ x :: head✝ :: tail✝

case cons.succ
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h✝ : n ≤ length l
head✝ : α
tail✝ : List α
l_ih : ∀ {n : ℕ}, n ≤ length tail✝ → insertNth n x tail✝ ~ x :: tail✝
n✝ : ℕ
h : succ n✝ ≤ length (head✝ :: tail✝)
⊢ insertNth (succ n✝) x (head✝ :: tail✝) ~ x :: head✝ :: tail✝
case cons
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n✝ : ℕ
h✝ : n✝ ≤ length l
head✝ : α
tail✝ : List α
l_ih : ∀ {n : ℕ}, n ≤ length tail✝ → insertNth n x tail✝ ~ x :: tail✝
n : ℕ
h : n ≤ length (head✝ :: tail✝)
⊢ insertNth n x (head✝ :: tail✝) ~ x :: head✝ :: tail✝
cases n
case nil.zero
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h✝ : n ≤ length l
h : zero ≤ length []
⊢ insertNth zero x [] ~ [x]

case nil.succ
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h✝ : n ≤ length l
n✝ : ℕ
h : succ n✝ ≤ length []
⊢ insertNth (succ n✝) x [] ~ [x]
case nil
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n✝ : ℕ
h✝ : n✝ ≤ length l
n : ℕ
h : n ≤ length []
⊢ insertNth n x [] ~ [x]
cases n
case nil.succ
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h✝ : n ≤ length l
n✝ : ℕ
h : succ n✝ ≤ length []
⊢ insertNth (succ n✝) x [] ~ [x]
case nil.zero
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h✝ : n ≤ length l
h : zero ≤ length []
⊢ insertNth zero x [] ~ [x]

case nil.succ
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h✝ : n ≤ length l
n✝ : ℕ
h : succ n✝ ≤ length []
⊢ insertNth (succ n✝) x [] ~ [x]
rfl
no goals
case nil.succ
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h✝ : n ≤ length l
n✝ : ℕ
h : succ n✝ ≤ length []
⊢ insertNth (succ n✝) x [] ~ [x]
cases h
no goals
case cons.zero
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h✝ : n ≤ length l
head✝ : α
tail✝ : List α
l_ih : ∀ {n : ℕ}, n ≤ length tail✝ → insertNth n x tail✝ ~ x :: tail✝
h : zero ≤ length (head✝ :: tail✝)
⊢ insertNth zero x (head✝ :: tail✝) ~ x :: head✝ :: tail✝
simp [insertNth]
case cons.succ
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h✝ : n ≤ length l
head✝ : α
tail✝ : List α
l_ih : ∀ {n : ℕ}, n ≤ length tail✝ → insertNth n x tail✝ ~ x :: tail✝
n✝ : ℕ
h : succ n✝ ≤ length (head✝ :: tail✝)
⊢ head✝ :: modifyNthTail (cons x) n✝ tail✝ ~ x :: head✝ :: tail✝
case cons.succ
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h✝ : n ≤ length l
head✝ : α
tail✝ : List α
l_ih : ∀ {n : ℕ}, n ≤ length tail✝ → insertNth n x tail✝ ~ x :: tail✝
n✝ : ℕ
h : succ n✝ ≤ length (head✝ :: tail✝)
⊢ insertNth (succ n✝) x (head✝ :: tail✝) ~ x :: head✝ :: tail✝
simp only [insertNth, modifyNthTail]
case cons.succ.refine'_1
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h✝ : n ≤ length l
head✝ : α
tail✝ : List α
l_ih : ∀ {n : ℕ}, n ≤ length tail✝ → insertNth n x tail✝ ~ x :: tail✝
n✝ : ℕ
h : succ n✝ ≤ length (head✝ :: tail✝)
⊢ n✝ ≤ length tail✝

case cons.succ.refine'_2
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h✝ : n ≤ length l
head✝ : α
tail✝ : List α
l_ih : ∀ {n : ℕ}, n ≤ length tail✝ → insertNth n x tail✝ ~ x :: tail✝
n✝ : ℕ
h : succ n✝ ≤ length (head✝ :: tail✝)
⊢ head✝ :: x :: tail✝ ~ x :: head✝ :: tail✝
case cons.succ
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h✝ : n ≤ length l
head✝ : α
tail✝ : List α
l_ih : ∀ {n : ℕ}, n ≤ length tail✝ → insertNth n x tail✝ ~ x :: tail✝
n✝ : ℕ
h : succ n✝ ≤ length (head✝ :: tail✝)
⊢ head✝ :: modifyNthTail (cons x) n✝ tail✝ ~ x :: head✝ :: tail✝
refine' Perm.trans (Perm.cons _ (l_ih _)) _
no goals
case cons.succ.refine'_1
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h✝ : n ≤ length l
head✝ : α
tail✝ : List α
l_ih : ∀ {n : ℕ}, n ≤ length tail✝ → insertNth n x tail✝ ~ x :: tail✝
n✝ : ℕ
h : succ n✝ ≤ length (head✝ :: tail✝)
⊢ n✝ ≤ length tail✝
apply Nat.le_of_succ_le_succ h
no goals
case cons.succ.refine'_2
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
x : α
l : List α
n : ℕ
h✝ : n ≤ length l
head✝ : α
tail✝ : List α
l_ih : ∀ {n : ℕ}, n ≤ length tail✝ → insertNth n x tail✝ ~ x :: tail✝
n✝ : ℕ
h : succ n✝ ≤ length (head✝ :: tail✝)
⊢ head✝ :: x :: tail✝ ~ x :: head✝ :: tail✝
apply Perm.swap