Theorem: CategoryTheory.List.joinF.naturality (Moncalc/CategoryTheory/List/Monad.lean)

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF =
    joinF ⋙ Prefunctor.obj mapF.toPrefunctor F
Tactic:
apply eqF_List
State after:
case a
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ ∀ (a : List (List α)),
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor a =
      Prefunctor.obj (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor a

case a
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ ∀ (a₁ a₂ : List (List α)) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor f)
      (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f)

State before:
case a
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ ∀ (a : List (List α)),
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor a =
      Prefunctor.obj (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor a

case a
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ ∀ (a₁ a₂ : List (List α)) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor f)
      (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f)
Tactic:
. intro ass
  induction ass
  case a.nil => rfl
  case a.cons as ass h_ind =>
    dsimp at *
    have : ∀ (as bs : List α), (mapF.obj F).obj (as++bs) = (mapF.obj F).obj as ++ (mapF.obj F).obj bs :=
      λ as bs => List.map_append F.obj _ _
    rw [this, h_ind]
State after:
case a
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ ∀ (a₁ a₂ : List (List α)) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor f)
      (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f)

State before:
case a
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ ∀ (a₁ a₂ : List (List α)) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor f)
      (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f)
Tactic:
. intros as₁ as₂ fs
  induction fs
  case a.nil => exact DVect2.Eq.nil_rfl
  case a.cons f fs h_ind =>
    dsimp
    have : ∀ {as₁ as₂ bs₁ bs₂ : List α} (fs₁ : as₁ ⟶ bs₁) (fs₂ : as₂ ⟶ bs₂), DVect2.Eq ((mapF.obj F).map (fs₁ ++ fs₂)) ((mapF.obj F).map fs₁ ++ (mapF.obj F).map fs₂) :=
      λ fs₁ fs₂ => DVect2.map_append F.obj F.obj F.map
    apply DVect2.Eq.trans _ (this f (joinF.map fs)).symm
    apply DVect2.eq_of_eq_append_eq (DVect2.Eq.of rfl) h_ind
State after:
no goals

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor [] =
    Prefunctor.obj (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor []
Tactic:
rfl
State after:
no goals

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as : List α
ass : List (List α)
h_ind :
  Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor ass =
    Prefunctor.obj (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor ass
⊢ Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor
      (as :: ass) =
    Prefunctor.obj (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as :: ass)
Tactic:
dsimp at *
State after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as : List α
ass : List (List α)
h_ind :
  Prefunctor.obj joinF.toPrefunctor
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (Prefunctor.obj joinF.toPrefunctor ass)
⊢ Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as ++
      Prefunctor.obj joinF.toPrefunctor
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as ++ Prefunctor.obj joinF.toPrefunctor ass)

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as : List α
ass : List (List α)
h_ind :
  Prefunctor.obj joinF.toPrefunctor
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (Prefunctor.obj joinF.toPrefunctor ass)
⊢ Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as ++
      Prefunctor.obj joinF.toPrefunctor
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as ++ Prefunctor.obj joinF.toPrefunctor ass)
Tactic:
have : ∀ (as bs : List α), (mapF.obj F).obj (as++bs) = (mapF.obj F).obj as ++ (mapF.obj F).obj bs :=
  λ as bs => List.map_append F.obj _ _
State after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as : List α
ass : List (List α)
h_ind :
  Prefunctor.obj joinF.toPrefunctor
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (Prefunctor.obj joinF.toPrefunctor ass)
this :
  ∀ (as bs : List α),
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as ++ bs) =
      Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as ++
        Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor bs
⊢ Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as ++
      Prefunctor.obj joinF.toPrefunctor
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as ++ Prefunctor.obj joinF.toPrefunctor ass)

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as : List α
ass : List (List α)
h_ind :
  Prefunctor.obj joinF.toPrefunctor
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (Prefunctor.obj joinF.toPrefunctor ass)
this :
  ∀ (as bs : List α),
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as ++ bs) =
      Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as ++
        Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor bs
⊢ Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as ++
      Prefunctor.obj joinF.toPrefunctor
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as ++ Prefunctor.obj joinF.toPrefunctor ass)
Tactic:
rw [this, h_ind]
State after:
no goals

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor
      DVect2.nil)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor DVect2.nil)
Tactic:
exact DVect2.Eq.nil_rfl
State after:
no goals

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
a✝ : List α
as✝ : List (List α)
b✝ : List α
bs✝ : List (List α)
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor fs)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor
      (DVect2.cons f fs))
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs))
Tactic:
dsimp
State after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
a✝ : List α
as✝ : List (List α)
b✝ : List α
bs✝ : List (List α)
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor fs)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map joinF.toPrefunctor
        (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor fs))
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (f ++ Prefunctor.map joinF.toPrefunctor fs))

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
a✝ : List α
as✝ : List (List α)
b✝ : List α
bs✝ : List (List α)
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor fs)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map joinF.toPrefunctor
        (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor fs))
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (f ++ Prefunctor.map joinF.toPrefunctor fs))
Tactic:
have : ∀ {as₁ as₂ bs₁ bs₂ : List α} (fs₁ : as₁ ⟶ bs₁) (fs₂ : as₂ ⟶ bs₂), DVect2.Eq ((mapF.obj F).map (fs₁ ++ fs₂)) ((mapF.obj F).map fs₁ ++ (mapF.obj F).map fs₂) :=
  λ fs₁ fs₂ => DVect2.map_append F.obj F.obj F.map
State after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
a✝ : List α
as✝ : List (List α)
b✝ : List α
bs✝ : List (List α)
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor fs)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs)
this :
  ∀ {as₁ as₂ bs₁ bs₂ : List α} (fs₁ : as₁ ⟶ bs₁) (fs₂ : as₂ ⟶ bs₂),
    DVect2.Eq (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs₁ ++ fs₂))
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs₁ ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs₂)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map joinF.toPrefunctor
        (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor fs))
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (f ++ Prefunctor.map joinF.toPrefunctor fs))

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
a✝ : List α
as✝ : List (List α)
b✝ : List α
bs✝ : List (List α)
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor fs)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs)
this :
  ∀ {as₁ as₂ bs₁ bs₂ : List α} (fs₁ : as₁ ⟶ bs₁) (fs₂ : as₂ ⟶ bs₂),
    DVect2.Eq (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs₁ ++ fs₂))
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs₁ ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs₂)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map joinF.toPrefunctor
        (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor fs))
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (f ++ Prefunctor.map joinF.toPrefunctor fs))
Tactic:
apply DVect2.Eq.trans _ (this f (joinF.map fs)).symm
State after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
a✝ : List α
as✝ : List (List α)
b✝ : List α
bs✝ : List (List α)
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor fs)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs)
this :
  ∀ {as₁ as₂ bs₁ bs₂ : List α} (fs₁ : as₁ ⟶ bs₁) (fs₂ : as₂ ⟶ bs₂),
    DVect2.Eq (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs₁ ++ fs₂))
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs₁ ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs₂)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map joinF.toPrefunctor
        (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor fs))
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (Prefunctor.map joinF.toPrefunctor fs))

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
a✝ : List α
as✝ : List (List α)
b✝ : List α
bs✝ : List (List α)
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor fs)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs)
this :
  ∀ {as₁ as₂ bs₁ bs₂ : List α} (fs₁ : as₁ ⟶ bs₁) (fs₂ : as₂ ⟶ bs₂),
    DVect2.Eq (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs₁ ++ fs₂))
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs₁ ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs₂)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map joinF.toPrefunctor
        (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor fs))
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (Prefunctor.map joinF.toPrefunctor fs))
Tactic:
apply DVect2.eq_of_eq_append_eq (DVect2.Eq.of rfl) h_ind
State after:
no goals