awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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
O : Type u_2
commRing : CommRing O
domain : IsDomain O
valuationRing : ValuationRing O
K : Type u_2
field : Field K
algebra : Algebra O K
isFractionRing : IsFractionRing O K
i₁ : Spec (CommRingCat.of K) ⟶ Proj 𝒜
i₂ : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of ↥(𝒜 0))
w : CommSq i₁ (Spec.map (CommRingCat.ofHom (algebraMap O K))) (toSpecZero 𝒜) i₂
x_1 : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x_1 : Set A)) ⊤
d : (i : A) → i ∈ x_1 → ℕ
hd : ∀ (i : A) (a : i ∈ x_1), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x_1), i ∈ 𝒜 (d i a)
i : ↥x_1
hi :
  Membership.mem (α := ↥(Proj 𝒜)) (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (↑i : A))
    (i₁ (IsLocalRing.closedPoint K) : ↥(Proj 𝒜))
this : Set.range (ι := ↥(Spec (CommRingCat.of K))) ⇑i₁ ⊆ (↑(Hom.opensRange (awayι 𝒜 (↑i : A) ⋯ ⋯)) : Set ↥(Proj 𝒜))
φ : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of (Away 𝒜 (↑i : A))) :=
  IsOpenImmersion.lift (awayι 𝒜 (↑i : A) ⋯ ⋯) i₁ this
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A))) ≫ Spec.preimage φ
i₀ : ↥x_1
φ' : Away 𝒜 ((↑i : A) * (↑i₀ : A)) →+* K
hφ : φ'.comp (awayMap 𝒜 ⋯ ⋯) = CommRingCat.Hom.hom (Spec.preimage φ)
hφ' :
  LE.le.{u_2} (α := Subring K) (RingHom.range (R := Away 𝒜 (↑i₀ : A)) (φ'.comp (awayMap 𝒜 ⋯ ⋯)))
    (RingHom.range (R := O) (algebraMap O K))
e : O ≃+* ↥(RingHom.range (R := O) (algebraMap O K)) := AlgEquiv.toRingEquiv (AlgEquiv.ofInjective (Algebra.ofId O K) ⋯)
φ'' : Away 𝒜 (↑i₀ : A) →+* O :=
  e.symm.toRingHom.comp ((Subring.inclusion hφ').comp (RingHom.rangeRestrict (φ'.comp (awayMap 𝒜 ⋯ ⋯))))
hφ'' : RingHom.comp (algebraMap O K) φ'' = φ'.comp (awayMap 𝒜 ⋯ ⋯)
x : (↑(CommRingCat.of ↥(𝒜 0)) : Type u_2)
⊢ Eq (α := K)
    ((φ' : (a : Away 𝒜 ((↑i : A) * (↑i₀ : A))) → K)
        ((awayMap 𝒜 ⋯ ⋯ : (a : HomogeneousLocalization 𝒜 (Submonoid.powers (↑i₀ : A))) → Away 𝒜 ((↑i : A) * (↑i₀ : A)))
            ((fromZeroRingHom 𝒜 (Submonoid.powers (↑i₀ : A)) :
                (a : ↥(𝒜 0)) → HomogeneousLocalization 𝒜 (Submonoid.powers (↑i₀ : A)))
              x) :
          Away 𝒜 ((↑i : A) * (↑i₀ : A))) :
      K)
    ((algebraMap O K : (a : O) → K) ((CommRingCat.Hom.hom (Spec.preimage i₂) : (a : ↥(𝒜 0)) → O) x : O) : K)
have refine_2 : Eq (α := K)
  ((CommRingCat.Hom.hom (Spec.preimage φ) : (a : Away 𝒜 (↑i : A)) → K)
      ((fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A)) :
            (a : ↥(𝒜 0)) → HomogeneousLocalization 𝒜 (Submonoid.powers (↑i : A)))
          x :
        HomogeneousLocalization 𝒜 (Submonoid.powers (↑i : A))) :
    K)
  ((algebraMap O K : (a : O) → K) ((CommRingCat.Hom.hom (Spec.preimage i₂) : (a : ↥(𝒜 0)) → O) x : O) : K)
Tactic: rw [awayMap_fromZeroRingHom, ← awayMap_fromZeroRingHom 𝒜 (hxd i₀ i₀.2) rfl,
      ← RingHom.comp_apply, hφ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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
⊢ UniversallyClosed (X := Proj 𝒜) (toSpecZero 𝒜)
have rw : (ValuativeCriterion.Existence ⊓ @QuasiCompact) (X := Proj 𝒜) (toSpecZero 𝒜)
Tactic: rw [UniversallyClosed.eq_valuativeCriterion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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)
⊢ HomogeneousLocalization.mk z ∈ carrier x ↔ (↑z.num : A) ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal
have rw : (↑z.num : A) ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal ↔
  (↑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)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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
⊢ HomogeneousLocalization.mk z ∈ carrier x ↔ (↑z.num : A) ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal
have hI : (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.IsPrime
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)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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
⊢ HomogeneousLocalization.mk z ∈ carrier x ↔ (↑z.num : A) ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal
have hM : Disjoint (↑(Submonoid.powers f) : Set A) (↑(↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal : Set A)
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)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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)
⊢ HomogeneousLocalization.mk z ∈ carrier x ↔ (↑z.num : A) ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal
have 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) sorry))
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)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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
have refine : IsPrime (α := Away f)
  (Ideal.map (F := A →+* Away f) (algebraMap A (Away f)) (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal)
Tactic: refine Ideal.IsPrime.comap _ (hK := ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
⊢ Continuous (X := ↥(pbo f)) (ToSpec.toFun f)
have 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)
Tactic: rw [PrimeSpectrum.isTopologicalBasis_basic_opens.continuous_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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)
⊢ 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)
have 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))
Tactic: obtain ⟨x, rfl⟩ := Quotient.mk''_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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))
    (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))
have 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 𝒜)))
Tactic: rw [ToSpec.preimage_basicOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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)
have rw : HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m ∈ 𝒜 (m • i)
Tactic: rw [← smul_eq_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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 ∈ 𝒜 (m * i)
have rw : f ^ i ∈ 𝒜 (i * m)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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)
have rw : HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m ∈ 𝒜 (m • i)
Tactic: rw [← smul_eq_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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 ∈ 𝒜 (m * i)
have rw : f ^ i ∈ 𝒜 (i * m)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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 : ℕ),
      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) ⋯))
have 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) sorry,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry } ∈
      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) sorry))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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) ⋯))
⊢ (∀ (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) ⋯))
have 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) sorry))) →
  ∀ (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) sorry,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry } ∈
      q.asIdeal
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (hypothesis)
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 : ℕ
⊢ 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) ⋯))
have 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) sorry,
      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry } ∈
  q.asIdeal
Tactic: specialize h i
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (hypothesis)
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 : ℕ
⊢ 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
have h₁ : 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) sorry))
Tactic: specialize h i
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (hypothesis)
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 :
  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) ⋯))
⊢ 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
have h₁ : ∃ (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) sorry) :
        Localization (Submonoid.powers f))
Tactic: rw [Set.mem_image] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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 :
  ∃ (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))
⊢ 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
have mpr : ∀ (x : A⁰_ f) (h : Membership.mem (γ := Set (A⁰_ f)) {s : A⁰_ f | s ∈ q.asIdeal} x)
  (hx :
    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) sorry) :
        Localization (Submonoid.powers f))),
  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) sorry,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry } ∈
    q.asIdeal
Tactic: rcases h with ⟨x, h, hx⟩
Cleared hypotheses: h