-- Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean
theorem toKaroubi_comp_karoubiFunctorCategoryEmbedding :
    toKaroubi _ ⋙ karoubiFunctorCategoryEmbedding J C =
      (whiskeringRight J _ _).obj (toKaroubi C)

Proof state:
case h_map.w.h.h
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
X Y : J ⥤ C
f : X ⟶ Y
j : J
⊢ (((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).map f).app j).f =
    ((eqToHom ⋯ ≫ ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).map f ≫ eqToHom ⋯).app j).f

Tactic:
simp

Result:
no goals

Proof state:
case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
X Y : J ⥤ C
f : X ⟶ Y
⊢ (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).map f =
    eqToHom ⋯ ≫ ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).map f ≫ eqToHom ⋯

Tactic:
ext j

Result:
case h_map.w.h.h
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
X Y : J ⥤ C
f : X ⟶ Y
j : J
⊢ (((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).map f).app j).f =
    ((eqToHom ⋯ ≫ ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).map f ≫ eqToHom ⋯).app j).f

Proof state:
case h_obj.h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
X : J ⥤ C
j : J
⊢ ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).obj j =
    (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).obj j

Tactic:
rfl

Result:
no goals

Proof state:
case h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
⊢ ∀ (X : J ⥤ C),
    (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X =
      ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X

Tactic:
intro X

Result:
case h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
X : J ⥤ C
⊢ (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X =
    ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X

Proof state:
case h_obj.h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
X : J ⥤ C
⊢ ∀ (X_1 : J),
    ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).obj X_1 =
      (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).obj X_1

Tactic:
intro j

Result:
case h_obj.h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
X : J ⥤ C
j : J
⊢ ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).obj j =
    (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).obj j

Proof state:
case h_obj.h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
X : J ⥤ C
⊢ autoParam
    (∀ (X_1 Y : J) (f : X_1 ⟶ Y),
      ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map f =
        eqToHom ⋯ ≫ (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map f ≫ eqToHom ⋯)
    _auto✝

Tactic:
intro j j' φ

Result:
case h_obj.h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
X : J ⥤ C
j j' : J
φ : j ⟶ j'
⊢ ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map φ =
    eqToHom ⋯ ≫ (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map φ ≫ eqToHom ⋯

Proof state:
case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
⊢ autoParam
    (∀ (X Y : J ⥤ C) (f : X ⟶ Y),
      (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).map f =
        eqToHom ⋯ ≫ ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).map f ≫ eqToHom ⋯)
    _auto✝

Tactic:
intro X Y f

Result:
case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
X Y : J ⥤ C
f : X ⟶ Y
⊢ (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).map f =
    eqToHom ⋯ ≫ ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).map f ≫ eqToHom ⋯

Proof state:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
⊢ toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C = (whiskeringRight J C (Karoubi C)).obj (toKaroubi C)

Tactic:
apply Functor.ext

Result:
case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
⊢ autoParam
    (∀ (X Y : J ⥤ C) (f : X ⟶ Y),
      (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).map f =
        eqToHom ⋯ ≫ ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).map f ≫ eqToHom ⋯)
    _auto✝

case h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
⊢ ∀ (X : J ⥤ C),
    (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X =
      ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X

Proof state:
case h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
X : J ⥤ C
⊢ (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X =
    ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X

Tactic:
apply Functor.ext

Result:
case h_obj.h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
X : J ⥤ C
⊢ autoParam
    (∀ (X_1 Y : J) (f : X_1 ⟶ Y),
      ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map f =
        eqToHom ⋯ ≫ (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map f ≫ eqToHom ⋯)
    _auto✝

case h_obj.h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
X : J ⥤ C
⊢ ∀ (X_1 : J),
    ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).obj X_1 =
      (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).obj X_1

Proof state:
case h_obj.h_map.h
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
X : J ⥤ C
j j' : J
φ : j ⟶ j'
⊢ (((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map φ).f =
    (eqToHom ⋯ ≫ (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map φ ≫ eqToHom ⋯).f

Tactic:
simp

Result:
no goals

Proof state:
case h_obj.h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
X : J ⥤ C
j j' : J
φ : j ⟶ j'
⊢ ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map φ =
    eqToHom ⋯ ≫ (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map φ ≫ eqToHom ⋯

Tactic:
ext

Result:
case h_obj.h_map.h
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
X : J ⥤ C
j j' : J
φ : j ⟶ j'
⊢ (((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map φ).f =
    (eqToHom ⋯ ≫ (((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map φ ≫ eqToHom ⋯).f