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

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
α₁ : Type u_1
β₁ : Type u_2
γ₁ : α₁ → β₁ → Type u_3
f : α → α₁
g : β → β₁
h : {a : α} → {b : β} → γ a b → γ₁ (f a) (g b)
head✝¹ : α
tail✝¹ x✝¹ : List α
head✝ : β
tail✝ x✝ : List β
a✝ : γ head✝¹ head✝
xs₁ : DVect2 γ tail✝¹ tail✝
xs₂ : DVect2 γ x✝¹ x✝
⊢ map f g (fun {a} {b} ↦ h) (cons a✝ xs₁ ++ xs₂) ≡
    map f g (fun {a} {b} ↦ h) (cons a✝ xs₁) ++ map f g (fun {a} {b} ↦ h) xs₂
Tactic:
dsimp [map]
State after:
α : Type u₁
β : Type u₂
γ : α → β → Type v
α₁ : Type u_1
β₁ : Type u_2
γ₁ : α₁ → β₁ → Type u_3
f : α → α₁
g : β → β₁
h : {a : α} → {b : β} → γ a b → γ₁ (f a) (g b)
head✝¹ : α
tail✝¹ x✝¹ : List α
head✝ : β
tail✝ x✝ : List β
a✝ : γ head✝¹ head✝
xs₁ : DVect2 γ tail✝¹ tail✝
xs₂ : DVect2 γ x✝¹ x✝
⊢ cons (h a✝) (map f g (fun {a} {b} ↦ h) (append xs₁ xs₂)) ≡
    cons (h a✝) (map f g (fun {a} {b} ↦ h) xs₁) ++ map f g (fun {a} {b} ↦ h) xs₂

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
α₁ : Type u_1
β₁ : Type u_2
γ₁ : α₁ → β₁ → Type u_3
f : α → α₁
g : β → β₁
h : {a : α} → {b : β} → γ a b → γ₁ (f a) (g b)
head✝¹ : α
tail✝¹ x✝¹ : List α
head✝ : β
tail✝ x✝ : List β
a✝ : γ head✝¹ head✝
xs₁ : DVect2 γ tail✝¹ tail✝
xs₂ : DVect2 γ x✝¹ x✝
⊢ cons (h a✝) (map f g (fun {a} {b} ↦ h) (append xs₁ xs₂)) ≡
    cons (h a✝) (map f g (fun {a} {b} ↦ h) xs₁) ++ map f g (fun {a} {b} ↦ h) xs₂
Tactic:
apply DVect2.Eq.descend rfl
State after:
α : Type u₁
β : Type u₂
γ : α → β → Type v
α₁ : Type u_1
β₁ : Type u_2
γ₁ : α₁ → β₁ → Type u_3
f : α → α₁
g : β → β₁
h : {a : α} → {b : β} → γ a b → γ₁ (f a) (g b)
head✝¹ : α
tail✝¹ x✝¹ : List α
head✝ : β
tail✝ x✝ : List β
a✝ : γ head✝¹ head✝
xs₁ : DVect2 γ tail✝¹ tail✝
xs₂ : DVect2 γ x✝¹ x✝
⊢ map f g (fun {a} {b} ↦ h) (append xs₁ xs₂) ≡ append (map f g (fun {a} {b} ↦ h) xs₁) (map f g (fun {a} {b} ↦ h) xs₂)

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
α₁ : Type u_1
β₁ : Type u_2
γ₁ : α₁ → β₁ → Type u_3
f : α → α₁
g : β → β₁
h : {a : α} → {b : β} → γ a b → γ₁ (f a) (g b)
head✝¹ : α
tail✝¹ x✝¹ : List α
head✝ : β
tail✝ x✝ : List β
a✝ : γ head✝¹ head✝
xs₁ : DVect2 γ tail✝¹ tail✝
xs₂ : DVect2 γ x✝¹ x✝
⊢ map f g (fun {a} {b} ↦ h) (append xs₁ xs₂) ≡ append (map f g (fun {a} {b} ↦ h) xs₁) (map f g (fun {a} {b} ↦ h) xs₂)
Tactic:
exact map_append f g h (xs₁:=xs₁) (xs₂:=xs₂)
State after:
no goals