no goals
ι : Type ?u.117403
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a✝ a b : α
j : ℕ
l : List α
⊢ 0 ≤ j → j ≤ length l → insertNth (j + 1) b (insertNth 0 a l) = insertNth 0 a (insertNth j b l)
simp [insertNth]
no goals
ι : Type ?u.117403
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a✝ a b : α
i j : ℕ
⊢ i + 1 ≤ j + 1 →
    j + 1 ≤ length [] → insertNth (j + 1 + 1) b (insertNth (i + 1) a []) = insertNth (i + 1) a (insertNth (j + 1) b [])
simp
ι : Type ?u.117403
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a✝ a b : α
i j : ℕ
c : α
l : List α
h₀ : i + 1 ≤ j + 1
h₁ : j + 1 ≤ length (c :: l)
⊢ modifyNthTail (cons b) (j + 1) (modifyNthTail (cons a) i l) = modifyNthTail (cons a) i (modifyNthTail (cons b) j l)
ι : Type ?u.117403
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a✝ a b : α
i j : ℕ
c : α
l : List α
h₀ : i + 1 ≤ j + 1
h₁ : j + 1 ≤ length (c :: l)
⊢ insertNth (j + 1 + 1) b (insertNth (i + 1) a (c :: l)) = insertNth (i + 1) a (insertNth (j + 1) b (c :: l))
simp [insertNth]
no goals
ι : Type ?u.117403
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a✝ a b : α
i j : ℕ
c : α
l : List α
h₀ : i + 1 ≤ j + 1
h₁ : j + 1 ≤ length (c :: l)
⊢ modifyNthTail (cons b) (j + 1) (modifyNthTail (cons a) i l) = modifyNthTail (cons a) i (modifyNthTail (cons b) j l)
exact insertNth_comm a b i j l (Nat.le_of_succ_le_succ h₀) (Nat.le_of_succ_le_succ h₁)