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 𝒜
i j :
  PreZeroHypercover.I₀ (S := Proj 𝒜)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (AffineOpenCover.openCover (affineOpenCover 𝒜)))
⊢ AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) j ≫ toSpecZero 𝒜 =
    Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))))
have refine_2 : Eq.{u_2 + 1} (α :=
  Spec (CommRingCat.of (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) ⟶ Spec (CommRingCat.of ↥(𝒜 0)))
  (Spec.map
    (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))
  (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))
Tactic: simp [affineOpenCover, affineOpenCoverOfIrrelevantLESpan, awayι_toSpecZero]
-- 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
⊢ LocallyOfFiniteType (X := Proj 𝒜) (toSpecZero 𝒜)
have obtain : ∀ (x : Finset A) (hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤)
  (hx' : ∀ i ∈ x, ∃ (n : ℕ), n ≠ 0 ∧ i ∈ 𝒜 n), LocallyOfFiniteType (X := Proj 𝒜) (toSpecZero 𝒜)
Tactic: obtain ⟨x, hx, hx'⟩ := GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero 𝒜
-- 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
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
hx' : ∀ i ∈ x, ∃ (n : ℕ), n ≠ 0 ∧ i ∈ 𝒜 n
⊢ LocallyOfFiniteType (X := Proj 𝒜) (toSpecZero 𝒜)
have choose : ∀ (d : (i : A) → i ∈ x → ℕ) (hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0) (hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)),
  LocallyOfFiniteType (X := Proj 𝒜) (toSpecZero 𝒜)
Tactic: choose d hd hxd using hx'
Cleared hypotheses: hx'
-- 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
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
⊢ LocallyOfFiniteType (X := Proj 𝒜) (toSpecZero 𝒜)
have rw : ∀ (i : ↥x),
  LocallyOfFiniteType (X := (↑(basicOpen 𝒜 (↑i : A)) : Scheme)) (Opens.ι (basicOpen 𝒜 (↑i : A)) ≫ toSpecZero 𝒜)
Tactic: rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := @LocallyOfFiniteType) _
    (Proj.iSup_basicOpen_eq_top' 𝒜 (ι := x) (↑) (fun i ↦ ⟨_, hxd _ i.2⟩) (by simpa using hx))]
-- 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
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
⊢ LocallyOfFiniteType (X := (↑(basicOpen 𝒜 (↑i : A)) : Scheme)) (Opens.ι (basicOpen 𝒜 (↑i : A)) ≫ toSpecZero 𝒜)
have rw : RingHom.FiniteType.{u_2, u_2} (A := (↑(CommRingCat.of ↥(𝒜 0)) : Type u_2)) (B :=
  (↑(CommRingCat.of (HomogeneousLocalization 𝒜 (Submonoid.powers (↑i : A)))) : Type u_2))
  (CommRingCat.Hom.hom (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A)))))
Tactic: rw [← MorphismProperty.cancel_left_of_respectsIso (P := @LocallyOfFiniteType)
    (Proj.basicOpenIsoSpec 𝒜 (i : A) (hxd _ i.2) (hd _ i.2).bot_lt).inv, ← Category.assoc,
    ← Proj.awayι, Proj.awayι_toSpecZero, HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)]
-- 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
⊢ QuasiCompact (X := Proj 𝒜) (toSpecZero 𝒜)
have rw : CompactSpace.{u_2} ↥(Proj 𝒜)
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := @QuasiCompact)]
-- 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
⊢ CompactSpace.{u_2} ↥(Proj 𝒜)
have obtain : ∀ (x : Finset A) (hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤)
  (hx' : ∀ i ∈ x, ∃ (n : ℕ), n ≠ 0 ∧ i ∈ 𝒜 n), CompactSpace.{u_2} ↥(Proj 𝒜)
Tactic: obtain ⟨x, hx, hx'⟩ := GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero 𝒜
-- 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
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
hx' : ∀ i ∈ x, ∃ (n : ℕ), n ≠ 0 ∧ i ∈ 𝒜 n
⊢ CompactSpace.{u_2} ↥(Proj 𝒜)
have choose : ∀ (d : (i : A) → i ∈ x → ℕ) (hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0) (hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)),
  CompactSpace.{u_2} ↥(Proj 𝒜)
Tactic: choose d hd hxd using hx'
Cleared hypotheses: hx'
-- 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
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
⊢ IsCompact (X := ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (basicOpen 𝒜 (↑i : A)))
have rw : IsCompact (X := ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (Hom.opensRange (awayι 𝒜 (↑i : A) sorry sorry)))
Tactic: rw [← Proj.opensRange_awayι _ _ (hxd _ i.2) (hd _ i.2).bot_lt]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (hypothesis)
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
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
⊢ CompactSpace.{u_2} ↥(Proj 𝒜)
have H : ∀ (i : ↥x), IsCompact (X := ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (basicOpen 𝒜 (↑i : A)))
Tactic: have H (i : x) : IsCompact (Proj.basicOpen 𝒜 (i : A)).1 := by
    rw [← Proj.opensRange_awayι _ _ (hxd _ i.2) (hd _ i.2).bot_lt]
    exact isCompact_range (Proj.awayι _ _ (hxd _ i.2) (hd _ i.2).bot_lt).continuous
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (hypothesis)
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
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
H : ∀ (i : ↥x), IsCompact (X := ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (basicOpen 𝒜 (↑i : A)))
⊢ CompactSpace.{u_2} ↥(Proj 𝒜)
have this : Eq.{u_2 + 1} (α := Set ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (⨆ (i : ↥x), basicOpen 𝒜 (↑i : A)))
  (TopologicalSpace.Opens.carrier ⊤)
Tactic: have := congr($(Proj.iSup_basicOpen_eq_top' 𝒜
    (ι := x) (↑) (fun i ↦ ⟨_, hxd _ i.2⟩) (by simpa using hx)).1)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (hypothesis)
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
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
H : ∀ (i : ↥x), IsCompact (X := ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (basicOpen 𝒜 (↑i : A)))
this :
  Eq.{u_2 + 1} (α := Set ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (⨆ (i : ↥x), basicOpen 𝒜 (↑i : A)))
    (TopologicalSpace.Opens.carrier ⊤)
⊢ CompactSpace.{u_2} ↥(Proj 𝒜)
have this₁ : Eq.{u_2 + 1} (α := Set ↥(Proj 𝒜)) (⋃ (i : ↥x), (↑(basicOpen 𝒜 (↑i : A)) : Set ↥(Proj 𝒜))) Set.univ
Tactic: simp only [TopologicalSpace.Opens.iSup_mk, TopologicalSpace.Opens.carrier_eq_coe,
    TopologicalSpace.Opens.coe_mk, TopologicalSpace.Opens.coe_top] at this
Cleared hypotheses: this
-- 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
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
H : ∀ (i : ↥x), IsCompact (X := ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (basicOpen 𝒜 (↑i : A)))
this : Eq.{u_2 + 1} (α := Set ↥(Proj 𝒜)) (⋃ (i : ↥x), (↑(basicOpen 𝒜 (↑i : A)) : Set ↥(Proj 𝒜))) Set.univ
⊢ CompactSpace.{u_2} ↥(Proj 𝒜)
have rw : IsCompact.{u_2} (X := ↥(Proj 𝒜)) (⋃ (i : ↥x), (↑(basicOpen 𝒜 (↑i : A)) : Set ↥(Proj 𝒜)))
Tactic: rw [← isCompact_univ_iff, ← this]
-- 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₂
⊢ ⋯.HasLift
have obtain : ∀ (x : Finset A) (hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤)
  (hx' : ∀ i ∈ x, ∃ (n : ℕ), n ≠ 0 ∧ i ∈ 𝒜 n), sorry.HasLift
Tactic: obtain ⟨x, hx, hx'⟩ := GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero 𝒜
-- 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 : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
hx' : ∀ i ∈ x, ∃ (n : ℕ), n ≠ 0 ∧ i ∈ 𝒜 n
⊢ ⋯.HasLift
have choose : ∀ (d : (i : A) → i ∈ x → ℕ) (hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0) (hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)),
  sorry.HasLift
Tactic: choose d hd hxd using hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (hypothesis)
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 : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
⊢ ⋯.HasLift
have this : Membership.mem (α := ↥(Proj 𝒜)) (γ := (Proj 𝒜).Opens) ⊤ (i₁ (IsLocalRing.closedPoint K) : ↥(Proj 𝒜))
Tactic: have : i₁ (IsLocalRing.closedPoint K) ∈ (⊤ : (Proj 𝒜).Opens) := trivial
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (hypothesis)
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 : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
this : Membership.mem (α := ↥(Proj 𝒜)) (γ := (Proj 𝒜).Opens) ⊤ (i₁ (IsLocalRing.closedPoint K) : ↥(Proj 𝒜))
⊢ ⋯.HasLift
have this₁ : ∃ (i : ↥x),
  Membership.mem (α := ↥(Proj 𝒜)) (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (↑i : A))
    (i₁ (IsLocalRing.closedPoint K) : ↥(Proj 𝒜))
Tactic: rw [← Proj.iSup_basicOpen_eq_top' 𝒜 (ι := x) (↑) (fun i ↦ ⟨_, hxd _ i.2⟩) (by simpa using hx),
    TopologicalSpace.Opens.mem_iSup] at this
Cleared hypotheses: this
-- 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 : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
this :
  ∃ (i : ↥x),
    Membership.mem (α := ↥(Proj 𝒜)) (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (↑i : A))
      (i₁ (IsLocalRing.closedPoint K) : ↥(Proj 𝒜))
⊢ ⋯.HasLift
have obtain : ∀ (i : ↥x)
  (hi :
    Membership.mem (α := ↥(Proj 𝒜)) (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (↑i : A))
      (i₁ (IsLocalRing.closedPoint K) : ↥(Proj 𝒜))),
  sorry.HasLift
Tactic: obtain ⟨i, hi⟩ := this
Cleared hypotheses: this
-- 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 : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
hi :
  Membership.mem (α := ↥(Proj 𝒜)) (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (↑i : A))
    (i₁ (IsLocalRing.closedPoint K) : ↥(Proj 𝒜))
⊢ Set.range (ι := ↥(Spec (CommRingCat.of K))) ⇑i₁ ⊆ (↑(Hom.opensRange (awayι 𝒜 (↑i : A) ⋯ ⋯)) : Set ↥(Proj 𝒜))
have rw : Set.range (ι := ↥(Spec (CommRingCat.of K))) ⇑i₁ ⊆ (↑(basicOpen 𝒜 (↑i : A)) : Set ↥(Proj 𝒜))
Tactic: rw [Proj.opensRange_awayι]
-- 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 𝒜))
x : ↥(Spec (CommRingCat.of K))
⊢ Membership.mem (α := ↥(Proj 𝒜)) (↑(basicOpen 𝒜 (↑i : A)) : Set ↥(Proj 𝒜)) (i₁ x : ↥(Proj 𝒜))
have obtain : Membership.mem (α := ↥(Proj 𝒜)) (↑(basicOpen 𝒜 (↑i : A)) : Set ↥(Proj 𝒜)) (i₁ (IsLocalRing.closedPoint K) : ↥(Proj 𝒜))
Tactic: obtain rfl := Subsingleton.elim x (IsLocalRing.closedPoint K)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (hypothesis)
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 : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
hi :
  Membership.mem (α := ↥(Proj 𝒜)) (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (↑i : A))
    (i₁ (IsLocalRing.closedPoint K) : ↥(Proj 𝒜))
⊢ ⋯.HasLift
have this : Set.range (ι := ↥(Spec (CommRingCat.of K))) ⇑i₁ ⊆ (↑(Hom.opensRange (awayι 𝒜 (↑i : A) sorry sorry)) : Set ↥(Proj 𝒜))
Tactic: have : Set.range i₁ ⊆ (Proj.awayι 𝒜 _ (hxd i i.2) (hd i i.2).bot_lt).opensRange := by
    rw [Proj.opensRange_awayι]
    rintro _ ⟨x, rfl⟩
    obtain rfl := Subsingleton.elim x (IsLocalRing.closedPoint K)
    exact hi
-- 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 : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
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
⊢ Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A))) ≫ Spec.preimage φ
have a : Spec.map (Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K)) =
  Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A))) ≫ Spec.preimage φ)
Tactic: apply Spec.map_injective
-- 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 : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
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
⊢ Spec.map (Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K)) =
    Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A))) ≫ Spec.preimage φ)
have a : i₁ ≫ toSpecZero 𝒜 = φ ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A))))
Tactic: simp only [Spec.map_comp, Spec.map_preimage, ← w.w]
-- 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 : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
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
⊢ i₁ ≫ toSpecZero 𝒜 = φ ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A))))
have a : 0 < d (↑i : A) sorry
Tactic: rw [← Proj.awayι_toSpecZero _ _ (hxd i i.2), IsOpenImmersion.lift_fac_assoc]