-- Mathlib/AlgebraicGeometry/Spec.lean
theorem Spec.sheafedSpaceMap_comp {R S T : CommRingCat.{u}} (f : R ⟶ S) (g : S ⟶ T) :
    Spec.sheafedSpaceMap (f ≫ g) = Spec.sheafedSpaceMap g ≫ Spec.sheafedSpaceMap f :=
  AlgebraicGeometry.PresheafedSpace.Hom.ext _ _ (Spec.topMap_comp f g) <| by
    ext
    -- Porting note: was one liner
    -- `dsimp, rw category_theory.functor.map_id, rw category.comp_id, erw comap_comp f g, refl`
    rw [NatTrans.comp_app, sheafedSpaceMap_c_app, whiskerRight_app, eqToHom_refl]
    erw [(sheafedSpaceObj T).presheaf.map_id]
    dsimp only [CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply]
    rw [comap_comp]
    rfl

Proof state:
case w.hf.a
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (𝟙
          ((sheafedSpaceObj T).presheaf.obj
            ((TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).base).op.obj (op U✝)))))
      ((CommRingCat.Hom.hom
          (CommRingCat.ofHom
            ((comap (CommRingCat.Hom.hom g) ?w.hf.a.V ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj U✝)
                  ?w.hf.a.hVW).comp
              (comap (CommRingCat.Hom.hom f) U✝ ?w.hf.a.V ?w.hf.a.hUV))))
        x✝) =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).c.app (op U✝))) x✝

case w.hf.a.V
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ TopologicalSpace.Opens ↑(PrimeSpectrum.Top ↑S)

case w.hf.a.hUV
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ ∀ p ∈ ?w.hf.a.V, (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p ∈ U✝

case w.hf.a.hVW
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ ∀ p ∈ (TopologicalSpace.Opens.map (topMap (f ≫ g))).obj U✝,
    (PrimeSpectrum.comap (CommRingCat.Hom.hom g)) p ∈ ?w.hf.a.V

Tactic:
rfl

Result:
no goals

Proof state:
case w.hf.a
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (((sheafedSpaceMap (f ≫ g)).c ≫ whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf).app (op U✝)))
      x✝ =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).c.app (op U✝))) x✝

Tactic:
rw [NatTrans.comp_app, sheafedSpaceMap_c_app, whiskerRight_app, eqToHom_refl]

Result:
case w.hf.a
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (comap (CommRingCat.Hom.hom (f ≫ g)) (unop (op U✝))
              ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (unop (op U✝))) ⋯) ≫
          (sheafedSpaceObj T).presheaf.map
            ((𝟙 (TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).base).op).app (op U✝))))
      x✝ =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).c.app (op U✝))) x✝

Proof state:
case w.hf.a
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (comap (CommRingCat.Hom.hom (f ≫ g)) (unop (op U✝))
              ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (unop (op U✝))) ⋯) ≫
          𝟙
            ((sheafedSpaceObj T).presheaf.obj
              ((TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).base).op.obj (op U✝)))))
      x✝ =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).c.app (op U✝))) x✝

Tactic:
dsimp only [CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply]

Result:
case w.hf.a
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (𝟙
          ((sheafedSpaceObj T).presheaf.obj
            ((TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).base).op.obj (op U✝)))))
      ((CommRingCat.Hom.hom
          (CommRingCat.ofHom
            (comap ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f)) U✝
              ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj U✝) ⋯)))
        x✝) =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).c.app (op U✝))) x✝

Proof state:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).c ≫ whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf =
    (sheafedSpaceMap g ≫ sheafedSpaceMap f).c

Tactic:
ext

Result:
case w.hf.a
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (((sheafedSpaceMap (f ≫ g)).c ≫ whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf).app (op U✝)))
      x✝ =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).c.app (op U✝))) x✝

Proof state:
case w.hf.a
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (𝟙
          ((sheafedSpaceObj T).presheaf.obj
            ((TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).base).op.obj (op U✝)))))
      ((CommRingCat.Hom.hom
          (CommRingCat.ofHom
            (comap ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f)) U✝
              ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj U✝) ⋯)))
        x✝) =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).c.app (op U✝))) x✝

Tactic:
rw [comap_comp]

Result:
case w.hf.a
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (𝟙
          ((sheafedSpaceObj T).presheaf.obj
            ((TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).base).op.obj (op U✝)))))
      ((CommRingCat.Hom.hom
          (CommRingCat.ofHom
            ((comap (CommRingCat.Hom.hom g) ?w.hf.a.V ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj U✝)
                  ?w.hf.a.hVW).comp
              (comap (CommRingCat.Hom.hom f) U✝ ?w.hf.a.V ?w.hf.a.hUV))))
        x✝) =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).c.app (op U✝))) x✝

case w.hf.a.V
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ TopologicalSpace.Opens ↑(PrimeSpectrum.Top ↑S)

case w.hf.a.hUV
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ ∀ p ∈ ?w.hf.a.V, (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p ∈ U✝

case w.hf.a.hVW
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ ∀ p ∈ (TopologicalSpace.Opens.map (topMap (f ≫ g))).obj U✝,
    (PrimeSpectrum.comap (CommRingCat.Hom.hom g)) p ∈ ?w.hf.a.V