no goals
α : Type u
β : Type v
γ : Type w
f : α → β
as : List α
bs : List β
⊢ mapTR.loop f as bs = reverse bs ++ map f as
induction as generalizing bs with
| nil => simp [mapTR.loop, map]
| cons a as ih =>
  simp [mapTR.loop, map]
  rw [ih (f a :: bs), reverse_cons, append_assoc]
  rfl
no goals
case nil
α : Type u
β : Type v
γ : Type w
f : α → β
bs : List β
⊢ mapTR.loop f nil bs = reverse bs ++ map f nil
simp [mapTR.loop, map]
case cons
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
as : List α
ih : ∀ (bs : List β), mapTR.loop f as bs = reverse bs ++ map f as
bs : List β
⊢ mapTR.loop f as (f a :: bs) = reverse bs ++ f a :: map f as
case cons
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
as : List α
ih : ∀ (bs : List β), mapTR.loop f as bs = reverse bs ++ map f as
bs : List β
⊢ mapTR.loop f (a :: as) bs = reverse bs ++ map f (a :: as)
simp [mapTR.loop, map]
case cons
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
as : List α
ih : ∀ (bs : List β), mapTR.loop f as bs = reverse bs ++ map f as
bs : List β
⊢ reverse bs ++ (f a :: nil ++ map f as) = reverse bs ++ f a :: map f as
case cons
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
as : List α
ih : ∀ (bs : List β), mapTR.loop f as bs = reverse bs ++ map f as
bs : List β
⊢ mapTR.loop f as (f a :: bs) = reverse bs ++ f a :: map f as
rw [ih (f a :: bs), reverse_cons, append_assoc]
no goals
case cons
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
as : List α
ih : ∀ (bs : List β), mapTR.loop f as bs = reverse bs ++ map f as
bs : List β
⊢ reverse bs ++ (f a :: nil ++ map f as) = reverse bs ++ f a :: map f as
rfl