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

State before:
α : Type u
inst✝ : Category α
⊢ Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF = 𝟭 (List α)
Tactic:
dsimp [Functor.comp, Functor.id]
State after:
α : Type u
inst✝ : Category α
⊢ Functor.mk
      { obj :=
          fun X ↦
            Prefunctor.obj joinF.toPrefunctor
              (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF).toPrefunctor X),
        map :=
          fun {X Y} f ↦
            Prefunctor.map joinF.toPrefunctor
              (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor singletonF).toPrefunctor f) } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }

State before:
α : Type u
inst✝ : Category α
⊢ Functor.mk
      { obj :=
          fun X ↦
            Prefunctor.obj joinF.toPrefunctor
              (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF).toPrefunctor X),
        map :=
          fun {X Y} f ↦
            Prefunctor.map joinF.toPrefunctor
              (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor singletonF).toPrefunctor f) } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }
Tactic:
dsimp [singletonF, joinF, mapF, DVect2.join]
State after:
α : Type u
inst✝ : Category α
⊢ Functor.mk
      { obj := fun X ↦ List.join (List.map (fun a ↦ [a]) X),
        map :=
          fun {X Y} f ↦
            DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) f) } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }

State before:
α : Type u
inst✝ : Category α
⊢ Functor.mk
      { obj := fun X ↦ List.join (List.map (fun a ↦ [a]) X),
        map :=
          fun {X Y} f ↦
            DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) f) } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }
Tactic:
apply eqF_List <;> dsimp
State after:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List α), List.join (List.map (fun a ↦ [a]) a) = a

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) f)) f

State before:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List α), List.join (List.map (fun a ↦ [a]) a) = a

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) f)) f
Tactic:
. intro as
  induction as
  case a.nil => rfl
  case a.cons a as h_ind => dsimp; rw [h_ind]
State after:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) f)) f

State before:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) f)) f
Tactic:
. intro as bs fs
  induction fs
  case a.nil =>
    dsimp [DVect2.map, DVect2.join]
    exact DVect2.Eq.of rfl
  case a.cons a as b bs f fs h_ind =>
    dsimp [DVect2.map, DVect2.join]
    rw [DVect2.cons_append, DVect2.nil_append]
    exact DVect2.Eq.descend rfl h_ind
State after:
no goals

State before:
α : Type u
inst✝ : Category α
⊢ List.join (List.map (fun a ↦ [a]) []) = []
Tactic:
rfl
State after:
no goals

State before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : List.join (List.map (fun a ↦ [a]) as) = as
⊢ List.join (List.map (fun a ↦ [a]) (a :: as)) = a :: as
Tactic:
dsimp
State after:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : List.join (List.map (fun a ↦ [a]) as) = as
⊢ a :: List.join (List.map (fun a ↦ [a]) as) = a :: as

State before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : List.join (List.map (fun a ↦ [a]) as) = as
⊢ a :: List.join (List.map (fun a ↦ [a]) as) = a :: as
Tactic:
rw [h_ind]
State after:
no goals

State before:
α : Type u
inst✝ : Category α
as bs : List α
⊢ DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) DVect2.nil))
    DVect2.nil
Tactic:
dsimp [DVect2.map, DVect2.join]
State after:
α : Type u
inst✝ : Category α
as bs : List α
⊢ DVect2.Eq DVect2.nil DVect2.nil

State before:
α : Type u
inst✝ : Category α
as bs : List α
⊢ DVect2.Eq DVect2.nil DVect2.nil
Tactic:
exact DVect2.Eq.of rfl
State after:
no goals

State before:
α : Type u
inst✝ : Category α
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
f : a ⟶ b
fs : DVect2 Quiver.Hom as bs
h_ind : DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs)) fs
⊢ DVect2.Eq
    (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) (DVect2.cons f fs)))
    (DVect2.cons f fs)
Tactic:
dsimp [DVect2.map, DVect2.join]
State after:
α : Type u
inst✝ : Category α
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
f : a ⟶ b
fs : DVect2 Quiver.Hom as bs
h_ind : DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs)) fs
⊢ DVect2.Eq
    (DVect2.cons f DVect2.nil ++
      DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs))
    (DVect2.cons f fs)

State before:
α : Type u
inst✝ : Category α
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
f : a ⟶ b
fs : DVect2 Quiver.Hom as bs
h_ind : DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs)) fs
⊢ DVect2.Eq
    (DVect2.cons f DVect2.nil ++
      DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs))
    (DVect2.cons f fs)
Tactic:
rw [DVect2.cons_append, DVect2.nil_append]
State after:
α : Type u
inst✝ : Category α
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
f : a ⟶ b
fs : DVect2 Quiver.Hom as bs
h_ind : DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs)) fs
⊢ DVect2.Eq
    (DVect2.cons f (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs)))
    (DVect2.cons f fs)

State before:
α : Type u
inst✝ : Category α
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
f : a ⟶ b
fs : DVect2 Quiver.Hom as bs
h_ind : DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs)) fs
⊢ DVect2.Eq
    (DVect2.cons f (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs)))
    (DVect2.cons f fs)
Tactic:
exact DVect2.Eq.descend rfl h_ind
State after:
no goals