awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
h :
  (↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) =
    (↑(PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg)) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f))))
⊢ Eq (α := (Spec (CommRingCat.of (Away 𝒜 f))).Opens) (awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g)
    (PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg))

Tactic:
ext1
-- 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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
trans :
  (↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) =
    Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) ⇑(Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg ⋯)))
trans₁ :
  Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) ⇑(Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg ⋯))) =
    (↑(PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg)) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f))))
⊢ (↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) =
    (↑(PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg)) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f))))

Tactic:
trans Set.range (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg rfl)))

Premises used: HomogeneousLocalization.awayMap, CategoryTheory.ConcreteCategory.hom, CommRingCat.ofHom, AlgebraicGeometry.Spec.map, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, Set.range, DFunLike.coe, rfl
-- 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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
rw :
  (↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) =
    Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g)))))
      ⇑(Iso.inv (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' ⋯) ≫
          Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm'))
⊢ (↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) =
    Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) ⇑(Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg ⋯)))

Tactic:
rw [← pullbackAwayιIso_inv_fst 𝒜 f_deg hm g_deg hm' rfl]

Premises used: AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst, rfl
-- 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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
simp :
  Eq (α := Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) (⇑(awayι 𝒜 f f_deg hm) ⁻¹' (↑(basicOpen 𝒜 g) : Set ↥(Proj 𝒜)))
    (Set.image (α :=
      ↥(Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))
      (⇑(TopCat.Hom.hom
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toHom
                (Scheme.Hom.toLRSHom' (Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))))) :
        (a : ↥(Limits.pullback (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm'))) → ↥(Spec (CommRingCat.of (Away 𝒜 f))))
      (Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g)))))
        (⇑(TopCat.Hom.hom
              (PresheafedSpace.Hom.base
                (LocallyRingedSpace.Hom.toHom
                  (Scheme.Hom.toLRSHom' (Iso.inv (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' ⋯)))))) :
          (a : ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) →
            ↥(Limits.pullback (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))))
⊢ (↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) =
    Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g)))))
      ⇑(Iso.inv (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' ⋯) ≫
          Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm'))

Tactic:
simp only [TopologicalSpace.Opens.map_coe, Scheme.Hom.comp_base,
      TopCat.hom_comp, ContinuousMap.coe_comp, Set.range_comp]

Premises used: TopologicalSpace.Opens.map_coe, Set.range_comp, ContinuousMap.coe_comp, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.hom_comp
-- 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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
⊢ Function.Surjective (α := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) (β :=
    ↥(Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))
    (⇑(TopCat.Hom.hom
          (PresheafedSpace.Hom.base
            (LocallyRingedSpace.Hom.toHom
              (Scheme.Hom.toLRSHom' (Iso.inv (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' ⋯)))))) :
      (a : ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) → ↥(Limits.pullback (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))

Tactic:
(pullbackAwayιIso 𝒜 f_deg hm g_deg hm' rfl).inv.homeomorph.surjective

Premises used: AlgebraicGeometry.Scheme.Hom.homeomorph, Homeomorph.surjective, CategoryTheory.Iso.inv, AlgebraicGeometry.Proj.pullbackAwayιIso, rfl
-- 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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
⊢ Function.Surjective (α := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) (β :=
    ↥(Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))
    (⇑(TopCat.Hom.hom
          (PresheafedSpace.Hom.base
            (LocallyRingedSpace.Hom.toHom
              (Scheme.Hom.toLRSHom' (Iso.inv (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' ⋯)))))) :
      (a : ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) → ↥(Limits.pullback (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))

Tactic:
exact
      (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' rfl).inv.homeomorph.surjective

Premises used: AlgebraicGeometry.Scheme.Hom.homeomorph, Homeomorph.surjective, CategoryTheory.Iso.inv, AlgebraicGeometry.Proj.pullbackAwayιIso, rfl
-- 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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
rw :
  Eq (α := Set ↥(Spec (CommRingCat.of (Away 𝒜 f))))
    (⇑(awayι 𝒜 f f_deg hm) ⁻¹' (↑(Scheme.Hom.opensRange (awayι 𝒜 g g_deg hm')) : Set ↥(Proj 𝒜)))
    (Set.image (α :=
      ↥(Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))
      (⇑(TopCat.Hom.hom
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toHom
                (Scheme.Hom.toLRSHom' (Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))))) :
        (a : ↥(Limits.pullback (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm'))) → ↥(Spec (CommRingCat.of (Away 𝒜 f))))
      Set.univ)
⊢ Eq (α := Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) (⇑(awayι 𝒜 f f_deg hm) ⁻¹' (↑(basicOpen 𝒜 g) : Set ↥(Proj 𝒜)))
    (Set.image (α :=
      ↥(Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))
      (⇑(TopCat.Hom.hom
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toHom
                (Scheme.Hom.toLRSHom' (Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))))) :
        (a : ↥(Limits.pullback (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm'))) → ↥(Spec (CommRingCat.of (Away 𝒜 f))))
      (Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g)))))
        (⇑(TopCat.Hom.hom
              (PresheafedSpace.Hom.base
                (LocallyRingedSpace.Hom.toHom
                  (Scheme.Hom.toLRSHom' (Iso.inv (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' ⋯)))))) :
          (a : ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) →
            ↥(Limits.pullback (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))))

Tactic:
rw [Set.range_eq_univ.mpr (by exact
      (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' rfl).inv.homeomorph.surjective),
      ← opensRange_awayι _ _ g_deg hm']

Premises used: Iff.mpr, Set.range_eq_univ, AlgebraicGeometry.Proj.opensRange_awayι
-- 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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
⊢ Eq (α := Set ↥(Spec (CommRingCat.of (Away 𝒜 f))))
    (⇑(awayι 𝒜 f f_deg hm) ⁻¹' (↑(Scheme.Hom.opensRange (awayι 𝒜 g g_deg hm')) : Set ↥(Proj 𝒜)))
    (Set.image (α :=
      ↥(Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))
      (⇑(TopCat.Hom.hom
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toHom
                (Scheme.Hom.toLRSHom' (Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))))) :
        (a : ↥(Limits.pullback (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm'))) → ↥(Spec (CommRingCat.of (Away 𝒜 f))))
      Set.univ)

Tactic:
simp [IsOpenImmersion.range_pullbackFst]

Premises used: AlgebraicGeometry.IsOpenImmersion.range_pullbackFst
-- 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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
this_1 : Algebra (Away 𝒜 f) (Away 𝒜 (f * g)) := RingHom.toAlgebra (awayMap 𝒜 g_deg ⋯)
this : IsLocalization.Away (R := Away 𝒜 f) (Away.isLocalizationElem f_deg g_deg) (Away 𝒜 (f * g)) := ⋯
⊢ Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) ⇑(Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg ⋯))) =
    (↑(PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg)) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f))))

Tactic:
PrimeSpectrum.localization_away_comap_range _ _

Premises used: HomogeneousLocalization.awayMap, HomogeneousLocalization, Quotient, PrimeSpectrum.comap, PrimeSpectrum.localization_away_comap_range
-- 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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
this_1 : Algebra (Away 𝒜 f) (Away 𝒜 (f * g)) := RingHom.toAlgebra (awayMap 𝒜 g_deg ⋯)
this : IsLocalization.Away (R := Away 𝒜 f) (Away.isLocalizationElem f_deg g_deg) (Away 𝒜 (f * g)) := ⋯
⊢ Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) ⇑(Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg ⋯))) =
    (↑(PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg)) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f))))

Tactic:
exact PrimeSpectrum.localization_away_comap_range _ _

Premises used: PrimeSpectrum.localization_away_comap_range
-- 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_1 g_1 : A
m_1 : ℕ
f_deg_1 : f_1 ∈ 𝒜 m_1
hm_1 : 0 < m_1
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x_1 : A
hx : x_1 = f_1 * g
ι : Type u_2
f : ι → A
m : ι → ℕ
f_deg : ∀ (i : ι), f i ∈ 𝒜 (m i)
hm : ∀ (i : ι), 0 < m i
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
x : ↥(Proj 𝒜)
rw :
  Membership.mem (γ := (Proj 𝒜).Opens)
    (basicOpen 𝒜
      (f
        (Exists.choose (p := fun (i : ι) ↦ Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x)
          ⋯)))
    x
⊢ Membership.mem (γ := (Proj 𝒜).Opens)
    (Scheme.Hom.opensRange (X :=
      Spec
        (CommRingCat.of
          (Away 𝒜
            (f
              (Exists.choose (p := fun (i : ι) ↦
                Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x) ⋯)))))
      (awayι 𝒜
        (f
          (Exists.choose (p := fun (i : ι) ↦
            Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x) ⋯))
        ⋯ ⋯))
    x

Tactic:
rw [opensRange_awayι]

Premises used: AlgebraicGeometry.Proj.opensRange_awayι
-- 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_1 g_1 : A
m_1 : ℕ
f_deg_1 : f_1 ∈ 𝒜 m_1
hm_1 : 0 < m_1
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x_1 : A
hx : x_1 = f_1 * g
ι : Type u_2
f : ι → A
m : ι → ℕ
f_deg : ∀ (i : ι), f i ∈ 𝒜 (m i)
hm : ∀ (i : ι), 0 < m i
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
x : ↥(Proj 𝒜)
⊢ Membership.mem (γ := (Proj 𝒜).Opens)
    (basicOpen 𝒜
      (f
        (Exists.choose (p := fun (i : ι) ↦ Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x)
          ⋯)))
    x

Tactic:
(mem_iSup.mp ((iSup_basicOpen_eq_top 𝒜 f hf).ge (Set.mem_univ x))).choose_spec

Premises used: Exists.choose_spec, Eq.ge, Set.Mem, TopologicalSpace.Opens.mem_iSup, Iff.mp, Set.mem_univ, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top
-- 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_1 g_1 : A
m_1 : ℕ
f_deg_1 : f_1 ∈ 𝒜 m_1
hm_1 : 0 < m_1
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x_1 : A
hx : x_1 = f_1 * g
ι : Type u_2
f : ι → A
m : ι → ℕ
f_deg : ∀ (i : ι), f i ∈ 𝒜 (m i)
hm : ∀ (i : ι), 0 < m i
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
x : ↥(Proj 𝒜)
⊢ Membership.mem (γ := (Proj 𝒜).Opens)
    (basicOpen 𝒜
      (f
        (Exists.choose (p := fun (i : ι) ↦ Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x)
          ⋯)))
    x

Tactic:
exact (mem_iSup.mp ((iSup_basicOpen_eq_top 𝒜 f hf).ge (Set.mem_univ x))).choose_spec

Premises used: Exists.choose_spec, Eq.ge, TopologicalSpace.Opens.mem_iSup, Iff.mp, Set.mem_univ, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top
-- 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_1 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
z : A
hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z
rw :
  Membership.mem (γ := Submodule A A)
    (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
    (∑
      i ∈
        DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
          ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z),
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            i) :
        A))
⊢ Membership.mem (γ := Submodule A A)
    (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) z

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 z]

Premises used: DirectSum.sum_support_decompose
-- 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_1 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
z : A
hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z
⊢ Membership.mem (γ := Submodule A A)
    (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
    (∑
      i ∈
        DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
          ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z),
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            i) :
        A))

Tactic:
Ideal.sum_mem _ fun c hc ↦ if hc0 : c = 0 then ?_ else
    Ideal.subset_span ⟨⟨⟨c, Nat.pos_iff_ne_zero.mpr hc0⟩, _⟩, rfl⟩

Premises used: Iff.mpr, Ideal.subset_span, Set.Mem, Nat.pos_iff_ne_zero, Ideal.sum_mem, dite, Subtype.mk, Exists.intro, Sigma.mk, OfNat.ofNat, Eq, DFunLike.coe, rfl, DirectSum.decompose
-- 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_1 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
z : A
hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z
refine :
  ∀ (c : ℕ)
    (hc :
      Membership.mem (γ := Finset ℕ)
        (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
          ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z))
        c)
    (hc0 : c = 0),
    Membership.mem (γ := Ideal A)
      (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            c) :
        A)
⊢ Membership.mem (γ := Submodule A A)
    (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
    (∑
      i ∈
        DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
          ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z),
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            i) :
        A))

Tactic:
refine Ideal.sum_mem _ fun c hc ↦ if hc0 : c = 0 then ?_ else
    Ideal.subset_span ⟨⟨⟨c, Nat.pos_iff_ne_zero.mpr hc0⟩, _⟩, rfl⟩
-- 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_1 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
z : A
hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z
c : ℕ
hc :
  Membership.mem (γ := Finset ℕ)
    (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
      ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z))
    c
hc0 : c = 0
⊢ Membership.mem (γ := Ideal A)
    (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) 0

Tactic:
Ideal.zero_mem _

Premises used: Ideal.zero_mem
-- 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_1 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
z : A
hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z
c : ℕ
hc :
  Membership.mem (γ := Finset ℕ)
    (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
      ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z))
    c
hc0 : c = 0
h :
  (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          c) :
      A) =
    0
⊢ Membership.mem (γ := Ideal A)
    (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
    (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          c) :
      A)

Tactic:
convert! Ideal.zero_mem _

Premises used: Ideal.zero_mem
-- 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_1 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
z : A
hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z
c : ℕ
hc :
  Membership.mem (γ := Finset ℕ)
    (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
      ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z))
    c
hc0 : c = 0
h :
  ∀
    (hc :
      Membership.mem (γ := Finset ℕ)
        (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
          ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z))
        0),
    (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            0) :
        A) =
      0
⊢ (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          c) :
      A) =
    0

Tactic:
subst hc0
-- 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_1 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
z : A
hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z
hc :
  Membership.mem (γ := Finset ℕ)
    (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
      ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z))
    0
⊢ (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          0) :
      A) =
    0

Tactic:
hz

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton
-- 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_1 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
z : A
hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z
hc :
  Membership.mem (γ := Finset ℕ)
    (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
      ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z))
    0
⊢ (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          0) :
      A) =
    0

Tactic:
exact hz
-- 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 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
refine : (↑(X.basicOpen x) : Scheme) ⟶ Spec (CommRingCat.of (Away 𝒜 t))
⊢ (↑(X.basicOpen x) : Scheme) ⟶ (↑(basicOpen 𝒜 t) : Scheme)

Tactic:
refine ?_ ≫ (basicOpenIsoSpec _ _ hd h0d).inv

Premises used: AlgebraicGeometry.Proj.basicOpenIsoSpec, CategoryTheory.Iso.inv