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
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 𝒜 ⋯ ⋯)
refine_2 :
  Spec.map
      (CategoryStruct.comp (Y := CommRingCat.of (Away 𝒜 (↑i₀ : A)))
        (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i₀ : A)))) (CommRingCat.ofHom φ'')) =
    i₂
⊢ 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₂

Tactic:
simp only [Category.assoc, Proj.awayι_toSpecZero, ← Spec.map_comp]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Proj.awayι_toSpecZero, AlgebraicGeometry.Spec.map_comp
-- 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
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 𝒜 ⋯ ⋯)
rw : Spec.map (Spec.preimage i₂)
| i₂

Tactic:
rw [← Spec.map_preimage i₂]

Premises used: AlgebraicGeometry.Spec.map_preimage
-- 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
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 𝒜 ⋯ ⋯)
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₂)
⊢ Spec.map
      (CategoryStruct.comp (Y := CommRingCat.of (Away 𝒜 (↑i₀ : A)))
        (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i₀ : A)))) (CommRingCat.ofHom φ'')) =
    i₂

Tactic:
conv_rhs => rw [← Spec.map_preimage i₂]

Premises used: AlgebraicGeometry.Spec.map_preimage
-- 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
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 𝒜 ⋯ ⋯)
refine_2 :
  CategoryStruct.comp (Y := CommRingCat.of (Away 𝒜 (↑i₀ : A)))
      (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i₀ : A)))) (CommRingCat.ofHom φ'') =
    Spec.preimage i₂
⊢ 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:
congr 1
-- 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
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 𝒜 ⋯ ⋯)
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))
⊢ CategoryStruct.comp (Y := CommRingCat.of (Away 𝒜 (↑i₀ : A)))
      (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i₀ : A)))) (CommRingCat.ofHom φ'') =
    Spec.preimage i₂

Tactic:
ext x
-- 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
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)
    ((algebraMap O K : (a : O) → K)
        ((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 :
          (↑(CommRingCat.of O) : Type u_2)) :
      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)

Tactic:
(DFunLike.congr_fun hφ'' (fromZeroRingHom 𝒜 _ _)).trans ?_

Premises used: DFunLike.congr_fun, HomogeneousLocalization.fromZeroRingHom, Classical.choose, DFunLike.coe, Eq.trans
-- 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
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)
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)
⊢ 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)

Tactic:
rw [awayMap_fromZeroRingHom, ← awayMap_fromZeroRingHom 𝒜 (hxd i₀ i₀.2) rfl,
      ← RingHom.comp_apply, hφ]

Premises used: HomogeneousLocalization.awayMap_fromZeroRingHom, RingHom.comp_apply, Subtype.val, rfl, Subtype.property
-- 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
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)
    ((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:
congr($(H.symm) x)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, Eq.symm, DFunLike.coe
-- 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
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)
    ((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:
exact congr($(H.symm) x)
-- 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
rw : (ValuativeCriterion.Existence ⊓ @QuasiCompact) (X := Proj 𝒜) (toSpecZero 𝒜)
⊢ UniversallyClosed (X := Proj 𝒜) (toSpecZero 𝒜)

Tactic:
rw [UniversallyClosed.eq_valuativeCriterion]

Premises used: AlgebraicGeometry.UniversallyClosed.eq_valuativeCriterion
-- 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:
⟨valuativeCriterion_existence 𝒜, inferInstance⟩

Premises used: AlgebraicGeometry.Proj.valuativeCriterion_existence, inferInstance, And.intro