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

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List α
tail✝¹ ass₂ : List (List α)
head✝ : List β
tail✝ bss₂ : List (List β)
fs₁ : DVect2 γ head✝¹ head✝
fss₁ : DVect2 (DVect2 γ) tail✝¹ tail✝
fss₂ : DVect2 (DVect2 γ) ass₂ bss₂
⊢ join (cons fs₁ fss₁ ++ fss₂) ≡ join (cons fs₁ fss₁) ++ join fss₂
Tactic:
have h_ind := join_append fss₁ fss₂
State after:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List α
tail✝¹ ass₂ : List (List α)
head✝ : List β
tail✝ bss₂ : List (List β)
fs₁ : DVect2 γ head✝¹ head✝
fss₁ : DVect2 (DVect2 γ) tail✝¹ tail✝
fss₂ : DVect2 (DVect2 γ) ass₂ bss₂
h_ind : join (fss₁ ++ fss₂) ≡ join fss₁ ++ join fss₂
⊢ join (cons fs₁ fss₁ ++ fss₂) ≡ join (cons fs₁ fss₁) ++ join fss₂

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

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List α
tail✝¹ ass₂ : List (List α)
head✝ : List β
tail✝ bss₂ : List (List β)
fs₁ : DVect2 γ head✝¹ head✝
fss₁ : DVect2 (DVect2 γ) tail✝¹ tail✝
fss₂ : DVect2 (DVect2 γ) ass₂ bss₂
h_ind : join (append fss₁ fss₂) ≡ append (join fss₁) (join fss₂)
⊢ append fs₁ (join (append fss₁ fss₂)) ≡ append (append fs₁ (join fss₁)) (join fss₂)
Tactic:
apply DVect2.Eq.trans _ (append_assoc fs₁ fss₁.join fss₂.join).symm
State after:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List α
tail✝¹ ass₂ : List (List α)
head✝ : List β
tail✝ bss₂ : List (List β)
fs₁ : DVect2 γ head✝¹ head✝
fss₁ : DVect2 (DVect2 γ) tail✝¹ tail✝
fss₂ : DVect2 (DVect2 γ) ass₂ bss₂
h_ind : join (append fss₁ fss₂) ≡ append (join fss₁) (join fss₂)
⊢ append fs₁ (join (append fss₁ fss₂)) ≡ fs₁ ++ (join fss₁ ++ join fss₂)

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List α
tail✝¹ ass₂ : List (List α)
head✝ : List β
tail✝ bss₂ : List (List β)
fs₁ : DVect2 γ head✝¹ head✝
fss₁ : DVect2 (DVect2 γ) tail✝¹ tail✝
fss₂ : DVect2 (DVect2 γ) ass₂ bss₂
h_ind : join (append fss₁ fss₂) ≡ append (join fss₁) (join fss₂)
⊢ append fs₁ (join (append fss₁ fss₂)) ≡ fs₁ ++ (join fss₁ ++ join fss₂)
Tactic:
induction fs₁
State after:
case nil
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List α
tail✝¹ ass₂ : List (List α)
head✝ : List β
tail✝ bss₂ : List (List β)
fss₁ : DVect2 (DVect2 γ) tail✝¹ tail✝
fss₂ : DVect2 (DVect2 γ) ass₂ bss₂
h_ind : join (append fss₁ fss₂) ≡ append (join fss₁) (join fss₂)
⊢ append nil (join (append fss₁ fss₂)) ≡ nil ++ (join fss₁ ++ join fss₂)

case cons
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List α
tail✝¹ ass₂ : List (List α)
head✝ : List β
tail✝ bss₂ : List (List β)
fss₁ : DVect2 (DVect2 γ) tail✝¹ tail✝
fss₂ : DVect2 (DVect2 γ) ass₂ bss₂
h_ind : join (append fss₁ fss₂) ≡ append (join fss₁) (join fss₂)
a✝² : α
as✝ : List α
b✝ : β
bs✝ : List β
a✝¹ : γ a✝² b✝
a✝ : DVect2 γ as✝ bs✝
a_ih✝ : append a✝ (join (append fss₁ fss₂)) ≡ a✝ ++ (join fss₁ ++ join fss₂)
⊢ append (cons a✝¹ a✝) (join (append fss₁ fss₂)) ≡ cons a✝¹ a✝ ++ (join fss₁ ++ join fss₂)

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List α
tail✝¹ ass₂ : List (List α)
head✝ : List β
tail✝ bss₂ : List (List β)
fss₁ : DVect2 (DVect2 γ) tail✝¹ tail✝
fss₂ : DVect2 (DVect2 γ) ass₂ bss₂
h_ind : join (append fss₁ fss₂) ≡ append (join fss₁) (join fss₂)
⊢ append nil (join (append fss₁ fss₂)) ≡ nil ++ (join fss₁ ++ join fss₂)
Tactic:
case nil => exact h_ind
State after:
no goals

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List α
tail✝¹ ass₂ : List (List α)
head✝ : List β
tail✝ bss₂ : List (List β)
fss₁ : DVect2 (DVect2 γ) tail✝¹ tail✝
fss₂ : DVect2 (DVect2 γ) ass₂ bss₂
h_ind : join (append fss₁ fss₂) ≡ append (join fss₁) (join fss₂)
a✝² : α
as✝ : List α
b✝ : β
bs✝ : List β
a✝¹ : γ a✝² b✝
a✝ : DVect2 γ as✝ bs✝
hfs : append a✝ (join (append fss₁ fss₂)) ≡ a✝ ++ (join fss₁ ++ join fss₂)
⊢ append (cons a✝¹ a✝) (join (append fss₁ fss₂)) ≡ cons a✝¹ a✝ ++ (join fss₁ ++ join fss₂)
Tactic:
case cons _ _ hfs =>
  exact DVect2.Eq.descend rfl hfs
State after:
no goals

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List α
tail✝¹ ass₂ : List (List α)
head✝ : List β
tail✝ bss₂ : List (List β)
fss₁ : DVect2 (DVect2 γ) tail✝¹ tail✝
fss₂ : DVect2 (DVect2 γ) ass₂ bss₂
h_ind : join (append fss₁ fss₂) ≡ append (join fss₁) (join fss₂)
⊢ append nil (join (append fss₁ fss₂)) ≡ nil ++ (join fss₁ ++ join fss₂)
Tactic:
exact h_ind
State after:
no goals

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List α
tail✝¹ ass₂ : List (List α)
head✝ : List β
tail✝ bss₂ : List (List β)
fss₁ : DVect2 (DVect2 γ) tail✝¹ tail✝
fss₂ : DVect2 (DVect2 γ) ass₂ bss₂
h_ind : join (append fss₁ fss₂) ≡ append (join fss₁) (join fss₂)
a✝² : α
as✝ : List α
b✝ : β
bs✝ : List β
a✝¹ : γ a✝² b✝
a✝ : DVect2 γ as✝ bs✝
hfs : append a✝ (join (append fss₁ fss₂)) ≡ a✝ ++ (join fss₁ ++ join fss₂)
⊢ append (cons a✝¹ a✝) (join (append fss₁ fss₂)) ≡ cons a✝¹ a✝ ++ (join fss₁ ++ join fss₂)
Tactic:
exact DVect2.Eq.descend rfl hfs
State after:
no goals