mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
U : Opens (ProjectiveSpectrum 𝒜)
V : Opens (ProjectiveSpectrum ℬ)
hUV : V.carrier ⊆ ⇑(ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier
x y : ↑((structureSheaf 𝒜).obj.obj (Opposite.op U))
⊢ ⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑(x + y), ⋯⟩ =
    ⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑x, ⋯⟩ +
      ⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑y, ⋯⟩

Tactic:
ext

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
U : Opens (ProjectiveSpectrum 𝒜)
V : Opens (ProjectiveSpectrum ℬ)
hUV : V.carrier ⊆ ⇑(ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier
x y : ↑((structureSheaf 𝒜).obj.obj (Opposite.op U))
x✝ : ↥(Opposite.unop (Opposite.op V))
⊢ val (↑⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑(x + y), ⋯⟩ x✝) =
    val
      (↑(⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑x, ⋯⟩ +
            ⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑y, ⋯⟩)
        x✝)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
⊢ (HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }).val =
    HomogeneousLocalization.val 0

Tactic:
HomogeneousLocalization.val_mk,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
⊢ Localization.mk ↑{ deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    HomogeneousLocalization.val 0
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
i : ℕ
s : A
hs : s ∈ 𝒜 i
n : ℕ
x : A
hx : x ∈ 𝒜 (n • i)
p : ↥(Opposite.unop (Opposite.op (basicOpen ℬ (f s))))
⊢ HomogeneousLocalization.mk
      ((fun x ↦ { deg := x.deg, num := ⟨f ↑x.num, ⋯⟩, den := ⟨f ↑x.den, ⋯⟩, den_mem := ⋯ })
        ((fun x ↦
            { deg := x.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x.num, ⋯⟩, den := ⟨(GradedRingHom.id 𝒜) ↑x.den, ⋯⟩,
              den_mem := ⋯ })
          { deg := n • i, num := ⟨x, hx⟩, den := ⟨s ^ n, ⋯⟩, den_mem := ⋯ })) =
    HomogeneousLocalization.mk
      ((fun x ↦
          { deg := x.deg, num := ⟨(GradedRingHom.id ℬ) ↑x.num, ⋯⟩, den := ⟨(GradedRingHom.id ℬ) ↑x.den, ⋯⟩,
            den_mem := ⋯ })
        { deg := n • i, num := ⟨f x, ⋯⟩, den := ⟨f s ^ n, ⋯⟩, den_mem := ⋯ })

Tactic:
ext

Goal state after:
A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
i : ℕ
s : A
hs : s ∈ 𝒜 i
n : ℕ
x : A
hx : x ∈ 𝒜 (n • i)
p : ↥(Opposite.unop (Opposite.op (basicOpen ℬ (f s))))
⊢ (HomogeneousLocalization.mk
        ((fun x ↦ { deg := x.deg, num := ⟨f ↑x.num, ⋯⟩, den := ⟨f ↑x.den, ⋯⟩, den_mem := ⋯ })
          ((fun x ↦
              { deg := x.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x.num, ⋯⟩, den := ⟨(GradedRingHom.id 𝒜) ↑x.den, ⋯⟩,
                den_mem := ⋯ })
            { deg := n • i, num := ⟨x, hx⟩, den := ⟨s ^ n, ⋯⟩, den_mem := ⋯ }))).val =
    (HomogeneousLocalization.mk
        ((fun x ↦
            { deg := x.deg, num := ⟨(GradedRingHom.id ℬ) ↑x.num, ⋯⟩, den := ⟨(GradedRingHom.id ℬ) ↑x.den, ⋯⟩,
              den_mem := ⋯ })
          { deg := n • i, num := ⟨f x, ⋯⟩, den := ⟨f s ^ n, ⋯⟩, den_mem := ⋯ })).val
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HomogeneousLocalization.mk { deg := m • n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ } *
    HomogeneousLocalization.mk
      { deg := m • (i - n), num := ⟨(proj 𝒜 (i - n)) x ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩, den_mem := ⋯ }
h : n ≤ i
⊢ (HomogeneousLocalization.mk
        { deg := m * i, num := ⟨(a * ↑(((decompose 𝒜) x) (i - n))) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }).val =
    (HomogeneousLocalization.mk { deg := m * n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ } *
        HomogeneousLocalization.mk
          { deg := m * (i - n), num := ⟨↑(((decompose 𝒜) x) (i - n)) ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩,
            den_mem := ⋯ }).val

Tactic:
HomogeneousLocalization.val_mk,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HomogeneousLocalization.mk { deg := m • n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ } *
    HomogeneousLocalization.mk
      { deg := m • (i - n), num := ⟨(proj 𝒜 (i - n)) x ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩, den_mem := ⋯ }
h : n ≤ i
⊢ Localization.mk
      ↑{ deg := m * i, num := ⟨(a * ↑(((decompose 𝒜) x) (i - n))) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * i, num := ⟨(a * ↑(((decompose 𝒜) x) (i - n))) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    (HomogeneousLocalization.mk { deg := m * n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ } *
        HomogeneousLocalization.mk
          { deg := m * (i - n), num := ⟨↑(((decompose 𝒜) x) (i - n)) ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩,
            den_mem := ⋯ }).val
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HomogeneousLocalization.mk { deg := m • n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ } *
    HomogeneousLocalization.mk
      { deg := m • (i - n), num := ⟨(proj 𝒜 (i - n)) x ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩, den_mem := ⋯ }
h : n ≤ i
⊢ Localization.mk
      ↑{ deg := m * i, num := ⟨(a * ↑(((decompose 𝒜) x) (i - n))) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * i, num := ⟨(a * ↑(((decompose 𝒜) x) (i - n))) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    (HomogeneousLocalization.mk
          { deg := m * n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ }).val *
      (HomogeneousLocalization.mk
          { deg := m * (i - n), num := ⟨↑(((decompose 𝒜) x) (i - n)) ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩,
            den_mem := ⋯ }).val

Tactic:
HomogeneousLocalization.val_mk,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HomogeneousLocalization.mk { deg := m • n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ } *
    HomogeneousLocalization.mk
      { deg := m • (i - n), num := ⟨(proj 𝒜 (i - n)) x ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩, den_mem := ⋯ }
h : n ≤ i
⊢ Localization.mk
      ↑{ deg := m * i, num := ⟨(a * ↑(((decompose 𝒜) x) (i - n))) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * i, num := ⟨(a * ↑(((decompose 𝒜) x) (i - n))) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    Localization.mk ↑{ deg := m * n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ }.num
        ⟨↑{ deg := m * n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ }.den, ⋯⟩ *
      (HomogeneousLocalization.mk
          { deg := m * (i - n), num := ⟨↑(((decompose 𝒜) x) (i - n)) ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩,
            den_mem := ⋯ }).val
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case hy.refine_3
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
j : ι'
⊢ Away.mk 𝒜 hf (dv j) (∏ i, v i ^ Pi.single j d i) ⋯ = isLocalizationElem hf ⋯

Tactic:
ext

Goal state after:
case hy.refine_3
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
j : ι'
⊢ val (Away.mk 𝒜 hf (dv j) (∏ i, v i ^ Pi.single j d i) ⋯) = val (isLocalizationElem hf ⋯)
Module: Mathlib.RingTheory.LocalRing.LocalSubring

Goal state before:
pp: case e_6
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) x s) =
    (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) y t)
H : ∀ (x : ↥P.primeCompl), ↑x ≠ 0
this : ↑x = ↑y * (↑↑t)⁻¹ * ↑↑s
⊢ ↑t * x = ↑s * y

Tactic:
ext

Goal state after:
case e_6
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) x s) =
    (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) y t)
H : ∀ (x : ↥P.primeCompl), ↑x ≠ 0
this : ↑x = ↑y * (↑↑t)⁻¹ * ↑↑s
⊢ ↑(↑t * x) = ↑(↑s * y)
Module: Mathlib.RingTheory.Valuation.Integral

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
this : Nontrivial O
⊢ IsIntegral O x ↔ v x ≤ 1

Tactic:
constructor

Goal state after:
case mp
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
this : Nontrivial O
⊢ IsIntegral O x → v x ≤ 1

case mpr
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
this : Nontrivial O
⊢ v x ≤ 1 → IsIntegral O x
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
⊢ Algebra.FiniteType (↥(𝒜 0)) (Away 𝒜 f)

Tactic:
constructor

Goal state after:
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
⊢ ⊤.FG
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
hs' : ∀ i ∈ s, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n
dx : ↥s → ℕ
hdx : ∀ (x : ↥s), dx x ≠ 0
hxd : ∀ (x : ↥s), ↑x ∈ 𝒜 (dx x)
hd : d = 0
f' : Away 𝒜 f := Away.mk 𝒜 hf 1 1 ⋯
a : ℕ
hai : ∑ i, 0 i • dx i = a • d
hai' : ∀ (i : ↥s), 0 i ≤ d
⊢ Away.mk 𝒜 hf a 1 ⋯ = f' ^ a

Tactic:
ext

Goal state after:
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
hs' : ∀ i ∈ s, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n
dx : ↥s → ℕ
hdx : ∀ (x : ↥s), dx x ≠ 0
hxd : ∀ (x : ↥s), ↑x ∈ 𝒜 (dx x)
hd : d = 0
f' : Away 𝒜 f := ⋯
a : ℕ
hai : ∑ i, 0 i • dx i = a • d
hai' : ∀ (i : ↥s), 0 i ≤ d
⊢ val (Away.mk 𝒜 hf a 1 ⋯) = val (f' ^ a)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
hs' : ∀ i ∈ s, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n
dx : ↥s → ℕ
hdx : ∀ (x : ↥s), dx x ≠ 0
hxd : ∀ (x : ↥s), ↑x ∈ 𝒜 (dx x)
hd : d > 0
b : ℕ := ∑ i, dx i
s' : Set (Fin (b + 1) × (↥s → Fin (d + 1))) := {ai | ∑ i, ↑(ai.2 i) * dx i = ↑ai.1 * d}
ai : ↑s'
⊢ ∏ i, ↑i ^ ↑((↑ai).2 i) ∈ 𝒜 (↑(↑ai).1 • d)

Tactic:
by convert! SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i; exact ai.2.symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
⊢ (HomogeneousLocalization.mk { deg := m * n, num := ⟨(proj 𝒜 n) y ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }).val =
    HomogeneousLocalization.val 0

Tactic:
HomogeneousLocalization.val_mk,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
⊢ Localization.mk ↑{ deg := m * n, num := ⟨(proj 𝒜 n) y ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * n, num := ⟨(proj 𝒜 n) y ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    HomogeneousLocalization.val 0
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
⊢ (HomogeneousLocalization.mk { deg := m * n, num := ⟨(proj 𝒜 n) x ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }).val =
    HomogeneousLocalization.val 0

Tactic:
HomogeneousLocalization.val_mk,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
⊢ Localization.mk ↑{ deg := m * n, num := ⟨(proj 𝒜 n) x ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * n, num := ⟨(proj 𝒜 n) x ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    HomogeneousLocalization.val 0
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
⊢ ⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) 1, ⋯⟩ = 1

Tactic:
ext

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ HomogeneousLocalization.val (↑⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) 1, ⋯⟩ x✝) =
    HomogeneousLocalization.val (↑1 x✝)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x✝¹ x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) (x✝¹ * x✝), ⋯⟩ =
    ⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) x✝¹, ⋯⟩ * ⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) x✝, ⋯⟩

Tactic:
ext

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x✝² x✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ HomogeneousLocalization.val (↑⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) (x✝² * x✝¹), ⋯⟩ x✝) =
    HomogeneousLocalization.val
      (↑(⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) x✝², ⋯⟩ * ⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) x✝¹, ⋯⟩)
        x✝)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
⊢ ⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) 0, ⋯⟩ = 0

Tactic:
ext

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ HomogeneousLocalization.val (↑⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) 0, ⋯⟩ x✝) =
    HomogeneousLocalization.val (↑0 x✝)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x✝¹ x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) (x✝¹ + x✝), ⋯⟩ =
    ⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) x✝¹, ⋯⟩ + ⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) x✝, ⋯⟩

Tactic:
ext

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x✝² x✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ HomogeneousLocalization.val (↑⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) (x✝² + x✝¹), ⋯⟩ x✝) =
    HomogeneousLocalization.val
      (↑(⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) x✝², ⋯⟩ + ⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) x✝¹, ⋯⟩)
        x✝)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (ConcreteCategory.hom (toSpec 𝒜 f).base) x =
    PrimeSpectrum.comap (mapId 𝒜 ⋯) (closedPoint (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))

Tactic:
by
  change PrimeSpectrum.comap (awayToΓ 𝒜 f ≫ (Proj| pbo f).presheaf.Γgerm x).hom
        (IsLocalRing.closedPoint ((Proj| pbo f).presheaf.stalk x)) = _
  rw [awayToΓ_ΓToStalk, CommRingCat.hom_comp, PrimeSpectrum.comap_comp]
  exact congr(PrimeSpectrum.comap _ $(@IsLocalRing.comap_closedPoint
    (HomogeneousLocalization.AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal) _ _
    ((Proj| pbo f).presheaf.stalk x) _ _ _ (isLocalHom_of_isIso _)))

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ¬IsUnit
        (HomogeneousLocalization.mk
            { deg := z.deg, num := ⟨(GradedRingHom.id 𝒜) ↑z.num, ⋯⟩, den := ⟨(GradedRingHom.id 𝒜) ↑z.den, ⋯⟩,
              den_mem := ⋯ }).val ↔
    ↑z.num ∈ (↑x).asHomogeneousIdeal

Tactic:
HomogeneousLocalization.val_mk,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ¬IsUnit
        (Localization.mk
          ↑{ deg := z.deg, num := ⟨(GradedRingHom.id 𝒜) ↑z.num, ⋯⟩, den := ⟨(GradedRingHom.id 𝒜) ↑z.den, ⋯⟩,
                den_mem := ⋯ }.num
          ⟨↑{ deg := z.deg, num := ⟨(GradedRingHom.id 𝒜) ↑z.num, ⋯⟩, den := ⟨(GradedRingHom.id 𝒜) ↑z.den, ⋯⟩,
                  den_mem := ⋯ }.den,
            ⋯⟩) ↔
    ↑z.num ∈ (↑x).asHomogeneousIdeal