awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ Eq (α := Γ(X, U) ⟶ X.presheaf.stalk x)
    (CategoryStruct.comp (Y := (↑U : Scheme).presheaf.stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))
        (U.topIso.inv ≫ (↑U : Scheme).presheaf.germ ⊤ (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) trivial)
        (inv (Hom.stalkMap U.ι (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))) :
      Γ(X, U) ⟶ X.presheaf.stalk x)
    (X.presheaf.germ U x hxU : X.presheaf.obj (op U) ⟶ X.presheaf.stalk x)
have e_f : Eq (α :=
  (↑U : Scheme).presheaf.obj (op ⊤) ⟶ (↑U : Scheme).presheaf.stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))
  ((↑U : Scheme).presheaf.germ ⊤ (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) trivial)
  (U.topIso.hom ≫
    CategoryStruct.comp (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)
      (Hom.stalkMap U.ι (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU)))
Tactic: rw [IsIso.comp_inv_eq, Iso.inv_comp_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ Eq (α :=
    (↑U : Scheme).presheaf.obj (op ⊤) ⟶ (↑U : Scheme).presheaf.stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))
    ((↑U : Scheme).presheaf.germ ⊤ (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) trivial)
    (U.topIso.hom ≫
      CategoryStruct.comp (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)
        (Hom.stalkMap U.ι (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU)))
have e_f : Eq (α :=
  (↑U : Scheme).presheaf.obj (op ⊤) ⟶ (↑U : Scheme).presheaf.stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))
  ((↑U : Scheme).presheaf.germ ⊤ (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) trivial)
  (U.topIso.hom ≫
    Hom.app U.ι U ≫ (↑U : Scheme).presheaf.germ (U.ι ⁻¹ᵁ U) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) hxU)
Tactic: erw [Hom.germ_stalkMap U.ι U ⟨x, hxU⟩]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ Eq (α :=
    (↑U : Scheme).presheaf.obj (op ⊤) ⟶ (↑U : Scheme).presheaf.stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))
    ((↑U : Scheme).presheaf.germ ⊤ (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) trivial)
    (U.topIso.hom ≫
      Hom.app U.ι U ≫ (↑U : Scheme).presheaf.germ (U.ι ⁻¹ᵁ U) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) hxU)
have e_f : Eq (α :=
  (↑U : Scheme).presheaf.obj (op ⊤) ⟶ (↑U : Scheme).presheaf.stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))
  ((↑U : Scheme).presheaf.germ ⊤ (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) trivial)
  (CategoryStruct.comp (Y := Γ(X, U.ι ''ᵁ U.ι ⁻¹ᵁ U))
    (X.presheaf.map (Quiver.Hom.op (eqToHom sorry) ≫ Quiver.Hom.op (homOfLE sorry)))
    ((↑U : Scheme).presheaf.germ (U.ι ⁻¹ᵁ U) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) hxU))
Tactic: rw [Opens.ι_app, Opens.topIso_hom, ← Functor.map_comp_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R : CommRingCat
x : ↥(Spec R)
⊢ (Spec R).fromSpecStalk x = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)
have rw : IsAffineOpen.fromSpecStalk sorry trivial = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)
Tactic: rw [← (isAffineOpen_top (Spec R)).fromSpecStalk_eq_fromSpecStalk (x := x) trivial,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpec_top, Scheme.isoSpec_Spec_inv,
    ← Spec.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R : CommRingCat
x : ↥(Spec R)
rw : IsAffineOpen.fromSpecStalk ⋯ trivial = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)
⊢ (Spec R).fromSpecStalk x = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)
have rw₁ : Eq (α := Spec ((Spec R).presheaf.stalk x) ⟶ Spec R) (map ((Spec R).presheaf.germ ⊤ x trivial) ≫ IsAffineOpen.fromSpec sorry)
  (map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial))
Tactic: rw [← (isAffineOpen_top (Spec R)).fromSpecStalk_eq_fromSpecStalk (x := x) trivial,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpec_top, Scheme.isoSpec_Spec_inv,
    ← Spec.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R : CommRingCat
x : ↥(Spec R)
rw : IsAffineOpen.fromSpecStalk ⋯ trivial = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)
rw₁ :
  Eq (α := Spec ((Spec R).presheaf.stalk x) ⟶ Spec R)
    (map ((Spec R).presheaf.germ ⊤ x trivial) ≫ IsAffineOpen.fromSpec ⋯)
    (map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial))
⊢ (Spec R).fromSpecStalk x = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)
have rw₂ : Eq (α := Spec ((Spec R).presheaf.stalk x) ⟶ Spec R)
  (map ((Spec R).presheaf.germ ⊤ x trivial) ≫ Iso.inv (Spec R).isoSpec)
  (map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial))
Tactic: rw [← (isAffineOpen_top (Spec R)).fromSpecStalk_eq_fromSpecStalk (x := x) trivial,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpec_top, Scheme.isoSpec_Spec_inv,
    ← Spec.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R : CommRingCat
x : ↥(Spec R)
rw : IsAffineOpen.fromSpecStalk ⋯ trivial = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)
rw₁ :
  Eq (α := Spec ((Spec R).presheaf.stalk x) ⟶ Spec R)
    (map ((Spec R).presheaf.germ ⊤ x trivial) ≫ IsAffineOpen.fromSpec ⋯)
    (map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial))
rw₂ :
  Eq (α := Spec ((Spec R).presheaf.stalk x) ⟶ Spec R)
    (map ((Spec R).presheaf.germ ⊤ x trivial) ≫ Iso.inv (Spec R).isoSpec)
    (map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial))
⊢ (Spec R).fromSpecStalk x = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)
have rw₃ : Eq (α := Spec ((Spec R).presheaf.stalk x) ⟶ Spec R)
  (map ((Spec R).presheaf.germ ⊤ x trivial) ≫ map (Scheme.ΓSpecIso R).inv)
  (map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial))
Tactic: rw [← (isAffineOpen_top (Spec R)).fromSpecStalk_eq_fromSpecStalk (x := x) trivial,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpec_top, Scheme.isoSpec_Spec_inv,
    ← Spec.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R : CommRingCat
x : ↥(Spec R)
rw : IsAffineOpen.fromSpecStalk ⋯ trivial = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)
rw₁ :
  Eq (α := Spec ((Spec R).presheaf.stalk x) ⟶ Spec R)
    (map ((Spec R).presheaf.germ ⊤ x trivial) ≫ IsAffineOpen.fromSpec ⋯)
    (map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial))
rw₂ :
  Eq (α := Spec ((Spec R).presheaf.stalk x) ⟶ Spec R)
    (map ((Spec R).presheaf.germ ⊤ x trivial) ≫ Iso.inv (Spec R).isoSpec)
    (map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial))
rw₃ :
  Eq (α := Spec ((Spec R).presheaf.stalk x) ⟶ Spec R)
    (map ((Spec R).presheaf.germ ⊤ x trivial) ≫ map (Scheme.ΓSpecIso R).inv)
    (map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial))
⊢ (Spec R).fromSpecStalk x = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)
have rw₄ : Eq (α := Spec ((Spec R).presheaf.stalk x) ⟶ Spec R) (map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial))
  (map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial))
Tactic: rw [← (isAffineOpen_top (Spec R)).fromSpecStalk_eq_fromSpecStalk (x := x) trivial,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpec_top, Scheme.isoSpec_Spec_inv,
    ← Spec.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
⊢ Eq (α := R ⟶ (Spec R).presheaf.stalk (closedPoint (↑R : Type u))) (Iso.inv (stalkClosedPointIso R))
    (StructureSheaf.toStalk (↑R : Type u) (closedPoint (↑R : Type u)))
have hf : ∀ (x : (↑R : Type u)),
  Eq (α := (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
    ((CommRingCat.Hom.hom (Iso.inv (stalkClosedPointIso R)) :
          (a : (↑R : Type u)) → (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
        x :
      (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
    ((CommRingCat.Hom.hom (StructureSheaf.toStalk (↑R : Type u) (closedPoint (↑R : Type u))) :
          (a : (↑R : Type u)) → (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
        x :
      (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
⊢ Eq (α := Γ(Spec R, ⊤) ⟶ (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
    ((Scheme.ΓSpecIso R).hom ≫ Iso.inv (stalkClosedPointIso R))
    ((Spec R).presheaf.germ ⊤ (closedPoint (↑R : Type u)) trivial)
have rw : Eq (α := R ⟶ (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
  (StructureSheaf.toStalk (↑R : Type u) (closedPoint (↑R : Type u)))
  ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ (closedPoint (↑R : Type u)) trivial)
Tactic: rw [stalkClosedPointIso_inv, ← Iso.eq_inv_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
⊢ CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
      ((Spec R).presheaf.germ ⊤ (closedPoint (↑R : Type u)) trivial) (Iso.hom (stalkClosedPointIso R)) =
    (Scheme.ΓSpecIso R).hom
have rw : CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
    ((Scheme.ΓSpecIso R).hom ≫ Iso.inv (stalkClosedPointIso R)) (Iso.hom (stalkClosedPointIso R)) =
  (Scheme.ΓSpecIso R).hom
Tactic: rw [← ΓSpecIso_hom_stalkClosedPointIso_inv, Category.assoc, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
rw :
  CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
      ((Scheme.ΓSpecIso R).hom ≫ Iso.inv (stalkClosedPointIso R)) (Iso.hom (stalkClosedPointIso R)) =
    (Scheme.ΓSpecIso R).hom
⊢ CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
      ((Spec R).presheaf.germ ⊤ (closedPoint (↑R : Type u)) trivial) (Iso.hom (stalkClosedPointIso R)) =
    (Scheme.ΓSpecIso R).hom
have rw₁ : (Scheme.ΓSpecIso R).hom ≫
    CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u))) (Iso.inv (stalkClosedPointIso R))
      (Iso.hom (stalkClosedPointIso R)) =
  (Scheme.ΓSpecIso R).hom
Tactic: rw [← ΓSpecIso_hom_stalkClosedPointIso_inv, Category.assoc, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
rw :
  CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
      ((Scheme.ΓSpecIso R).hom ≫ Iso.inv (stalkClosedPointIso R)) (Iso.hom (stalkClosedPointIso R)) =
    (Scheme.ΓSpecIso R).hom
rw₁ :
  (Scheme.ΓSpecIso R).hom ≫
      CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u))) (Iso.inv (stalkClosedPointIso R))
        (Iso.hom (stalkClosedPointIso R)) =
    (Scheme.ΓSpecIso R).hom
⊢ CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
      ((Spec R).presheaf.germ ⊤ (closedPoint (↑R : Type u)) trivial) (Iso.hom (stalkClosedPointIso R)) =
    (Scheme.ΓSpecIso R).hom
have rw₂ : (Scheme.ΓSpecIso R).hom ≫ 𝟙 R = (Scheme.ΓSpecIso R).hom
Tactic: rw [← ΓSpecIso_hom_stalkClosedPointIso_inv, Category.assoc, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
rw :
  CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
      ((Scheme.ΓSpecIso R).hom ≫ Iso.inv (stalkClosedPointIso R)) (Iso.hom (stalkClosedPointIso R)) =
    (Scheme.ΓSpecIso R).hom
rw₁ :
  (Scheme.ΓSpecIso R).hom ≫
      CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u))) (Iso.inv (stalkClosedPointIso R))
        (Iso.hom (stalkClosedPointIso R)) =
    (Scheme.ΓSpecIso R).hom
rw₂ : (Scheme.ΓSpecIso R).hom ≫ 𝟙 R = (Scheme.ΓSpecIso R).hom
⊢ CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
      ((Spec R).presheaf.germ ⊤ (closedPoint (↑R : Type u)) trivial) (Iso.hom (stalkClosedPointIso R)) =
    (Scheme.ΓSpecIso R).hom
have rw₃ : (Scheme.ΓSpecIso R).hom = (Scheme.ΓSpecIso R).hom
Tactic: rw [← ΓSpecIso_hom_stalkClosedPointIso_inv, Category.assoc, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
⊢ Eq (α := Spec ((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) ⟶ Spec R)
    (Spec.map (Iso.inv (stalkClosedPointIso R))) ((Spec R).fromSpecStalk (closedPoint (↑R : Type u)))
have rw : Eq.{u + 1} (α := Spec ((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) ⟶ Spec R)
  (Spec.map (StructureSheaf.toStalk (↑R : Type u) (closedPoint (↑R : Type u))))
  ((Spec R).fromSpecStalk (closedPoint (↑R : Type u)))
Tactic: rw [stalkClosedPointIso_inv, Spec.fromSpecStalk_eq']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
rw :
  Eq.{u + 1} (α := Spec ((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) ⟶ Spec R)
    (Spec.map (StructureSheaf.toStalk (↑R : Type u) (closedPoint (↑R : Type u))))
    ((Spec R).fromSpecStalk (closedPoint (↑R : Type u)))
⊢ Eq (α := Spec ((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) ⟶ Spec R)
    (Spec.map (Iso.inv (stalkClosedPointIso R))) ((Spec R).fromSpecStalk (closedPoint (↑R : Type u)))
have rw₁ : Eq.{u + 1} (α := Spec ((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) ⟶ Spec R)
  (Spec.map (StructureSheaf.toStalk (↑R : Type u) (closedPoint (↑R : Type u))))
  (Spec.map (StructureSheaf.toStalk (↑R : Type u) (closedPoint (↑R : Type u))))
Tactic: rw [stalkClosedPointIso_inv, Spec.fromSpecStalk_eq']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X Y : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
g : X ⟶ Y
⊢ Eq (α := Y.presheaf.stalk ((f ≫ g) (closedPoint (↑R : Type u))) ⟶ R) (stalkClosedPointTo (f ≫ g))
    (Hom.stalkMap g (f (closedPoint (↑R : Type u))) ≫ stalkClosedPointTo f)
have rw : Eq (α := Y.presheaf.stalk ((f ≫ g) (closedPoint (↑R : Type u))) ⟶ R)
  ((Hom.stalkMap g (f (closedPoint (↑R : Type u))) ≫ Hom.stalkMap f (closedPoint (↑R : Type u))) ≫
    Iso.hom (stalkClosedPointIso R))
  (Hom.stalkMap g (f (closedPoint (↑R : Type u))) ≫ stalkClosedPointTo f)
Tactic: rw [stalkClosedPointTo, Scheme.Hom.stalkMap_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R S : CommRingCat
inst : IsLocalRing.{u_1} (↑S : Type u_1)
φ : R ⟶ S
⊢ CategoryStruct.comp (Y := (Spec R).presheaf.stalk ((Spec.map φ) (closedPoint (↑S : Type u_1))))
      ((Spec R).presheaf.germ ⊤ ((Spec.map φ) (closedPoint (↑S : Type u_1))) trivial)
      (stalkClosedPointTo (Spec.map φ)) =
    (ΓSpecIso R).hom ≫ φ
have rw : φ ≫
    (ΓSpecIso S).inv ≫
      CategoryStruct.comp (Y := (Spec S).presheaf.stalk (closedPoint (↑S : Type u_1)))
        ((Spec S).presheaf.germ (Spec.map φ ⁻¹ᵁ ⊤) (closedPoint (↑S : Type u_1)) trivial)
        (Iso.hom (stalkClosedPointIso S)) =
  φ
Tactic: rw [stalkClosedPointTo, Scheme.Hom.germ_stalkMap_assoc, ← Iso.inv_comp_eq,
    ← ΓSpecIso_inv_naturality_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R S : CommRingCat
inst : IsLocalRing.{u_1} (↑S : Type u_1)
φ : R ⟶ S
⊢ φ ≫
      (ΓSpecIso S).inv ≫
        CategoryStruct.comp (Y := (Spec S).presheaf.stalk (closedPoint (↑S : Type u_1)))
          ((Spec S).presheaf.germ ⊤ (closedPoint (↑S : Type u_1)) trivial) (Iso.hom (stalkClosedPointIso S)) =
    φ
have rw : φ ≫ (ΓSpecIso S).inv ≫ (ΓSpecIso S).hom = φ
Tactic: rw [germ_stalkClosedPointIso_hom, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R S : CommRingCat
inst : IsLocalRing.{u_1} (↑S : Type u_1)
φ : R ⟶ S
rw : φ ≫ (ΓSpecIso S).inv ≫ (ΓSpecIso S).hom = φ
⊢ φ ≫
      (ΓSpecIso S).inv ≫
        CategoryStruct.comp (Y := (Spec S).presheaf.stalk (closedPoint (↑S : Type u_1)))
          ((Spec S).presheaf.germ ⊤ (closedPoint (↑S : Type u_1)) trivial) (Iso.hom (stalkClosedPointIso S)) =
    φ
have rw₁ : φ ≫ 𝟙 S = φ
Tactic: rw [germ_stalkClosedPointIso_hom, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
R S : CommRingCat
inst : IsLocalRing.{u_1} (↑S : Type u_1)
φ : R ⟶ S
rw : φ ≫ (ΓSpecIso S).inv ≫ (ΓSpecIso S).hom = φ
rw₁ : φ ≫ 𝟙 S = φ
⊢ φ ≫
      (ΓSpecIso S).inv ≫
        CategoryStruct.comp (Y := (Spec S).presheaf.stalk (closedPoint (↑S : Type u_1)))
          ((Spec S).presheaf.germ ⊤ (closedPoint (↑S : Type u_1)) trivial) (Iso.hom (stalkClosedPointIso S)) =
    φ
have rw₂ : φ = φ
Tactic: rw [germ_stalkClosedPointIso_hom, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
U : X.Opens
hU : Membership.mem (α := ↥X) U (f (closedPoint (↑R : Type u)) : ↥X)
⊢ X.presheaf.germ U (f (closedPoint (↑R : Type u))) hU ≫ stalkClosedPointTo f =
    Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (Iso.op (eqToIso ⋯)) ≪≫ ΓSpecIso R).hom
have rw : Hom.app f U ≫
    CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
      ((Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint (↑R : Type u)) hU) (Iso.hom (stalkClosedPointIso R)) =
  Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (Iso.op (eqToIso sorry))).hom ≫ (ΓSpecIso R).hom
Tactic: rw [stalkClosedPointTo, Scheme.Hom.germ_stalkMap_assoc, Iso.trans_hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
U : X.Opens
hU : Membership.mem (α := ↥X) U (f (closedPoint (↑R : Type u)) : ↥X)
⊢ Hom.app f U ≫
      CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
        ((Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint (↑R : Type u)) hU) (Iso.hom (stalkClosedPointIso R)) =
    Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (Iso.op (eqToIso ⋯))).hom ≫ (ΓSpecIso R).hom
have e_a : CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
    ((Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint (↑R : Type u)) hU) (Iso.hom (stalkClosedPointIso R)) =
  (Functor.mapIso (Spec R).presheaf (Iso.op (eqToIso sorry))).hom ≫ (ΓSpecIso R).hom
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
U : X.Opens
hU : Membership.mem (α := ↥X) U (f (closedPoint (↑R : Type u)) : ↥X)
⊢ CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
      ((Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint (↑R : Type u)) hU) (Iso.hom (stalkClosedPointIso R)) =
    (Functor.mapIso (Spec R).presheaf (Iso.op (eqToIso ⋯))).hom ≫ (ΓSpecIso R).hom
have e_a : Eq (α := Γ(Spec R, f ⁻¹ᵁ U) ⟶ (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
  ((Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint (↑R : Type u)) hU)
  ((Functor.mapIso (Spec R).presheaf (Iso.op (eqToIso sorry))).hom ≫
    (Spec R).presheaf.germ ⊤ (closedPoint (↑R : Type u)) trivial)
Tactic: rw [← Iso.eq_comp_inv, Category.assoc, ΓSpecIso_hom_stalkClosedPointIso_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst_1 : IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)
U : X.Opens
hU : Membership.mem (α := ↥X) U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) : ↥X)
⊢ (Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) = x
have rw : (X.fromSpecStalk x) ((Spec.map f) (closedPoint (↑R : Type u)) : ↥(Spec (X.presheaf.stalk x))) = x
Tactic: rw [Hom.comp_apply, Spec_closedPoint, fromSpecStalk_closedPoint]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst_1 : IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)
U : X.Opens
hU : Membership.mem (α := ↥X) U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) : ↥X)
rw : (X.fromSpecStalk x) ((Spec.map f) (closedPoint (↑R : Type u)) : ↥(Spec (X.presheaf.stalk x))) = x
⊢ (Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) = x
have rw₁ : (X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u)) = x
Tactic: rw [Hom.comp_apply, Spec_closedPoint, fromSpecStalk_closedPoint]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst_1 : IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)
U : X.Opens
hU : Membership.mem (α := ↥X) U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) : ↥X)
rw : (X.fromSpecStalk x) ((Spec.map f) (closedPoint (↑R : Type u)) : ↥(Spec (X.presheaf.stalk x))) = x
rw₁ : (X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u)) = x
⊢ (Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) = x
have rw₂ : x = x
Tactic: rw [Hom.comp_apply, Spec_closedPoint, fromSpecStalk_closedPoint]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (hypothesis)
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst_1 : IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)
U : X.Opens
hU : Membership.mem (α := ↥X) U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) : ↥X)
⊢ X.presheaf.germ U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u))) hU ≫
      stalkClosedPointTo (Spec.map f ≫ X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯ ≫ f
have this : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) = x
Tactic: have : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint R) = x := by
    rw [Hom.comp_apply, Spec_closedPoint, fromSpecStalk_closedPoint]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (hypothesis)
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst_1 : IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)
U : X.Opens
hU : Membership.mem (α := ↥X) U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) : ↥X)
this : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) = x
⊢ X.presheaf.germ U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u))) hU ≫
      stalkClosedPointTo (Spec.map f ≫ X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯ ≫ f
have this₁ : x ∈ U
Tactic: have : x ∈ U := this ▸ hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst_1 : IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)
U : X.Opens
hU : Membership.mem (α := ↥X) U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) : ↥X)
this_1 : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) = x
this : x ∈ U
⊢ X.presheaf.germ U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u))) hU ≫
      stalkClosedPointTo (Spec.map f ≫ X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯ ≫ f
have simp : X.presheaf.germ U x this ≫ Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫ Hom.appLE (Spec.map f) ⊤ ⊤ sorry ≫ (ΓSpecIso R).hom =
  X.presheaf.germ U x sorry ≫ f
Tactic: simp only [germ_stalkClosedPointTo, Hom.comp_app,
    fromSpecStalk_app (X := X) (x := x) this, Category.assoc, Iso.trans_hom, Functor.mapIso_hom,
      (Spec.map f).app_eq_appLE, Hom.appLE_map_assoc, Hom.map_appLE_assoc]