ι : Type ?u.247779
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β → β
b : β
a : α
l : List α
⊢ f a (foldr (fun a x => (f a x.fst, x.fst :: x.snd)) (b, []) l).fst = f a (foldr f b l)
ι : Type ?u.247779
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β → β
b : β
a : α
l : List α
⊢ scanr f b (a :: l) = foldr f b (a :: l) :: scanr f b l
simp only [scanr, foldr, cons.injEq, and_true]
no goals
ι : Type ?u.247779
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β → β
b : β
a : α
l : List α
⊢ f a (foldr (fun a x => (f a x.fst, x.fst :: x.snd)) (b, []) l).fst = f a (foldr f b l)
induction l generalizing a with
| nil => rfl
| cons hd tl ih => simp only [foldr, ih]
no goals
case nil
ι : Type ?u.247779
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β → β
b : β
a : α
⊢ f a (foldr (fun a x => (f a x.fst, x.fst :: x.snd)) (b, []) []).fst = f a (foldr f b [])
rfl
no goals
case cons
ι : Type ?u.247779
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β → β
b : β
hd : α
tl : List α
ih : ∀ (a : α), f a (foldr (fun a x => (f a x.fst, x.fst :: x.snd)) (b, []) tl).fst = f a (foldr f b tl)
a : α
⊢ f a (foldr (fun a x => (f a x.fst, x.fst :: x.snd)) (b, []) (hd :: tl)).fst = f a (foldr f b (hd :: tl))
simp only [foldr, ih]