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

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : α
tail✝¹ x✝³ x✝² : List α
head✝ : β
tail✝ x✝¹ x✝ : List β
f : γ head✝¹ head✝
fs₁ : DVect2 γ tail✝¹ tail✝
fs₂ : DVect2 γ x✝³ x✝¹
fs₃ : DVect2 γ x✝² x✝
⊢ cons f fs₁ ++ fs₂ ++ fs₃ ≡ cons f fs₁ ++ (fs₂ ++ fs₃)
Tactic:
have h_ind := append_assoc fs₁ fs₂ fs₃
State after:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : α
tail✝¹ x✝³ x✝² : List α
head✝ : β
tail✝ x✝¹ x✝ : List β
f : γ head✝¹ head✝
fs₁ : DVect2 γ tail✝¹ tail✝
fs₂ : DVect2 γ x✝³ x✝¹
fs₃ : DVect2 γ x✝² x✝
h_ind : fs₁ ++ fs₂ ++ fs₃ ≡ fs₁ ++ (fs₂ ++ fs₃)
⊢ cons f fs₁ ++ fs₂ ++ fs₃ ≡ cons f fs₁ ++ (fs₂ ++ fs₃)

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : α
tail✝¹ x✝³ x✝² : List α
head✝ : β
tail✝ x✝¹ x✝ : List β
f : γ head✝¹ head✝
fs₁ : DVect2 γ tail✝¹ tail✝
fs₂ : DVect2 γ x✝³ x✝¹
fs₃ : DVect2 γ x✝² x✝
h_ind : fs₁ ++ fs₂ ++ fs₃ ≡ fs₁ ++ (fs₂ ++ fs₃)
⊢ cons f fs₁ ++ fs₂ ++ fs₃ ≡ cons f fs₁ ++ (fs₂ ++ fs₃)
Tactic:
dsimp [HAppend.hAppend, DVect2.append] at *
State after:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : α
tail✝¹ x✝³ x✝² : List α
head✝ : β
tail✝ x✝¹ x✝ : List β
f : γ head✝¹ head✝
fs₁ : DVect2 γ tail✝¹ tail✝
fs₂ : DVect2 γ x✝³ x✝¹
fs₃ : DVect2 γ x✝² x✝
h_ind : append (append fs₁ fs₂) fs₃ ≡ append fs₁ (append fs₂ fs₃)
⊢ cons f (append (append fs₁ fs₂) fs₃) ≡ cons f (append fs₁ (append fs₂ fs₃))

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : α
tail✝¹ x✝³ x✝² : List α
head✝ : β
tail✝ x✝¹ x✝ : List β
f : γ head✝¹ head✝
fs₁ : DVect2 γ tail✝¹ tail✝
fs₂ : DVect2 γ x✝³ x✝¹
fs₃ : DVect2 γ x✝² x✝
h_ind : append (append fs₁ fs₂) fs₃ ≡ append fs₁ (append fs₂ fs₃)
⊢ cons f (append (append fs₁ fs₂) fs₃) ≡ cons f (append fs₁ (append fs₂ fs₃))
Tactic:
exact DVect2.Eq.descend rfl h_ind
State after:
no goals