awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
⊢ (ValuativeCriterion.Existence ⊓ @QuasiCompact) (X := Proj 𝒜) (toSpecZero 𝒜)

Tactic:
exact ⟨valuativeCriterion_existence 𝒜, inferInstance⟩
-- 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
x :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
rw :
  (↑z.num : A) ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal ↔
    (↑z.num : A) ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal
hI : (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.IsPrime
hM : Disjoint (↑(Submonoid.powers f) : Set A) (↑(↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal : Set A)
hy :
  IsUnit (M := Away f)
    (IsLocalization.mk' (Localization (Submonoid.powers f)) 1
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (↑z.den : A) ⋯))
⊢ HomogeneousLocalization.mk z ∈ carrier x ↔ (↑z.num : A) ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal

Tactic:
rw [carrier, Ideal.mem_comap, HomogeneousLocalization.algebraMap_apply,
    HomogeneousLocalization.val_mk, Localization.mk_eq_mk', IsLocalization.mk'_eq_mul_mk'_one,
    mul_comm, Ideal.unit_mul_mem_iff_mem, ← Ideal.mem_under,
    IsLocalization.under_map_of_isPrime_disjoint (.powers f)]

Premises used: Localization.mk_eq_mk', AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier, IsLocalization.mk'_eq_mul_mk'_one, HomogeneousLocalization.val_mk, Ideal.mem_under, Submonoid.powers, Ideal.unit_mul_mem_iff_mem, mul_comm, Ideal.mem_comap, HomogeneousLocalization.algebraMap_apply, IsLocalization.under_map_of_isPrime_disjoint
-- 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
x :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ (↑z.num : A) ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal ↔
    (↑z.num : A) ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal

Tactic:
rfl
-- 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
x :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.IsPrime

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
x :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Disjoint (↑(Submonoid.powers f) : Set A) (↑(↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal : Set A)

Tactic:
(disjoint_powers_iff_notMem_of_isPrime _).mpr x.2

Premises used: Iff.mpr, Ideal.disjoint_powers_iff_notMem_of_isPrime, Subtype.property
-- 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
x :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Disjoint (↑(Submonoid.powers f) : Set A) (↑(↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal : Set A)

Tactic:
exact (disjoint_powers_iff_notMem_of_isPrime _).mpr x.2

Premises used: Iff.mpr, Ideal.disjoint_powers_iff_notMem_of_isPrime, Subtype.property
-- 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
x :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ IsUnit (M := Away f)
    (IsLocalization.mk' (Localization (Submonoid.powers f)) 1
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (↑z.den : A) ⋯))

Tactic:
isUnit_of_invertible _

Premises used: isUnit_of_invertible
-- 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
x :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ IsUnit (M := Away f)
    (IsLocalization.mk' (Localization (Submonoid.powers f)) 1
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (↑z.den : A) ⋯))

Tactic:
exact isUnit_of_invertible _

Premises used: isUnit_of_invertible
-- 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
x :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
⊢ (carrier x).IsPrime

Tactic:
Ideal.IsPrime.comap _ (hK := ?_)

Premises used: AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier, Ideal.IsPrime.comap
-- 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
x :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
refine :
  IsPrime (α := Away f)
    (Ideal.map (F := A →+* Away f) (algebraMap A (Away f)) (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal)
⊢ (carrier x).IsPrime

Tactic:
refine Ideal.IsPrime.comap _ (hK := ?_)

Premises used: Ideal.IsPrime.comap
-- 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
x :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
⊢ IsPrime (α := Away f)
    (Ideal.map (F := A →+* Away f) (algebraMap A (Away f)) (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal)

Tactic:
IsLocalization.isPrime_of_isPrime_disjoint
    (Submonoid.powers f) _ _ inferInstance
    ((disjoint_powers_iff_notMem_of_isPrime _).mpr x.2)

Premises used: Iff.mpr, inferInstance, IsLocalization.isPrime_of_isPrime_disjoint, Submonoid.powers, Ideal.disjoint_powers_iff_notMem_of_isPrime, Subtype.property
-- 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
x :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
⊢ IsPrime (α := Away f)
    (Ideal.map (F := A →+* Away f) (algebraMap A (Away f)) (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal)

Tactic:
exact IsLocalization.isPrime_of_isPrime_disjoint
    (Submonoid.powers f) _ _ inferInstance
    ((disjoint_powers_iff_notMem_of_isPrime _).mpr x.2)

Premises used: Iff.mpr, inferInstance, IsLocalization.isPrime_of_isPrime_disjoint, Submonoid.powers, Ideal.disjoint_powers_iff_notMem_of_isPrime, Subtype.property
-- 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
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ toFun f ⁻¹' (↑(sbo HomogeneousLocalization.mk z) : Set (PrimeSpectrum (A⁰_ f))) =
    Subtype.val (p := fun (x : (↑Proj.T : Type u_1)) ↦ Membership.mem (γ := Opens (↑Proj.T : Type u_1)) (pbo f) x) ⁻¹'
      (↑(pbo (↑z.num : A)) : Set (ProjectiveSpectrum 𝒜))

Tactic:
Set.ext fun y ↦ (mk_mem_carrier y z).not

Premises used: Set.ext, Iff.not, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier
-- 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
rw :
  ∀ (s : Set (PrimeSpectrum (↑(CommRingCat.of (A⁰_ f)) : Type u_1))),
    Membership.mem (γ := Set (Set (PrimeSpectrum (↑(CommRingCat.of (A⁰_ f)) : Type u_1))))
        (Set.range fun (r : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)) ↦
          (↑(sbo r) : Set (PrimeSpectrum (↑(CommRingCat.of (A⁰_ f)) : Type u_1))))
        s →
      IsOpen (ToSpec.toFun f ⁻¹' s)
⊢ Continuous (X := ↥(pbo f)) (ToSpec.toFun f)

Tactic:
rw [PrimeSpectrum.isTopologicalBasis_basic_opens.continuous_iff]

Premises used: PrimeSpectrum.isTopologicalBasis_basic_opens, TopologicalSpace.IsTopologicalBasis.continuous_iff
-- 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
x : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)
obtain :
  ∀ (x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)),
    IsOpen (X := ↥(pbo f))
      (ToSpec.toFun f ⁻¹'
        (fun (r : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)) ↦
            (↑(sbo r) : Set (PrimeSpectrum (↑(CommRingCat.of (A⁰_ f)) : Type u_1))))
          (Quotient.mk'' x))
⊢ IsOpen (X := ↥(pbo f))
    (ToSpec.toFun f ⁻¹'
      (fun (r : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)) ↦
          (↑(sbo r) : Set (PrimeSpectrum (↑(CommRingCat.of (A⁰_ f)) : Type u_1))))
        x)

Tactic:
obtain ⟨x, rfl⟩ := Quotient.mk''_surjective x

Premises used: Quotient.mk''_surjective, rfl
-- 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
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
rw :
  IsOpen (X := ↥(pbo f))
    (Subtype.val (p := fun (x : (↑Proj.T : Type u_1)) ↦ Membership.mem (γ := Opens (↑Proj.T : Type u_1)) (pbo f) x) ⁻¹'
      (↑(pbo (↑x.num : A)) : Set (ProjectiveSpectrum 𝒜)))
⊢ IsOpen (X := ↥(pbo f))
    (ToSpec.toFun f ⁻¹'
      (fun (r : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)) ↦
          (↑(sbo r) : Set (PrimeSpectrum (↑(CommRingCat.of (A⁰_ f)) : Type u_1))))
        (Quotient.mk'' x))

Tactic:
rw [ToSpec.preimage_basicOpen]

Premises used: AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen
-- 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
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ IsOpen (X := ↥(pbo f))
    (Subtype.val (p := fun (x : (↑Proj.T : Type u_1)) ↦ Membership.mem (γ := Opens (↑Proj.T : Type u_1)) (pbo f) x) ⁻¹'
      (↑(pbo (↑x.num : A)) : Set (ProjectiveSpectrum 𝒜)))

Tactic:
(pbo (x.num : A)).2.preimage continuous_subtype_val

Premises used: HomogeneousLocalization.NumDenSameDeg.num, continuous_subtype_val, ProjectiveSpectrum.basicOpen, Set.Mem, setOf, TopologicalSpace.Opens.is_open', IsOpen.preimage, Subtype.val
-- 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
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ IsOpen (X := ↥(pbo f))
    (Subtype.val (p := fun (x : (↑Proj.T : Type u_1)) ↦ Membership.mem (γ := Opens (↑Proj.T : Type u_1)) (pbo f) x) ⁻¹'
      (↑(pbo (↑x.num : A)) : Set (ProjectiveSpectrum 𝒜)))

Tactic:
exact (pbo (x.num : A)).2.preimage continuous_subtype_val

Premises used: HomogeneousLocalization.NumDenSameDeg.num, continuous_subtype_val, ProjectiveSpectrum.basicOpen, TopologicalSpace.Opens.is_open', IsOpen.preimage, Subtype.val
-- 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
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Eq (α :=
    Set
      (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  ⋯).toPresheafedSpace :
            TopCat) :
        Type u_1))
    ((⇑(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))
            (toSpec 𝒜 f)) :
        (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
          (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)) ⁻¹'
      (↑(sbo HomogeneousLocalization.mk z) : Set (PrimeSpectrum (A⁰_ f))))
    (Subtype.val (p := fun (x : (↑Proj.T : Type u_1)) ↦ Membership.mem (γ := Opens (↑Proj.T : Type u_1)) (pbo f) x) ⁻¹'
      (↑(pbo (↑z.num : A)) : Set (ProjectiveSpectrum 𝒜)))

Tactic:
ToSpec.preimage_basicOpen f z

Premises used: Set.Mem, setOf, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen
-- 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_1 f_deg : f ∈ 𝒜 m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
i : ℕ
rw : HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m ∈ 𝒜 (m • i)
⊢ HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m ∈ 𝒜 (m * i)

Tactic:
rw [← smul_eq_mul]

Premises used: smul_eq_mul
-- 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_1 f_deg : f ∈ 𝒜 m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
i : ℕ
⊢ HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m ∈ 𝒜 (m • i)

Tactic:
mem_tac
-- 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_1 f_deg : f ∈ 𝒜 m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
i : ℕ
rw : f ^ i ∈ 𝒜 (i * m)
⊢ f ^ i ∈ 𝒜 (m * i)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- 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_1 f_deg : f ∈ 𝒜 m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (i * m)

Tactic:
mem_tac
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
i : ℕ
rw : HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m ∈ 𝒜 (m • i)
⊢ HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m ∈ 𝒜 (m * i)

Tactic:
rw [← smul_eq_mul]

Premises used: smul_eq_mul
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
i : ℕ
⊢ HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m ∈ 𝒜 (m • i)

Tactic:
mem_tac
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
i : ℕ
rw : f ^ i ∈ 𝒜 (i * m)
⊢ f ^ i ∈ 𝒜 (m * i)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (i * m)

Tactic:
mem_tac
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
⊢ a ∈ carrier f_deg q ↔
    ∀ (i : ℕ),
      HomogeneousLocalization.mk
          { deg := m * i,
            num :=
              Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m) ⋯,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
        q.asIdeal

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
mp :
  (∀ (i : ℕ),
      HomogeneousLocalization.mk
          { deg := m * i,
            num :=
              Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m) ⋯,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
        q.asIdeal) →
    ∀ (i : ℕ),
      Membership.mem (γ := Set (Localization.Away f))
        (Set.image (α := A⁰_ f) (⇑(algebraMap (A⁰_ f) (Localization.Away f)) : (a : A⁰_ f) → Localization.Away f)
          {s : A⁰_ f | s ∈ q.asIdeal})
        (Localization.mk (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯))
mpr :
  (∀ (i : ℕ),
      Membership.mem (γ := Set (Localization.Away f))
        (Set.image (α := A⁰_ f) (⇑(algebraMap (A⁰_ f) (Localization.Away f)) : (a : A⁰_ f) → Localization.Away f)
          {s : A⁰_ f | s ∈ q.asIdeal})
        (Localization.mk (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯))) →
    ∀ (i : ℕ),
      HomogeneousLocalization.mk
          { deg := m * i,
            num :=
              Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m) ⋯,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
        q.asIdeal
⊢ (∀ (i : ℕ),
      HomogeneousLocalization.mk
          { deg := m * i,
            num :=
              Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m) ⋯,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
        q.asIdeal) ↔
    ∀ (i : ℕ),
      Membership.mem (γ := Set (Localization.Away f))
        (Set.image (α := A⁰_ f) (⇑(algebraMap (A⁰_ f) (Localization.Away f)) : (a : A⁰_ f) → Localization.Away f)
          {s : A⁰_ f | s ∈ q.asIdeal})
        (Localization.mk (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯))

Tactic:
constructor
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
h :
  ∀ (i : ℕ),
    HomogeneousLocalization.mk
        { deg := m * i,
          num :=
            Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
      q.asIdeal
i : ℕ
⊢ HomogeneousLocalization.mk
      { deg := m * i,
        num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
specialize h i
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
h :
  ∀ (i : ℕ),
    Membership.mem (γ := Set (Localization.Away f))
      (Set.image (α := A⁰_ f) (⇑(algebraMap (A⁰_ f) (Localization.Away f)) : (a : A⁰_ f) → Localization.Away f)
        {s : A⁰_ f | s ∈ q.asIdeal})
      (Localization.mk (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯))
i : ℕ
⊢ Membership.mem (γ := Set (Localization.Away f))
    (Set.image (α := A⁰_ f) (⇑(algebraMap (A⁰_ f) (Localization.Away f)) : (a : A⁰_ f) → Localization.Away f)
      {s : A⁰_ f | s ∈ q.asIdeal})
    (Localization.mk (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯))

Tactic:
specialize h i
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
i : ℕ
h :
  HomogeneousLocalization.mk
      { deg := m * i,
        num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
    q.asIdeal
⊢ ∃ (x : A⁰_ f),
    Membership.mem (γ := Set (A⁰_ f)) {s : A⁰_ f | s ∈ q.asIdeal} x ∧
      Eq (α := Localization (Submonoid.powers f))
        ((algebraMap (A⁰_ f) (Localization.Away f) : (a : A⁰_ f) → Localization.Away f) x : Localization.Away f)
        (Localization.mk (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m)
            (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯) :
          Localization (Submonoid.powers f))

Tactic:
⟨_, h, rfl⟩

Premises used: And.intro, Exists.intro, rfl