awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X.Hom Y
x : ↥X
h :
  ((↑(Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier) (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                    (ofHom
                      { toFun := ⇑f, continuous_toFun := ⋯ :
                        C((↑X.toPresheafedSpace.1 : Type u_1), (↑Y.toPresheafedSpace.1 : Type u_1)) }) :
                  (a : ↥X) → ↥Y)
                x)) :
          Type u_1) →+*
        (↑(X.presheaf.stalk x) : Type u_1)) =
      ((↑(Y.presheaf.stalk (f x)) : Type u_1) →+* (↑(X.presheaf.stalk x) : Type u_1)) →
    Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                (ofHom
                  { toFun := ⇑f, continuous_toFun := ⋯ :
                    C((↑X.toPresheafedSpace.1 : Type u_1), (↑Y.toPresheafedSpace.1 : Type u_1)) }) :
              (a : ↥X) → ↥Y)
            x) =
        Y.presheaf.stalk (f x) →
      HEq (α := (↑X.toPresheafedSpace : TopCat) ⟶ (↑Y.toPresheafedSpace : TopCat))
          (ofHom { toFun := ⇑f, continuous_toFun := ⋯ }) (β :=
          (↑X.toPresheafedSpace : TopCat) ⟶ (↑Y.toPresheafedSpace : TopCat)) (PresheafedSpace.Hom.base f.toLRSHom'.1) →
        f.c ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom = PresheafedSpace.Hom.c f.toLRSHom'.1
⊢ IsLocalHom (R :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                (ofHom { toFun := ⇑f, continuous_toFun := ⋯ }) :
              (a : ↥X) → ↥Y)
            x)) :
      Type u_1))
    (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
    (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  carrier) (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                  (ofHom { toFun := ⇑f, continuous_toFun := ⋯ }) :
                (a : ↥X) → ↥Y)
              x)) :
        Type u_1) →+*
      (↑(X.presheaf.stalk x) : Type u_1))
    (CommRingCat.Hom.hom
      ({ base := ofHom { toFun := ⇑f, continuous_toFun := ⋯ },
            c := f.c ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom }.stalkMap
        x))

Tactic:
convert! f.prop x using 4

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.LocallyRingedSpace.Hom.prop
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X.Hom Y
g : ↥X → ↥Y
h : ⇑f = g
subst : f.copyBase ⇑f ⋯ = f
⊢ f.copyBase g h = f

Tactic:
subst h
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X.Hom Y
obtain :
  ∀ (f₁ : ↥X → ↥Y) (f₂ : Continuous f₁)
    (f₃ :
      Y.presheaf ⟶
        Functor.obj
          (Presheaf.pushforward CommRingCat
            { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
              (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) })
          X.presheaf)
    (f₄ :
      ∀ (x : ↥X),
        IsLocalHom (R :=
          (↑(Y.presheaf.stalk
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                      carrier)
                      {
                          base :=
                            { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                              (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
                          c := f₃ : X.Hom Y.toPresheafedSpace }.base :
                    (a : ↥X) → ↥Y)
                  x)) :
            Type u_1))
          (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
          (↑(Y.presheaf.stalk
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                        carrier)
                        {
                            base :=
                              { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                                (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
                            c := f₃ : X.Hom Y.toPresheafedSpace }.base :
                      (a : ↥X) → ↥Y)
                    x)) :
              Type u_1) →+*
            (↑(X.presheaf.stalk x) : Type u_1))
          (CommRingCat.Hom.hom ({ base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃ }.stalkMap x))),
    {
            base :=
              { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
            c := f₃, prop := f₄ : X.Hom Y }.copyBase
        ⇑{
            base :=
              { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
            c := f₃, prop := f₄ : X.Hom Y }
        ⋯ =
      { base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃, prop := f₄ }
⊢ f.copyBase ⇑f ⋯ = f

Tactic:
obtain ⟨⟨⟨f₁, f₂⟩, f₃⟩, f₄⟩ := f
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f₁ : ↥X → ↥Y
f₂ : Continuous f₁
f₃ :
  Y.presheaf ⟶
    Functor.obj
      (Presheaf.pushforward CommRingCat
        { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
          (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) })
      X.presheaf
f₄ :
  ∀ (x : ↥X),
    IsLocalHom (R :=
      (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  carrier)
                  {
                      base :=
                        { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                          (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
                      c := f₃ : X.Hom Y.toPresheafedSpace }.base :
                (a : ↥X) → ↥Y)
              x)) :
        Type u_1))
      (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
      (↑(Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier)
                    {
                        base :=
                          { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                            (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
                        c := f₃ : X.Hom Y.toPresheafedSpace }.base :
                  (a : ↥X) → ↥Y)
                x)) :
          Type u_1) →+*
        (↑(X.presheaf.stalk x) : Type u_1))
      (CommRingCat.Hom.hom ({ base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃ }.stalkMap x))
simp :
  {
      base :=
        ofHom
          {
            toFun :=
              (⇑(@ConcreteCategory.hom _ TopCat.instCategory
                    (fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) carrier _ _
                    (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)
                    { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                      (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) }) :
                (a : ↥X) → ↥Y),
            continuous_toFun := ⋯ : C((↑X.toPresheafedSpace.1 : Type u_1), (↑Y.toPresheafedSpace.1 : Type u_1)) },
      c := f₃ ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom, prop := ⋯ : X.Hom Y } =
    { base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃, prop := f₄ }
⊢ {
          base :=
            { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
              (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
          c := f₃, prop := f₄ : X.Hom Y }.copyBase
      ⇑{
          base :=
            { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
              (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
          c := f₃, prop := f₄ : X.Hom Y }
      ⋯ =
    { base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃, prop := f₄ }

Tactic:
simp only [Hom.copyBase]

Premises used: AlgebraicGeometry.Scheme.Hom.copyBase
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f₁ : ↥X → ↥Y
f₂ : Continuous f₁
f₃ :
  Y.presheaf ⟶
    Functor.obj
      (Presheaf.pushforward CommRingCat
        { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
          (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) })
      X.presheaf
f₄ :
  ∀ (x : ↥X),
    IsLocalHom (R :=
      (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  carrier)
                  {
                      base :=
                        { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                          (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
                      c := f₃ : X.Hom Y.toPresheafedSpace }.base :
                (a : ↥X) → ↥Y)
              x)) :
        Type u_1))
      (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
      (↑(Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier)
                    {
                        base :=
                          { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                            (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
                        c := f₃ : X.Hom Y.toPresheafedSpace }.base :
                  (a : ↥X) → ↥Y)
                x)) :
          Type u_1) →+*
        (↑(X.presheaf.stalk x) : Type u_1))
      (CommRingCat.Hom.hom ({ base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃ }.stalkMap x))
e_toLRSHom' : f₃ ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom = f₃
⊢ {
      base :=
        ofHom
          {
            toFun :=
              (⇑(@ConcreteCategory.hom _ TopCat.instCategory
                    (fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) carrier _ _
                    (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)
                    { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                      (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) }) :
                (a : ↥X) → ↥Y),
            continuous_toFun := ⋯ : C((↑X.toPresheafedSpace.1 : Type u_1), (↑Y.toPresheafedSpace.1 : Type u_1)) },
      c := f₃ ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom, prop := ⋯ : X.Hom Y } =
    { base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃, prop := f₄ }

Tactic:
congr
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
⊢ (Spec R).toLocallyRingedSpace = Spec.locallyRingedSpaceObj R

Tactic:
rfl

Premises used: AlgebraicGeometry.Spec.locallyRingedSpaceObj, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
⊢ map (𝟙 R) = 𝟙 (Spec R)

Tactic:
Scheme.Hom.ext' <| Spec.locallyRingedSpaceMap_id R

Premises used: AlgebraicGeometry.Scheme.Hom.ext', AlgebraicGeometry.Spec.locallyRingedSpaceMap_id
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ map (f ≫ g) = map g ≫ map f

Tactic:
Scheme.Hom.ext' <| Spec.locallyRingedSpaceMap_comp f g

Premises used: AlgebraicGeometry.Scheme.Hom.ext', AlgebraicGeometry.Spec.locallyRingedSpaceMap_comp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCatᵒᵖ
⊢ Spec.map (Quiver.Hom.unop (𝟙 R)) = 𝟙 (Spec (unop R))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y Z : CommRingCatᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ Spec.map (f ≫ g).unop = Spec.map f.unop ≫ Spec.map g.unop

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R S : CommRingCat
e : R = S
subst : map (eqToHom ⋯) = eqToHom ⋯
⊢ map (eqToHom e) = eqToHom ⋯

Tactic:
subst e
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
⊢ map (eqToHom ⋯) = eqToHom ⋯

Tactic:
Spec.map_id _

Premises used: Eq.mpr, CategoryTheory.eqToHom, AlgebraicGeometry.Spec.map_id
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
⊢ map (eqToHom ⋯) = eqToHom ⋯

Tactic:
exact Spec.map_id _

Premises used: AlgebraicGeometry.Spec.map_id
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R S : CommRingCat
f : R ⟶ S
inst : IsIso f
⊢ IsIso (Spec.map f)

Tactic:
inferInstanceAs (IsIso <| Scheme.Spec.map f.op)

Premises used: _private.0.AlgebraicGeometry.instIsIsoSchemeMapOfCommRingCat._proof_1
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R S : CommRingCat
f : R ⟶ S
inst : IsIso f
change : Scheme.Spec.map (inv f).op = inv (Scheme.Spec.map f.op)
⊢ map (inv f) = inv (map f)

Tactic:
change Scheme.Spec.map (inv f).op = inv (Scheme.Spec.map f.op)

Premises used: Quiver.Hom.op, AlgebraicGeometry.Scheme.Spec, CategoryTheory.Functor.map, CategoryTheory.inv
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R S : CommRingCat
f : R ⟶ S
inst : IsIso f
rw : Scheme.Spec.map (inv f.op) = inv (Scheme.Spec.map f.op)
rw₁ rw₂ : Scheme.Spec.map (inv f.op) = Scheme.Spec.map (inv f.op)
⊢ Scheme.Spec.map (inv f).op = inv (Scheme.Spec.map f.op)

Tactic:
rw [op_inv, ← Scheme.Spec.map_inv]

Premises used: AlgebraicGeometry.Scheme.Spec, CategoryTheory.Functor.map_inv, CategoryTheory.op_inv
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
⊢ ↥(Spec R) = PrimeSpectrum (↑R : Type u)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
⊢ Eq.{u + 2} (α := TopCat.Sheaf CommRingCat (↑(Spec R).toPresheafedSpace : TopCat)) (Spec R).sheaf
    (Spec.structureSheaf (↑R : Type u))

Tactic:
rfl

Premises used: Set.Mem, AlgebraicGeometry.Spec.structureSheaf, AlgebraicGeometry.structurePresheafInCommRingCat, AlgebraicGeometry.SheafedSpace.sheaf, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
⊢ (Spec R).presheaf =
    ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
      (Spec.structureSheaf (↑R : Type u))

Tactic:
rfl

Premises used: AlgebraicGeometry.structurePresheafInCommRingCat, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ (map f).base = ofHom { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ }

Tactic:
rfl

Premises used: AlgebraicGeometry.Spec.topMap, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R S : CommRingCat
f : R ⟶ S
x : ↥(Spec S)
⊢ (map f) x = PrimeSpectrum.comap (CommRingCat.Hom.hom f) x

Tactic:
rfl

Premises used: PrimeSpectrum.comap, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R S : CommRingCat
f : R ⟶ S
U : (Spec R).Opens
⊢ Scheme.Hom.app (map f) U = CommRingCat.ofHom (StructureSheaf.comap (CommRingCat.Hom.hom f) U (map f ⁻¹ᵁ U) ⋯)

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R S : CommRingCat
f : R ⟶ S
U : (Spec S).Opens
V : (Spec R).Opens
e : U ≤ map f ⁻¹ᵁ V
⊢ Scheme.Hom.appLE (map f) V U e = CommRingCat.ofHom (StructureSheaf.comap (CommRingCat.Hom.hom f) V U e)

Tactic:
rfl

Premises used: Set.Mem, setOf, AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.StructureSheaf.comap, AlgebraicGeometry.StructureSheaf.comapFun, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R S : CommRingCat
f : R ⟶ S
A : CommRingCat
inst : Nontrivial.{u_1} (↑A : Type u_1)
⊢ Nonempty.{u_1 + 1} ↥(Spec A)

Tactic:
inferInstanceAs <| Nonempty (PrimeSpectrum A)

Premises used: _private.0.AlgebraicGeometry.instNonemptyCarrierCarrierCommRingCatSpecOfNontrivialCarrier._proof_1
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
W X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
i : W ⟶ X
j : W ⟶ Y
h : CommSq i j f g
H : Disjoint (α := Set ↥S) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)
⊢ IsEmpty.{u + 1} ↥W

Tactic:
⟨fun x ↦ (Set.disjoint_iff_inter_eq_empty.mp H).le
    ⟨⟨i x, congr($(h.w) x)⟩, ⟨j x, rfl⟩⟩⟩

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, Eq.le, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', IsEmpty.mk, Set.disjoint_iff_inter_eq_empty, And.intro, Exists.intro, Iff.mp, AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.CommSq.w, DFunLike.coe, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
⊢ Γ = forgetToLocallyRingedSpace.op ⋙ LocallyRingedSpace.Γ

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.Γ, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Schemeᵒᵖ
⊢ Γ.obj X = Γ(unop X, ⊤)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
⊢ Γ.obj (op X) = Γ(X, ⊤)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Schemeᵒᵖ
f : X ⟶ Y
⊢ Γ.map f = Hom.appTop f.unop

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ Γ.map f.op = Hom.appTop f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
⊢ SpecΓIdentity.app R = ΓSpecIso R

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.ΓSpecIso, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
⊢ SpecΓIdentity.hom.app R = (ΓSpecIso R).hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
⊢ SpecΓIdentity.inv.app R = (ΓSpecIso R).inv

Tactic:
rfl

Premises used: AlgebraicGeometry.toSpecΓ, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ Hom.appTop (Spec.map f) ≫ (ΓSpecIso S).hom = (ΓSpecIso R).hom ≫ f

Tactic:
SpecΓIdentity.hom.naturality f

Premises used: Set.Mem, AlgebraicGeometry.Scheme.SpecΓIdentity, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ f ≫ (ΓSpecIso S).inv = (ΓSpecIso R).inv ≫ Hom.appTop (Spec.map f)

Tactic:
SpecΓIdentity.inv.naturality f

Premises used: Set.Mem, AlgebraicGeometry.Scheme.SpecΓIdentity, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
⊢ (ΓSpecIso R).inv =
    CommRingCat.ofHom
      (algebraMap (↑R : Type u)
        (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
            (structureSheafInType (↑R : Type u) (↑R : Type u)))
          (op ⊤)))

Tactic:
rfl

Premises used: Set.Mem, setOf, AlgebraicGeometry.toSpecΓ, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
U : TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)
⊢ Eq (α :=
    CommRingCat.of (↑R : Type u) ⟶
      CommRingCat.of (↑(Functor.obj (Sheaf.presheaf (Spec.structureSheaf (↑R : Type u))) (op U)) : Type u))
    (CommRingCat.ofHom
      (algebraMap (↑R : Type u) (↑(Functor.obj (Sheaf.presheaf (Spec.structureSheaf (↑R : Type u))) (op U)) : Type u)))
    ((ΓSpecIso R).inv ≫ (Spec R).presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
rfl

Premises used: Set.Mem, setOf, AlgebraicGeometry.StructureSheaf.sectionsSubalgebra, RingHom.codRestrict, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
K : Type u_1
inst : Field K
⊢ Eq.{u_1 + 1} (α := Ideal (↑(CommRingCat.of K) : Type u_1)) (PrimeSpectrum.asIdeal default) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
f : (↑Γ(X, U) : Type u_1)
x : ↥X
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:
RingedSpace.mem_basicOpen _ _ _ _

Premises used: Set.Mem, AlgebraicGeometry.RingedSpace.mem_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
f : (↑Γ(X, U) : Type u_1)
x : ↥U
⊢ (↑x : ↥X) ∈ X.basicOpen f ↔
    IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥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)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u_1))
          f :
        (↑(X.presheaf.stalk (↑x : ↥X)) : Type u_1))

Tactic:
RingedSpace.mem_basicOpen _ _ _ _

Premises used: Set.Mem, AlgebraicGeometry.RingedSpace.mem_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
f : (↑Γ(X, U) : Type u_1)
x : ↥X
⊢ x ∈ X.basicOpen f ↔
    ∃ (m : 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 m) :
              (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:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
f : (↑Γ(X, ⊤) : Type u_1)
x : ↥X
⊢ 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) (X := X.presheaf.obj (op ⊤)) (Y := X.presheaf.stalk x)
              (X.presheaf.germ ⊤ x _root_.trivial) :
            (a : (↑(X.presheaf.obj (op ⊤)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          f :
        (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
RingedSpace.mem_top_basicOpen _ f x

Premises used: Set.Mem, AlgebraicGeometry.RingedSpace.mem_top_basicOpen, setOf
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
V U : X.Opens
f : (↑Γ(X, U) : Type u_1)
i : op U ⟶ op V
⊢ X.basicOpen (U := 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, U) : Type u_1)) → (↑Γ(X, V) : Type u_1))
        f) =
    V ⊓ X.basicOpen f

Tactic:
RingedSpace.basicOpen_res _ i f

Premises used: AlgebraicGeometry.RingedSpace.basicOpen_res, AlgebraicGeometry.Scheme.basicOpen
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
V U : X.Opens
f : (↑Γ(X, U) : Type u_1)
i : op U ⟶ op V
inst : IsIso i
⊢ X.basicOpen (U := 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, U) : Type u_1)) → (↑Γ(X, V) : Type u_1))
        f) =
    X.basicOpen f

Tactic:
RingedSpace.basicOpen_res_eq _ i f

Premises used: AlgebraicGeometry.RingedSpace.basicOpen_res_eq, AlgebraicGeometry.Scheme.basicOpen
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
f : (↑Γ(X, U) : Type u_1)
⊢ X.basicOpen f ≤ U

Tactic:
RingedSpace.basicOpen_le _ _

Premises used: Set.Mem, AlgebraicGeometry.RingedSpace.basicOpen_le
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
V U : X.Opens
i : V ⟶ U
f : (↑Γ(X, U) : Type u_1)
⊢ X.basicOpen
      (Presheaf.restrict (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        CommRingCat.carrier) f i) ≤
    X.basicOpen f

Tactic:
(Scheme.basicOpen_res _ _ _).trans_le inf_le_right

Premises used: Set.Mem, TopCat.Presheaf.restrict, setOf, inf_le_right, Eq.trans_le, AlgebraicGeometry.Scheme.basicOpen_res