case nil
ι : Type ?u.122867
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n✝ : ℕ
h✝ : length l < n✝
n : ℕ
h : length [] < n
⊢ insertNth n x [] = []

case cons
ι : Type ?u.122867
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n✝ : ℕ
h✝ : length l < n✝
hd : α
tl : List α
IH : ∀ (n : ℕ), length tl < n → insertNth n x tl = tl
n : ℕ
h : length (hd :: tl) < n
⊢ insertNth n x (hd :: tl) = hd :: tl
ι : Type ?u.122867
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
h : length l < n
⊢ insertNth n x l = l
induction' l with hd tl IH generalizing n
case nil.zero
ι : Type ?u.122867
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
h✝ : length l < n
h : length [] < zero
⊢ insertNth zero x [] = []

case nil.succ
ι : Type ?u.122867
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
h✝ : length l < n
n✝ : ℕ
h : length [] < succ n✝
⊢ insertNth (succ n✝) x [] = []
case nil
ι : Type ?u.122867
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n✝ : ℕ
h✝ : length l < n✝
n : ℕ
h : length [] < n
⊢ insertNth n x [] = []
cases n
no goals
case nil.zero
ι : Type ?u.122867
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
h✝ : length l < n
h : length [] < zero
⊢ insertNth zero x [] = []
simp at h
no goals
case nil.succ
ι : Type ?u.122867
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
h✝ : length l < n
n✝ : ℕ
h : length [] < succ n✝
⊢ insertNth (succ n✝) x [] = []
simp
case cons.zero
ι : Type ?u.122867
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
h✝ : length l < n
hd : α
tl : List α
IH : ∀ (n : ℕ), length tl < n → insertNth n x tl = tl
h : length (hd :: tl) < zero
⊢ insertNth zero x (hd :: tl) = hd :: tl

case cons.succ
ι : Type ?u.122867
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
h✝ : length l < n
hd : α
tl : List α
IH : ∀ (n : ℕ), length tl < n → insertNth n x tl = tl
n✝ : ℕ
h : length (hd :: tl) < succ n✝
⊢ insertNth (succ n✝) x (hd :: tl) = hd :: tl
case cons
ι : Type ?u.122867
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n✝ : ℕ
h✝ : length l < n✝
hd : α
tl : List α
IH : ∀ (n : ℕ), length tl < n → insertNth n x tl = tl
n : ℕ
h : length (hd :: tl) < n
⊢ insertNth n x (hd :: tl) = hd :: tl
cases n
no goals
case cons.zero
ι : Type ?u.122867
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
h✝ : length l < n
hd : α
tl : List α
IH : ∀ (n : ℕ), length tl < n → insertNth n x tl = tl
h : length (hd :: tl) < zero
⊢ insertNth zero x (hd :: tl) = hd :: tl
simp at h
case cons.succ
ι : Type ?u.122867
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
h✝ : length l < n
hd : α
tl : List α
IH : ∀ (n : ℕ), length tl < n → insertNth n x tl = tl
n✝ : ℕ
h : length tl < n✝
⊢ insertNth (succ n✝) x (hd :: tl) = hd :: tl
case cons.succ
ι : Type ?u.122867
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
h✝ : length l < n
hd : α
tl : List α
IH : ∀ (n : ℕ), length tl < n → insertNth n x tl = tl
n✝ : ℕ
h : length (hd :: tl) < succ n✝
⊢ insertNth (succ n✝) x (hd :: tl) = hd :: tl
simp only [Nat.succ_lt_succ_iff, length] at h
no goals
case cons.succ
ι : Type ?u.122867
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
h✝ : length l < n
hd : α
tl : List α
IH : ∀ (n : ℕ), length tl < n → insertNth n x tl = tl
n✝ : ℕ
h : length tl < n✝
⊢ insertNth (succ n✝) x (hd :: tl) = hd :: tl
simpa using IH _ h