internlm/Lean-Github huggingface dataset:
Theorem: CategoryTheory.List.joinF.associator_right_left
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
⊢ joinF.associatorRight (([] :: ass) :: asss) ≫ joinF.associatorLeft (([] :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (([] :: ass) :: asss))
Tactic:
case nil => simp; exact h_indss
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associator_right_left
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
a : α
as : List α
h_inds :
  joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))
⊢ joinF.associatorRight (((a :: as) :: ass) :: asss) ≫ joinF.associatorLeft (((a :: as) :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (((a :: as) :: ass) :: asss))
Tactic:
case cons a as h_inds => simp; rw [h_inds]; rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associator_right_left
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
⊢ joinF.associatorRight (([] :: ass) :: asss) ≫ joinF.associatorLeft (([] :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (([] :: ass) :: asss))
Tactic:
simp
Proof state after:
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
⊢ joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj joinF.toPrefunctor (ass ++ Prefunctor.obj joinF.toPrefunctor asss))
Theorem: CategoryTheory.List.joinF.associator_right_left
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
⊢ joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj joinF.toPrefunctor (ass ++ Prefunctor.obj joinF.toPrefunctor asss))
Tactic:
exact h_indss
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associator_right_left
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
a : α
as : List α
h_inds :
  joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))
⊢ joinF.associatorRight (((a :: as) :: ass) :: asss) ≫ joinF.associatorLeft (((a :: as) :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (((a :: as) :: ass) :: asss))
Tactic:
simp
Proof state after:
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
a : α
as : List α
h_inds :
  joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))
⊢ DVect2.cons (𝟙 a) (joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss)) =
    DVect2.cons (𝟙 a) (𝟙 (as ++ Prefunctor.obj joinF.toPrefunctor (ass ++ Prefunctor.obj joinF.toPrefunctor asss)))
Theorem: CategoryTheory.List.joinF.associator_right_left
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
a : α
as : List α
h_inds :
  joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))
⊢ DVect2.cons (𝟙 a) (joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss)) =
    DVect2.cons (𝟙 a) (𝟙 (as ++ Prefunctor.obj joinF.toPrefunctor (ass ++ Prefunctor.obj joinF.toPrefunctor asss)))
Tactic:
rw [h_inds]
Proof state after:
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
a : α
as : List α
h_inds :
  joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))
⊢ DVect2.cons (𝟙 a) (𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))) =
    DVect2.cons (𝟙 a) (𝟙 (as ++ Prefunctor.obj joinF.toPrefunctor (ass ++ Prefunctor.obj joinF.toPrefunctor asss)))
Theorem: CategoryTheory.List.joinF.associator_right_left
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
a : α
as : List α
h_inds :
  joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))
⊢ DVect2.cons (𝟙 a) (𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))) =
    DVect2.cons (𝟙 a) (𝟙 (as ++ Prefunctor.obj joinF.toPrefunctor (ass ++ Prefunctor.obj joinF.toPrefunctor asss)))
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.Functor.triangle
Proof state before:
A : Type u₁
inst✝³ : Category A
B : Type u₂
inst✝² : Category B
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F : A ⥤ B
G : B ⥤ C
⊢ (associator F (𝟭 B) G).hom ≫ whiskerLeft F (leftUnitor G).hom = whiskerRight (rightUnitor F).hom G
Tactic:
ext
Proof state after:
case w.h
A : Type u₁
inst✝³ : Category A
B : Type u₂
inst✝² : Category B
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F : A ⥤ B
G : B ⥤ C
x✝ : A
⊢ NatTrans.app ((associator F (𝟭 B) G).hom ≫ whiskerLeft F (leftUnitor G).hom) x✝ =
    NatTrans.app (whiskerRight (rightUnitor F).hom G) x✝
Theorem: CategoryTheory.Functor.triangle
Proof state before:
case w.h
A : Type u₁
inst✝³ : Category A
B : Type u₂
inst✝² : Category B
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F : A ⥤ B
G : B ⥤ C
x✝ : A
⊢ NatTrans.app ((associator F (𝟭 B) G).hom ≫ whiskerLeft F (leftUnitor G).hom) x✝ =
    NatTrans.app (whiskerRight (rightUnitor F).hom G) x✝
Tactic:
dsimp
Proof state after:
case w.h
A : Type u₁
inst✝³ : Category A
B : Type u₂
inst✝² : Category B
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F : A ⥤ B
G : B ⥤ C
x✝ : A
⊢ 𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)) ≫
      𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)) =
    Prefunctor.map G.toPrefunctor (𝟙 (Prefunctor.obj F.toPrefunctor x✝))
Theorem: CategoryTheory.Functor.triangle
Proof state before:
case w.h
A : Type u₁
inst✝³ : Category A
B : Type u₂
inst✝² : Category B
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F : A ⥤ B
G : B ⥤ C
x✝ : A
⊢ 𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)) ≫
      𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)) =
    Prefunctor.map G.toPrefunctor (𝟙 (Prefunctor.obj F.toPrefunctor x✝))
Tactic:
simp
Proof state after:
no goals
Theorem: CategoryTheory.Functor.pentagon
Proof state before:
A : Type u₁
inst✝⁴ : Category A
B : Type u₂
inst✝³ : Category B
C : Type u₃
inst✝² : Category C
D : Type u₄
inst✝¹ : Category D
E : Type u₅
inst✝ : Category E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
⊢ whiskerRight (associator F G H).hom K ≫ (associator F (G ⋙ H) K).hom ≫ whiskerLeft F (associator G H K).hom =
    (associator (F ⋙ G) H K).hom ≫ (associator F G (H ⋙ K)).hom
Tactic:
ext
Proof state after:
case w.h
A : Type u₁
inst✝⁴ : Category A
B : Type u₂
inst✝³ : Category B
C : Type u₃
inst✝² : Category C
D : Type u₄
inst✝¹ : Category D
E : Type u₅
inst✝ : Category E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
x✝ : A
⊢ NatTrans.app
      (whiskerRight (associator F G H).hom K ≫ (associator F (G ⋙ H) K).hom ≫ whiskerLeft F (associator G H K).hom) x✝ =
    NatTrans.app ((associator (F ⋙ G) H K).hom ≫ (associator F G (H ⋙ K)).hom) x✝
Theorem: CategoryTheory.Functor.pentagon
Proof state before:
case w.h
A : Type u₁
inst✝⁴ : Category A
B : Type u₂
inst✝³ : Category B
C : Type u₃
inst✝² : Category C
D : Type u₄
inst✝¹ : Category D
E : Type u₅
inst✝ : Category E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
x✝ : A
⊢ NatTrans.app
      (whiskerRight (associator F G H).hom K ≫ (associator F (G ⋙ H) K).hom ≫ whiskerLeft F (associator G H K).hom) x✝ =
    NatTrans.app ((associator (F ⋙ G) H K).hom ≫ (associator F G (H ⋙ K)).hom) x✝
Tactic:
dsimp
Proof state after:
case w.h
A : Type u₁
inst✝⁴ : Category A
B : Type u₂
inst✝³ : Category B
C : Type u₃
inst✝² : Category C
D : Type u₄
inst✝¹ : Category D
E : Type u₅
inst✝ : Category E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
x✝ : A
⊢ Prefunctor.map K.toPrefunctor
        (𝟙 (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) ≫
      𝟙
          (Prefunctor.obj K.toPrefunctor
            (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) ≫
        𝟙
          (Prefunctor.obj K.toPrefunctor
            (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) =
    𝟙
        (Prefunctor.obj K.toPrefunctor
          (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) ≫
      𝟙
        (Prefunctor.obj K.toPrefunctor
          (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝))))
Theorem: CategoryTheory.Functor.pentagon
Proof state before:
case w.h
A : Type u₁
inst✝⁴ : Category A
B : Type u₂
inst✝³ : Category B
C : Type u₃
inst✝² : Category C
D : Type u₄
inst✝¹ : Category D
E : Type u₅
inst✝ : Category E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
x✝ : A
⊢ Prefunctor.map K.toPrefunctor
        (𝟙 (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) ≫
      𝟙
          (Prefunctor.obj K.toPrefunctor
            (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) ≫
        𝟙
          (Prefunctor.obj K.toPrefunctor
            (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) =
    𝟙
        (Prefunctor.obj K.toPrefunctor
          (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) ≫
      𝟙
        (Prefunctor.obj K.toPrefunctor
          (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝))))
Tactic:
simp
Proof state after:
no goals
Theorem: DVect2.append_nil
Proof state before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : α
tail✝¹ : List α
head✝ : β
tail✝ : List β
f : γ head✝¹ head✝
fs : DVect2 γ tail✝¹ tail✝
⊢ cons f fs ++ nil ≡ cons f fs
Tactic:
rw [cons_append]
Proof state after:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : α
tail✝¹ : List α
head✝ : β
tail✝ : List β
f : γ head✝¹ head✝
fs : DVect2 γ tail✝¹ tail✝
⊢ cons f (fs ++ nil) ≡ cons f fs
Theorem: DVect2.append_nil
Proof state before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : α
tail✝¹ : List α
head✝ : β
tail✝ : List β
f : γ head✝¹ head✝
fs : DVect2 γ tail✝¹ tail✝
⊢ cons f (fs ++ nil) ≡ cons f fs
Tactic:
exact DVect2.Eq.descend rfl (append_nil fs)
Proof state after:
no goals
Theorem: DVect2.append_assoc
Proof 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₃
Proof 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₃)
Theorem: DVect2.append_assoc
Proof 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 *
Proof 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₃))
Theorem: DVect2.append_assoc
Proof 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
Proof state after:
no goals
Theorem: DVect2.map_append
Proof 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]
Proof 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₂
Theorem: DVect2.map_append
Proof 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
Proof 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₂)
Theorem: DVect2.map_append
Proof 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₂)
Proof state after:
no goals
Theorem: DVect2.join_append
Proof 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₂
Proof 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₂
Theorem: DVect2.join_append
Proof 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 *
Proof 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₂)
Theorem: DVect2.join_append
Proof 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
Proof 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₂)
Theorem: DVect2.join_append
Proof 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₁
Proof 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₂)
Theorem: DVect2.join_append
Proof 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
Proof state after:
no goals
Theorem: DVect2.join_append
Proof 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
Proof state after:
no goals
Theorem: DVect2.join_append
Proof 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
Proof state after:
no goals
Theorem: DVect2.join_append
Proof 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
Proof state after:
no goals