-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
@[reassoc]
lemma evaluation_naturality {V : Opens Y} (x : (Opens.map f.base).obj V) :
    Y.evaluation ⟨f.base x, x.property⟩ ≫ residueFieldMap f x.val =
      f.c.app (op V) ≫ X.evaluation x

Proof state:
case hf.a
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (CommRingCat.Hom.hom
        (Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯ ≫
          CommRingCat.ofHom (IsLocalRing.residue ↑(Y.presheaf.stalk ((ConcreteCategory.hom f.base) ↑x))) ≫
            CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f ↑x)))))
      a =
    (CommRingCat.Hom.hom
        (f.c.app (op V) ≫
          X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯ ≫
            CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))))
      a

Tactic:
simp only [CommRingCat.comp_apply]

Result:
case hf.a
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (ConcreteCategory.hom (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f ↑x)))))
      ((ConcreteCategory.hom
          (CommRingCat.ofHom (IsLocalRing.residue ↑(Y.presheaf.stalk ((ConcreteCategory.hom f.base) ↑x)))))
        ((ConcreteCategory.hom (Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯)) a)) =
    (ConcreteCategory.hom (CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a))

Proof state:
case hf.a
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))
      ((CommRingCat.Hom.hom (Hom.stalkMap f ↑x))
        ((ConcreteCategory.hom (Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯)) a)) =
    (ConcreteCategory.hom (CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a))

Tactic:
rw [LocallyRingedSpace.stalkMap_germ_apply]

Result:
case hf.a
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a)) =
    (ConcreteCategory.hom (CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a))

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
⊢ Y.evaluation ⟨(ConcreteCategory.hom f.base) ↑x, ⋯⟩ ≫ residueFieldMap f ↑x = f.c.app (op V) ≫ X.evaluation x

Tactic:
dsimp only [LocallyRingedSpace.evaluation,
  LocallyRingedSpace.residueFieldMap]

Result:
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
⊢ (Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯ ≫
        CommRingCat.ofHom (IsLocalRing.residue ↑(Y.presheaf.stalk ((ConcreteCategory.hom f.base) ↑x)))) ≫
      CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f ↑x))) =
    f.c.app (op V) ≫
      X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯ ≫ CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
⊢ (Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯ ≫
        CommRingCat.ofHom (IsLocalRing.residue ↑(Y.presheaf.stalk ((ConcreteCategory.hom f.base) ↑x)))) ≫
      CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f ↑x))) =
    f.c.app (op V) ≫
      X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯ ≫ CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))

Tactic:
rw [Category.assoc]

Result:
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
⊢ Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯ ≫
      CommRingCat.ofHom (IsLocalRing.residue ↑(Y.presheaf.stalk ((ConcreteCategory.hom f.base) ↑x))) ≫
        CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f ↑x))) =
    f.c.app (op V) ≫
      X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯ ≫ CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))

Proof state:
case hf.a
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a)) =
    (ConcreteCategory.hom (CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a))

Tactic:
rfl

Result:
no goals

Proof state:
case hf.a
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (ConcreteCategory.hom (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f ↑x)))))
      ((ConcreteCategory.hom
          (CommRingCat.ofHom (IsLocalRing.residue ↑(Y.presheaf.stalk ((ConcreteCategory.hom f.base) ↑x)))))
        ((ConcreteCategory.hom (Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯)) a)) =
    (ConcreteCategory.hom (CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a))

Tactic:
erw [IsLocalRing.ResidueField.map_residue]

Result:
case hf.a
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))
      ((CommRingCat.Hom.hom (Hom.stalkMap f ↑x))
        ((ConcreteCategory.hom (Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯)) a)) =
    (ConcreteCategory.hom (CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a))

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
⊢ Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯ ≫
      CommRingCat.ofHom (IsLocalRing.residue ↑(Y.presheaf.stalk ((ConcreteCategory.hom f.base) ↑x))) ≫
        CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f ↑x))) =
    f.c.app (op V) ≫
      X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯ ≫ CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))

Tactic:
ext a

Result:
case hf.a
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (CommRingCat.Hom.hom
        (Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯ ≫
          CommRingCat.ofHom (IsLocalRing.residue ↑(Y.presheaf.stalk ((ConcreteCategory.hom f.base) ↑x))) ≫
            CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f ↑x)))))
      a =
    (CommRingCat.Hom.hom
        (f.c.app (op V) ≫
          X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯ ≫
            CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))))
      a