α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : AddGroup α
as : List α
⊢ map (fun a => Sub.sub a default) as = as
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : AddGroup α
as : List α
⊢ sub as [] = as
rw [sub, @pointwise_nil _ _ _ ⟨0⟩ ⟨0⟩]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : AddGroup α
as : List α
⊢ map (fun a => Sub.sub a default) as = map id as
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : AddGroup α
as : List α
⊢ map (fun a => Sub.sub a default) as = as
apply Eq.trans _ (map_id as)
case e_f.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : AddGroup α
as : List α
x : α
⊢ Sub.sub x default = id x
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : AddGroup α
as : List α
⊢ map (fun a => Sub.sub a default) as = map id as
congr with x
no goals
case e_f.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝ : AddGroup α
as : List α
x : α
⊢ Sub.sub x default = id x
exact sub_zero x