Theorem: CategoryTheory.List.mapF.obj_id (Moncalc/CategoryTheory/List/Basic.lean)

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

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map
        (Prefunctor.obj mapF.toPrefunctor (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f })).toPrefunctor f)
      f

State before:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List α),
    Prefunctor.obj
        (Prefunctor.obj mapF.toPrefunctor (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f })).toPrefunctor a =
      a

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map
        (Prefunctor.obj mapF.toPrefunctor (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f })).toPrefunctor f)
      f
Tactic:
. intro as
  change List.map id as = as
  rw [List.map_id]
State after:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map
        (Prefunctor.obj mapF.toPrefunctor (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f })).toPrefunctor f)
      f

State before:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map
        (Prefunctor.obj mapF.toPrefunctor (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f })).toPrefunctor f)
      f
Tactic:
. intro as₁ as₂ fs
  change DVect2.Eq (DVect2.map id id id fs) fs
  exact DVect2.map_id
State after:
no goals