α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
⊢ (foldl (fun l x => { down := l.down + 1 }) { down := 0 } xs).down = List.length (toList xs)
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
⊢ length xs = List.length (toList xs)
unfold length
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } (toList xs)).down = List.length (toList xs)
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
⊢ (foldl (fun l x => { down := l.down + 1 }) { down := 0 } xs).down = List.length (toList xs)
rw [foldl_toList]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } ys).down = List.length ys
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } (toList xs)).down = List.length (toList xs)
generalize toList xs = ys
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } ys).down = List.length ys + 0
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } ys).down = List.length ys
rw [← Nat.add_zero ys.length]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
ys : List α
n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } ys).down = List.length ys + n
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } ys).down = List.length ys + 0
generalize 0 = n
case nil
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
n✝ n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } []).down = List.length [] + n

case cons
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
n✝ : ℕ
head✝ : α
tail✝ : List α
ih : ∀ (n : ℕ), (List.foldl (fun l x => { down := l.down + 1 }) { down := n } tail✝).down = List.length tail✝ + n
n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } (head✝ :: tail✝)).down =
    List.length (head✝ :: tail✝) + n
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
ys : List α
n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } ys).down = List.length ys + n
induction' ys with _ _ ih generalizing n
case cons
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
n✝ : ℕ
head✝ : α
tail✝ : List α
ih : ∀ (n : ℕ), (List.foldl (fun l x => { down := l.down + 1 }) { down := n } tail✝).down = List.length tail✝ + n
n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } (head✝ :: tail✝)).down =
    List.length (head✝ :: tail✝) + n
case nil
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
n✝ n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } []).down = List.length [] + n

case cons
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
n✝ : ℕ
head✝ : α
tail✝ : List α
ih : ∀ (n : ℕ), (List.foldl (fun l x => { down := l.down + 1 }) { down := n } tail✝).down = List.length tail✝ + n
n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } (head✝ :: tail✝)).down =
    List.length (head✝ :: tail✝) + n
. simp
no goals
case cons
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
n✝ : ℕ
head✝ : α
tail✝ : List α
ih : ∀ (n : ℕ), (List.foldl (fun l x => { down := l.down + 1 }) { down := n } tail✝).down = List.length tail✝ + n
n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } (head✝ :: tail✝)).down =
    List.length (head✝ :: tail✝) + n
. simp_arith [ih]
no goals
case nil
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
n✝ n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } []).down = List.length [] + n
simp
no goals
case cons
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
n✝ : ℕ
head✝ : α
tail✝ : List α
ih : ∀ (n : ℕ), (List.foldl (fun l x => { down := l.down + 1 }) { down := n } tail✝).down = List.length tail✝ + n
n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } (head✝ :: tail✝)).down =
    List.length (head✝ :: tail✝) + n
simp_arith [ih]