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

Premises used: zero_ne_one
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u)
f : (↑(X.presheaf.obj (op U)) : Type u)
hf : IsNilpotent f
obtain : ∀ (n : ℕ) (hn : f ^ n = 0), X.toRingedSpace.basicOpen f = ⊥
⊢ X.toRingedSpace.basicOpen f = ⊥

Tactic:
obtain ⟨n, hn⟩ := hf
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u)
f : (↑(X.presheaf.obj (op U)) : Type u)
n : ℕ
hn : f ^ n = 0
h : n > 0
inr :
  Eq.{u + 1} (α := Opens (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))
    (X.toRingedSpace.basicOpen (U := U) 0) ⊥
⊢ X.toRingedSpace.basicOpen f = ⊥

Tactic:
rw [← X.toRingedSpace.basicOpen_pow f n h, hn]

Premises used: AlgebraicGeometry.LocallyRingedSpace.toRingedSpace, AlgebraicGeometry.RingedSpace.basicOpen_pow
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u)
f : (↑(X.presheaf.obj (op U)) : Type u)
n : ℕ
hn : f ^ n = 0
h : n > 0
⊢ Eq.{u + 1} (α := Opens (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))
    (X.toRingedSpace.basicOpen (U := U) 0) ⊥

Tactic:
simp [basicOpen_zero]

Premises used: AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u)
f : (↑(X.presheaf.obj (op U)) : Type u)
n : ℕ
hn : f ^ n = 0
h : n = 0
⊢ Eq.{u + 1} (α := (↑(X.presheaf.obj (op U)) : Type u)) 1 0

Tactic:
rw [h, pow_zero] at hn

Premises used: pow_zero
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u)
f : (↑(X.presheaf.obj (op U)) : Type u)
n : ℕ
hn : f ^ n = 0
h : n = 0
hn₁ : Eq.{u + 1} (α := (↑(X.presheaf.obj (op U)) : Type u)) 1 0
⊢ n = 0

Tactic:
rw [h, pow_zero] at hn

Premises used: pow_zero
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u)
f : (↑(X.presheaf.obj (op U)) : Type u)
n : ℕ
hn : Eq.{u + 1} (α := (↑(X.presheaf.obj (op U)) : Type u)) 1 0
h : n = 0
⊢ X.toRingedSpace.basicOpen f = ⊥

Tactic:
simp [eq_zero_of_zero_eq_one hn.symm f, basicOpen_zero]

Premises used: AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero, eq_zero_of_zero_eq_one, Eq.symm
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u)
f : (↑(X.presheaf.obj (op U)) : Type u)
n : ℕ
hn : f ^ n = 0
⊢ n = 0 ∨ n > 0

Tactic:
cases n.eq_zero_or_pos with
  | inr h =>
    rw [← X.toRingedSpace.basicOpen_pow f n h, hn]
    simp [basicOpen_zero]
  | inl h =>
    rw [h, pow_zero] at hn
    simp [eq_zero_of_zero_eq_one hn.symm f, basicOpen_zero]

Premises used: AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero, pow_zero, eq_zero_of_zero_eq_one, Nat.eq_zero_or_pos
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X : LocallyRingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u)
hU : Nonempty.{u + 1} ↥U
⊢ Nontrivial.{u} (↑(X.presheaf.obj (op U)) : Type u)

Tactic:
(X.presheaf.germ _ _ hU.some.2).hom.domain_nontrivial

Premises used: CommRingCat.Hom.hom, Nonempty.some, TopCat.Presheaf.germ, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, RingHom.domain_nontrivial, Subtype.property
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
e : X ≅ Y
⊢ e.hom.base ≫ e.inv.base = 𝟙 (↑X.toPresheafedSpace : TopCat)

Tactic:
simp only [← comp_base, Iso.hom_inv_id, id_toHom, PresheafedSpace.id_base]

Premises used: CategoryTheory.Iso.hom_inv_id, AlgebraicGeometry.LocallyRingedSpace.comp_base, AlgebraicGeometry.PresheafedSpace.id_base, AlgebraicGeometry.LocallyRingedSpace.id_toHom
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
e : X ≅ Y
x : (↑X.toTopCat : Type u)
change :
  Eq (α := (↑(↑X.toPresheafedSpace : TopCat) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (e.hom.base ≫ e.inv.base) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
        x :
      (↑(↑X.toPresheafedSpace : TopCat) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (PresheafedSpace.Hom.base (𝟙 X.toPresheafedSpace)) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
        x :
      (↑(↑X.toPresheafedSpace : TopCat) : Type u))
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) e.inv.base :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              e.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x :
        (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) =
    x

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

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

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

Tactic:
simp only [← comp_base, Iso.inv_hom_id, id_toHom, PresheafedSpace.id_base]

Premises used: CategoryTheory.Iso.inv_hom_id, AlgebraicGeometry.LocallyRingedSpace.comp_base, AlgebraicGeometry.PresheafedSpace.id_base, AlgebraicGeometry.LocallyRingedSpace.id_toHom
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
e : X ≅ Y
y : (↑Y.toTopCat : Type u)
change :
  Eq (α := (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (e.inv.base ≫ e.hom.base) :
          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
        y :
      (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (PresheafedSpace.Hom.base (𝟙 Y.toPresheafedSpace)) :
          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
        y :
      (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) e.hom.base :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              e.inv.base :
            (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
          y :
        (↑(↑X.toPresheafedSpace : TopCat) : Type u)) =
    y

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

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

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
⊢ Hom.stalkMap (𝟙 X) x = 𝟙 (X.presheaf.stalk x)

Tactic:
PresheafedSpace.stalkMap.id _ x

Premises used: AlgebraicGeometry.PresheafedSpace.stalkMap.id, AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X.toTopCat : Type u)
⊢ Hom.stalkMap (f ≫ g) x =
    Hom.stalkMap g
        ((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) ≫
      Hom.stalkMap f x

Tactic:
PresheafedSpace.stalkMap.comp f.toHom g.toHom x

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.PresheafedSpace.stalkMap.comp, AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
x x' : (↑X.toTopCat : Type u)
h : x ⤳ x'
⊢ Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x = Hom.stalkMap f x' ≫ X.presheaf.stalkSpecializes h

Tactic:
PresheafedSpace.stalkMap.stalkSpecializes_stalkMap f.toHom h

Premises used: AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
hfg : f = g
x x' : (↑X.toTopCat : Type u)
hxx' : x = x'
subst : Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x'
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap g x'

Tactic:
subst hfg
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
x x' : (↑X.toTopCat : Type u)
hxx' : x = x'
subst : Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x'

Tactic:
subst hxx'
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : (↑X.toTopCat : Type u)
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
hfg : f = g
x : (↑X.toTopCat : Type u)
subst : Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x
⊢ Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap g x

Tactic:
subst hfg
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : (↑X.toTopCat : Type u)
⊢ Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
e : X ≅ Y
y : (↑Y.toTopCat : Type u)
⊢ y =
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) e.hom.base :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              e.inv.base :
            (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
          y :
        (↑(↑X.toPresheafedSpace : TopCat) : Type u))

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
e : X ≅ Y
y : (↑Y.toTopCat : Type u)
⊢ e.inv ≫ e.hom = 𝟙 Y

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
e : X ≅ Y
y : (↑Y.toTopCat : Type u)
rw : Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (𝟙 Y) y = Y.presheaf.stalkSpecializes ⋯
⊢ Hom.stalkMap e.hom
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              e.inv.base :
            (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
          y) ≫
      Hom.stalkMap e.inv y =
    Y.presheaf.stalkSpecializes ⋯

Tactic:
rw [← stalkMap_comp, LocallyRingedSpace.stalkMap_congr_hom (e.inv ≫ e.hom) (𝟙 _) (by simp)]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, AlgebraicGeometry.LocallyRingedSpace.stalkMap_comp, CategoryTheory.Iso.inv, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
e : X ≅ Y
y : (↑Y.toTopCat : Type u)
⊢ Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (𝟙 Y) y = Y.presheaf.stalkSpecializes ⋯

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
e : X ≅ Y
y : (↑Y.toTopCat : Type u)
z :
  (↑(Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              e.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  e.inv.base :
                (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
              y :
            (↑(↑X.toPresheafedSpace : TopCat) : Type u)))) :
    Type u)
⊢ y =
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) e.hom.base :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              e.inv.base :
            (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
          y :
        (↑(↑X.toPresheafedSpace : TopCat) : Type u))

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
e : X ≅ Y
x : (↑X.toTopCat : Type u)
⊢ x =
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) e.inv.base :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              e.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x :
        (↑(↑Y.toPresheafedSpace : TopCat) : Type u))

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
e : X ≅ Y
x : (↑X.toTopCat : Type u)
⊢ e.hom ≫ e.inv = 𝟙 X

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
e : X ≅ Y
x : (↑X.toTopCat : Type u)
rw : X.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (𝟙 X) x = X.presheaf.stalkSpecializes ⋯
⊢ Hom.stalkMap e.inv
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              e.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x) ≫
      Hom.stalkMap e.hom x =
    X.presheaf.stalkSpecializes ⋯

Tactic:
rw [← stalkMap_comp, LocallyRingedSpace.stalkMap_congr_hom (e.hom ≫ e.inv) (𝟙 _) (by simp)]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, AlgebraicGeometry.LocallyRingedSpace.stalkMap_comp, CategoryTheory.Iso.inv, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
e : X ≅ Y
x : (↑X.toTopCat : Type u)
⊢ X.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (𝟙 X) x = X.presheaf.stalkSpecializes ⋯

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
e : X ≅ Y
x : (↑X.toTopCat : Type u)
y :
  (↑(X.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              e.inv.base :
            (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  e.hom.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
              x :
            (↑(↑Y.toPresheafedSpace : TopCat) : Type u)))) :
    Type u)
⊢ x =
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) e.inv.base :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              e.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x :
        (↑(↑Y.toPresheafedSpace : TopCat) : Type u))

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens (↑Y.toTopCat : Type u)
x : (↑X.toTopCat : Type u)
hx :
  Membership.mem (α := (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) U
    ((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 :
      (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
⊢ Y.presheaf.germ U
        ((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)
        hx ≫
      Hom.stalkMap f x =
    f.c.app (op U) ≫ X.presheaf.germ ((Opens.map f.base).obj U) x hx

Tactic:
PresheafedSpace.stalkMap_germ f.toHom U x hx

Premises used: AlgebraicGeometry.PresheafedSpace.stalkMap_germ, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens (↑Y.toTopCat : Type u)
s : (↑(Y.presheaf.obj (op U)) : Type u)
h :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)),
    x ∈ (↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s)) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u)) ↔
      x ∈
        (↑(X.toRingedSpace.basicOpen (U := (Opens.map f.base).obj U)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (X := Y.presheaf.obj (op U)) (f.c.app (op U)) :
                  (a : (↑(Y.presheaf.obj (op U)) : Type u)) →
                    (↑(((Presheaf.pushforward CommRingCat f.base).obj X.presheaf).obj (op U)) : Type u))
                s)) :
          Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
⊢ (Opens.map f.base).obj (Y.toRingedSpace.basicOpen s) =
    X.toRingedSpace.basicOpen (U := (Opens.map f.base).obj U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Y.presheaf.obj (op U)) (f.c.app (op U)) :
          (a : (↑(Y.presheaf.obj (op U)) : Type u)) →
            (↑(((Presheaf.pushforward CommRingCat f.base).obj X.presheaf).obj (op U)) : Type u))
        s)

Tactic:
ext x
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens (↑Y.toTopCat : Type u)
s : (↑(Y.presheaf.obj (op U)) : Type u)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)
h :
  x ∈ (↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s)) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
    x ∈
      (↑(X.toRingedSpace.basicOpen (U := (Opens.map f.base).obj U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := Y.presheaf.obj (op U)) (f.c.app (op U)) :
                (a : (↑(Y.presheaf.obj (op U)) : Type u)) →
                  (↑(((Presheaf.pushforward CommRingCat f.base).obj X.presheaf).obj (op U)) : Type u))
              s)) :
        Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
h₁ :
  x ∈
      (↑(X.toRingedSpace.basicOpen (U := (Opens.map f.base).obj U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := Y.presheaf.obj (op U)) (f.c.app (op U)) :
                (a : (↑(Y.presheaf.obj (op U)) : Type u)) →
                  (↑(((Presheaf.pushforward CommRingCat f.base).obj X.presheaf).obj (op U)) : Type u))
              s)) :
        Set (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
    x ∈ (↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s)) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
⊢ x ∈ (↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s)) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u)) ↔
    x ∈
      (↑(X.toRingedSpace.basicOpen (U := (Opens.map f.base).obj U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := Y.presheaf.obj (op U)) (f.c.app (op U)) :
                (a : (↑(Y.presheaf.obj (op U)) : Type u)) →
                  (↑(((Presheaf.pushforward CommRingCat f.base).obj X.presheaf).obj (op U)) : Type u))
              s)) :
        Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))

Tactic:
constructor