awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
Goal:
X Y : RingedSpace
f g : X ⟶ Y
H : f = g
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
h :
  IsLocalHom (R :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) f.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
            x)) :
      Type u_1))
    (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
    (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) f.hom.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
              x)) :
        Type u_1) →+*
      (↑(X.presheaf.stalk x) : Type u_1))
    (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f.hom x))
⊢ IsLocalHom (R :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) g.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
            x)) :
      Type u_1))
    (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
    (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) g.hom.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
              x)) :
        Type u_1) →+*
      (↑(X.presheaf.stalk x) : Type u_1))
    (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap g.hom x))
have rw : IsLocalHom (R :=
  (↑(Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) g.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
          x)) :
    Type u_1))
  (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
  (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) g.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
            x)) :
      Type u_1) →+*
    (↑(X.presheaf.stalk x) : Type u_1))
  (CommRingCat.Hom.hom (eqToHom sorry ≫ PresheafedSpace.Hom.stalkMap f.hom x))
Tactic: rw [PresheafedSpace.stalkMap.congr_hom _ _ (congr_arg InducedCategory.Hom.hom H.symm) x]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ PreservesColimit F forgetToSheafedSpace
have suffices : PreservesColimit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
  forgetToSheafedSpace
Tactic: suffices PreservesColimit (parallelPair (F.map WalkingParallelPairHom.left)
        (F.map WalkingParallelPairHom.right)) forgetToSheafedSpace from
      preservesColimit_of_iso_diagram _ (diagramIsoParallelPair F).symm
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ PreservesColimit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
    forgetToSheafedSpace
have apply : IsColimit (F :=
  parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right) ⋙ forgetToSheafedSpace)
  (forgetToSheafedSpace.mapCocone
    (coequalizerCofork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))
Tactic: apply preservesColimit_of_preserves_colimit_cocone (coequalizerCoforkIsColimit _ _)
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ IsColimit (F :=
    parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right) ⋙ forgetToSheafedSpace)
    (forgetToSheafedSpace.mapCocone
      (coequalizerCofork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))
have apply : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply (isColimitMapCoconeCoforkEquiv _ _).symm _
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have dsimp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: dsimp only [forgetToSheafedSpace]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField (goal)
Goal:
X : LocallyRingedSpace
U : Opens (↑X.toTopCat : Type u)
x : ↥U
f : (↑(X.presheaf.obj (op U)) : Type u)
⊢ Eq (α := (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X.evaluation x) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
          f :
        (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
      (0 : (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u)) ↔
    (↑x : (↑X.toTopCat : Type u)) ∉ X.toRingedSpace.basicOpen f
have rw : ¬Eq (α := (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X.evaluation x) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
          f :
        (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
      (0 : (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u)) ↔
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk (↑x : (↑X.toTopCat : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk (↑x : (↑X.toTopCat : Type u)))
            (X.toRingedSpace.presheaf.germ U (↑x : (↑X.toTopCat : Type u)) sorry) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u)) →
            (↑(X.toRingedSpace.presheaf.stalk (↑x : (↑X.toTopCat : Type u))) : Type u))
        f :
      (↑(X.toRingedSpace.presheaf.stalk (↑x : (↑X.toTopCat : Type u))) : Type u))
Tactic: rw [X.toRingedSpace.mem_basicOpen f x.1 x.2, ← not_iff_not, not_not]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField (goal)
Goal:
X : LocallyRingedSpace
U : Opens (↑X.toTopCat : Type u)
f : (↑(X.presheaf.obj (op U)) : Type u)
⊢ X.toRingedSpace.basicOpen f = ⊥ ↔
    ∀ (x : ↥U),
      Eq (α := (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.evaluation x) :
              (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
            f :
          (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
        (0 : (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
have simp : X.toRingedSpace.basicOpen f = ⊥ ↔ ∀ (a : (↑X.toTopCat : Type u)) (b : a ∈ U), a ∉ X.toRingedSpace.basicOpen f
Tactic: simp only [evaluation_eq_zero_iff_notMem_basicOpen, Subtype.forall]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField (goal)
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
⊢ residueFieldMap (𝟙 X) x = 𝟙 (X.residueField x)
have hf : CommRingCat.Hom.hom (residueFieldMap (𝟙 X) x) = CommRingCat.Hom.hom (𝟙 (X.residueField x))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField (goal)
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
⊢ CommRingCat.Hom.hom (residueFieldMap (𝟙 X) x) = CommRingCat.Hom.hom (𝟙 (X.residueField x))
have hf : CommRingCat.Hom.hom (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (𝟙 (X.presheaf.stalk x))))) =
  CommRingCat.Hom.hom (𝟙 (X.residueField x))
Tactic: simp only [residueFieldMap, stalkMap_id]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField (goal)
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
Z : LocallyRingedSpace
g : Y ⟶ Z
x : (↑X.toTopCat : Type u)
⊢ residueFieldMap (f ≫ g) x =
    residueFieldMap g
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              f.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x) ≫
      residueFieldMap f x
have hf : CommRingCat.Hom.hom (residueFieldMap (f ≫ g) x) =
  CommRingCat.Hom.hom
    (residueFieldMap g
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              f.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x) ≫
      residueFieldMap f x)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField (goal)
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
Z : LocallyRingedSpace
g : Y ⟶ Z
x : (↑X.toTopCat : Type u)
⊢ CommRingCat.Hom.hom (residueFieldMap (f ≫ g) x) =
    CommRingCat.Hom.hom
      (residueFieldMap g
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x) ≫
        residueFieldMap f x)
have hf : Eq (α :=
  (↑(Z.residueField
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (f ≫ g).base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u) →+*
    (↑(X.residueField x) : Type u))
  (CommRingCat.Hom.hom
    (CommRingCat.ofHom
      (IsLocalRing.ResidueField.map
        (CommRingCat.Hom.hom
          (Hom.stalkMap g
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                x) ≫
            Hom.stalkMap f x)))))
  (CommRingCat.Hom.hom
    (CategoryStruct.comp (Y :=
      Y.residueField
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              f.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x))
      (CommRingCat.ofHom
        (IsLocalRing.ResidueField.map
          (CommRingCat.Hom.hom
            (Hom.stalkMap g
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                x)))))
      (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x))))))
Tactic: simp only [residueFieldMap, stalkMap_comp]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace (goal)
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
h : f.toHom = g.toHom
⊢ f = g
have mk : ∀ (toHom : X.Hom Y.toPresheafedSpace)
  (prop :
    ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)),
      IsLocalHom (R :=
        (↑(Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    toHom.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                x)) :
          Type u))
        (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
        (↑(Y.presheaf.stalk
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      toHom.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                  x)) :
            Type u) →+*
          (↑(X.presheaf.stalk x) : Type u))
        (CommRingCat.Hom.hom (toHom.stalkMap x)))
  (h : { toHom := toHom, prop := prop : X.Hom Y }.toHom = g.toHom), { toHom := toHom, prop := prop : X.Hom Y } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace (goal)
Goal:
X Y : LocallyRingedSpace
g : X ⟶ Y
toHom : X.Hom Y.toPresheafedSpace
prop :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)),
    IsLocalHom (R :=
      (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  toHom.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u))
      (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
      (↑(Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    toHom.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                x)) :
          Type u) →+*
        (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (toHom.stalkMap x))
h : { toHom := toHom, prop := prop : X.Hom Y }.toHom = g.toHom
⊢ { toHom := toHom, prop := prop : X.Hom Y } = g
have mk : ∀ (toHom_1 : X.Hom Y.toPresheafedSpace)
  (prop_1 :
    ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)),
      IsLocalHom (R :=
        (↑(Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    toHom_1.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                x)) :
          Type u))
        (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
        (↑(Y.presheaf.stalk
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      toHom_1.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                  x)) :
            Type u) →+*
          (↑(X.presheaf.stalk x) : Type u))
        (CommRingCat.Hom.hom (toHom_1.stalkMap x)))
  (h : { toHom := toHom, prop := prop : X.Hom Y }.toHom = { toHom := toHom_1, prop := prop_1 }.toHom),
  { toHom := toHom, prop := prop : X.Hom Y } = { toHom := toHom_1, prop := prop_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace (goal)
Goal:
X_1 X : LocallyRingedSpace
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)
⊢ IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(X.presheaf.stalk x) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (𝟙 X.toPresheafedSpace) x))
have erw : IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u))
  (CommRingCat.Hom.hom (𝟙 (X.presheaf.stalk x)))
Tactic: erw [PresheafedSpace.stalkMap.id]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace (goal)
Goal:
X_1 X Y Z : LocallyRingedSpace
f : X.Hom Y
g : Y.Hom Z
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)
⊢ IsLocalHom (R :=
    (↑(Z.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                (↑X.toPresheafedSpace : TopCat)) (Y := (↑Z.toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (f.toHom ≫ g.toHom)) :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u))
    (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Z.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Z.toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base (f.toHom ≫ g.toHom)) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u) →+*
      (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (f.toHom ≫ g.toHom) x))
have rw : IsLocalHom (R :=
  (↑(Z.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              (↑X.toPresheafedSpace : TopCat)) (Y := (↑Z.toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base (f.toHom ≫ g.toHom)) :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
          x)) :
    Type u))
  (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
  (↑(Z.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                (↑X.toPresheafedSpace : TopCat)) (Y := (↑Z.toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (f.toHom ≫ g.toHom)) :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u) →+*
    (↑(X.presheaf.stalk x) : Type u))
  (CommRingCat.Hom.hom
    (g.stalkMap
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x) ≫
      f.stalkMap x))
Tactic: rw [PresheafedSpace.stalkMap.comp]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace (goal)
Goal:
X_1 X Y Z : LocallyRingedSpace
f : X.Hom Y
g : Y.Hom Z
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)
⊢ IsLocalHom (R :=
    (↑(Z.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                (↑X.toPresheafedSpace : TopCat)) (Y := (↑Z.toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (f.toHom ≫ g.toHom)) :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u))
    (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Z.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Z.toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base (f.toHom ≫ g.toHom)) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u) →+*
      (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom
      (g.stalkMap
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x) ≫
        f.stalkMap x))
have inst : IsLocalHom (R :=
  (↑(Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x)) :
    Type u))
  (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
  (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u) →+*
    (↑(X.presheaf.stalk x) : Type u))
  (CommRingCat.Hom.hom' (f.stalkMap x))
Tactic: apply +allowSynthFailures RingHom.isLocalHom_comp
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace (goal)
Goal:
X : LocallyRingedSpace
X_1 Y : LocallyRingedSpace
a₁ a₂ : X_1 ⟶ Y
h : forgetToSheafedSpace.map a₁ = forgetToSheafedSpace.map a₂
⊢ a₁ = a₂
have h₁ : a₁.toHom = a₂.toHom
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace (goal)
Goal:
X_1 X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ homOfSheafedSpaceHomOfIsIso f.hom ≫ homOfSheafedSpaceHomOfIsIso f.inv = 𝟙 X
have h : (homOfSheafedSpaceHomOfIsIso f.hom ≫ homOfSheafedSpaceHomOfIsIso f.inv).toHom = Hom.toHom (𝟙 X)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace (goal)
Goal:
X_1 X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ (homOfSheafedSpaceHomOfIsIso f.hom ≫ homOfSheafedSpaceHomOfIsIso f.inv).toHom = Hom.toHom (𝟙 X)
have h : f.hom.hom ≫ f.inv.hom = 𝟙 X.toPresheafedSpace
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace (goal)
Goal:
X_1 X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 X.toPresheafedSpace
have h : (f.hom ≫ f.inv).hom = 𝟙 X.toPresheafedSpace
Tactic: rw [← InducedCategory.comp_hom, f.hom_inv_id, SheafedSpace.id_hom]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace (goal)
Goal:
X_1 X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
h : (f.hom ≫ f.inv).hom = 𝟙 X.toPresheafedSpace
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 X.toPresheafedSpace
have h₁ : InducedCategory.Hom.hom (𝟙 X.toSheafedSpace) = 𝟙 X.toPresheafedSpace
Tactic: rw [← InducedCategory.comp_hom, f.hom_inv_id, SheafedSpace.id_hom]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace (goal)
Goal:
X_1 X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
h : (f.hom ≫ f.inv).hom = 𝟙 X.toPresheafedSpace
h₁ : InducedCategory.Hom.hom (𝟙 X.toSheafedSpace) = 𝟙 X.toPresheafedSpace
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 X.toPresheafedSpace
have h₂ : 𝟙 X.toPresheafedSpace = 𝟙 X.toPresheafedSpace
Tactic: rw [← InducedCategory.comp_hom, f.hom_inv_id, SheafedSpace.id_hom]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace (goal)
Goal:
X_1 X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ homOfSheafedSpaceHomOfIsIso f.inv ≫ homOfSheafedSpaceHomOfIsIso f.hom = 𝟙 Y
have h : (homOfSheafedSpaceHomOfIsIso f.inv ≫ homOfSheafedSpaceHomOfIsIso f.hom).toHom = Hom.toHom (𝟙 Y)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace (goal)
Goal:
X_1 X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ (homOfSheafedSpaceHomOfIsIso f.inv ≫ homOfSheafedSpaceHomOfIsIso f.hom).toHom = Hom.toHom (𝟙 Y)
have h : f.inv.hom ≫ f.hom.hom = 𝟙 Y.toPresheafedSpace
Tactic: dsimp