ι : Type ?u.126934
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < length l
⊢ n + k + 1 < length l + 1
ι : Type ?u.126934
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < length l
⊢ n + k + 1 < length (insertNth n x l)
rw [length_insertNth _ _ (le_self_add.trans hk'.le)]
no goals
ι : Type ?u.126934
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < length l
⊢ n + k + 1 < length l + 1
exact Nat.succ_lt_succ_iff.2 hk'
case nil
ι : Type ?u.126934
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n✝ k✝ : ℕ
hk'✝ : n✝ + k✝ < length l
hk✝ : optParam (n✝ + k✝ + 1 < length (insertNth n✝ x l)) (_ : n✝ + k✝ + 1 < length (insertNth n✝ x l))
n k : ℕ
hk' : n + k < length []
hk : optParam (n + k + 1 < length (insertNth n x [])) (_ : n + k + 1 < length (insertNth n x []))
⊢ get (insertNth n x []) { val := n + k + 1, isLt := hk } = get [] { val := n + k, isLt := hk' }

case cons
ι : Type ?u.126934
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n✝ k✝ : ℕ
hk'✝ : n✝ + k✝ < length l
hk✝ : optParam (n✝ + k✝ + 1 < length (insertNth n✝ x l)) (_ : n✝ + k✝ + 1 < length (insertNth n✝ x l))
hd : α
tl : List α
IH :
  ∀ (n k : ℕ) (hk' : n + k < length tl)
    (hk : optParam (n + k + 1 < length (insertNth n x tl)) (_ : n + k + 1 < length (insertNth n x tl))),
    get (insertNth n x tl) { val := n + k + 1, isLt := hk } = get tl { val := n + k, isLt := hk' }
n k : ℕ
hk' : n + k < length (hd :: tl)
hk : optParam (n + k + 1 < length (insertNth n x (hd :: tl))) (_ : n + k + 1 < length (insertNth n x (hd :: tl)))
⊢ get (insertNth n x (hd :: tl)) { val := n + k + 1, isLt := hk } = get (hd :: tl) { val := n + k, isLt := hk' }
ι : Type ?u.126934
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < length l
hk : optParam (n + k + 1 < length (insertNth n x l)) (_ : n + k + 1 < length (insertNth n x l))
⊢ get (insertNth n x l) { val := n + k + 1, isLt := hk } = get l { val := n + k, isLt := hk' }
induction' l with hd tl IH generalizing n k
no goals
case nil
ι : Type ?u.126934
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n✝ k✝ : ℕ
hk'✝ : n✝ + k✝ < length l
hk✝ : optParam (n✝ + k✝ + 1 < length (insertNth n✝ x l)) (_ : n✝ + k✝ + 1 < length (insertNth n✝ x l))
n k : ℕ
hk' : n + k < length []
hk : optParam (n + k + 1 < length (insertNth n x [])) (_ : n + k + 1 < length (insertNth n x []))
⊢ get (insertNth n x []) { val := n + k + 1, isLt := hk } = get [] { val := n + k, isLt := hk' }
simp at hk'
case cons.zero
ι : Type ?u.126934
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n k✝ : ℕ
hk'✝ : n + k✝ < length l
hk✝ : optParam (n + k✝ + 1 < length (insertNth n x l)) (_ : n + k✝ + 1 < length (insertNth n x l))
hd : α
tl : List α
IH :
  ∀ (n k : ℕ) (hk' : n + k < length tl)
    (hk : optParam (n + k + 1 < length (insertNth n x tl)) (_ : n + k + 1 < length (insertNth n x tl))),
    get (insertNth n x tl) { val := n + k + 1, isLt := hk } = get tl { val := n + k, isLt := hk' }
k : ℕ
hk' : zero + k < length (hd :: tl)
hk :
  optParam (zero + k + 1 < length (insertNth zero x (hd :: tl)))
    (_ : zero + k + 1 < length (insertNth zero x (hd :: tl)))
⊢ get (insertNth zero x (hd :: tl)) { val := zero + k + 1, isLt := hk } =
    get (hd :: tl) { val := zero + k, isLt := hk' }

case cons.succ
ι : Type ?u.126934
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n k✝ : ℕ
hk'✝ : n + k✝ < length l
hk✝ : optParam (n + k✝ + 1 < length (insertNth n x l)) (_ : n + k✝ + 1 < length (insertNth n x l))
hd : α
tl : List α
IH :
  ∀ (n k : ℕ) (hk' : n + k < length tl)
    (hk : optParam (n + k + 1 < length (insertNth n x tl)) (_ : n + k + 1 < length (insertNth n x tl))),
    get (insertNth n x tl) { val := n + k + 1, isLt := hk } = get tl { val := n + k, isLt := hk' }
k n✝ : ℕ
hk' : succ n✝ + k < length (hd :: tl)
hk :
  optParam (succ n✝ + k + 1 < length (insertNth (succ n✝) x (hd :: tl)))
    (_ : succ n✝ + k + 1 < length (insertNth (succ n✝) x (hd :: tl)))
⊢ get (insertNth (succ n✝) x (hd :: tl)) { val := succ n✝ + k + 1, isLt := hk } =
    get (hd :: tl) { val := succ n✝ + k, isLt := hk' }
case cons
ι : Type ?u.126934
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n✝ k✝ : ℕ
hk'✝ : n✝ + k✝ < length l
hk✝ : optParam (n✝ + k✝ + 1 < length (insertNth n✝ x l)) (_ : n✝ + k✝ + 1 < length (insertNth n✝ x l))
hd : α
tl : List α
IH :
  ∀ (n k : ℕ) (hk' : n + k < length tl)
    (hk : optParam (n + k + 1 < length (insertNth n x tl)) (_ : n + k + 1 < length (insertNth n x tl))),
    get (insertNth n x tl) { val := n + k + 1, isLt := hk } = get tl { val := n + k, isLt := hk' }
n k : ℕ
hk' : n + k < length (hd :: tl)
hk : optParam (n + k + 1 < length (insertNth n x (hd :: tl))) (_ : n + k + 1 < length (insertNth n x (hd :: tl)))
⊢ get (insertNth n x (hd :: tl)) { val := n + k + 1, isLt := hk } = get (hd :: tl) { val := n + k, isLt := hk' }
cases n
no goals
case cons.zero
ι : Type ?u.126934
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n k✝ : ℕ
hk'✝ : n + k✝ < length l
hk✝ : optParam (n + k✝ + 1 < length (insertNth n x l)) (_ : n + k✝ + 1 < length (insertNth n x l))
hd : α
tl : List α
IH :
  ∀ (n k : ℕ) (hk' : n + k < length tl)
    (hk : optParam (n + k + 1 < length (insertNth n x tl)) (_ : n + k + 1 < length (insertNth n x tl))),
    get (insertNth n x tl) { val := n + k + 1, isLt := hk } = get tl { val := n + k, isLt := hk' }
k : ℕ
hk' : zero + k < length (hd :: tl)
hk :
  optParam (zero + k + 1 < length (insertNth zero x (hd :: tl)))
    (_ : zero + k + 1 < length (insertNth zero x (hd :: tl)))
⊢ get (insertNth zero x (hd :: tl)) { val := zero + k + 1, isLt := hk } =
    get (hd :: tl) { val := zero + k, isLt := hk' }
simp
no goals
case cons.succ
ι : Type ?u.126934
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n k✝ : ℕ
hk'✝ : n + k✝ < length l
hk✝ : optParam (n + k✝ + 1 < length (insertNth n x l)) (_ : n + k✝ + 1 < length (insertNth n x l))
hd : α
tl : List α
IH :
  ∀ (n k : ℕ) (hk' : n + k < length tl)
    (hk : optParam (n + k + 1 < length (insertNth n x tl)) (_ : n + k + 1 < length (insertNth n x tl))),
    get (insertNth n x tl) { val := n + k + 1, isLt := hk } = get tl { val := n + k, isLt := hk' }
k n✝ : ℕ
hk' : succ n✝ + k < length (hd :: tl)
hk :
  optParam (succ n✝ + k + 1 < length (insertNth (succ n✝) x (hd :: tl)))
    (_ : succ n✝ + k + 1 < length (insertNth (succ n✝) x (hd :: tl)))
⊢ get (insertNth (succ n✝) x (hd :: tl)) { val := succ n✝ + k + 1, isLt := hk } =
    get (hd :: tl) { val := succ n✝ + k, isLt := hk' }
simpa [succ_add] using IH _ _ _