-- Mathlib/AlgebraicGeometry/Stalk.lean
theorem IsAffineOpen.fromSpecStalk_eq (x : X) (hxU : x ∈ U) (hxV : x ∈ V) :
    hU.fromSpecStalk hxU = hV.fromSpecStalk hxV

Proof state:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ hU.fromSpecStalk hxU = fromSpecStalk h₁ h₂

Tactic:
delta fromSpecStalk

Result:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec = Spec.map (X.presheaf.germ U' x h₂) ≫ fromSpec h₁

Proof state:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec = Spec.map (X.presheaf.germ U' x h₂) ≫ fromSpec h₁

Tactic:
rw [← hU.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_left).op]

Result:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec =
    Spec.map (X.presheaf.germ U' x h₂) ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op) ≫ hU.fromSpec

Proof state:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec =
    Spec.map (X.presheaf.germ U' x h₂) ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op) ≫ hU.fromSpec

Tactic:
erw [← Scheme.Spec_map (X.presheaf.map _).op, ← Scheme.Spec_map (X.presheaf.germ _ x h₂).op]

Result:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec =
    Scheme.Spec.map (X.presheaf.germ U' x h₂).op ≫ Scheme.Spec.map (X.presheaf.map (homOfLE ⋯).op).op ≫ hU.fromSpec

Proof state:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ fromSpecStalk h₁ h₂ = hV.fromSpecStalk hxV

Tactic:
delta fromSpecStalk

Result:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.germ U' x h₂) ≫ fromSpec h₁ = Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec

Proof state:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.germ U' x h₂) ≫ fromSpec h₁ = Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec

Tactic:
rw [← hV.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_right).op]

Result:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.germ U' x h₂) ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op) ≫ hV.fromSpec =
    Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec

Proof state:
case intro.intro.intro
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ hU.fromSpecStalk hxU = hV.fromSpecStalk hxV

Tactic:
transitivity fromSpecStalk h₁ h₂

Result:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ hU.fromSpecStalk hxU = fromSpecStalk h₁ h₂

X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ fromSpecStalk h₁ h₂ = hV.fromSpecStalk hxV

Proof state:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.germ U' x h₂) ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op) ≫ hV.fromSpec =
    Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec

Tactic:
erw [← Scheme.Spec_map (X.presheaf.map _).op, ← Scheme.Spec_map (X.presheaf.germ _ x h₂).op]

Result:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Scheme.Spec.map (X.presheaf.germ U' x h₂).op ≫ Scheme.Spec.map (X.presheaf.map (homOfLE ⋯).op).op ≫ hV.fromSpec =
    Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec

Proof state:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec =
    Scheme.Spec.map (X.presheaf.germ U' x h₂).op ≫ Scheme.Spec.map (X.presheaf.map (homOfLE ⋯).op).op ≫ hU.fromSpec

Tactic:
rw [← Functor.map_comp_assoc, ← op_comp, TopCat.Presheaf.germ_res, Scheme.Spec_map,
  Quiver.Hom.unop_op]

Result:
no goals

Proof state:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
⊢ hU.fromSpecStalk hxU = hV.fromSpecStalk hxV

Tactic:
obtain ⟨U', h₁, h₂, h₃ : U' ≤ U ⊓ V⟩ :=
  Opens.isBasis_iff_nbhd.mp (isBasis_affine_open X) (show x ∈ U ⊓ V from ⟨hxU, hxV⟩)

Result:
case intro.intro.intro
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ hU.fromSpecStalk hxU = hV.fromSpecStalk hxV

Proof state:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↑↑X.toPresheafedSpace
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Scheme.Spec.map (X.presheaf.germ U' x h₂).op ≫ Scheme.Spec.map (X.presheaf.map (homOfLE ⋯).op).op ≫ hV.fromSpec =
    Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec

Tactic:
rw [← Functor.map_comp_assoc, ← op_comp, TopCat.Presheaf.germ_res, Scheme.Spec_map,
  Quiver.Hom.unop_op]

Result:
no goals