awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X Y Z : LocallyRingedSpace
f : X.Hom Y
g : Y.Hom Z
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)
                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 isLocalHomValStalkMap

Premises used: AlgebraicGeometry.LocallyRingedSpace.isLocalHomValStalkMap
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
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 :=
    (↑(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))
    (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) →+*
      (↑(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))
    (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)))

Tactic:
apply isLocalHomValStalkMap

Premises used: AlgebraicGeometry.LocallyRingedSpace.isLocalHomValStalkMap
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
X_1 Y : LocallyRingedSpace
a₁ a₂ : X_1 ⟶ Y
h : forgetToSheafedSpace.map a₁ = forgetToSheafedSpace.map a₂
h₁ : a₁.toHom = a₂.toHom
⊢ a₁ = a₂

Tactic:
ext : 1
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
X_1 Y : LocallyRingedSpace
a₁ a₂ : X_1 ⟶ Y
h : forgetToSheafedSpace.map a₁ = forgetToSheafedSpace.map a₂
⊢ a₁.toHom = a₂.toHom

Tactic:
congr_arg InducedCategory.Hom.hom h

Premises used: congr_arg, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
X_1 Y : LocallyRingedSpace
a₁ a₂ : X_1 ⟶ Y
h : forgetToSheafedSpace.map a₁ = forgetToSheafedSpace.map a₂
⊢ a₁.toHom = a₂.toHom

Tactic:
exact congr_arg InducedCategory.Hom.hom h

Premises used: congr_arg, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X Y : LocallyRingedSpace
f : X.toSheafedSpace ⟶ Y.toSheafedSpace
h :
  ∀ (x : (↑X.toTopCat : Type u)),
    IsLocalHom (R :=
      (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  f.hom.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.hom.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                x)) :
          Type u) →+*
        (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f.hom x))
⊢ ∀ (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)
                  f.hom.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.hom.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                x)) :
          Type u) →+*
        (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f.hom x))

Tactic:
assumption
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
⊢ Hom.toHom (𝟙 X) = 𝟙 X.toPresheafedSpace

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).toHom = f.toHom ≫ g.toHom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.toShHom (f ≫ g) = Hom.toShHom f ≫ Hom.toShHom g

Tactic:
rfl

Premises used: CategoryTheory.InducedCategory.homMk, rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
⊢ Hom.toShHom (𝟙 X) = 𝟙 X.toSheafedSpace

Tactic:
rfl

Premises used: CategoryTheory.InducedCategory.homMk, rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).base = f.base ≫ g.base

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).c = g.c ≫ map (Presheaf.pushforward CommRingCat g.base) f.c

Tactic:
rfl

Premises used: CategoryTheory.Functor.op, Set.Mem, setOf, CategoryTheory.Functor.comp, Set.preimage, TopologicalSpace.Opens.map, rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
U : (Opens (↑Z.toTopCat : Type u))ᵒᵖ
⊢ (f ≫ g).c.app U = g.c.app U ≫ f.c.app (op ((Opens.map g.base).obj (unop U)))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
h : (homOfSheafedSpaceHomOfIsIso f.hom ≫ homOfSheafedSpaceHomOfIsIso f.inv).toHom = Hom.toHom (𝟙 X)
⊢ homOfSheafedSpaceHomOfIsIso f.hom ≫ homOfSheafedSpaceHomOfIsIso f.inv = 𝟙 X

Tactic:
ext : 1
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
h : f.hom.hom ≫ f.inv.hom = 𝟙 X.toPresheafedSpace
⊢ (homOfSheafedSpaceHomOfIsIso f.hom ≫ homOfSheafedSpaceHomOfIsIso f.inv).toHom = Hom.toHom (𝟙 X)

Tactic:
dsimp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
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
h₂ h₃ : 𝟙 X.toPresheafedSpace = 𝟙 X.toPresheafedSpace
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 X.toPresheafedSpace

Tactic:
rw [← InducedCategory.comp_hom, f.hom_inv_id, SheafedSpace.id_hom]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.InducedCategory.comp_hom, AlgebraicGeometry.SheafedSpace.id_hom
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
h : (homOfSheafedSpaceHomOfIsIso f.inv ≫ homOfSheafedSpaceHomOfIsIso f.hom).toHom = Hom.toHom (𝟙 Y)
⊢ homOfSheafedSpaceHomOfIsIso f.inv ≫ homOfSheafedSpaceHomOfIsIso f.hom = 𝟙 Y

Tactic:
ext : 1
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
h : f.inv.hom ≫ f.hom.hom = 𝟙 Y.toPresheafedSpace
⊢ (homOfSheafedSpaceHomOfIsIso f.inv ≫ homOfSheafedSpaceHomOfIsIso f.hom).toHom = Hom.toHom (𝟙 Y)

Tactic:
dsimp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
h : (f.inv ≫ f.hom).hom = 𝟙 Y.toPresheafedSpace
h₁ : InducedCategory.Hom.hom (𝟙 Y.toSheafedSpace) = 𝟙 Y.toPresheafedSpace
h₂ h₃ : 𝟙 Y.toPresheafedSpace = 𝟙 Y.toPresheafedSpace
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 Y.toPresheafedSpace

Tactic:
rw [← InducedCategory.comp_hom, f.inv_hom_id, SheafedSpace.id_hom]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.InducedCategory.comp_hom, AlgebraicGeometry.SheafedSpace.id_hom
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X Y : LocallyRingedSpace
f : X ⟶ Y
inst : IsIso f
⊢ IsIso (Hom.toShHom f)

Tactic:
LocallyRingedSpace.forgetToSheafedSpace.map_isIso f

Premises used: CategoryTheory.InducedCategory.homMk, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, CategoryTheory.Functor.map_isIso
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 : LocallyRingedSpace
U : TopCat
X : LocallyRingedSpace
f : U ⟶ X.toTopCat
h :
  IsOpenEmbedding (X := (↑U : Type u)) (Y := (↑X.toTopCat : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑U : Type u)) → (↑X.toTopCat : Type u))
x : (↑(↑(X.restrict h).toPresheafedSpace : TopCat) : Type u)
e :
  (↑(X.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
              (a : (↑U : Type u)) → (↑X.toTopCat : Type u))
            x)) :
      Type u) ≃+*
    (↑((X.restrict h).presheaf.stalk x) : Type u)
⊢ IsLocalRing.{u} (↑((X.restrict h).presheaf.stalk x) : Type u)

Tactic:
apply @RingEquiv.isLocalRing _ _ _ (X.isLocalRing (f x))

Premises used: RingEquiv.isLocalRing
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 : LocallyRingedSpace
U : TopCat
X : LocallyRingedSpace
f : U ⟶ X.toTopCat
h :
  IsOpenEmbedding (X := (↑U : Type u)) (Y := (↑X.toTopCat : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑U : Type u)) → (↑X.toTopCat : Type u))
x : (↑(↑(X.restrict h).toPresheafedSpace : TopCat) : Type u)
⊢ (↑(X.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
              (a : (↑U : Type u)) → (↑X.toTopCat : Type u))
            x)) :
      Type u) ≃+*
    (↑((X.restrict h).presheaf.stalk x) : Type u)

Tactic:
exact (X.restrictStalkIso h x).symm.commRingCatIsoToRingEquiv

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.Iso.symm, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.PresheafedSpace.restrictStalkIso
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
⊢ Γ = forgetToSheafedSpace.op ⋙ SheafedSpace.Γ

Tactic:
rfl

Premises used: AlgebraicGeometry.LocallyRingedSpace.Γ, rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpaceᵒᵖ
⊢ Γ.obj X = (unop X).presheaf.obj (op ⊤)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
⊢ Γ.obj (op X) = X.presheaf.obj (op ⊤)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpaceᵒᵖ
f : X ⟶ Y
⊢ Γ.map f = f.unop.c.app (op ⊤)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
⊢ Γ.map f.op = f.c.app (op ⊤)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X : LocallyRingedSpace
⊢ Continuous (Y := (↑X.toPresheafedSpace.1 : Type u)) fun (x : PEmpty.{u + 1}) ↦ x.elim

Tactic:
fun_prop
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X : LocallyRingedSpace
U : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u))ᵒᵖ
refine_1 : Eq.{u + 1} (α := PUnit.{u + 1}) (0 1) 1
refine_2 :
  ∀ (x y : (↑(X.presheaf.1 U) : Type u)),
    OneHom.toFun { toFun := 0, map_one' := ⋯ } (x * y) =
      HMul.hMul (α := PUnit.{u + 1})
        (OneHom.toFun { toFun := 0, map_one' := ⋯ : OneHom (↑(X.presheaf.1 U) : Type u) PUnit.{u + 1} } x)
        (OneHom.toFun { toFun := 0, map_one' := ⋯ : OneHom (↑(X.presheaf.1 U) : Type u) PUnit.{u + 1} } y)
refine_3 :
  Eq.{u + 1} (α := PUnit.{u + 1})
    (OneHom.toFun (M := (↑(X.presheaf.1 U) : Type u))
      (↑{ toFun := 0, map_one' := ⋯, map_mul' := ⋯ } : OneHom (↑(X.presheaf.1 U) : Type u) PUnit.{u + 1}) 0)
    0
refine_4 :
  ∀ (x y : (↑(X.presheaf.1 U) : Type u)),
    OneHom.toFun (↑{ toFun := 0, map_one' := ⋯, map_mul' := ⋯ } : OneHom (↑(X.presheaf.1 U) : Type u) PUnit.{u + 1})
        (x + y) =
      HAdd.hAdd (α := PUnit.{u + 1})
        (OneHom.toFun
          (↑{ toFun := 0, map_one' := ⋯, map_mul' := ⋯ : (↑(X.presheaf.1 U) : Type u) →* PUnit.{u + 1} } :
            OneHom (↑(X.presheaf.1 U) : Type u) PUnit.{u + 1})
          x)
        (OneHom.toFun
          (↑{ toFun := 0, map_one' := ⋯, map_mul' := ⋯ : (↑(X.presheaf.1 U) : Type u) →* PUnit.{u + 1} } :
            OneHom (↑(X.presheaf.1 U) : Type u) PUnit.{u + 1})
          y)
⊢ (↑(X.presheaf.1 U) : Type u) →+* PUnit.{u + 1}

Tactic:
refine ⟨⟨⟨0, ?_⟩, ?_⟩, ?_, ?_⟩
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X : LocallyRingedSpace
U : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u))ᵒᵖ
⊢ Eq.{u + 1} (α := PUnit.{u + 1}) (0 1) 1

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X : LocallyRingedSpace
U : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u))ᵒᵖ
x y : (↑(X.presheaf.1 U) : Type u)
⊢ OneHom.toFun { toFun := 0, map_one' := ⋯ } (x * y) =
    HMul.hMul (α := PUnit.{u + 1})
      (OneHom.toFun { toFun := 0, map_one' := ⋯ : OneHom (↑(X.presheaf.1 U) : Type u) PUnit.{u + 1} } x)
      (OneHom.toFun { toFun := 0, map_one' := ⋯ : OneHom (↑(X.presheaf.1 U) : Type u) PUnit.{u + 1} } y)

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X : LocallyRingedSpace
U : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u))ᵒᵖ
⊢ Eq.{u + 1} (α := PUnit.{u + 1})
    (OneHom.toFun (M := (↑(X.presheaf.1 U) : Type u))
      (↑{ toFun := 0, map_one' := ⋯, map_mul' := ⋯ } : OneHom (↑(X.presheaf.1 U) : Type u) PUnit.{u + 1}) 0)
    0

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X : LocallyRingedSpace
U : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u))ᵒᵖ
x y : (↑(X.presheaf.1 U) : Type u)
⊢ OneHom.toFun (↑{ toFun := 0, map_one' := ⋯, map_mul' := ⋯ } : OneHom (↑(X.presheaf.1 U) : Type u) PUnit.{u + 1})
      (x + y) =
    HAdd.hAdd (α := PUnit.{u + 1})
      (OneHom.toFun
        (↑{ toFun := 0, map_one' := ⋯, map_mul' := ⋯ : (↑(X.presheaf.1 U) : Type u) →* PUnit.{u + 1} } :
          OneHom (↑(X.presheaf.1 U) : Type u) PUnit.{u + 1})
        x)
      (OneHom.toFun
        (↑{ toFun := 0, map_one' := ⋯, map_mul' := ⋯ : (↑(X.presheaf.1 U) : Type u) →* PUnit.{u + 1} } :
          OneHom (↑(X.presheaf.1 U) : Type u) PUnit.{u + 1})
        y)

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X : LocallyRingedSpace
f : ∅ ⟶ X
h :
  ∀ (carrier : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u)) (is_open' : IsOpen carrier)
    (x : (↑(X.presheaf.obj (op { carrier := carrier, is_open' := is_open' })) : Type u)),
    Eq (α :=
      (↑(((Opens.map X.emptyTo.base).op ⋙ (toSheafedSpace ∅).presheaf).obj
            (op { carrier := carrier, is_open' := is_open' })) :
        Type u))
      ((CommRingCat.Hom.hom
              (NatTrans.app (f.c ≫ whiskerRight (eqToHom ⋯) (toSheafedSpace ∅).presheaf)
                (op { carrier := carrier, is_open' := is_open' })) :
            (a : (↑(X.presheaf.obj (op { carrier := carrier, is_open' := is_open' })) : Type u)) →
              (↑(((Opens.map X.emptyTo.base).op ⋙ ∅.presheaf).obj (op { carrier := carrier, is_open' := is_open' })) :
                Type u))
          x :
        (↑(((Opens.map X.emptyTo.base).op ⋙ (toSheafedSpace ∅).presheaf).obj
              (op { carrier := carrier, is_open' := is_open' })) :
          Type u))
      ((CommRingCat.Hom.hom (X.emptyTo.c.app (op { carrier := carrier, is_open' := is_open' })) :
            (a : (↑(X.presheaf.obj (op { carrier := carrier, is_open' := is_open' })) : Type u)) →
              (↑(((Opens.map X.emptyTo.base).op ⋙ ∅.presheaf).obj (op { carrier := carrier, is_open' := is_open' })) :
                Type u))
          x :
        (↑(((Opens.map X.emptyTo.base).op ⋙ (toSheafedSpace ∅).presheaf).obj
              (op { carrier := carrier, is_open' := is_open' })) :
          Type u))
⊢ f = X.emptyTo

Tactic:
ext ⟨⟩ x
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X : LocallyRingedSpace
f : ∅ ⟶ X
carrier : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u)
is_open' : IsOpen carrier
x : (↑(X.presheaf.obj (op { carrier := carrier, is_open' := is_open' })) : Type u)
h h₁ h₂ h₃ :
  Eq (α :=
    (↑(((Opens.map X.emptyTo.base).op ⋙ (toSheafedSpace ∅).presheaf).obj
          (op { carrier := carrier, is_open' := is_open' })) :
      Type u))
    ((CommRingCat.Hom.hom
            (NatTrans.app (f.c ≫ whiskerRight (eqToHom ⋯) (toSheafedSpace ∅).presheaf)
              (op { carrier := carrier, is_open' := is_open' })) :
          (a : (↑(X.presheaf.obj (op { carrier := carrier, is_open' := is_open' })) : Type u)) →
            (↑(((Opens.map X.emptyTo.base).op ⋙ ∅.presheaf).obj (op { carrier := carrier, is_open' := is_open' })) :
              Type u))
        x :
      (↑(((Opens.map X.emptyTo.base).op ⋙ (toSheafedSpace ∅).presheaf).obj
            (op { carrier := carrier, is_open' := is_open' })) :
        Type u))
    ((CommRingCat.Hom.hom (X.emptyTo.c.app (op { carrier := carrier, is_open' := is_open' })) :
          (a : (↑(X.presheaf.obj (op { carrier := carrier, is_open' := is_open' })) : Type u)) →
            (↑(((Opens.map X.emptyTo.base).op ⋙ ∅.presheaf).obj (op { carrier := carrier, is_open' := is_open' })) :
              Type u))
        x :
      (↑(((Opens.map X.emptyTo.base).op ⋙ (toSheafedSpace ∅).presheaf).obj
            (op { carrier := carrier, is_open' := is_open' })) :
        Type u))
⊢ Eq (α :=
    (↑(((Opens.map X.emptyTo.base).op ⋙ (toSheafedSpace ∅).presheaf).obj
          (op { carrier := carrier, is_open' := is_open' })) :
      Type u))
    ((CommRingCat.Hom.hom
            (NatTrans.app (f.c ≫ whiskerRight (eqToHom ⋯) (toSheafedSpace ∅).presheaf)
              (op { carrier := carrier, is_open' := is_open' })) :
          (a : (↑(X.presheaf.obj (op { carrier := carrier, is_open' := is_open' })) : Type u)) →
            (↑(((Opens.map X.emptyTo.base).op ⋙ ∅.presheaf).obj (op { carrier := carrier, is_open' := is_open' })) :
              Type u))
        x :
      (↑(((Opens.map X.emptyTo.base).op ⋙ (toSheafedSpace ∅).presheaf).obj
            (op { carrier := carrier, is_open' := is_open' })) :
        Type u))
    ((CommRingCat.Hom.hom (X.emptyTo.c.app (op { carrier := carrier, is_open' := is_open' })) :
          (a : (↑(X.presheaf.obj (op { carrier := carrier, is_open' := is_open' })) : Type u)) →
            (↑(((Opens.map X.emptyTo.base).op ⋙ ∅.presheaf).obj (op { carrier := carrier, is_open' := is_open' })) :
              Type u))
        x :
      (↑(((Opens.map X.emptyTo.base).op ⋙ (toSheafedSpace ∅).presheaf).obj
            (op { carrier := carrier, is_open' := is_open' })) :
        Type u))

Tactic:
cat_disch
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u)
h :
  ∀ (x : (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u)),
    x ∈ (↑(X.toRingedSpace.basicOpen (U := U) 0) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u)) ↔
      x ∈ (↑⊥ : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))
⊢ Eq.{u + 1} (α := Opens (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))
    (X.toRingedSpace.basicOpen (U := U) 0) ⊥

Tactic:
ext x
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u)
x : (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u)
h :
  ∀ (x_1 : x ∈ U),
    ¬IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : 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.toRingedSpace.presheaf.germ U x ⋯) :
              (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u))
            0 :
          (↑(X.toRingedSpace.presheaf.stalk x) : Type u))
⊢ x ∈ (↑(X.toRingedSpace.basicOpen (U := U) 0) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u)) ↔
    x ∈ (↑⊥ : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))

Tactic:
simp only [RingedSpace.basicOpen, Opens.coe_mk, Set.mem_setOf_eq,
    Opens.coe_bot, Set.mem_empty_iff_false,
    iff_false, not_exists]

Premises used: iff_false, not_exists, Set.mem_setOf_eq, AlgebraicGeometry.RingedSpace.basicOpen, TopologicalSpace.Opens.coe_mk, TopologicalSpace.Opens.coe_bot, Set.mem_empty_iff_false
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u)
x : (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u)
hx : x ∈ U
h : ¬Eq.{u + 1} (α := (↑(X.toRingedSpace.presheaf.stalk x) : Type u)) 0 1
⊢ ¬IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : 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.toRingedSpace.presheaf.germ U x ⋯) :
            (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u))
          0 :
        (↑(X.toRingedSpace.presheaf.stalk x) : Type u))

Tactic:
rw [map_zero, isUnit_zero_iff]

Premises used: map_zero, isUnit_zero_iff
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u)
x : (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u)
hx : x ∈ U
h : Ne.{u + 1} (α := (↑(X.presheaf.stalk x) : Type u)) 0 1
⊢ ¬Eq.{u + 1} (α := (↑(X.toRingedSpace.presheaf.stalk x) : Type u)) 0 1

Tactic:
change (0 : X.presheaf.stalk x) ≠ (1 : X.presheaf.stalk x)

Premises used: OfNat.ofNat
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u)
x : (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u)
hx : x ∈ U
⊢ Ne.{u + 1} (α := (↑(X.presheaf.stalk x) : Type u)) 0 1

Tactic:
zero_ne_one

Premises used: zero_ne_one