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))
⊢ 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:
exact X.presheaf.germ_res_apply _ _ _ _

Premises used: TopCat.Presheaf.germ_res_apply, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
f : (↑(X.presheaf.obj U) : Type u_1)
h :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)),
    x ∈
        (↑(X.basicOpen (U := unop V)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                    CommRingCat.carrier) (X.presheaf.map i) :
                  (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
                f)) :
          Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ↔
      x ∈ (↑(unop V ⊓ X.basicOpen f) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
⊢ X.basicOpen (U := unop V)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i) :
          (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
        f) =
    unop V ⊓ X.basicOpen f

Tactic:
ext x
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
f : (↑(X.presheaf.obj U) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
h :
  x ∈
      (↑(X.basicOpen (U := unop V)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map i) :
                (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
              f)) :
        Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) →
    x ∈ (↑(unop V ⊓ X.basicOpen f) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
h₁ :
  x ∈ (↑(unop V ⊓ X.basicOpen f) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) →
    x ∈
      (↑(X.basicOpen (U := unop V)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map i) :
                (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
              f)) :
        Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
⊢ x ∈
      (↑(X.basicOpen (U := unop V)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map i) :
                (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
              f)) :
        Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ↔
    x ∈ (↑(unop V ⊓ X.basicOpen f) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))

Tactic:
constructor
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
f : (↑(X.presheaf.obj U) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxV : x ∈ unop V
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 (unop V) x hxV) :
          (a : (↑(X.presheaf.obj (op (unop V))) : 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 i) :
              (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
            f :
          (↑(X.presheaf.obj V) : Type u_1)) :
      (↑(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 (unop U) x ⋯) :
          (a : (↑(X.presheaf.obj (op (unop U))) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
rw [germ_res_apply' X.presheaf] at hx

Premises used: TopCat.Presheaf.germ_res_apply', AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
f : (↑(X.presheaf.obj U) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxV : x ∈ unop V
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 (unop U) x ⋯) :
          (a : (↑(X.presheaf.obj (op (unop U))) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
⊢ x ∈ (↑(unop V ⊓ X.basicOpen f) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))

Tactic:
⟨hxV, i.unop.le hxV, hx⟩

Premises used: Set.Mem, Quiver.Hom.le, setOf, Quiver.Hom.unop, Set.inter, And.intro, Exists.intro
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
f : (↑(X.presheaf.obj U) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxV : x ∈ unop V
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 (unop U) x ⋯) :
          (a : (↑(X.presheaf.obj (op (unop U))) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
⊢ x ∈ (↑(unop V ⊓ X.basicOpen f) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))

Tactic:
exact ⟨hxV, i.unop.le hxV, hx⟩
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
f : (↑(X.presheaf.obj U) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxV : x ∈ (↑(unop V) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
w : x ∈ unop 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 (unop U) x w) :
          (a : (↑(X.presheaf.obj (op (unop U))) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
⊢ x ∈
    (↑(X.basicOpen (U := unop V)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X.presheaf.map i) :
              (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
            f)) :
      Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))

Tactic:
⟨hxV, ?_⟩

Premises used: Set.Mem, setOf, Exists.intro
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
f : (↑(X.presheaf.obj U) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxV : x ∈ (↑(unop V) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
w : x ∈ unop 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 (unop U) x w) :
          (a : (↑(X.presheaf.obj (op (unop U))) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
h :
  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 (unop V) x hxV) :
          (a : (↑(X.presheaf.obj (op (unop V))) : 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 i) :
              (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
            f :
          (↑(X.presheaf.obj V) : Type u_1)) :
      (↑(X.presheaf.stalk x) : Type u_1))
⊢ x ∈
    (↑(X.basicOpen (U := unop V)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X.presheaf.map i) :
              (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
            f)) :
      Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))

Tactic:
refine ⟨hxV, ?_⟩
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
f : (↑(X.presheaf.obj U) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxV : x ∈ (↑(unop V) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
w : x ∈ unop 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 (unop U) x w) :
          (a : (↑(X.presheaf.obj (op (unop U))) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
h :
  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 (unop U) x ⋯) :
          (a : (↑(X.presheaf.obj (op (unop 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 (unop V) x hxV) :
          (a : (↑(X.presheaf.obj (op (unop V))) : 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 i) :
              (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
            f :
          (↑(X.presheaf.obj V) : Type u_1)) :
      (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
rw [germ_res_apply' X.presheaf]

Premises used: TopCat.Presheaf.germ_res_apply', AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
f : (↑(X.presheaf.obj U) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxV : x ∈ (↑(unop V) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
w : x ∈ unop 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 (unop U) x w) :
          (a : (↑(X.presheaf.obj (op (unop 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 (unop U) x ⋯) :
          (a : (↑(X.presheaf.obj (op (unop 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 V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
f : (↑(X.presheaf.obj U) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxV : x ∈ (↑(unop V) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
w : x ∈ unop 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 (unop U) x w) :
          (a : (↑(X.presheaf.obj (op (unop 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 (unop U) x ⋯) :
          (a : (↑(X.presheaf.obj (op (unop U))) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
exact hx
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
inst : IsIso i
f : (↑(X.presheaf.obj U) : Type u_1)
a :
  X.basicOpen (U := unop V)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i) :
          (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
        f) ≤
    X.basicOpen f
a₁ :
  X.basicOpen f ≤
    X.basicOpen (U := unop V)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i) :
          (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
        f)
⊢ X.basicOpen (U := unop V)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i) :
          (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
        f) =
    X.basicOpen f

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
inst : IsIso i
f : (↑(X.presheaf.obj U) : Type u_1)
a : unop V ⊓ X.basicOpen f ≤ X.basicOpen f
⊢ X.basicOpen (U := unop V)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i) :
          (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
        f) ≤
    X.basicOpen f

Tactic:
rw [X.basicOpen_res i f]

Premises used: AlgebraicGeometry.RingedSpace.basicOpen_res
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
inst : IsIso i
f : (↑(X.presheaf.obj U) : Type u_1)
⊢ unop V ⊓ X.basicOpen f ≤ X.basicOpen f

Tactic:
inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
inst : IsIso i
f : (↑(X.presheaf.obj U) : Type u_1)
⊢ unop V ⊓ X.basicOpen f ≤ X.basicOpen f

Tactic:
exact inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
inst : IsIso i
f : (↑(X.presheaf.obj U) : Type u_1)
⊢ X.basicOpen (U := unop U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (inv i)) :
          (a : (↑(X.presheaf.obj V) : Type u_1)) → (↑(X.presheaf.obj U) : 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) :
              (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
            f :
          (↑(X.presheaf.obj V) : Type u_1))) =
    unop U ⊓
      X.basicOpen (U := unop V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.map i) :
            (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
          f)

Tactic:
have := X.basicOpen_res (inv i) (X.presheaf.map i f)
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
inst : IsIso i
f : (↑(X.presheaf.obj U) : Type u_1)
this :
  X.basicOpen (U := unop U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (inv i)) :
          (a : (↑(X.presheaf.obj V) : Type u_1)) → (↑(X.presheaf.obj U) : 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) :
              (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
            f :
          (↑(X.presheaf.obj V) : Type u_1))) =
    unop U ⊓
      X.basicOpen (U := unop V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.map i) :
            (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
          f)
⊢ X.basicOpen f =
    unop U ⊓
      X.basicOpen (U := unop V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.map i) :
            (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
          f)

Tactic:
rw [← CommRingCat.comp_apply, ← X.presheaf.map_comp, IsIso.hom_inv_id, X.presheaf.map_id,
        CommRingCat.id_apply] at this

Premises used: CommRingCat.id_apply, CategoryTheory.Functor.map_id, CommRingCat.comp_apply, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp, CategoryTheory.IsIso.hom_inv_id, AlgebraicGeometry.SheafedSpace.toPresheafedSpace
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
inst : IsIso i
f : (↑(X.presheaf.obj U) : Type u_1)
this :
  X.basicOpen f =
    unop U ⊓
      X.basicOpen (U := unop V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.map i) :
            (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
          f)
a :
  unop U ⊓
      X.basicOpen (U := unop V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.map i) :
            (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
          f) ≤
    X.basicOpen (U := unop V)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i) :
          (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
        f)
⊢ X.basicOpen f ≤
    X.basicOpen (U := unop V)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i) :
          (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
        f)

Tactic:
rw [this]
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
inst : IsIso i
f : (↑(X.presheaf.obj U) : Type u_1)
this :
  X.basicOpen f =
    unop U ⊓
      X.basicOpen (U := unop V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.map i) :
            (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
          f)
⊢ unop U ⊓
      X.basicOpen (U := unop V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.map i) :
            (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
          f) ≤
    X.basicOpen (U := unop V)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i) :
          (a : (↑(X.presheaf.obj U) : Type u_1)) → (↑(X.presheaf.obj V) : Type u_1))
        f)

Tactic:
inf_le_right

Premises used: inf_le_right