no goals
ι : Type ?u.125684
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn : n ≤ length l
⊢ n < length (insertNth n x l)
rwa [length_insertNth _ _ hn, Nat.lt_succ_iff]
case nil
ι : Type ?u.125684
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n✝ : ℕ
hn✝ : n✝ ≤ length l
hn'✝ : optParam (n✝ < length (insertNth n✝ x l)) (_ : n✝ < length (insertNth n✝ x l))
n : ℕ
hn : n ≤ length []
hn' : optParam (n < length (insertNth n x [])) (_ : n < length (insertNth n x []))
⊢ get (insertNth n x []) { val := n, isLt := hn' } = x

case cons
ι : Type ?u.125684
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n✝ : ℕ
hn✝ : n✝ ≤ length l
hn'✝ : optParam (n✝ < length (insertNth n✝ x l)) (_ : n✝ < length (insertNth n✝ x l))
hd : α
tl : List α
IH :
  ∀ (n : ℕ) (hn : n ≤ length tl) (hn' : optParam (n < length (insertNth n x tl)) (_ : n < length (insertNth n x tl))),
    get (insertNth n x tl) { val := n, isLt := hn' } = x
n : ℕ
hn : n ≤ length (hd :: tl)
hn' : optParam (n < length (insertNth n x (hd :: tl))) (_ : n < length (insertNth n x (hd :: tl)))
⊢ get (insertNth n x (hd :: tl)) { val := n, isLt := hn' } = x
ι : Type ?u.125684
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn : n ≤ length l
hn' : optParam (n < length (insertNth n x l)) (_ : n < length (insertNth n x l))
⊢ get (insertNth n x l) { val := n, isLt := hn' } = x
induction' l with hd tl IH generalizing n
case nil
ι : Type ?u.125684
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n✝ : ℕ
hn✝¹ : n✝ ≤ length l
hn'✝ : optParam (n✝ < length (insertNth n✝ x l)) (_ : n✝ < length (insertNth n✝ x l))
n : ℕ
hn✝ : n ≤ length []
hn' : optParam (n < length (insertNth n x [])) (_ : n < length (insertNth n x []))
hn : n = 0
⊢ get (insertNth n x []) { val := n, isLt := hn' } = x
case nil
ι : Type ?u.125684
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n✝ : ℕ
hn✝ : n✝ ≤ length l
hn'✝ : optParam (n✝ < length (insertNth n✝ x l)) (_ : n✝ < length (insertNth n✝ x l))
n : ℕ
hn : n ≤ length []
hn' : optParam (n < length (insertNth n x [])) (_ : n < length (insertNth n x []))
⊢ get (insertNth n x []) { val := n, isLt := hn' } = x
simp only [length, nonpos_iff_eq_zero] at hn
case nil.refl
ι : Type ?u.125684
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn✝ : n ≤ length l
hn'✝ : optParam (n < length (insertNth n x l)) (_ : n < length (insertNth n x l))
hn : 0 ≤ length []
hn' : optParam (0 < length (insertNth 0 x [])) (_ : 0 < length (insertNth 0 x []))
⊢ get (insertNth 0 x []) { val := 0, isLt := hn' } = x
case nil
ι : Type ?u.125684
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n✝ : ℕ
hn✝¹ : n✝ ≤ length l
hn'✝ : optParam (n✝ < length (insertNth n✝ x l)) (_ : n✝ < length (insertNth n✝ x l))
n : ℕ
hn✝ : n ≤ length []
hn' : optParam (n < length (insertNth n x [])) (_ : n < length (insertNth n x []))
hn : n = 0
⊢ get (insertNth n x []) { val := n, isLt := hn' } = x
cases hn
no goals
case nil.refl
ι : Type ?u.125684
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn✝ : n ≤ length l
hn'✝ : optParam (n < length (insertNth n x l)) (_ : n < length (insertNth n x l))
hn : 0 ≤ length []
hn' : optParam (0 < length (insertNth 0 x [])) (_ : 0 < length (insertNth 0 x []))
⊢ get (insertNth 0 x []) { val := 0, isLt := hn' } = x
simp only [insertNth_zero, get_singleton]
case cons.zero
ι : Type ?u.125684
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn✝ : n ≤ length l
hn'✝ : optParam (n < length (insertNth n x l)) (_ : n < length (insertNth n x l))
hd : α
tl : List α
IH :
  ∀ (n : ℕ) (hn : n ≤ length tl) (hn' : optParam (n < length (insertNth n x tl)) (_ : n < length (insertNth n x tl))),
    get (insertNth n x tl) { val := n, isLt := hn' } = x
hn : zero ≤ length (hd :: tl)
hn' : optParam (zero < length (insertNth zero x (hd :: tl))) (_ : zero < length (insertNth zero x (hd :: tl)))
⊢ get (insertNth zero x (hd :: tl)) { val := zero, isLt := hn' } = x

case cons.succ
ι : Type ?u.125684
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn✝ : n ≤ length l
hn'✝ : optParam (n < length (insertNth n x l)) (_ : n < length (insertNth n x l))
hd : α
tl : List α
IH :
  ∀ (n : ℕ) (hn : n ≤ length tl) (hn' : optParam (n < length (insertNth n x tl)) (_ : n < length (insertNth n x tl))),
    get (insertNth n x tl) { val := n, isLt := hn' } = x
n✝ : ℕ
hn : succ n✝ ≤ length (hd :: tl)
hn' :
  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 := hn' } = x
case cons
ι : Type ?u.125684
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n✝ : ℕ
hn✝ : n✝ ≤ length l
hn'✝ : optParam (n✝ < length (insertNth n✝ x l)) (_ : n✝ < length (insertNth n✝ x l))
hd : α
tl : List α
IH :
  ∀ (n : ℕ) (hn : n ≤ length tl) (hn' : optParam (n < length (insertNth n x tl)) (_ : n < length (insertNth n x tl))),
    get (insertNth n x tl) { val := n, isLt := hn' } = x
n : ℕ
hn : n ≤ length (hd :: tl)
hn' : optParam (n < length (insertNth n x (hd :: tl))) (_ : n < length (insertNth n x (hd :: tl)))
⊢ get (insertNth n x (hd :: tl)) { val := n, isLt := hn' } = x
cases n
no goals
case cons.zero
ι : Type ?u.125684
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn✝ : n ≤ length l
hn'✝ : optParam (n < length (insertNth n x l)) (_ : n < length (insertNth n x l))
hd : α
tl : List α
IH :
  ∀ (n : ℕ) (hn : n ≤ length tl) (hn' : optParam (n < length (insertNth n x tl)) (_ : n < length (insertNth n x tl))),
    get (insertNth n x tl) { val := n, isLt := hn' } = x
hn : zero ≤ length (hd :: tl)
hn' : optParam (zero < length (insertNth zero x (hd :: tl))) (_ : zero < length (insertNth zero x (hd :: tl)))
⊢ get (insertNth zero x (hd :: tl)) { val := zero, isLt := hn' } = x
simp
case cons.succ
ι : Type ?u.125684
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn✝¹ : n ≤ length l
hn'✝ : optParam (n < length (insertNth n x l)) (_ : n < length (insertNth n x l))
hd : α
tl : List α
IH :
  ∀ (n : ℕ) (hn : n ≤ length tl) (hn' : optParam (n < length (insertNth n x tl)) (_ : n < length (insertNth n x tl))),
    get (insertNth n x tl) { val := n, isLt := hn' } = x
n✝ : ℕ
hn✝ : succ n✝ ≤ length (hd :: tl)
hn' :
  optParam (succ n✝ < length (insertNth (succ n✝) x (hd :: tl)))
    (_ : succ n✝ < length (insertNth (succ n✝) x (hd :: tl)))
hn : n✝ ≤ length tl
⊢ get (insertNth (succ n✝) x (hd :: tl)) { val := succ n✝, isLt := hn' } = x
case cons.succ
ι : Type ?u.125684
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn✝ : n ≤ length l
hn'✝ : optParam (n < length (insertNth n x l)) (_ : n < length (insertNth n x l))
hd : α
tl : List α
IH :
  ∀ (n : ℕ) (hn : n ≤ length tl) (hn' : optParam (n < length (insertNth n x tl)) (_ : n < length (insertNth n x tl))),
    get (insertNth n x tl) { val := n, isLt := hn' } = x
n✝ : ℕ
hn : succ n✝ ≤ length (hd :: tl)
hn' :
  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 := hn' } = x
simp only [Nat.succ_le_succ_iff, length] at hn
no goals
case cons.succ
ι : Type ?u.125684
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
x : α
n : ℕ
hn✝¹ : n ≤ length l
hn'✝ : optParam (n < length (insertNth n x l)) (_ : n < length (insertNth n x l))
hd : α
tl : List α
IH :
  ∀ (n : ℕ) (hn : n ≤ length tl) (hn' : optParam (n < length (insertNth n x tl)) (_ : n < length (insertNth n x tl))),
    get (insertNth n x tl) { val := n, isLt := hn' } = x
n✝ : ℕ
hn✝ : succ n✝ ≤ length (hd :: tl)
hn' :
  optParam (succ n✝ < length (insertNth (succ n✝) x (hd :: tl)))
    (_ : succ n✝ < length (insertNth (succ n✝) x (hd :: tl)))
hn : n✝ ≤ length tl
⊢ get (insertNth (succ n✝) x (hd :: tl)) { val := succ n✝, isLt := hn' } = x
simpa using IH _ hn