case inl
ι : Type ?u.123956
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn : n ≤ length l
⊢ length l ≤ length (insertNth n x l)

case inr
ι : Type ?u.123956
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn : length l < n
⊢ length l ≤ length (insertNth n x l)
ι : Type ?u.123956
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
⊢ length l ≤ length (insertNth n x l)
cases' le_or_lt n l.length with hn hn
case inl
ι : Type ?u.123956
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn : n ≤ length l
⊢ length l ≤ length l + 1
case inl
ι : Type ?u.123956
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn : n ≤ length l
⊢ length l ≤ length (insertNth n x l)
rw [length_insertNth _ _ hn]
no goals
case inl
ι : Type ?u.123956
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn : n ≤ length l
⊢ length l ≤ length l + 1
exact (Nat.lt_succ_self _).le
no goals
case inr
ι : Type ?u.123956
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn : length l < n
⊢ length l ≤ length (insertNth n x l)
rw [insertNth_of_length_lt _ _ _ hn]