-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
@[simp]
lemma residueFieldMap_comp {Z : LocallyRingedSpace.{u}} (g : Y ⟶ Z) (x : X) :
    residueFieldMap (f ≫ g) x = residueFieldMap g (f.base x) ≫ residueFieldMap f x

Proof state:
case hf
X Y : LocallyRingedSpace
f : X ⟶ Y
Z : LocallyRingedSpace
g : Y ⟶ Z
x : ↑X.toTopCat
⊢ CommRingCat.Hom.hom
      (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap (f ≫ g) x)))) =
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x))))).comp
      (CommRingCat.Hom.hom
        (CommRingCat.ofHom
          (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap g ((ConcreteCategory.hom f.base) x))))))

Tactic:
simp_rw [stalkMap_comp]

Result:
case hf
X Y : LocallyRingedSpace
f : X ⟶ Y
Z : LocallyRingedSpace
g : Y ⟶ Z
x : ↑X.toTopCat
⊢ CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalRing.ResidueField.map
          (CommRingCat.Hom.hom (Hom.stalkMap g ((ConcreteCategory.hom f.base) x) ≫ Hom.stalkMap f x)))) =
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x))))).comp
      (CommRingCat.Hom.hom
        (CommRingCat.ofHom
          (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap g ((ConcreteCategory.hom f.base) x))))))

Proof state:
case hf
X Y : LocallyRingedSpace
f : X ⟶ Y
Z : LocallyRingedSpace
g : Y ⟶ Z
x : ↑X.toTopCat
⊢ CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalRing.ResidueField.map
          (CommRingCat.Hom.hom (Hom.stalkMap g ((ConcreteCategory.hom f.base) x) ≫ Hom.stalkMap f x)))) =
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x))))).comp
      (CommRingCat.Hom.hom
        (CommRingCat.ofHom
          (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap g ((ConcreteCategory.hom f.base) x))))))

Tactic:
apply IsLocalRing.ResidueField.map_comp (Hom.stalkMap g (f.base x)).hom (Hom.stalkMap f x).hom

Result:
no goals

Proof state:
case hf
X Y : LocallyRingedSpace
f : X ⟶ Y
Z : LocallyRingedSpace
g : Y ⟶ Z
x : ↑X.toTopCat
⊢ CommRingCat.Hom.hom (residueFieldMap (f ≫ g) x) =
    CommRingCat.Hom.hom (residueFieldMap g ((ConcreteCategory.hom f.base) x) ≫ residueFieldMap f x)

Tactic:
simp only [comp_toShHom, SheafedSpace.comp_base, Function.comp_apply, residueFieldMap,
  CommRingCat.hom_comp, TopCat.comp_app]

Result:
case hf
X Y : LocallyRingedSpace
f : X ⟶ Y
Z : LocallyRingedSpace
g : Y ⟶ Z
x : ↑X.toTopCat
⊢ CommRingCat.Hom.hom
      (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap (f ≫ g) x)))) =
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x))))).comp
      (CommRingCat.Hom.hom
        (CommRingCat.ofHom
          (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap g ((ConcreteCategory.hom f.base) x))))))

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
Z : LocallyRingedSpace
g : Y ⟶ Z
x : ↑X.toTopCat
⊢ residueFieldMap (f ≫ g) x = residueFieldMap g ((ConcreteCategory.hom f.base) x) ≫ residueFieldMap f x

Tactic:
ext : 1

Result:
case hf
X Y : LocallyRingedSpace
f : X ⟶ Y
Z : LocallyRingedSpace
g : Y ⟶ Z
x : ↑X.toTopCat
⊢ CommRingCat.Hom.hom (residueFieldMap (f ≫ g) x) =
    CommRingCat.Hom.hom (residueFieldMap g ((ConcreteCategory.hom f.base) x) ≫ residueFieldMap f x)