case h_map
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category (D i)
A : Type u₁
inst✝ : Category A
f : (i : I) → A ⥤ C i
i : I
⊢ autoParam
    (∀ (X Y : A) (f_1 : X ⟶ Y),
      (pi' f ⋙ Pi.eval C i).map f_1 =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫ (f i).map f_1 ≫ eqToHom (_ : (f i).obj Y = (pi' f ⋙ Pi.eval C i).obj Y))
    _auto✝

case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category (D i)
A : Type u₁
inst✝ : Category A
f : (i : I) → A ⥤ C i
i : I
⊢ ∀ (X : A), (pi' f ⋙ Pi.eval C i).obj X = (f i).obj X
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category (D i)
A : Type u₁
inst✝ : Category A
f : (i : I) → A ⥤ C i
i : I
⊢ pi' f ⋙ Pi.eval C i = f i
apply Functor.ext
case h_map
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category (D i)
A : Type u₁
inst✝ : Category A
f : (i : I) → A ⥤ C i
i : I
X✝ Y✝ : A
f✝ : X✝ ⟶ Y✝
⊢ (pi' f ⋙ Pi.eval C i).map f✝ =
    eqToHom (_ : ?F.obj X✝ = ?G.obj X✝) ≫ (f i).map f✝ ≫ eqToHom (_ : (f i).obj Y✝ = (pi' f ⋙ Pi.eval C i).obj Y✝)

case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category (D i)
A : Type u₁
inst✝ : Category A
f : (i : I) → A ⥤ C i
i : I
⊢ ∀ (X : A), (pi' f ⋙ Pi.eval C i).obj X = (f i).obj X
case h_map
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category (D i)
A : Type u₁
inst✝ : Category A
f : (i : I) → A ⥤ C i
i : I
⊢ autoParam
    (∀ (X Y : A) (f_1 : X ⟶ Y),
      (pi' f ⋙ Pi.eval C i).map f_1 =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫ (f i).map f_1 ≫ eqToHom (_ : (f i).obj Y = (pi' f ⋙ Pi.eval C i).obj Y))
    _auto✝

case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category (D i)
A : Type u₁
inst✝ : Category A
f : (i : I) → A ⥤ C i
i : I
⊢ ∀ (X : A), (pi' f ⋙ Pi.eval C i).obj X = (f i).obj X
intro _ _ _
no goals
case h_map
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category (D i)
A : Type u₁
inst✝ : Category A
f : (i : I) → A ⥤ C i
i : I
X✝ Y✝ : A
f✝ : X✝ ⟶ Y✝
⊢ (pi' f ⋙ Pi.eval C i).map f✝ =
    eqToHom (_ : ?F.obj X✝ = ?G.obj X✝) ≫ (f i).map f✝ ≫ eqToHom (_ : (f i).obj Y✝ = (pi' f ⋙ Pi.eval C i).obj Y✝)
simp
case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category (D i)
A : Type u₁
inst✝ : Category A
f : (i : I) → A ⥤ C i
i : I
X✝ : A
⊢ (pi' f ⋙ Pi.eval C i).obj X✝ = (f i).obj X✝
case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category (D i)
A : Type u₁
inst✝ : Category A
f : (i : I) → A ⥤ C i
i : I
⊢ ∀ (X : A), (pi' f ⋙ Pi.eval C i).obj X = (f i).obj X
intro _
no goals
case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category (D i)
A : Type u₁
inst✝ : Category A
f : (i : I) → A ⥤ C i
i : I
X✝ : A
⊢ (pi' f ⋙ Pi.eval C i).obj X✝ = (f i).obj X✝
rfl