case zero
ι : Type ?u.124628
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l✝ : List α
x : α
n k✝ : ℕ
hn✝ : k✝ < n
hk✝ : k✝ < length l✝
hk'✝ : optParam (k✝ < length (insertNth n x l✝)) (_ : k✝ < length (insertNth n x l✝))
l : List α
k : ℕ
hn : k < zero
hk : k < length l
hk' : optParam (k < length (insertNth zero x l)) (_ : k < length (insertNth zero x l))
⊢ get (insertNth zero x l) { val := k, isLt := hk' } = get l { val := k, isLt := hk }

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

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

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