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

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

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

State before:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
β₁ : Type u₁
β₂ : Type u₂
γ : β₁ → β₂ → Type v
f₁ : α → β₁
f₂ : α → β₂
g : (a : α) → γ (f₁ a) (f₂ a)
a : α
as bs : List α
⊢ cons (g a) (dfromList f₁ f₂ g (as ++ bs)) ≡ cons (g a) (dfromList f₁ f₂ g as ++ dfromList f₁ f₂ g bs)
Tactic:
apply DVect2.Eq.descend rfl
State after:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
β₁ : Type u₁
β₂ : Type u₂
γ : β₁ → β₂ → Type v
f₁ : α → β₁
f₂ : α → β₂
g : (a : α) → γ (f₁ a) (f₂ a)
a : α
as bs : List α
⊢ dfromList f₁ f₂ g (as ++ bs) ≡ dfromList f₁ f₂ g as ++ dfromList f₁ f₂ g bs

State before:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
β₁ : Type u₁
β₂ : Type u₂
γ : β₁ → β₂ → Type v
f₁ : α → β₁
f₂ : α → β₂
g : (a : α) → γ (f₁ a) (f₂ a)
a : α
as bs : List α
⊢ dfromList f₁ f₂ g (as ++ bs) ≡ dfromList f₁ f₂ g as ++ dfromList f₁ f₂ g bs
Tactic:
exact dfromList_append f₁ f₂ g (as:=as) (bs:=bs)
State after:
no goals