case zero.nil
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
b : β
h : zero + 1 < length (scanl f b [])
⊢ nthLe (scanl f b []) (zero + 1) h =
    f (nthLe (scanl f b []) zero (_ : zero < length (scanl f b []))) (nthLe [] zero (_ : zero < length []))

case zero.cons
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
b : β
head✝ : α
tail✝ : List α
h : zero + 1 < length (scanl f b (head✝ :: tail✝))
⊢ nthLe (scanl f b (head✝ :: tail✝)) (zero + 1) h =
    f (nthLe (scanl f b (head✝ :: tail✝)) zero (_ : zero < length (scanl f b (head✝ :: tail✝))))
      (nthLe (head✝ :: tail✝) zero (_ : zero < length (head✝ :: tail✝)))
case zero
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
b : β
l : List α
h : zero + 1 < length (scanl f b l)
⊢ nthLe (scanl f b l) (zero + 1) h =
    f (nthLe (scanl f b l) zero (_ : zero < length (scanl f b l))) (nthLe l zero (_ : zero < length l))
cases l
no goals
case zero.nil
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
b : β
h : zero + 1 < length (scanl f b [])
⊢ nthLe (scanl f b []) (zero + 1) h =
    f (nthLe (scanl f b []) zero (_ : zero < length (scanl f b []))) (nthLe [] zero (_ : zero < length []))
simp only [length, zero_add, scanl_nil] at h
no goals
case zero.cons
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
b : β
head✝ : α
tail✝ : List α
h : zero + 1 < length (scanl f b (head✝ :: tail✝))
⊢ nthLe (scanl f b (head✝ :: tail✝)) (zero + 1) h =
    f (nthLe (scanl f b (head✝ :: tail✝)) zero (_ : zero < length (scanl f b (head✝ :: tail✝))))
      (nthLe (head✝ :: tail✝) zero (_ : zero < length (head✝ :: tail✝)))
simp [scanl_cons, singleton_append, nthLe_zero_scanl, nthLe_cons]
case succ.nil
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
i : ℕ
hi :
  ∀ {b : β} {l : List α} {h : i + 1 < length (scanl f b l)},
    nthLe (scanl f b l) (i + 1) h =
      f (nthLe (scanl f b l) i (_ : i < length (scanl f b l))) (nthLe l i (_ : i < length l))
b : β
h : succ i + 1 < length (scanl f b [])
⊢ nthLe (scanl f b []) (succ i + 1) h =
    f (nthLe (scanl f b []) (succ i) (_ : succ i < length (scanl f b []))) (nthLe [] (succ i) (_ : succ i < length []))

case succ.cons
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
i : ℕ
hi :
  ∀ {b : β} {l : List α} {h : i + 1 < length (scanl f b l)},
    nthLe (scanl f b l) (i + 1) h =
      f (nthLe (scanl f b l) i (_ : i < length (scanl f b l))) (nthLe l i (_ : i < length l))
b : β
head✝ : α
tail✝ : List α
h : succ i + 1 < length (scanl f b (head✝ :: tail✝))
⊢ nthLe (scanl f b (head✝ :: tail✝)) (succ i + 1) h =
    f (nthLe (scanl f b (head✝ :: tail✝)) (succ i) (_ : succ i < length (scanl f b (head✝ :: tail✝))))
      (nthLe (head✝ :: tail✝) (succ i) (_ : succ i < length (head✝ :: tail✝)))
case succ
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
i : ℕ
hi :
  ∀ {b : β} {l : List α} {h : i + 1 < length (scanl f b l)},
    nthLe (scanl f b l) (i + 1) h =
      f (nthLe (scanl f b l) i (_ : i < length (scanl f b l))) (nthLe l i (_ : i < length l))
b : β
l : List α
h : succ i + 1 < length (scanl f b l)
⊢ nthLe (scanl f b l) (succ i + 1) h =
    f (nthLe (scanl f b l) (succ i) (_ : succ i < length (scanl f b l))) (nthLe l (succ i) (_ : succ i < length l))
cases l
case succ.nil
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
i : ℕ
hi :
  ∀ {b : β} {l : List α} {h : i + 1 < length (scanl f b l)},
    nthLe (scanl f b l) (i + 1) h =
      f (nthLe (scanl f b l) i (_ : i < length (scanl f b l))) (nthLe l i (_ : i < length l))
b : β
h✝ : succ i + 1 < length (scanl f b [])
h : succ i < 0
⊢ nthLe (scanl f b []) (succ i + 1) h✝ =
    f (nthLe (scanl f b []) (succ i) (_ : succ i < length (scanl f b []))) (nthLe [] (succ i) (_ : succ i < length []))
case succ.nil
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
i : ℕ
hi :
  ∀ {b : β} {l : List α} {h : i + 1 < length (scanl f b l)},
    nthLe (scanl f b l) (i + 1) h =
      f (nthLe (scanl f b l) i (_ : i < length (scanl f b l))) (nthLe l i (_ : i < length l))
b : β
h : succ i + 1 < length (scanl f b [])
⊢ nthLe (scanl f b []) (succ i + 1) h =
    f (nthLe (scanl f b []) (succ i) (_ : succ i < length (scanl f b []))) (nthLe [] (succ i) (_ : succ i < length []))
simp only [length, add_lt_iff_neg_right, scanl_nil] at h
no goals
case succ.nil
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
i : ℕ
hi :
  ∀ {b : β} {l : List α} {h : i + 1 < length (scanl f b l)},
    nthLe (scanl f b l) (i + 1) h =
      f (nthLe (scanl f b l) i (_ : i < length (scanl f b l))) (nthLe l i (_ : i < length l))
b : β
h✝ : succ i + 1 < length (scanl f b [])
h : succ i < 0
⊢ nthLe (scanl f b []) (succ i + 1) h✝ =
    f (nthLe (scanl f b []) (succ i) (_ : succ i < length (scanl f b []))) (nthLe [] (succ i) (_ : succ i < length []))
exact absurd h (not_lt_of_lt Nat.succ_pos')
case succ.cons
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
i : ℕ
hi :
  ∀ {b : β} {l : List α} {h : i + 1 < length (scanl f b l)},
    nthLe (scanl f b l) (i + 1) h =
      f (nthLe (scanl f b l) i (_ : i < length (scanl f b l))) (nthLe l i (_ : i < length l))
b : β
head✝ : α
tail✝ : List α
h : succ i + 1 < length (scanl f b (head✝ :: tail✝))
⊢ nthLe ([b] ++ scanl f (f b head✝) tail✝) (succ i + 1) (_ : succ i + 1 < length ([b] ++ scanl f (f b head✝) tail✝)) =
    f (nthLe ([b] ++ scanl f (f b head✝) tail✝) (succ i) (_ : succ i < length ([b] ++ scanl f (f b head✝) tail✝)))
      (nthLe (head✝ :: tail✝) (succ i) (_ : succ i < length (head✝ :: tail✝)))
case succ.cons
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
i : ℕ
hi :
  ∀ {b : β} {l : List α} {h : i + 1 < length (scanl f b l)},
    nthLe (scanl f b l) (i + 1) h =
      f (nthLe (scanl f b l) i (_ : i < length (scanl f b l))) (nthLe l i (_ : i < length l))
b : β
head✝ : α
tail✝ : List α
h : succ i + 1 < length (scanl f b (head✝ :: tail✝))
⊢ nthLe (scanl f b (head✝ :: tail✝)) (succ i + 1) h =
    f (nthLe (scanl f b (head✝ :: tail✝)) (succ i) (_ : succ i < length (scanl f b (head✝ :: tail✝))))
      (nthLe (head✝ :: tail✝) (succ i) (_ : succ i < length (head✝ :: tail✝)))
simp_rw [scanl_cons]
case succ.cons
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
i : ℕ
hi :
  ∀ {b : β} {l : List α} {h : i + 1 < length (scanl f b l)},
    nthLe (scanl f b l) (i + 1) h =
      f (nthLe (scanl f b l) i (_ : i < length (scanl f b l))) (nthLe l i (_ : i < length l))
b : β
head✝ : α
tail✝ : List α
h : succ i + 1 < length (scanl f b (head✝ :: tail✝))
⊢ nthLe (scanl f (f b head✝) tail✝) (succ i + 1 - length [b])
      (_ : succ i + 1 - length [b] < length (scanl f (f b head✝) tail✝)) =
    f (nthLe ([b] ++ scanl f (f b head✝) tail✝) (succ i) (_ : succ i < length ([b] ++ scanl f (f b head✝) tail✝)))
      (nthLe (head✝ :: tail✝) (succ i) (_ : succ i < length (head✝ :: tail✝)))

case succ.cons.h₁
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
i : ℕ
hi :
  ∀ {b : β} {l : List α} {h : i + 1 < length (scanl f b l)},
    nthLe (scanl f b l) (i + 1) h =
      f (nthLe (scanl f b l) i (_ : i < length (scanl f b l))) (nthLe l i (_ : i < length l))
b : β
head✝ : α
tail✝ : List α
h : succ i + 1 < length (scanl f b (head✝ :: tail✝))
⊢ length [b] ≤ succ i + 1
case succ.cons
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
i : ℕ
hi :
  ∀ {b : β} {l : List α} {h : i + 1 < length (scanl f b l)},
    nthLe (scanl f b l) (i + 1) h =
      f (nthLe (scanl f b l) i (_ : i < length (scanl f b l))) (nthLe l i (_ : i < length l))
b : β
head✝ : α
tail✝ : List α
h : succ i + 1 < length (scanl f b (head✝ :: tail✝))
⊢ nthLe ([b] ++ scanl f (f b head✝) tail✝) (succ i + 1) (_ : succ i + 1 < length ([b] ++ scanl f (f b head✝) tail✝)) =
    f (nthLe ([b] ++ scanl f (f b head✝) tail✝) (succ i) (_ : succ i < length ([b] ++ scanl f (f b head✝) tail✝)))
      (nthLe (head✝ :: tail✝) (succ i) (_ : succ i < length (head✝ :: tail✝)))
rw [nthLe_append_right]
case succ.cons
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
i : ℕ
hi :
  ∀ {b : β} {l : List α} {h : i + 1 < length (scanl f b l)},
    nthLe (scanl f b l) (i + 1) h =
      f (nthLe (scanl f b l) i (_ : i < length (scanl f b l))) (nthLe l i (_ : i < length l))
b : β
head✝ : α
tail✝ : List α
h : succ i + 1 < length (scanl f b (head✝ :: tail✝))
⊢ f (nthLe (scanl f (f b head✝) tail✝) i (_ : i < length (scanl f (f b head✝) tail✝)))
      (nthLe tail✝ i (_ : i < length tail✝)) =
    f (nthLe ([b] ++ scanl f (f b head✝) tail✝) (succ i) (_ : succ i < length ([b] ++ scanl f (f b head✝) tail✝)))
      (nthLe (head✝ :: tail✝) (succ i) (_ : succ i < length (head✝ :: tail✝)))
case succ.cons
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
i : ℕ
hi :
  ∀ {b : β} {l : List α} {h : i + 1 < length (scanl f b l)},
    nthLe (scanl f b l) (i + 1) h =
      f (nthLe (scanl f b l) i (_ : i < length (scanl f b l))) (nthLe l i (_ : i < length l))
b : β
head✝ : α
tail✝ : List α
h : succ i + 1 < length (scanl f b (head✝ :: tail✝))
⊢ nthLe (scanl f (f b head✝) tail✝) (succ i + 1 - length [b])
      (_ : succ i + 1 - length [b] < length (scanl f (f b head✝) tail✝)) =
    f (nthLe ([b] ++ scanl f (f b head✝) tail✝) (succ i) (_ : succ i < length ([b] ++ scanl f (f b head✝) tail✝)))
      (nthLe (head✝ :: tail✝) (succ i) (_ : succ i < length (head✝ :: tail✝)))
simp only [length, zero_add 1, succ_add_sub_one, hi]
no goals
case succ.cons
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
i : ℕ
hi :
  ∀ {b : β} {l : List α} {h : i + 1 < length (scanl f b l)},
    nthLe (scanl f b l) (i + 1) h =
      f (nthLe (scanl f b l) i (_ : i < length (scanl f b l))) (nthLe l i (_ : i < length l))
b : β
head✝ : α
tail✝ : List α
h : succ i + 1 < length (scanl f b (head✝ :: tail✝))
⊢ f (nthLe (scanl f (f b head✝) tail✝) i (_ : i < length (scanl f (f b head✝) tail✝)))
      (nthLe tail✝ i (_ : i < length tail✝)) =
    f (nthLe ([b] ++ scanl f (f b head✝) tail✝) (succ i) (_ : succ i < length ([b] ++ scanl f (f b head✝) tail✝)))
      (nthLe (head✝ :: tail✝) (succ i) (_ : succ i < length (head✝ :: tail✝)))
rfl
no goals
case succ.cons.h₁
ι : Type ?u.243601
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
a : α
i : ℕ
hi :
  ∀ {b : β} {l : List α} {h : i + 1 < length (scanl f b l)},
    nthLe (scanl f b l) (i + 1) h =
      f (nthLe (scanl f b l) i (_ : i < length (scanl f b l))) (nthLe l i (_ : i < length l))
b : β
head✝ : α
tail✝ : List α
h : succ i + 1 < length (scanl f b (head✝ :: tail✝))
⊢ length [b] ≤ succ i + 1
simp only [length, Nat.zero_le, le_add_iff_nonneg_left]