awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 𝒜))
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
⊢ ⋯.HasLift
have H : Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
  CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A))) ≫ Spec.preimage φ
Tactic: have H : Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
      CommRingCat.ofHom (fromZeroRingHom 𝒜 _) ≫ Spec.preimage φ := by
    apply Spec.map_injective
    simp only [Spec.map_comp, Spec.map_preimage, ← w.w]
    rw [← Proj.awayι_toSpecZero _ _ (hxd i i.2), IsOpenImmersion.lift_fac_assoc]
    exact Nat.zero_lt_of_ne_zero (hd i i.2)
-- 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
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A))) ≫ Spec.preimage φ
⊢ ⋯.HasLift
have obtain : ∀ (i₀ : ↥x) (φ' : Away 𝒜 ((↑i : A) * (↑i₀ : A)) →+* K)
  (hφ : φ'.comp (awayMap 𝒜 sorry sorry) = CommRingCat.Hom.hom (Spec.preimage φ))
  (hφ' :
    LE.le.{u_2} (α := Subring K) (RingHom.range (R := Away 𝒜 (↑i₀ : A)) (φ'.comp (awayMap 𝒜 sorry sorry)))
      (RingHom.range (R := O) (algebraMap O K))),
  sorry.HasLift
Tactic: obtain ⟨i₀, φ', hφ, hφ'⟩ :=
    valuativeCriterion_existence_aux 𝒜 (Spec.preimage i₂).hom x (↑) (by simpa using hx) i
      (O := O) (K := K) (Spec.preimage φ).hom congr(($H).hom)
      (fun i ↦ d _ i.2) (fun i ↦ (hd _ i.2).bot_lt) (fun i ↦ hxd _ i.2)
-- 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
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A))) ≫ Spec.preimage φ
i₀ : ↥x
φ' : 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 𝒜 ⋯ ⋯))))
⊢ RingHom.comp (algebraMap O K) φ'' = φ'.comp (awayMap 𝒜 ⋯ ⋯)
have a : ∀ (x_1 : Away 𝒜 (↑i₀ : A)),
  Eq (α := K) ((RingHom.comp (algebraMap O K) φ'' : (a : Away 𝒜 (↑i₀ : A)) → K) x_1 : K)
    ((φ'.comp (awayMap 𝒜 sorry sorry) : (a : Away 𝒜 (↑i₀ : A)) → K) x_1 : K)
Tactic: ext 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 𝒜))
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
φ' : 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 𝒜 ⋯ ⋯))))
⊢ ⋯.HasLift
have hφ'' : RingHom.comp (algebraMap O K) φ'' = φ'.comp (awayMap 𝒜 sorry sorry)
Tactic: have hφ'' : (algebraMap O K).comp φ'' = φ'.comp (awayMap 𝒜 (hxd _ i.2) (mul_comm _ _)) := by
    ext x
    exact congr_arg Subtype.val (e.apply_symm_apply _)
-- 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
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A))) ≫ Spec.preimage φ
i₀ : ↥x
φ' : 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 𝒜 ⋯ ⋯)
⊢ CategoryStruct.comp (Y := Proj 𝒜) (Spec.map (CommRingCat.ofHom φ'') ≫ awayι 𝒜 (↑i₀ : A) ⋯ ⋯) (toSpecZero 𝒜) =
    { R := O, commRing := commRing, domain := domain, valuationRing := valuationRing, K := K, field := field,
        algebra := algebra, isFractionRing := isFractionRing, i₁ := i₁, i₂ := i₂, commSq := w :
        ValuativeCommSq (X := Proj 𝒜) (toSpecZero 𝒜) }.i₂
have refine_2 : Spec.map
    (CategoryStruct.comp (Y := CommRingCat.of (Away 𝒜 (↑i₀ : A)))
      (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i₀ : A)))) (CommRingCat.ofHom φ'')) =
  i₂
Tactic: simp only [Category.assoc, Proj.awayι_toSpecZero, ← Spec.map_comp]
-- 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
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A))) ≫ Spec.preimage φ
i₀ : ↥x
φ' : 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 𝒜 ⋯ ⋯)
| i₂
have rw : Spec.map (Spec.preimage i₂)
Tactic: rw [← Spec.map_preimage i₂]
-- 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
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A))) ≫ Spec.preimage φ
i₀ : ↥x
φ' : 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 𝒜 ⋯ ⋯)
⊢ Spec.map
      (CategoryStruct.comp (Y := CommRingCat.of (Away 𝒜 (↑i₀ : A)))
        (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i₀ : A)))) (CommRingCat.ofHom φ'')) =
    i₂
have refine_2 : Spec.map
    (CategoryStruct.comp (Y := CommRingCat.of (Away 𝒜 (↑i₀ : A)))
      (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i₀ : A)))) (CommRingCat.ofHom φ'')) =
  Spec.map (Spec.preimage i₂)
Tactic: conv_rhs => rw [← Spec.map_preimage i₂]
-- 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
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A))) ≫ Spec.preimage φ
i₀ : ↥x
φ' : 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 𝒜 ⋯ ⋯)
⊢ Spec.map
      (CategoryStruct.comp (Y := CommRingCat.of (Away 𝒜 (↑i₀ : A)))
        (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i₀ : A)))) (CommRingCat.ofHom φ'')) =
    Spec.map (Spec.preimage i₂)
have refine_2 : CategoryStruct.comp (Y := CommRingCat.of (Away 𝒜 (↑i₀ : A)))
    (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i₀ : A)))) (CommRingCat.ofHom φ'') =
  Spec.preimage i₂
Tactic: congr 1
-- 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
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A))) ≫ Spec.preimage φ
i₀ : ↥x
φ' : 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 𝒜 ⋯ ⋯)
⊢ CategoryStruct.comp (Y := CommRingCat.of (Away 𝒜 (↑i₀ : A)))
      (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i₀ : A)))) (CommRingCat.ofHom φ'') =
    Spec.preimage i₂
have refine_2 : ∀ (x_1 : (↑(CommRingCat.of ↥(𝒜 0)) : Type u_2)),
  Eq (α := (↑(CommRingCat.of O) : Type u_2))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y := CommRingCat.of (Away 𝒜 (↑i₀ : A)))
              (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i₀ : A)))) (CommRingCat.ofHom φ'')) :
          (a : (↑(CommRingCat.of ↥(𝒜 0)) : Type u_2)) → (↑(CommRingCat.of O) : Type u_2))
        x_1 :
      (↑(CommRingCat.of O) : Type u_2))
    ((CommRingCat.Hom.hom (Spec.preimage i₂) :
          (a : (↑(CommRingCat.of ↥(𝒜 0)) : Type u_2)) → (↑(CommRingCat.of O) : Type u_2))
        x_1 :
      (↑(CommRingCat.of O) : Type u_2))
Tactic: ext x
-- 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)
    ((φ'.comp (awayMap 𝒜 ⋯ ⋯) : (a : HomogeneousLocalization 𝒜 (Submonoid.powers (↑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 : (↑(CommRingCat.of ↥(𝒜 0)) : Type u_2)) → (↑(CommRingCat.of O) : Type u_2))
            x :
          (↑(CommRingCat.of O) : Type u_2)) :
      K)
have refine_2 : Eq (α := K)
  ((φ' : (a : Away 𝒜 ((↑i : A) * (↑i₀ : A))) → K)
      ((awayMap 𝒜 sorry sorry : (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)
Tactic: simp only [RingHom.coe_comp, Function.comp_apply]