J : Type u'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : Opens ↑↑(F.obj j₃)
⊢ (F.map f).base ≫ (F.map g).base = (F.map f ≫ F.map g).base
J : Type u'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : Opens ↑↑(F.obj j₃)
⊢ (F.map f).base ≫ (F.map g).base = (F.map (f ≫ g)).base
rw [F.map_comp]
no goals
J : Type u'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : Opens ↑↑(F.obj j₃)
⊢ (F.map f).base ≫ (F.map g).base = (F.map f ≫ F.map g).base
rfl
case mk
J : Type u'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
carrier✝ : Set ↑↑(F.obj j₃)
is_open'✝ : IsOpen carrier✝
⊢ (F.map (f ≫ g)).c.app { carrier := carrier✝, is_open' := is_open'✝ }.op =
    (F.map g).c.app { carrier := carrier✝, is_open' := is_open'✝ }.op ≫
      (pushforwardMap (F.map g).base (F.map f).c).app { carrier := carrier✝, is_open' := is_open'✝ }.op ≫
        (Pushforward.comp (F.obj j₁).presheaf (F.map f).base (F.map g).base).inv.app
            { carrier := carrier✝, is_open' := is_open'✝ }.op ≫
          (pushforwardEq (_ : (F.map f).base ≫ (F.map g).base = (F.map (f ≫ g)).base) (F.obj j₁).presheaf).hom.app
            { carrier := carrier✝, is_open' := is_open'✝ }.op
J : Type u'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : Opens ↑↑(F.obj j₃)
⊢ (F.map (f ≫ g)).c.app U.op =
    (F.map g).c.app U.op ≫
      (pushforwardMap (F.map g).base (F.map f).c).app U.op ≫
        (Pushforward.comp (F.obj j₁).presheaf (F.map f).base (F.map g).base).inv.app U.op ≫
          (pushforwardEq (_ : (F.map f).base ≫ (F.map g).base = (F.map (f ≫ g)).base) (F.obj j₁).presheaf).hom.app U.op
cases U
no goals
case mk
J : Type u'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
carrier✝ : Set ↑↑(F.obj j₃)
is_open'✝ : IsOpen carrier✝
⊢ (F.map (f ≫ g)).c.app { carrier := carrier✝, is_open' := is_open'✝ }.op =
    (F.map g).c.app { carrier := carrier✝, is_open' := is_open'✝ }.op ≫
      (pushforwardMap (F.map g).base (F.map f).c).app { carrier := carrier✝, is_open' := is_open'✝ }.op ≫
        (Pushforward.comp (F.obj j₁).presheaf (F.map f).base (F.map g).base).inv.app
            { carrier := carrier✝, is_open' := is_open'✝ }.op ≫
          (pushforwardEq (_ : (F.map f).base ≫ (F.map g).base = (F.map (f ≫ g)).base) (F.obj j₁).presheaf).hom.app
            { carrier := carrier✝, is_open' := is_open'✝ }.op
simp [PresheafedSpace.congr_app (F.map_comp f g)]