awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
this : Scheme.Hom.coborderRange g = ⊤
rw : IsIso.{u, u + 1} (X := (↑⊤ : Scheme)) (Iso.hom (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).topIso)
⊢ IsIso (Scheme.Hom.coborderRange g).ι

Tactic:
rw [this, ← Scheme.topIso_hom]

Premises used: AlgebraicGeometry.Scheme.topIso_hom
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
this : Scheme.Hom.coborderRange g = ⊤
⊢ IsIso.{u, u + 1} (X := (↑⊤ : Scheme)) (Iso.hom (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).topIso)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
this : Scheme.Hom.coborderRange g = ⊤
⊢ IsIso (Scheme.Hom.coborderRange g).ι

Tactic:
have : IsIso g.coborderRange.ι := by rw [this, ← Scheme.topIso_hom]; infer_instance
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
this_1 : Scheme.Hom.coborderRange g = ⊤
this : IsIso (Scheme.Hom.coborderRange g).ι
rw : IsClosedImmersion (Scheme.Hom.liftCoborder g ≫ (Scheme.Hom.coborderRange g).ι)
⊢ IsClosedImmersion g

Tactic:
rw [← g.liftCoborder_ι]

Premises used: AlgebraicGeometry.Scheme.Hom.liftCoborder_ι
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
this_1 : Scheme.Hom.coborderRange g = ⊤
this : IsIso (Scheme.Hom.coborderRange g).ι
⊢ IsClosedImmersion (Scheme.Hom.liftCoborder g ≫ (Scheme.Hom.coborderRange g).ι)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
this_1 : Scheme.Hom.coborderRange g = ⊤
this : IsClosedImmersion g
obtain :
  ∀ (I : Ideal (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u))
    (e : V ≅ Spec (CommRingCat.of ((↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u) ⧸ I)))
    [inst : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))]
    (hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R)
    (this : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) = ⊤)
    (this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))),
    IsIso (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
⊢ IsIso g

Tactic:
obtain ⟨I, e, rfl⟩ := IsClosedImmersion.Spec_iff.mp this

Premises used: AlgebraicGeometry.IsClosedImmersion.Spec_iff, Iff.mp, rfl
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
inst : CompactSpace.{u} ↥V
I : Ideal (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
e : V ≅ Spec (CommRingCat.of ((↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u) ⧸ I))
inst_1 : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
this_1 : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
rwa rwa₁ rwa₂ rwa₃ : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
⊢ (f ≫ e.hom) ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R

Tactic:
rwa [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
inst : CompactSpace.{u} ↥V
I : Ideal (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
e : V ≅ Spec (CommRingCat.of ((↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u) ⧸ I))
inst_1 : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
this_1 : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
obtain :
  ∀
    (e :
      V ≅
        Spec
          (CommRingCat.of
            (HasQuotient.Quotient (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u) (B :=
              Ideal (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)) ⊥)))
    [inst : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))]
    (hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)) = sigmaSpec R)
    (this : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥))) = ⊤)
    (this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))),
    IsIso (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
⊢ IsIso (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))

Tactic:
obtain rfl := eq_bot_of_comp_quotientMk_eq_sigmaSpec R I (f ≫ e.hom) (by rwa [Category.assoc])

Premises used: AlgebraicGeometry.eq_bot_of_comp_quotientMk_eq_sigmaSpec, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, rfl
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
inst : CompactSpace.{u} ↥V
e :
  V ≅
    Spec
      (CommRingCat.of
        (HasQuotient.Quotient (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u) (B :=
          Ideal (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)) ⊥))
inst_1 : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)) = sigmaSpec R
this_1 : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
convert_to :
  IsIso (Y := Spec (CommRingCat.of (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)))
    (e.hom ≫
      Spec.map
        (Iso.inv
          (RingEquiv.toCommRingCatIso
            (RingEquiv.quotientBot (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)))))
⊢ IsIso (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))

Tactic:
convert_to IsIso (e.hom ≫ Spec.map (RingEquiv.quotientBot _).toCommRingCatIso.inv)

Premises used: CategoryTheory.IsIso, RingEquiv.toCommRingCatIso, AlgebraicGeometry.Spec.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
inst : CompactSpace.{u} ↥V
e :
  V ≅
    Spec
      (CommRingCat.of
        (HasQuotient.Quotient (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u) (B :=
          Ideal (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)) ⊥))
inst_1 : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)) = sigmaSpec R
this_1 : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
⊢ IsIso (Y := Spec (CommRingCat.of (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)))
    (e.hom ≫
      Spec.map
        (Iso.inv
          (RingEquiv.toCommRingCatIso
            (RingEquiv.quotientBot (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)))))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : QuasiSeparatedSpace.{u} ↥X
f g : Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))) ⟶ X
e : pointsPi R X f = pointsPi R X g
h :
  ∀ (i : ι),
    Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i ≫ sigmaSpec R ≫ f =
      Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i ≫ sigmaSpec R ≫ g
⊢ sigmaSpec R ≫ f = sigmaSpec R ≫ g

Tactic:
ext1 i
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : QuasiSeparatedSpace.{u} ↥X
f g : Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))) ⟶ X
e : pointsPi R X f = pointsPi R X g
i : ι
⊢ Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i ≫ sigmaSpec R ≫ f =
    Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i ≫ sigmaSpec R ≫ g

Tactic:
simpa using congr_fun e i

Premises used: congr_fun
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : QuasiSeparatedSpace.{u} ↥X
f g : Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))) ⟶ X
e : pointsPi R X f = pointsPi R X g
⊢ CategoryStruct.comp (Y := equalizer f g) (equalizer.lift (sigmaSpec R) ⋯) (equalizer.ι f g) = sigmaSpec R

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : QuasiSeparatedSpace.{u} ↥X
f g : Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))) ⟶ X
e : pointsPi R X f = pointsPi R X g
⊢ IsIso (X := equalizer f g) (equalizer.ι f g)

Tactic:
have := isIso_of_comp_eq_sigmaSpec R (V := equalizer f g)
    (equalizer.lift (sigmaSpec R) (by ext1 i; simpa using congr_fun e i))
    (equalizer.ι f g) (by simp)
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : QuasiSeparatedSpace.{u} ↥X
f g : Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))) ⟶ X
e : pointsPi R X f = pointsPi R X g
this : IsIso (X := equalizer f g) (equalizer.ι f g)
rw : Eq (α := equalizer f g ⟶ X) (equalizer.ι f g ≫ f) (equalizer.ι f g ≫ g)
rw₁ rw₂ : Eq (α := equalizer f g ⟶ X) (equalizer.ι f g ≫ g) (equalizer.ι f g ≫ g)
⊢ f = g

Tactic:
rw [← cancel_epi (equalizer.ι f g), equalizer.condition]

Premises used: CategoryTheory.Limits.equalizer.condition, CategoryTheory.Limits.equalizer.ι, CategoryTheory.cancel_epi
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
⊢ ∃ (a : Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))) ⟶ X), pointsPi R X a = f

Tactic:
⟨Spec.map (CommRingCat.ofHom
    (Pi.ringHom fun i ↦ (Spec.preimage (f i ≫ X.isoSpec.hom)).1)) ≫ X.isoSpec.inv, ?_⟩

Premises used: AlgebraicGeometry.Scheme.isoSpec, CommRingCat.ofHom, AlgebraicGeometry.Spec.map, Pi.ringHom, Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Spec.preimage, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CommRingCat.Hom.hom'
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
refine :
  pointsPi R X
      (Spec.map
          (CommRingCat.ofHom
            (Pi.ringHom (f := fun (i : ι) ↦ (↑(R i) : Type u)) fun (i : ι) ↦
              (Spec.preimage (f i ≫ X.isoSpec.hom)).hom')) ≫
        X.isoSpec.inv) =
    f
⊢ ∃ (a : Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))) ⟶ X), pointsPi R X a = f

Tactic:
refine ⟨Spec.map (CommRingCat.ofHom
    (Pi.ringHom fun i ↦ (Spec.preimage (f i ≫ X.isoSpec.hom)).1)) ≫ X.isoSpec.inv, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
h :
  ∀ (i : ι),
    pointsPi R X
        (Spec.map
            (CommRingCat.ofHom
              (Pi.ringHom (f := fun (i : ι) ↦ (↑(R i) : Type u)) fun (i : ι) ↦
                (Spec.preimage (f i ≫ X.isoSpec.hom)).hom')) ≫
          X.isoSpec.inv)
        i =
      f i
⊢ pointsPi R X
      (Spec.map
          (CommRingCat.ofHom
            (Pi.ringHom (f := fun (i : ι) ↦ (↑(R i) : Type u)) fun (i : ι) ↦
              (Spec.preimage (f i ≫ X.isoSpec.hom)).hom')) ≫
        X.isoSpec.inv) =
    f

Tactic:
ext i : 1
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
i : ι
h :
  Spec.map
      (CategoryStruct.comp (Y := CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
        (CommRingCat.ofHom
          (Pi.ringHom (f := fun (i : ι) ↦ (↑(R i) : Type u)) fun (i : ι) ↦ (Spec.preimage (f i ≫ X.isoSpec.hom)).hom'))
        (CommRingCat.ofHom (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i))) =
    f i ≫ X.isoSpec.hom
⊢ pointsPi R X
      (Spec.map
          (CommRingCat.ofHom
            (Pi.ringHom (f := fun (i : ι) ↦ (↑(R i) : Type u)) fun (i : ι) ↦
              (Spec.preimage (f i ≫ X.isoSpec.hom)).hom')) ≫
        X.isoSpec.inv)
      i =
    f i

Tactic:
simp only [pointsPi, ← Spec.map_comp_assoc, Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq, AlgebraicGeometry.pointsPi, AlgebraicGeometry.Spec.map_comp_assoc
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
i : ι
⊢ Spec.map
      (CategoryStruct.comp (Y := CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
        (CommRingCat.ofHom
          (Pi.ringHom (f := fun (i : ι) ↦ (↑(R i) : Type u)) fun (i : ι) ↦ (Spec.preimage (f i ≫ X.isoSpec.hom)).hom'))
        (CommRingCat.ofHom (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i))) =
    f i ≫ X.isoSpec.hom

Tactic:
Spec.map_preimage _

Premises used: Quiver.Hom.unop, AlgebraicGeometry.Spec.map_preimage, AlgebraicGeometry.Spec.preimage
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
i : ι
⊢ Spec.map
      (CategoryStruct.comp (Y := CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
        (CommRingCat.ofHom
          (Pi.ringHom (f := fun (i : ι) ↦ (↑(R i) : Type u)) fun (i : ι) ↦ (Spec.preimage (f i ≫ X.isoSpec.hom)).hom'))
        (CommRingCat.ofHom (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i))) =
    f i ≫ X.isoSpec.hom

Tactic:
exact Spec.map_preimage _

Premises used: AlgebraicGeometry.Spec.map_preimage
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
x : ↥(Proj 𝒜)
⊢ Membership.mem (γ := (Proj 𝒜).Opens) (basicOpen 𝒜 f) x ↔ f ∉ x.asHomogeneousIdeal

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Not
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ Eq (α := (Proj 𝒜).Opens) (basicOpen 𝒜 1) ⊤

Tactic:
ProjectiveSpectrum.basicOpen_one ..

Premises used: Set.Mem, setOf, AlgebraicGeometry.Proj.basicOpen, ProjectiveSpectrum.basicOpen_one
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ Eq (α := (Proj 𝒜).Opens) (basicOpen 𝒜 0) ⊥

Tactic:
ProjectiveSpectrum.basicOpen_zero ..

Premises used: Set.Mem, setOf, AlgebraicGeometry.Proj.basicOpen, ProjectiveSpectrum.basicOpen_zero
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
n : ℕ
hn : 0 < n
⊢ Eq (α := (Proj 𝒜).Opens) (basicOpen 𝒜 (f ^ n)) (basicOpen 𝒜 f)

Tactic:
ProjectiveSpectrum.basicOpen_pow 𝒜 f n hn

Premises used: Set.Mem, setOf, AlgebraicGeometry.Proj.basicOpen, ProjectiveSpectrum.basicOpen_pow
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g : A
⊢ Eq (α := (Proj 𝒜).Opens) (basicOpen 𝒜 (f * g)) (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g)

Tactic:
ProjectiveSpectrum.basicOpen_mul ..

Premises used: Set.Mem, setOf, AlgebraicGeometry.Proj.basicOpen, ProjectiveSpectrum.basicOpen_mul
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
⊢ Eq (α := (Proj 𝒜).Opens) (basicOpen 𝒜 f) (⨆ (i : ℕ), basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f))

Tactic:
ProjectiveSpectrum.basicOpen_eq_union_of_projection ..

Premises used: Set.Mem, setOf, AlgebraicGeometry.Proj.basicOpen, ProjectiveSpectrum.basicOpen_eq_union_of_projection
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ TopologicalSpace.IsTopologicalBasis.{u} (α := ProjectiveSpectrum 𝒜)
    (Set.range fun (r : A) ↦ (↑(ProjectiveSpectrum.basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜)))

Tactic:
ProjectiveSpectrum.isTopologicalBasis_basic_opens 𝒜

Premises used: ProjectiveSpectrum.isTopologicalBasis_basic_opens
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
h :
  ↥(Proj 𝒜) = ProjectiveSpectrum 𝒜 →
    Set.image (α := TopologicalSpace.Opens ↥(Proj 𝒜)) SetLike.coe (Set.range (basicOpen 𝒜)) =
      Set.range fun (r : A) ↦ (↑(ProjectiveSpectrum.basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))
⊢ TopologicalSpace.IsTopologicalBasis
    (Set.image (α := TopologicalSpace.Opens ↥(Proj 𝒜)) SetLike.coe (Set.range (basicOpen 𝒜)))

Tactic:
convert! ProjectiveSpectrum.isTopologicalBasis_basic_opens 𝒜

Premises used: ProjectiveSpectrum.isTopologicalBasis_basic_opens
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e_1 : ↥(Proj 𝒜) = ProjectiveSpectrum 𝒜
⊢ Set.image (α := TopologicalSpace.Opens ↥(Proj 𝒜)) SetLike.coe (Set.range (basicOpen 𝒜)) =
    Set.range fun (r : A) ↦ (↑(ProjectiveSpectrum.basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))

Tactic:
(Set.range_comp _ _).symm

Premises used: Set.range_comp, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e_1 : ↥(Proj 𝒜) = ProjectiveSpectrum 𝒜
⊢ Set.image (α := TopologicalSpace.Opens ↥(Proj 𝒜)) SetLike.coe (Set.range (basicOpen 𝒜)) =
    Set.range fun (r : A) ↦ (↑(ProjectiveSpectrum.basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))

Tactic:
exact (Set.range_comp _ _).symm

Premises used: Set.range_comp, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
⊢ Eq.{u + 1} (α := (Proj 𝒜).Opens) (⨆ (i : ι), basicOpen 𝒜 (f i)) ⊤

Tactic:
top_le_iff.mp fun x hx ↦ TopologicalSpace.Opens.mem_iSup.mpr ?_

Premises used: Iff.mpr, TopologicalSpace.Opens.mem_iSup, top_le_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
refine :
  ∀ (x : ↥(Proj 𝒜)) (hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x),
    ∃ (i : ι), Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x
⊢ Eq.{u + 1} (α := (Proj 𝒜).Opens) (⨆ (i : ι), basicOpen 𝒜 (f i)) ⊤

Tactic:
refine top_le_iff.mp fun x hx ↦ TopologicalSpace.Opens.mem_iSup.mpr ?_

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
x : ↥(Proj 𝒜)
hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x
by_contra! : ∀ (H : ∀ (i : ι), x ∉ basicOpen 𝒜 (f i)), False
⊢ ∃ (i : ι), Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x

Tactic:
by_contra! H
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
x : ↥(Proj 𝒜)
hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x
H : ∀ (i : ι), x ∉ basicOpen 𝒜 (f i)
⊢ ∀ (i : ι), f i ∈ x.asHomogeneousIdeal

Tactic:
simp only [mem_basicOpen, Decidable.not_not] at H

Premises used: AlgebraicGeometry.Proj.mem_basicOpen, Decidable.not_not
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
x : ↥(Proj 𝒜)
hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x
H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal
⊢ False

Tactic:
x.not_irrelevant_le (hf.trans ?_)

Premises used: ProjectiveSpectrum.not_irrelevant_le, LE.le.trans
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
x : ↥(Proj 𝒜)
hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x
H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal
refine : Ideal.span (Set.range f) ≤ x.asHomogeneousIdeal.toSubmodule
⊢ False

Tactic:
refine x.not_irrelevant_le (hf.trans ?_)

Premises used: ProjectiveSpectrum.not_irrelevant_le, LE.le.trans
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
x : ↥(Proj 𝒜)
hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x
H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal
rwa : Set.range f ⊆ (↑x.asHomogeneousIdeal.toSubmodule : Set A)
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (y : ι), f y ∈ (↑x.asHomogeneousIdeal.toSubmodule : Set A)
⊢ Ideal.span (Set.range f) ≤ x.asHomogeneousIdeal.toSubmodule

Tactic:
rwa [Ideal.span_le, Set.range_subset_iff]

Premises used: Ideal.span_le, Set.range_subset_iff