awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  IsIso (X :=
    (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
            ⋯).toPresheafedSpace :
      TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f)))
x :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
⊢ IsIso (X :=
    (Spec A⁰_ f).presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (X :=
            (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                    ⋯).toPresheafedSpace :
              TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
          (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
        x))
    (Y :=
    (Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
            ⋯).presheaf.stalk
      x)
    (Iso.hom (specStalkEquiv 𝒜 f x f_deg hm) ≫
      Iso.inv (RingEquiv.toCommRingCatIso («Proj».stalkIso' 𝒜 (↑x : ProjectiveSpectrum 𝒜))) ≫
        Iso.inv (Proj.restrictStalkIso ⋯ x))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  IsIso (X :=
    (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
            ⋯).toPresheafedSpace :
      TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f)))
⊢ ∀
    (x :
      (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toTopCat :
        Type u_1)),
    IsIso (X :=
      (Spec A⁰_ f).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (X :=
              (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                      ⋯).toPresheafedSpace :
                TopCat))
              (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
          x))
      (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)

Tactic:
haveI _ (x) : IsIso ((toSpec 𝒜 f).stalkMap x) := by
    rw [stalkMap_toSpec 𝒜 f x f_deg hm]; infer_instance
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  IsIso (X :=
    (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
            ⋯).toPresheafedSpace :
      TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f)))
h :
  ∀
    (x :
      (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toTopCat :
        Type u_1)),
    IsIso (X :=
      (Spec A⁰_ f).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (X :=
              (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                      ⋯).toPresheafedSpace :
                TopCat))
              (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
          x))
      (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)
⊢ LocallyRingedSpace.IsOpenImmersion (X :=
    Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯) (toSpec 𝒜 f)

Tactic:
haveI : LocallyRingedSpace.IsOpenImmersion (toSpec 𝒜 f) :=
    LocallyRingedSpace.IsOpenImmersion.of_stalk_iso (toSpec 𝒜 f)
      (TopCat.homeoOfIso (asIso <| (toSpec 𝒜 f).base)).isOpenEmbedding
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this_1 :
  IsIso (X :=
    (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
            ⋯).toPresheafedSpace :
      TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f)))
h :
  ∀
    (x :
      (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toTopCat :
        Type u_1)),
    IsIso (X :=
      (Spec A⁰_ f).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (X :=
              (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                      ⋯).toPresheafedSpace :
                TopCat))
              (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
          x))
      (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)
this :
  LocallyRingedSpace.IsOpenImmersion (X :=
    Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯) (toSpec 𝒜 f)
⊢ IsIso (X := Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯)
    (toSpec 𝒜 f)

Tactic:
LocallyRingedSpace.IsOpenImmersion.to_iso _

Premises used: AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.to_iso
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this_1 :
  IsIso (X :=
    (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
            ⋯).toPresheafedSpace :
      TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f)))
h :
  ∀
    (x :
      (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toTopCat :
        Type u_1)),
    IsIso (X :=
      (Spec A⁰_ f).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (X :=
              (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                      ⋯).toPresheafedSpace :
                TopCat))
              (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
          x))
      (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)
this :
  LocallyRingedSpace.IsOpenImmersion (X :=
    Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯) (toSpec 𝒜 f)
⊢ IsIso (X := Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯)
    (toSpec 𝒜 f)

Tactic:
exact LocallyRingedSpace.IsOpenImmersion.to_iso _

Premises used: AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.to_iso
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑Proj.T : Type u_1)
by_contra! : ∀ (this : ∀ (f : A) (m : ℕ), f ∈ 𝒜 m → 0 < m → f ∈ x.asHomogeneousIdeal), False
⊢ ∃ (f : A) (m : ℕ) (_ : f ∈ 𝒜 m) (_ : 0 < m), f ∉ x.asHomogeneousIdeal

Tactic:
by_contra!
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑Proj.T : Type u_1)
this : ∀ (f : A) (m : ℕ), f ∈ 𝒜 m → 0 < m → f ∈ x.asHomogeneousIdeal
⊢ False

Tactic:
x.not_irrelevant_le fun z hz ↦ ?_

Premises used: ProjectiveSpectrum.not_irrelevant_le
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑Proj.T : Type u_1)
this : ∀ (f : A) (m : ℕ), f ∈ 𝒜 m → 0 < m → f ∈ x.asHomogeneousIdeal
refine :
  ∀ (z : A) (hz : Membership.mem (γ := HomogeneousIdeal 𝒜) (HomogeneousIdeal.irrelevant 𝒜) z), z ∈ x.asHomogeneousIdeal
⊢ False

Tactic:
refine x.not_irrelevant_le fun z hz ↦ ?_

Premises used: ProjectiveSpectrum.not_irrelevant_le
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑Proj.T : Type u_1)
this : ∀ (f : A) (m : ℕ), f ∈ 𝒜 m → 0 < m → f ∈ x.asHomogeneousIdeal
z : A
hz : Membership.mem (γ := HomogeneousIdeal 𝒜) (HomogeneousIdeal.irrelevant 𝒜) z
rw :
  ∑ i ∈ DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) z),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) z : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) ∈
    x.asHomogeneousIdeal
⊢ z ∈ x.asHomogeneousIdeal

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 z]

Premises used: DirectSum.sum_support_decompose
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑Proj.T : Type u_1)
this : ∀ (f : A) (m : ℕ), f ∈ 𝒜 m → 0 < m → f ∈ x.asHomogeneousIdeal
z : A
hz : Membership.mem (γ := HomogeneousIdeal 𝒜) (HomogeneousIdeal.irrelevant 𝒜) z
k : ℕ
hk :
  Membership.mem (γ := Finset ℕ)
    (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) z)) k
⊢ ¬0 < k → False

Tactic:
aesop
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑Proj.T : Type u_1)
this : ∀ (f : A) (m : ℕ), f ∈ 𝒜 m → 0 < m → f ∈ x.asHomogeneousIdeal
z : A
hz : Membership.mem (γ := HomogeneousIdeal 𝒜) (HomogeneousIdeal.irrelevant 𝒜) z
⊢ ∑ i ∈ DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) z),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) z : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) ∈
    x.asHomogeneousIdeal

Tactic:
exact x.1.toIdeal.sum_mem fun k hk ↦ this _ k (SetLike.coe_mem _) <| by_contra <| by aesop

Premises used: SetLike.coe_mem, Ideal.sum_mem, by_contra, Subtype.val, HomogeneousIdeal.toIdeal, ProjectiveSpectrum.asHomogeneousIdeal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑Proj.T : Type u_1)
obtain :
  ∀ (f : A) (m : ℕ) (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (hx : f ∉ x.asHomogeneousIdeal),
    ∃ (U : OpenNhds x) (R : CommRingCat.{u_1}),
      Nonempty.{u_1 + 1} (Proj.restrict ⋯ ≅ «Spec».toLocallyRingedSpace.obj (op R))
⊢ ∃ (U : OpenNhds x) (R : CommRingCat.{u_1}),
    Nonempty.{u_1 + 1} (Proj.restrict ⋯ ≅ «Spec».toLocallyRingedSpace.obj (op R))

Tactic:
obtain ⟨f, m, f_deg, hm, hx⟩ : ∃ (f : A) (m : ℕ) (_ : f ∈ 𝒜 m) (_ : 0 < m), f ∉ x.1 := by
      by_contra!
      refine x.not_irrelevant_le fun z hz ↦ ?_
      rw [← DirectSum.sum_support_decompose 𝒜 z]
      exact x.1.toIdeal.sum_mem fun k hk ↦ this _ k (SetLike.coe_mem _) <| by_contra <| by aesop

Premises used: ProjectiveSpectrum.asHomogeneousIdeal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑Proj.T : Type u_1)
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
hx : f ∉ x.asHomogeneousIdeal
⊢ ∃ (U : OpenNhds x) (R : CommRingCat.{u_1}),
    Nonempty.{u_1 + 1} (Proj.restrict ⋯ ≅ «Spec».toLocallyRingedSpace.obj (op R))

Tactic:
⟨⟨pbo f, hx⟩, .of (A⁰_ f), ⟨projIsoSpec 𝒜 f f_deg hm⟩⟩

Premises used: ProjectiveSpectrum.basicOpen, Nonempty.intro, Subtype.mk, CommRingCat.of, Exists.intro, AlgebraicGeometry.projIsoSpec, HomogeneousLocalization.Away
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑Proj.T : Type u_1)
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
hx : f ∉ x.asHomogeneousIdeal
⊢ ∃ (U : OpenNhds x) (R : CommRingCat.{u_1}),
    Nonempty.{u_1 + 1} (Proj.restrict ⋯ ≅ «Spec».toLocallyRingedSpace.obj (op R))

Tactic:
exact ⟨⟨pbo f, hx⟩, .of (A⁰_ f), ⟨projIsoSpec 𝒜 f f_deg hm⟩⟩
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑Proj.T : Type u_1)
obtain : ∃ (f : A) (m : ℕ) (_ : f ∈ 𝒜 m) (_ : 0 < m), f ∉ x.asHomogeneousIdeal
obtain₁ :
  ∀ (f : A) (m : ℕ) (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (hx : f ∉ x.asHomogeneousIdeal),
    ∃ (U : OpenNhds x) (R : CommRingCat.{u_1}),
      Nonempty.{u_1 + 1} (Proj.restrict ⋯ ≅ «Spec».toLocallyRingedSpace.obj (op R))
⊢ ∃ (U : OpenNhds x) (R : CommRingCat.{u_1}),
    Nonempty.{u_1 + 1} (Proj.restrict ⋯ ≅ «Spec».toLocallyRingedSpace.obj (op R))

Tactic:
classical
    obtain ⟨f, m, f_deg, hm, hx⟩ : ∃ (f : A) (m : ℕ) (_ : f ∈ 𝒜 m) (_ : 0 < m), f ∉ x.1 := by
      by_contra!
      refine x.not_irrelevant_le fun z hz ↦ ?_
      rw [← DirectSum.sum_support_decompose 𝒜 z]
      exact x.1.toIdeal.sum_mem fun k hk ↦ this _ k (SetLike.coe_mem _) <| by_contra <| by aesop
    exact ⟨⟨pbo f, hx⟩, .of (A⁰_ f), ⟨projIsoSpec 𝒜 f f_deg hm⟩⟩

Premises used: ProjectiveSpectrum.asHomogeneousIdeal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
V U : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
i : V ⟶ U
f : (x : ↥U) → at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
j : ℕ
r s : ↥(𝒜 j)
h : ∀ (x : ↥U), (↑s : A) ∉ (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal
w : ∀ (x : ↥U), f x = HomogeneousLocalization.mk { deg := j, num := r, den := s, den_mem := ⋯ }
⊢ IsFraction.{u_1, u_2} (σ := σ) (𝒜 := 𝒜) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)

Tactic:
⟨j, r, s, (h <| i ·), (w <| i ·)⟩

Premises used: AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.IsFraction, Exists.intro, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
V U : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
i : V ⟶ U
f : (x : ↥U) → at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
j : ℕ
r s : ↥(𝒜 j)
h : ∀ (x : ↥U), (↑s : A) ∉ (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal
w : ∀ (x : ↥U), f x = HomogeneousLocalization.mk { deg := j, num := r, den := s, den_mem := ⋯ }
⊢ IsFraction.{u_1, u_2} (σ := σ) (𝒜 := 𝒜) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)

Tactic:
exact ⟨j, r, s, (h <| i ·), (w <| i ·)⟩
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
U : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
⊢ PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
    at x)
    (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
        (isLocallyFraction 𝒜) :
      PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
    (U := unop U) (0 : (x : ↥(unop U)) → at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))

Tactic:
fun x =>
  ⟨unop U, x.2, 𝟙 (unop U), ⟨0, ⟨0, zero_mem _⟩, ⟨1, one_mem_graded _⟩, _, fun _ => rfl⟩⟩

Premises used: CategoryTheory.CategoryStruct.id, Subtype.mk, SetLike.one_mem_graded, HomogeneousLocalization.NumDenSameDeg.instOne._proof_2, Exists.intro, Ideal.primeCompl, ZeroMemClass.zero_mem, OfNat.ofNat, Subtype.val, HomogeneousIdeal.toIdeal, DFunLike.coe, Opposite.unop, ProjectiveSpectrum.asHomogeneousIdeal, rfl, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
U : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
⊢ PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
    at x)
    (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
        (isLocallyFraction 𝒜) :
      PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
    (U := unop U) (1 : (x : ↥(unop U)) → at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))

Tactic:
fun x =>
  ⟨unop U, x.2, 𝟙 (unop U), ⟨0, ⟨1, one_mem_graded _⟩, ⟨1, one_mem_graded _⟩, _, fun _ => rfl⟩⟩

Premises used: CategoryTheory.CategoryStruct.id, Subtype.mk, SetLike.one_mem_graded, HomogeneousLocalization.NumDenSameDeg.instOne._proof_2, Exists.intro, Ideal.primeCompl, OfNat.ofNat, Subtype.val, HomogeneousIdeal.toIdeal, DFunLike.coe, Opposite.unop, ProjectiveSpectrum.asHomogeneousIdeal, rfl, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
U : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
a b : (x : ↥(unop U)) → at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
ha :
  PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
    at x)
    (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
        (isLocallyFraction 𝒜) :
      PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
    a
hb :
  PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
    at x)
    (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
        (isLocallyFraction 𝒜) :
      PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
    b
x : ↥(unop U)
rcases :
  ∀ (Va : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (ma : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ Va)
    (ia : Va ⟶ unop U) (ja : ℕ) (ra : A) (ra_mem : ra ∈ 𝒜 ja) (sa : A) (sa_mem : sa ∈ 𝒜 ja)
    (hwa :
      ∀ (x : ↥Va),
        (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 ja) sa sa_mem) : A) ∉
          (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal)
    (wa :
      ∀ (x : ↥Va),
        Eq (α := at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
          ((fun (x : ↥Va) ↦
              (a ((ia : (a : ↥Va) → ↥(unop U)) x) :
                at (↑((ia : (a : ↥Va) → ↥(unop U)) x) : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))))
            x)
          (HomogeneousLocalization.mk
            { deg := ja, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 ja) ra ra_mem,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 ja) sa sa_mem, den_mem := ⋯ })),
    ∃ (V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (_ : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V) (i
      : V ⟶ unop U),
      PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
        at x)
        (isFractionPrelocal 𝒜 :
          PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
        (U := V) fun (x : ↥V) ↦ (a + b) ((i : (a : ↥V) → ↥(unop U)) x)
⊢ ∃ (V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (_ : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V) (i :
    V ⟶ unop U),
    PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
      at x)
      (isFractionPrelocal 𝒜 :
        PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
      (U := V) fun (x : ↥V) ↦ (a + b) ((i : (a : ↥V) → ↥(unop U)) x)

Tactic:
rcases ha x with ⟨Va, ma, ia, ja, ⟨ra, ra_mem⟩, ⟨sa, sa_mem⟩, hwa, wa⟩