awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f g : (↑(X.presheaf.obj (op U)) : Type u_1)
h :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)),
    x ∈ (↑(X.basicOpen (f * g)) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ↔
      x ∈ (↑(X.basicOpen f ⊓ X.basicOpen g) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
⊢ X.basicOpen (f * g) = X.basicOpen f ⊓ X.basicOpen g

Tactic:
ext x
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f g : (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
pos :
  ∀ (hx : x ∈ U),
    x ∈ (↑(X.basicOpen (f * g)) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ↔
      x ∈ (↑(X.basicOpen f ⊓ X.basicOpen g) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
neg :
  ∀ (hx : x ∉ U),
    x ∈ (↑(X.basicOpen (f * g)) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ↔
      x ∈ (↑(X.basicOpen f ⊓ X.basicOpen g) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
⊢ x ∈ (↑(X.basicOpen (f * g)) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ↔
    x ∈ (↑(X.basicOpen f ⊓ X.basicOpen g) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))

Tactic:
by_cases hx : x ∈ U
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f g : (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hx : x ∈ U
⊢ x ∈ (↑(X.basicOpen (f * g)) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ↔
    x ∈ (↑(X.basicOpen f ⊓ X.basicOpen g) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))

Tactic:
simp [mem_basicOpen (hx := hx)]

Premises used: AlgebraicGeometry.RingedSpace.mem_basicOpen
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f g : (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hx : x ∉ U
⊢ x ∈ (↑(X.basicOpen (f * g)) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ↔
    x ∈ (↑(X.basicOpen f ⊓ X.basicOpen g) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))

Tactic:
simp [mt (basicOpen_le X _ ·) hx]

Premises used: mt, AlgebraicGeometry.RingedSpace.basicOpen_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)
n : ℕ
h : 0 < n
obtain : ∀ (k : ℕ) (h : 0 < k + Nat.succ 0), X.basicOpen (f ^ (k + Nat.succ 0)) = X.basicOpen f
⊢ X.basicOpen (f ^ n) = X.basicOpen f

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' h

Premises used: Nat.exists_eq_add_of_le', rfl
-- 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 : 0 < 0 + Nat.succ 0
⊢ X.basicOpen (f ^ (0 + Nat.succ 0)) = X.basicOpen f

Tactic:
simp
-- 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)
n : ℕ
hn : ∀ (h : 0 < n + Nat.succ 0), X.basicOpen (f ^ (n + Nat.succ 0)) = X.basicOpen f
h : 0 < n + 1 + Nat.succ 0
succ : X.basicOpen (f ^ (n + 1) * f ^ Nat.succ 0) = X.basicOpen f
⊢ X.basicOpen (f ^ (n + 1 + Nat.succ 0)) = X.basicOpen f

Tactic:
rw [pow_add]

Premises used: pow_add
-- 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)
n : ℕ
hn : ∀ (h : 0 < n + Nat.succ 0), X.basicOpen (f ^ (n + Nat.succ 0)) = X.basicOpen f
h : 0 < n + 1 + Nat.succ 0
⊢ X.basicOpen (f ^ (n + 1) * f ^ Nat.succ 0) = X.basicOpen f

Tactic:
simp_all
-- 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)
k : ℕ
h : 0 < k + Nat.succ 0
zero : ∀ (h : 0 < 0 + Nat.succ 0), X.basicOpen (f ^ (0 + Nat.succ 0)) = X.basicOpen f
succ :
  ∀ (n : ℕ) (hn : ∀ (h : 0 < n + Nat.succ 0), X.basicOpen (f ^ (n + Nat.succ 0)) = X.basicOpen f)
    (h : 0 < n + 1 + Nat.succ 0), X.basicOpen (f ^ (n + 1 + Nat.succ 0)) = X.basicOpen f
⊢ X.basicOpen (f ^ (k + Nat.succ 0)) = X.basicOpen f

Tactic:
induction k with
  | zero => simp
  | succ n hn => rw [pow_add]; simp_all

Premises used: pow_add
-- 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)
hf : IsUnit f
a : X.basicOpen f ≤ U
a₁ : U ≤ X.basicOpen f
⊢ X.basicOpen f = U

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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)
hf : IsUnit f
⊢ X.basicOpen f ≤ U

Tactic:
X.basicOpen_le f

Premises used: AlgebraicGeometry.RingedSpace.basicOpen_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)
hf : IsUnit f
⊢ X.basicOpen f ≤ U

Tactic:
exact X.basicOpen_le f

Premises used: AlgebraicGeometry.RingedSpace.basicOpen_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)
hf : IsUnit f
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hx : x ∈ U
a :
  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))
⊢ x ∈ X.basicOpen f

Tactic:
rw [X.mem_basicOpen f x hx]

Premises used: AlgebraicGeometry.RingedSpace.mem_basicOpen
-- 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)
hf : IsUnit f
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))

Tactic:
RingHom.isUnit_map _ hf

Premises used: RingHom.isUnit_map
-- 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)
hf : IsUnit f
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))

Tactic:
exact RingHom.isUnit_map _ hf

Premises used: RingHom.isUnit_map
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
s : Set (↑(X.presheaf.obj (op U)) : Type u_1)
h : ∀ i ∈ s, IsClosed (↑(X.basicOpen i) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᶜ
⊢ IsClosed (X.zeroLocus s)

Tactic:
apply isClosed_biInter

Premises used: isClosed_biInter
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
s : Set (↑(X.presheaf.obj (op U)) : Type u_1)
i : (↑(X.presheaf.obj (op U)) : Type u_1)
h : i ∈ s → IsClosed (↑(X.basicOpen i) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᶜ
⊢ i ∈ s → IsClosed (↑(X.basicOpen i) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᶜ

Tactic:
_
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
s : Set (↑(X.presheaf.obj (op U)) : Type u_1)
i : (↑(X.presheaf.obj (op U)) : Type u_1)
h_1 : i ∈ s
h : IsOpen (↑(X.basicOpen i) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
⊢ IsClosed (↑(X.basicOpen i) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᶜ

Tactic:
simp only [isClosed_compl_iff]

Premises used: isClosed_compl_iff
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
s : Set (↑(X.presheaf.obj (op U)) : Type u_1)
i : (↑(X.presheaf.obj (op U)) : Type u_1)
h : i ∈ s
⊢ IsOpen (↑(X.basicOpen i) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))

Tactic:
Opens.isOpen (X.basicOpen i)

Premises used: AlgebraicGeometry.RingedSpace.basicOpen, TopologicalSpace.Opens.isOpen
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
s : Set (↑(X.presheaf.obj (op U)) : Type u_1)
i : (↑(X.presheaf.obj (op U)) : Type u_1)
h : i ∈ s
⊢ IsOpen (↑(X.basicOpen i) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))

Tactic:
exact Opens.isOpen (X.basicOpen i)

Premises used: AlgebraicGeometry.RingedSpace.basicOpen, TopologicalSpace.Opens.isOpen
-- 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.zeroLocus (U := U) {f} = (X.basicOpen f).carrierᶜ

Tactic:
simp [zeroLocus]

Premises used: AlgebraicGeometry.RingedSpace.zeroLocus
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
⊢ X.zeroLocus (U := U) ∅ = Set.univ

Tactic:
simp [zeroLocus]

Premises used: AlgebraicGeometry.RingedSpace.zeroLocus
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
s : Set (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
⊢ x ∈ X.zeroLocus s ↔ ∀ f ∈ s, x ∉ X.basicOpen f

Tactic:
simp [zeroLocus]

Premises used: AlgebraicGeometry.RingedSpace.zeroLocus
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{w', w} J
inst_2 : Small.{v, w} J
F : J ⥤ SheafedSpace.{u, v, v} C
inst_3 : HasLimitsOfShape.{w', w, v, u} Jᵒᵖ C
c : Cocone F
hc : IsColimit c
x : (↑(↑c.pt.toPresheafedSpace : TopCat) : Type v)
⊢ ∃ (i : J) (y : (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (c.ι.app i).hom.base :
          (a : (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)) →
            (↑(↑(((Functor.const J).obj c.pt).obj i).toPresheafedSpace : TopCat) : Type v))
        y =
      x

Tactic:
Concrete.isColimit_exists_rep (F ⋙ forget C) (isColimitOfPreserves (forget C) hc) x

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.Concrete.isColimit_exists_rep, AlgebraicGeometry.SheafedSpace.forget, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{w', w} J
inst_2 : Small.{v, w} J
F : J ⥤ SheafedSpace.{u, v, v} C
inst_3 : HasLimitsOfShape.{w', w, v, u} Jᵒᵖ C
x : (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v)
⊢ ∃ (i : J) (y : (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (Y :=
            (↑(colimit F).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι F i))) :
          (a : (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)) →
            (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))
        y =
      x

Tactic:
Concrete.isColimit_exists_rep (F ⋙ SheafedSpace.forget C)
    (isColimitOfPreserves (SheafedSpace.forget _) (colimit.isColimit F)) x

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.Concrete.isColimit_exists_rep, AlgebraicGeometry.SheafedSpace.forget, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{w', w} J
inst_2 : Small.{v, w} J
F : J ⥤ SheafedSpace.{u, v, v} C
inst_3 : HasLimits.{v, u} C
X Y : SheafedSpace.{u, v, v} C
f g : X ⟶ Y
rw :
  Epi (X := (↑Y.toPresheafedSpace : TopCat)) (Y := (↑(coequalizer f g).toPresheafedSpace : TopCat))
    (CategoryStruct.comp (Y :=
        coequalizer (X := Functor.obj (forget C) X) (CategoryTheory.Functor.map (forget C) f)
          (CategoryTheory.Functor.map (forget C) g))
        (coequalizer.π (CategoryTheory.Functor.map (forget C) f) (CategoryTheory.Functor.map (forget C) g))
        (Iso.hom (PreservesCoequalizer.iso (forget C) f g)) :
      Functor.obj (forget C) Y ⟶ Functor.obj (forget C) (coequalizer f g))
⊢ Epi (Y := (↑(coequalizer f g).toPresheafedSpace : TopCat))
    (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π f g)))

Tactic:
rw [← show _ = (coequalizer.π f g).hom.base from
      ι_comp_coequalizerComparison f g (SheafedSpace.forget C),
      ← PreservesCoequalizer.iso_hom]

Premises used: AlgebraicGeometry.SheafedSpace.forget, CategoryTheory.Limits.PreservesCoequalizer.iso_hom, CategoryTheory.Limits.ι_comp_coequalizerComparison
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{w', w} J
inst_2 : Small.{v, w} J
F : J ⥤ SheafedSpace.{u, v, v} C
inst_3 : HasLimits.{v, u} C
X Y : SheafedSpace.{u, v, v} C
f g : X ⟶ Y
⊢ Epi (X := (↑Y.toPresheafedSpace : TopCat)) (Y := (↑(coequalizer f g).toPresheafedSpace : TopCat))
    (CategoryStruct.comp (Y :=
        coequalizer (X := Functor.obj (forget C) X) (CategoryTheory.Functor.map (forget C) f)
          (CategoryTheory.Functor.map (forget C) g))
        (coequalizer.π (CategoryTheory.Functor.map (forget C) f) (CategoryTheory.Functor.map (forget C) g))
        (Iso.hom (PreservesCoequalizer.iso (forget C) f g)) :
      Functor.obj (forget C) Y ⟶ Functor.obj (forget C) (coequalizer f g))

Tactic:
apply epi_comp

Premises used: CategoryTheory.epi_comp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
ι : Type v
inst : Small.{u, v} ι
F : CategoryTheory.Functor.{v, u, v, u + 1} (Discrete ι) LocallyRingedSpace
x : (↑(↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat) : Type u)
obtain :
  ∀ (i : Discrete ι) (y : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)),
    IsLocalRing.{u}
      (↑((colimit (F ⋙ forgetToSheafedSpace)).presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) (Y := (↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i))) :
                (a : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)) →
                  (↑(↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat) : Type u))
              y)) :
        Type u)
⊢ IsLocalRing.{u} (↑((colimit (F ⋙ forgetToSheafedSpace)).presheaf.stalk x) : Type u)

Tactic:
obtain ⟨i, y, ⟨⟩⟩ := SheafedSpace.colimit_exists_rep (F ⋙ forgetToSheafedSpace) x

Premises used: AlgebraicGeometry.SheafedSpace.colimit_exists_rep, CategoryTheory.Functor.comp, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
ι : Type v
inst : Small.{u, v} ι
F : CategoryTheory.Functor.{v, u, v, u + 1} (Discrete ι) LocallyRingedSpace
i : Discrete ι
y : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)
⊢ IsLocalRing.{u} (↑(((F ⋙ forgetToSheafedSpace).obj i).presheaf.stalk y) : Type u)

Tactic:
haveI : IsLocalRing (((F ⋙ forgetToSheafedSpace).obj i).presheaf.stalk y) :=
      (F.obj i).isLocalRing _
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
ι : Type v
inst : Small.{u, v} ι
F : CategoryTheory.Functor.{v, u, v, u + 1} (Discrete ι) LocallyRingedSpace
i : Discrete ι
y : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)
this : IsLocalRing.{u} (↑(((F ⋙ forgetToSheafedSpace).obj i).presheaf.stalk y) : Type u)
⊢ IsLocalRing.{u}
    (↑((colimit (F ⋙ forgetToSheafedSpace)).presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (Y := (↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i))) :
              (a : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat) : Type u))
            y)) :
      Type u)

Tactic:
(asIso ((colimit.ι (C := SheafedSpace.{u + 1, u, u} CommRingCat.{u})
        (F ⋙ forgetToSheafedSpace) i :).hom.stalkMap y)).symm.commRingCatIsoToRingEquiv.isLocalRing

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, AlgebraicGeometry.PresheafedSpace.Hom.stalkMap, CategoryTheory.Functor.comp, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, RingEquiv.isLocalRing, CategoryTheory.Iso.symm, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.asIso, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
ι : Type v
inst : Small.{u, v} ι
F : CategoryTheory.Functor.{v, u, v, u + 1} (Discrete ι) LocallyRingedSpace
i : Discrete ι
y : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)
this : IsLocalRing.{u} (↑(((F ⋙ forgetToSheafedSpace).obj i).presheaf.stalk y) : Type u)
⊢ IsLocalRing.{u}
    (↑((colimit (F ⋙ forgetToSheafedSpace)).presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (Y := (↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i))) :
              (a : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat) : Type u))
            y)) :
      Type u)

Tactic:
exact
      (asIso ((colimit.ι (C := SheafedSpace.{u + 1, u, u} CommRingCat.{u})
        (F ⋙ forgetToSheafedSpace) i :).hom.stalkMap y)).symm.commRingCatIsoToRingEquiv.isLocalRing
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
ι : Type v
inst : Small.{u, v} ι
F : CategoryTheory.Functor.{v, u, v, u + 1} (Discrete ι) LocallyRingedSpace
x x_1 : Discrete ι
j j' : ι
x_2 : { as := j : Discrete ι } ⟶ { as := j' }
f : j = j'
subst :
  ∀ (x : { as := j : Discrete ι } ⟶ { as := j }),
    Eq (α :=
      F.obj { as := j : Discrete ι } ⟶
        Functor.obj (Functor.obj (Functor.const (Discrete ι)) (coproduct F)) { as := j : Discrete ι })
      (F.map
          { down := { down := ⋯ : PLift ({ as := j : Discrete ι }.as = { as := j : Discrete ι }.as) } :
            ULift.{v, 0} (PLift ({ as := j : Discrete ι }.as = { as := j : Discrete ι }.as)) } ≫
        homMk (colimit.ι (F ⋙ forgetToSheafedSpace) { as := j }) ⋯)
      (homMk (colimit.ι (F ⋙ forgetToSheafedSpace) { as := j }) ⋯ ≫
        CategoryTheory.Functor.map (Functor.obj (Functor.const (Discrete ι)) (coproduct F))
          { down := { down := ⋯ : PLift ({ as := j : Discrete ι }.as = { as := j : Discrete ι }.as) } :
            ULift.{v, 0} (PLift ({ as := j : Discrete ι }.as = { as := j : Discrete ι }.as)) })
⊢ Eq (α :=
    F.obj { as := j : Discrete ι } ⟶
      Functor.obj (Functor.obj (Functor.const (Discrete ι)) (coproduct F)) { as := j' : Discrete ι })
    (F.map
        { down := { down := f : PLift ({ as := j : Discrete ι }.as = { as := j' : Discrete ι }.as) } :
          ULift.{v, 0} (PLift ({ as := j : Discrete ι }.as = { as := j' : Discrete ι }.as)) } ≫
      homMk (colimit.ι (F ⋙ forgetToSheafedSpace) { as := j' }) ⋯)
    (homMk (colimit.ι (F ⋙ forgetToSheafedSpace) { as := j }) ⋯ ≫
      CategoryTheory.Functor.map (Functor.obj (Functor.const (Discrete ι)) (coproduct F))
        { down := { down := f : PLift ({ as := j : Discrete ι }.as = { as := j' : Discrete ι }.as) } :
          ULift.{v, 0} (PLift ({ as := j : Discrete ι }.as = { as := j' : Discrete ι }.as)) })

Tactic:
subst f
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
ι : Type v
inst : Small.{u, v} ι
F : CategoryTheory.Functor.{v, u, v, u + 1} (Discrete ι) LocallyRingedSpace
x x_1 : Discrete ι
j : ι
x_2 : { as := j : Discrete ι } ⟶ { as := j }
⊢ Eq (α :=
    F.obj { as := j : Discrete ι } ⟶
      Functor.obj (Functor.obj (Functor.const (Discrete ι)) (coproduct F)) { as := j : Discrete ι })
    (F.map
        { down := { down := ⋯ : PLift ({ as := j : Discrete ι }.as = { as := j : Discrete ι }.as) } :
          ULift.{v, 0} (PLift ({ as := j : Discrete ι }.as = { as := j : Discrete ι }.as)) } ≫
      homMk (colimit.ι (F ⋙ forgetToSheafedSpace) { as := j }) ⋯)
    (homMk (colimit.ι (F ⋙ forgetToSheafedSpace) { as := j }) ⋯ ≫
      CategoryTheory.Functor.map (Functor.obj (Functor.const (Discrete ι)) (coproduct F))
        { down := { down := ⋯ : PLift ({ as := j : Discrete ι }.as = { as := j : Discrete ι }.as) } :
          ULift.{v, 0} (PLift ({ as := j : Discrete ι }.as = { as := j : Discrete ι }.as)) })

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
ι : Type v
inst : Small.{u, v} ι
F : CategoryTheory.Functor.{v, u, v, u + 1} (Discrete ι) LocallyRingedSpace
s : Cocone F
i : Discrete ι
y : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have := PresheafedSpace.stalkMap.comp
          (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom
          (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom y