awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : Opens ↥X
x : ↥U
f s : (↑Γ(X, U) : Type u)
hx :
  IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        s :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
n : ℕ
hf : s ^ n * f = 0
rw :
  IsUnit
    (HPow.hPow (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
          s :
        (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
      n)
⊢ IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        (s ^ n) :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))

Tactic:
rw [map_pow]

Premises used: map_pow
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : Opens ↥X
x : ↥U
f s : (↑Γ(X, U) : Type u)
hx :
  IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        s :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
n : ℕ
hf : s ^ n * f = 0
⊢ IsUnit
    (HPow.hPow (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
          s :
        (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
      n)

Tactic:
IsUnit.pow n hx

Premises used: IsUnit.pow
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : Opens ↥X
x : ↥U
f s : (↑Γ(X, U) : Type u)
hx :
  IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        s :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
n : ℕ
hf : s ^ n * f = 0
⊢ IsUnit
    (HPow.hPow (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
          s :
        (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
      n)

Tactic:
exact IsUnit.pow n hx

Premises used: IsUnit.pow
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : Opens ↥X
x : ↥U
f s : (↑Γ(X, U) : Type u)
hx :
  IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        s :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
n : ℕ
hf : s ^ n * f = 0
⊢ IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        (s ^ n) :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))

Tactic:
have hu : IsUnit (X.presheaf.germ _ x x.2 (s ^ n)) := by
    rw [map_pow]
    exact IsUnit.pow n hx
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
e : X ≅ Y
⊢ e.hom.base ≫ e.inv.base = 𝟙 (↑X.toPresheafedSpace : TopCat)

Tactic:
LocallyRingedSpace.iso_hom_base_inv_base (Scheme.forgetToLocallyRingedSpace.mapIso e)

Premises used: AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace, CategoryTheory.Functor.mapIso, AlgebraicGeometry.LocallyRingedSpace.iso_hom_base_inv_base
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
e : X ≅ Y
x : ↥X
change :
  Eq (α := ↥X) ((e.hom ≫ e.inv) x : ↥X)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (PresheafedSpace.Hom.base (𝟙 X.toPresheafedSpace)) :
          (a : ↥X) → ↥X)
        x :
      ↥X)
⊢ e.inv (e.hom x : ↥Y) = x

Tactic:
change (e.hom ≫ e.inv) x = 𝟙 X.toPresheafedSpace x

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.id, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Iso.inv, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
e : X ≅ Y
x : ↥X
⊢ Eq (α := ↥X) ((e.hom ≫ e.inv) x : ↥X)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (PresheafedSpace.Hom.base (𝟙 X.toPresheafedSpace)) :
          (a : ↥X) → ↥X)
        x :
      ↥X)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
e : X ≅ Y
⊢ e.inv.base ≫ e.hom.base = 𝟙 (↑Y.toPresheafedSpace : TopCat)

Tactic:
LocallyRingedSpace.iso_inv_base_hom_base (Scheme.forgetToLocallyRingedSpace.mapIso e)

Premises used: AlgebraicGeometry.LocallyRingedSpace.iso_inv_base_hom_base, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace, CategoryTheory.Functor.mapIso
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
e : X ≅ Y
y : ↥Y
change :
  Eq (α := ↥Y) ((e.inv ≫ e.hom) y : ↥Y)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (PresheafedSpace.Hom.base (𝟙 Y.toPresheafedSpace)) :
          (a : ↥Y) → ↥Y)
        y :
      ↥Y)
⊢ e.hom (e.inv y : ↥X) = y

Tactic:
change (e.inv ≫ e.hom) y = 𝟙 Y.toPresheafedSpace y

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.id, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Iso.inv, AlgebraicGeometry.Scheme.toLocallyRingedSpace