Theorem: DVect2.fromList_append (Moncalc/Data/DVect2/Basic.lean)

State before:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
γ : α → α → Type v
f : (a : α) → γ a a
head✝ : α
as bs : List α
⊢ fromList γ f (head✝ :: as ++ bs) = fromList γ f (head✝ :: as) ++ fromList γ f bs
Tactic:
dsimp [fromList]
State after:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
γ : α → α → Type v
f : (a : α) → γ a a
head✝ : α
as bs : List α
⊢ cons (f head✝) (fromList γ f (as ++ bs)) = cons (f head✝) (fromList γ f as) ++ fromList γ f bs

State before:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
γ : α → α → Type v
f : (a : α) → γ a a
head✝ : α
as bs : List α
⊢ cons (f head✝) (fromList γ f (as ++ bs)) = cons (f head✝) (fromList γ f as) ++ fromList γ f bs
Tactic:
rw [cons_append]
State after:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
γ : α → α → Type v
f : (a : α) → γ a a
head✝ : α
as bs : List α
⊢ cons (f head✝) (fromList γ f (as ++ bs)) = cons (f head✝) (fromList γ f as ++ fromList γ f bs)

State before:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
γ : α → α → Type v
f : (a : α) → γ a a
head✝ : α
as bs : List α
⊢ cons (f head✝) (fromList γ f (as ++ bs)) = cons (f head✝) (fromList γ f as ++ fromList γ f bs)
Tactic:
rw [fromList_append γ f (as:=as) (bs:=bs)]
State after:
no goals