awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxU : x ∈ U
hx :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
V : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
i : V ⟶ U
hxV : x ∈ V
hf :
  IsUnit (M := (↑(X.presheaf.obj (op V)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
        f :
      (↑(X.presheaf.obj (op V)) : Type u_1))
y : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hy : y ∈ V.carrier
h :
  IsUnit (M := (↑(X.presheaf.stalk y) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk y) (X.presheaf.germ U y ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk y) : Type u_1))
        f :
      (↑(X.presheaf.stalk y) : Type u_1))
⊢ Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
    {x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1) |
      ∃ (hx : x ∈ U),
        IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
                (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
              f :
            (↑(X.presheaf.stalk x) : Type u_1))}
    y

Tactic:
use i.le hy

Premises used: Quiver.Hom.le
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxU : x ∈ U
hx :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
V : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
i : V ⟶ U
hxV : x ∈ V
hf :
  IsUnit (M := (↑(X.presheaf.obj (op V)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
        f :
      (↑(X.presheaf.obj (op V)) : Type u_1))
y : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hy : y ∈ V.carrier
⊢ IsUnit (M := (↑(X.presheaf.stalk y) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ V y hy) :
          (a : (↑(X.presheaf.obj (op V)) : Type u_1)) → (↑(X.presheaf.stalk y) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X.presheaf.map i.op) :
              (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
            f :
          (↑(X.presheaf.obj (op V)) : Type u_1)) :
      (↑(X.presheaf.stalk y) : Type u_1))

Tactic:
RingHom.isUnit_map (X.presheaf.germ _ y hy).hom hf

Premises used: CommRingCat.Hom.hom, TopCat.Presheaf.germ, AlgebraicGeometry.PresheafedSpace.presheaf, RingHom.isUnit_map, AlgebraicGeometry.SheafedSpace.toPresheafedSpace
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxU : x ∈ U
hx :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
V : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
i : V ⟶ U
hxV : x ∈ V
hf :
  IsUnit (M := (↑(X.presheaf.obj (op V)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
        f :
      (↑(X.presheaf.obj (op V)) : Type u_1))
y : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hy : y ∈ V.carrier
h :
  Eq (α := (↑(X.presheaf.stalk y) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk y) (X.presheaf.germ U y ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk y) : Type u_1))
        f :
      (↑(X.presheaf.stalk y) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ V y hy) :
          (a : (↑(X.presheaf.obj (op V)) : Type u_1)) → (↑(X.presheaf.stalk y) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X.presheaf.map i.op) :
              (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
            f :
          (↑(X.presheaf.obj (op V)) : Type u_1)) :
      (↑(X.presheaf.stalk y) : Type u_1))
⊢ IsUnit (M := (↑(X.presheaf.stalk y) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk y) (X.presheaf.germ U y ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk y) : Type u_1))
        f :
      (↑(X.presheaf.stalk y) : Type u_1))

Tactic:
convert! RingHom.isUnit_map (X.presheaf.germ _ y hy).hom hf

Premises used: CommRingCat.Hom.hom, TopCat.Presheaf.germ, AlgebraicGeometry.PresheafedSpace.presheaf, RingHom.isUnit_map, AlgebraicGeometry.SheafedSpace.toPresheafedSpace
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxU : x ∈ U
hx :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
V : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
i : V ⟶ U
hxV : x ∈ V
hf :
  IsUnit (M := (↑(X.presheaf.obj (op V)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
        f :
      (↑(X.presheaf.obj (op V)) : Type u_1))
y : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hy : y ∈ V.carrier
⊢ Eq (α := (↑(X.presheaf.stalk y) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk y) (X.presheaf.germ U y ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk y) : Type u_1))
        f :
      (↑(X.presheaf.stalk y) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ V y hy) :
          (a : (↑(X.presheaf.obj (op V)) : Type u_1)) → (↑(X.presheaf.stalk y) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X.presheaf.map i.op) :
              (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
            f :
          (↑(X.presheaf.obj (op V)) : Type u_1)) :
      (↑(X.presheaf.stalk y) : Type u_1))

Tactic:
(X.presheaf.germ_res_apply i y hy f).symm

Premises used: TopCat.Presheaf.germ_res_apply, Set.Mem, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Eq.symm
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxU : x ∈ U
hx :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
V : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
i : V ⟶ U
hxV : x ∈ V
hf :
  IsUnit (M := (↑(X.presheaf.obj (op V)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
        f :
      (↑(X.presheaf.obj (op V)) : Type u_1))
y : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hy : y ∈ V.carrier
⊢ Eq (α := (↑(X.presheaf.stalk y) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk y) (X.presheaf.germ U y ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk y) : Type u_1))
        f :
      (↑(X.presheaf.stalk y) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ V y hy) :
          (a : (↑(X.presheaf.obj (op V)) : Type u_1)) → (↑(X.presheaf.stalk y) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X.presheaf.map i.op) :
              (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
            f :
          (↑(X.presheaf.obj (op V)) : Type u_1)) :
      (↑(X.presheaf.stalk y) : Type u_1))

Tactic:
exact (X.presheaf.germ_res_apply i y hy f).symm

Premises used: TopCat.Presheaf.germ_res_apply, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Eq.symm
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hx : x ∈ U
⊢ x ∈ X.basicOpen f ↔
    IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          f :
        (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
⟨Exists.choose_spec, (⟨hx, ·⟩)⟩

Premises used: Exists.choose_spec, Iff.intro, Exists.intro
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
x : ↥U
⊢ (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ∈ X.basicOpen f ↔
    IsUnit (M := (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)))
              (X.presheaf.germ U (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ⋯) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) →
              (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
          f :
        (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))

Tactic:
mem_basicOpen X f x.1 x.2

Premises used: Subtype.val, AlgebraicGeometry.RingedSpace.mem_basicOpen, Subtype.property
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
f : (↑(X.presheaf.obj (op ⊤)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
⊢ x ∈ X.basicOpen f ↔
    IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.Γgerm x) :
            (a : (↑(X.presheaf.obj (op ⊤)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          f :
        (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
mem_basicOpen X f x .intro

Premises used: AlgebraicGeometry.RingedSpace.mem_basicOpen, True.intro
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
h : x ∈ U
h_1 :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x h) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
⊢ x ∈ U

Tactic:
h
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
h : x ∈ U
h_1 :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x h) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
⊢ x ∈ U

Tactic:
exact h
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
h :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) (hx : x ∈ X.basicOpen f),
    IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ (X.basicOpen f) x hx) :
            (a : (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u_1))
              f :
            (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u_1)) :
        (↑(X.presheaf.stalk x) : Type u_1))
⊢ IsUnit (M := (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u_1))
        f :
      (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u_1))

Tactic:
apply isUnit_of_isUnit_germ

Premises used: AlgebraicGeometry.RingedSpace.isUnit_of_isUnit_germ
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxU : x ∈ U
hx :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
⊢ IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
hx
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxU : x ∈ U
hx :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
h :
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.obj (op (X.basicOpen f))) (Y := X.presheaf.stalk x)
            (X.presheaf.germ (X.basicOpen f) x ⋯) :
          (a : (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
              (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u_1))
            f :
          (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u_1)) :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
⊢ IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.obj (op (X.basicOpen f))) (Y := X.presheaf.stalk x)
            (X.presheaf.germ (X.basicOpen f) x ⋯) :
          (a : (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
              (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u_1))
            f :
          (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u_1)) :
      (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
convert! hx
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxU : x ∈ U
hx :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
⊢ Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.obj (op (X.basicOpen f))) (Y := X.presheaf.stalk x)
            (X.presheaf.germ (X.basicOpen f) x ⋯) :
          (a : (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
              (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u_1))
            f :
          (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u_1)) :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
X.presheaf.germ_res_apply _ _ _ _

Premises used: TopCat.Presheaf.germ_res_apply, Set.Mem, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace