case h_map
C : Type u
inst✝ : Category C
X : TopCat
⊢ autoParam
    (∀ (X_1 Y : Presheaf C X) (f : X_1 ⟶ Y),
      (pushforward C (𝟙 X)).map f =
        eqToHom (_ : ?F.obj X_1 = ?G.obj X_1) ≫
          (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj Y = (pushforward C (𝟙 X)).obj Y))
    _auto✝

case h_obj
C : Type u
inst✝ : Category C
X : TopCat
⊢ ∀ (X_1 : Presheaf C X), (pushforward C (𝟙 X)).obj X_1 = (𝟭 (Presheaf C X)).obj X_1
C : Type u
inst✝ : Category C
X : TopCat
⊢ pushforward C (𝟙 X) = 𝟭 (Presheaf C X)
apply CategoryTheory.Functor.ext
case h_map
C : Type u
inst✝ : Category C
X : TopCat
a b : Presheaf C X
f : a ⟶ b
⊢ (pushforward C (𝟙 X)).map f =
    eqToHom (_ : ?F.obj a = ?G.obj a) ≫
      (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj b = (pushforward C (𝟙 X)).obj b)
case h_map
C : Type u
inst✝ : Category C
X : TopCat
⊢ autoParam
    (∀ (X_1 Y : Presheaf C X) (f : X_1 ⟶ Y),
      (pushforward C (𝟙 X)).map f =
        eqToHom (_ : ?F.obj X_1 = ?G.obj X_1) ≫
          (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj Y = (pushforward C (𝟙 X)).obj Y))
    _auto✝
intros a b f
case h_map
C : Type u
inst✝ : Category C
X : TopCat
a b : Presheaf C X
f : a ⟶ b
U : (Opens ↑X)ᵒᵖ
⊢ ((pushforward C (𝟙 X)).map f).app U =
    (eqToHom (_ : ?F.obj a = ?G.obj a) ≫
          (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj b = (pushforward C (𝟙 X)).obj b)).app
      U
case h_map
C : Type u
inst✝ : Category C
X : TopCat
a b : Presheaf C X
f : a ⟶ b
⊢ (pushforward C (𝟙 X)).map f =
    eqToHom (_ : ?F.obj a = ?G.obj a) ≫
      (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj b = (pushforward C (𝟙 X)).obj b)
refine NatTrans.ext _ _ (funext fun U => ?_)
no goals
case h_map
C : Type u
inst✝ : Category C
X : TopCat
a b : Presheaf C X
f : a ⟶ b
U : (Opens ↑X)ᵒᵖ
⊢ ((pushforward C (𝟙 X)).map f).app U =
    (eqToHom (_ : ?F.obj a = ?G.obj a) ≫
          (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj b = (pushforward C (𝟙 X)).obj b)).app
      U
. erw [NatTrans.congr f (Opens.op_map_id_obj U)]
  simp only [Functor.op_obj, eqToHom_refl, CategoryTheory.Functor.map_id,
    Category.comp_id, Category.id_comp, Functor.id_obj, Functor.id_map]
  apply Pushforward.id_eq
case h_map
C : Type u
inst✝ : Category C
X : TopCat
a b : Presheaf C X
f : a ⟶ b
U : (Opens ↑X)ᵒᵖ
⊢ a.map (eqToHom (_ : (Functor.op (Opens.map (𝟙 X))).obj U = U)) ≫
      f.app U ≫ b.map (eqToHom (_ : U = (Functor.op (Opens.map (𝟙 X))).obj U)) =
    (eqToHom (_ : ?F.obj a = ?G.obj a) ≫
          (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj b = (pushforward C (𝟙 X)).obj b)).app
      U

case h_obj
C : Type u
inst✝ : Category C
X : TopCat
⊢ ∀ (X_1 : Presheaf C X), (pushforward C (𝟙 X)).obj X_1 = (𝟭 (Presheaf C X)).obj X_1
case h_map
C : Type u
inst✝ : Category C
X : TopCat
a b : Presheaf C X
f : a ⟶ b
U : (Opens ↑X)ᵒᵖ
⊢ ((pushforward C (𝟙 X)).map f).app U =
    (eqToHom (_ : ?F.obj a = ?G.obj a) ≫
          (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj b = (pushforward C (𝟙 X)).obj b)).app
      U
erw [NatTrans.congr f (Opens.op_map_id_obj U)]
case h_obj
C : Type u
inst✝ : Category C
X : TopCat
⊢ ∀ (X_1 : Presheaf C X), (pushforward C (𝟙 X)).obj X_1 = (𝟭 (Presheaf C X)).obj X_1
case h_map
C : Type u
inst✝ : Category C
X : TopCat
a b : Presheaf C X
f : a ⟶ b
U : (Opens ↑X)ᵒᵖ
⊢ a.map (eqToHom (_ : (Functor.op (Opens.map (𝟙 X))).obj U = U)) ≫
      f.app U ≫ b.map (eqToHom (_ : U = (Functor.op (Opens.map (𝟙 X))).obj U)) =
    (eqToHom (_ : ?F.obj a = ?G.obj a) ≫
          (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj b = (pushforward C (𝟙 X)).obj b)).app
      U

case h_obj
C : Type u
inst✝ : Category C
X : TopCat
⊢ ∀ (X_1 : Presheaf C X), (pushforward C (𝟙 X)).obj X_1 = (𝟭 (Presheaf C X)).obj X_1
simp only [Functor.op_obj, eqToHom_refl, CategoryTheory.Functor.map_id,
  Category.comp_id, Category.id_comp, Functor.id_obj, Functor.id_map]
no goals
case h_obj
C : Type u
inst✝ : Category C
X : TopCat
⊢ ∀ (X_1 : Presheaf C X), (pushforward C (𝟙 X)).obj X_1 = (𝟭 (Presheaf C X)).obj X_1
apply Pushforward.id_eq