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

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List (List α)
tail✝¹ : List (List (List α))
head✝ : List (List β)
tail✝ : List (List (List β))
fs : DVect2 (DVect2 γ) head✝¹ head✝
fsss : DVect2 (DVect2 (DVect2 γ)) tail✝¹ tail✝
⊢ join (join (cons fs fsss)) ≡ join (map List.join List.join (fun {a} {b} ↦ join) (cons fs fsss))
Tactic:
dsimp [DVect2.join, DVect2.map]
State after:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List (List α)
tail✝¹ : List (List (List α))
head✝ : List (List β)
tail✝ : List (List (List β))
fs : DVect2 (DVect2 γ) head✝¹ head✝
fsss : DVect2 (DVect2 (DVect2 γ)) tail✝¹ tail✝
⊢ join (fs ++ join fsss) ≡ join fs ++ join (map List.join List.join (fun {a} {b} ↦ join) fsss)

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List (List α)
tail✝¹ : List (List (List α))
head✝ : List (List β)
tail✝ : List (List (List β))
fs : DVect2 (DVect2 γ) head✝¹ head✝
fsss : DVect2 (DVect2 (DVect2 γ)) tail✝¹ tail✝
⊢ join (fs ++ join fsss) ≡ join fs ++ join (map List.join List.join (fun {a} {b} ↦ join) fsss)
Tactic:
apply DVect2.Eq.trans (DVect2.join_append fs _) _
State after:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List (List α)
tail✝¹ : List (List (List α))
head✝ : List (List β)
tail✝ : List (List (List β))
fs : DVect2 (DVect2 γ) head✝¹ head✝
fsss : DVect2 (DVect2 (DVect2 γ)) tail✝¹ tail✝
⊢ join fs ++ join (join fsss) ≡ join fs ++ join (map List.join List.join (fun {a} {b} ↦ join) fsss)

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List (List α)
tail✝¹ : List (List (List α))
head✝ : List (List β)
tail✝ : List (List (List β))
fs : DVect2 (DVect2 γ) head✝¹ head✝
fsss : DVect2 (DVect2 (DVect2 γ)) tail✝¹ tail✝
⊢ join fs ++ join (join fsss) ≡ join fs ++ join (map List.join List.join (fun {a} {b} ↦ join) fsss)
Tactic:
apply eq_of_eq_append_eq (DVect2.Eq.of rfl)
State after:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List (List α)
tail✝¹ : List (List (List α))
head✝ : List (List β)
tail✝ : List (List (List β))
fs : DVect2 (DVect2 γ) head✝¹ head✝
fsss : DVect2 (DVect2 (DVect2 γ)) tail✝¹ tail✝
⊢ join (join fsss) ≡ join (map List.join List.join (fun {a} {b} ↦ join) fsss)

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List (List α)
tail✝¹ : List (List (List α))
head✝ : List (List β)
tail✝ : List (List (List β))
fs : DVect2 (DVect2 γ) head✝¹ head✝
fsss : DVect2 (DVect2 (DVect2 γ)) tail✝¹ tail✝
⊢ join (join fsss) ≡ join (map List.join List.join (fun {a} {b} ↦ join) fsss)
Tactic:
exact join_join fsss
State after:
no goals