-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
rw : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = X.fromSpecStalk x ≫ f
rw₁ : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₂ :
  Spec.map (Hom.stalkMap f x) ≫ Spec.map (Y.presheaf.germ U (f x) hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₃ :
  Spec.map (Y.presheaf.germ U (f x) hxU ≫ Hom.stalkMap f x) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₄ :
  Spec.map (Hom.app f U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₅ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (Hom.app f U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
rw₆ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
rw₇ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.map (homOfLE hVU).op ≫ X.presheaf.germ V x hxV) ≫
      Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
rw₈ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.germ V x hxV) ≫
      Spec.map (X.presheaf.map (homOfLE hVU).op) ≫ Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
rw₉ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.germ V x hxV) ≫
      Spec.map (X.presheaf.map (homOfLE hVU).op) ≫ Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
    (Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV ≫ f)
rw₁₀ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.germ V x hxV) ≫
      Spec.map (Hom.app f U ≫ X.presheaf.map (homOfLE hVU).op) ≫ IsAffineOpen.fromSpec hU)
    (Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV ≫ f)
rw₁₁ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.germ V x hxV) ≫
      Spec.map (Hom.appLE f U (f ⁻¹ᵁ U) ⋯ ≫ X.presheaf.map (homOfLE hVU).op) ≫ IsAffineOpen.fromSpec hU)
    (Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV ≫ f)
rw₁₂ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.germ V x hxV) ≫ Spec.map (Hom.appLE f U V ⋯) ≫ IsAffineOpen.fromSpec hU)
    (Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV ≫ f)
rw₁₃ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y) (Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV ≫ f)
    (Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV ≫ f)
hV₁ : IsAffineOpen V
rw₁₄ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y) (Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV ≫ f)
    (Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV ≫ f)
hV₂ : IsAffineOpen V
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f

Tactic:
rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, ← hV.fromSpecStalk_eq_fromSpecStalk hxV,
    IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc, Scheme.Hom.germ_stalkMap f _ x hxU,
    IsAffineOpen.fromSpecStalk, Spec.map_comp_assoc, ← X.presheaf.germ_res (homOfLE hVU) x hxV,
    Spec.map_comp_assoc, Category.assoc, ← Spec.map_comp_assoc (f.app _),
      Hom.app_eq_appLE, Hom.appLE_map, IsAffineOpen.SpecMap_appLE_fromSpec]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Spec.map_comp_assoc, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.Presheaf.germ_res, AlgebraicGeometry.Scheme.Hom.app, AlgebraicGeometry.Scheme.Hom.germ_stalkMap, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.IsAffineOpen.fromSpecStalk, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec, AlgebraicGeometry.Scheme.Hom.appLE_map, AlgebraicGeometry.Scheme.toLocallyRingedSpace, AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk