-- Mathlib/AlgebraicGeometry/RationalMap.lean
lemma fromSpecStalkOfMem_restrict (f : X.PartialMap Y)
    {U : X.Opens} (hU : Dense (U : Set X)) (hU' : U ≤ f.domain) {x} (hx : x ∈ U) :
    (f.restrict U hU hU').fromSpecStalkOfMem hx = f.fromSpecStalkOfMem (hU' hx)

Proof state:
case e_a.e_a.e_f
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
e : ⟨x, ⋯⟩ = (ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩
⊢ Hom.stalkMap f.domain.ι ⟨x, ⋯⟩ ≫ ((↑f.domain).presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ =
    (X.presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (X.homOfLE hU' ≫ f.domain.ι) ⟨x, hx⟩

Tactic:
simp only [restrictFunctor_obj_left, homOfLE_leOfHom, TopCat.Presheaf.stalkCongr_hom]

Result:
case e_a.e_a.e_f
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
e : ⟨x, ⋯⟩ = (ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩
⊢ Hom.stalkMap f.domain.ι ⟨x, ⋯⟩ ≫ (↑f.domain).presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ =
    X.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (X.homOfLE hU' ≫ f.domain.ι) ⟨x, hx⟩

Proof state:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ (Spec.map (inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫ (↑U).fromSpecStalk ⟨x, hx⟩) ≫ X.homOfLE hU' ≫ f.hom =
    (Spec.map (inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫ (↑f.domain).fromSpecStalk ⟨x, ⋯⟩) ≫ f.hom

Tactic:
have e : ⟨x, hU' hx⟩ = (X.homOfLE hU').base ⟨x, hx⟩ := by
  rw [Scheme.homOfLE_base]
  rfl

Result:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
e : ⟨x, ⋯⟩ = (ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩
⊢ (Spec.map (inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫ (↑U).fromSpecStalk ⟨x, hx⟩) ≫ X.homOfLE hU' ≫ f.hom =
    (Spec.map (inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫ (↑f.domain).fromSpecStalk ⟨x, ⋯⟩) ≫ f.hom

Proof state:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
e : ⟨x, ⋯⟩ = (ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩
⊢ Spec.map (inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫
      Spec.map (Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩) ≫
        (↑f.domain).fromSpecStalk ((ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩) ≫ f.hom =
    (Spec.map (inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫
        Spec.map ((↑f.domain).presheaf.stalkCongr ⋯).inv ≫
          (↑f.domain).fromSpecStalk ((ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩)) ≫
      f.hom

Tactic:
simp only [← Category.assoc, ← Spec.map_comp]

Result:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
e : ⟨x, ⋯⟩ = (ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩
⊢ (Spec.map (Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ ≫ inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫
        (↑f.domain).fromSpecStalk ((ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩)) ≫
      f.hom =
    (Spec.map (((↑f.domain).presheaf.stalkCongr ⋯).inv ≫ inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫
        (↑f.domain).fromSpecStalk ((ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩)) ≫
      f.hom

Proof state:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
e : ⟨x, ⋯⟩ = (ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩
⊢ (Spec.map (inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫ (↑U).fromSpecStalk ⟨x, hx⟩) ≫ X.homOfLE hU' ≫ f.hom =
    (Spec.map (inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫ (↑f.domain).fromSpecStalk ⟨x, ⋯⟩) ≫ f.hom

Tactic:
rw [Category.assoc, ← Spec_map_stalkMap_fromSpecStalk_assoc,
  ← Spec_map_stalkSpecializes_fromSpecStalk (Inseparable.of_eq e).specializes,
  ← TopCat.Presheaf.stalkCongr_inv _ (Inseparable.of_eq e)]

Result:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
e : ⟨x, ⋯⟩ = (ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩
⊢ Spec.map (inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫
      Spec.map (Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩) ≫
        (↑f.domain).fromSpecStalk ((ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩) ≫ f.hom =
    (Spec.map (inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫
        Spec.map ((↑f.domain).presheaf.stalkCongr ⋯).inv ≫
          (↑f.domain).fromSpecStalk ((ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩)) ≫
      f.hom

Proof state:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ (f.restrict U hU hU').fromSpecStalkOfMem hx = f.fromSpecStalkOfMem ⋯

Tactic:
dsimp only [fromSpecStalkOfMem, restrict, Scheme.Opens.fromSpecStalkOfMem]

Result:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ (Spec.map (inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫ (↑U).fromSpecStalk ⟨x, hx⟩) ≫ X.homOfLE hU' ≫ f.hom =
    (Spec.map (inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫ (↑f.domain).fromSpecStalk ⟨x, ⋯⟩) ≫ f.hom

Proof state:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ ⟨x, ⋯⟩ = (ConcreteCategory.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE hU'))) ⟨x, hx⟩

Tactic:
rfl

Result:
no goals

Proof state:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ ⟨x, ⋯⟩ = (ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩

Tactic:
rw [Scheme.homOfLE_base]

Result:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ ⟨x, ⋯⟩ = (ConcreteCategory.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE hU'))) ⟨x, hx⟩

Proof state:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
e : ⟨x, ⋯⟩ = (ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩
⊢ (Spec.map (Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ ≫ inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫
        (↑f.domain).fromSpecStalk ((ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩)) ≫
      f.hom =
    (Spec.map (((↑f.domain).presheaf.stalkCongr ⋯).inv ≫ inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫
        (↑f.domain).fromSpecStalk ((ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩)) ≫
      f.hom

Tactic:
congr 3

Result:
case e_a.e_a.e_f
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
e : ⟨x, ⋯⟩ = (ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩
⊢ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ ≫ inv (Hom.stalkMap U.ι ⟨x, hx⟩) =
    ((↑f.domain).presheaf.stalkCongr ⋯).inv ≫ inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)

Proof state:
case e_a.e_a.e_f
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
e : ⟨x, ⋯⟩ = (ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩
⊢ Hom.stalkMap f.domain.ι ⟨x, ⋯⟩ ≫ (↑f.domain).presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ =
    X.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (X.homOfLE hU' ≫ f.domain.ι) ⟨x, hx⟩

Tactic:
rw [← stalkSpecializes_stalkMap_assoc, stalkMap_comp]

Result:
no goals