mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case e'_3
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ Localization.mk (↑c2.num * ↑c4.num) ⟨↑c2.den * ↑c4.den, ⋯⟩ =
    Localization.mk (↑c2.num * ↑c4.num) (⟨↑c2.den, ⋯⟩ * ⟨↑c4.den, ⋯⟩)

Tactic:
]

Goal state after:
case e'_3
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ Localization.mk (↑c2.num * ↑c4.num) ⟨↑c2.den * ↑c4.den, ⋯⟩ =
    Localization.mk (↑c2.num * ↑c4.num) (⟨↑c2.den, ⋯⟩ * ⟨↑c4.den, ⋯⟩)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 + y2).num ⟨↑(y1 + y2).den, ⋯⟩ =
    Localization.mk (↑⟨↑y1.den, ⋯⟩ * ↑y2.num + ↑⟨↑y2.den, ⋯⟩ * ↑y1.num) (⟨↑y1.den, ⋯⟩ * ⟨↑y2.den, ⋯⟩)

Tactic:
]

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 + y2).num ⟨↑(y1 + y2).den, ⋯⟩ =
    Localization.mk (↑⟨↑y1.den, ⋯⟩ * ↑y2.num + ↑⟨↑y2.den, ⋯⟩ * ↑y1.num) (⟨↑y1.den, ⋯⟩ * ⟨↑y2.den, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst✝ : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ ((restrictFunctor f).obj M).presheaf.germ U x hxU ≫
      (𝟙 (restrictFunctor f ⋙ toPresheaf X ⋙ TopCat.Presheaf.stalkFunctor Ab x)).app M =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU

Tactic:
]

Goal state after:
X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst✝ : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ ((restrictFunctor f).obj M).presheaf.germ U x hxU ≫
      (𝟙 (restrictFunctor f ⋙ toPresheaf X ⋙ TopCat.Presheaf.stalkFunctor Ab x)).app M =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 * y2).num ⟨↑(y1 * y2).den, ⋯⟩ = Localization.mk (↑y1.num * ↑y2.num) (⟨↑y1.den, ⋯⟩ * ⟨↑y2.den, ⋯⟩)

Tactic:
]

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 * y2).num ⟨↑(y1 * y2).den, ⋯⟩ = Localization.mk (↑y1.num * ↑y2.num) (⟨↑y1.den, ⋯⟩ * ⟨↑y2.den, ⋯⟩)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
y1 y2 : HomogeneousLocalization 𝒜 x
⊢ (y1 - y2).val = (y1 + -y2).val

Tactic:
]

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
y1 y2 : HomogeneousLocalization 𝒜 x
⊢ (y1 - y2).val = (y1 + -y2).val
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case refine_1.refine_1
X Y Z T : Scheme
M✝ N K : X.Modules
φ✝ : M✝ ⟶ N
U✝ V : X.Opens
R S : CommRingCat
φ : R ⟶ S
M : Sheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))
U : (TopologicalSpace.Opens ↥(Spec R))ᵒᵖ
⊢ (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ))).comp (CommRingCat.Hom.hom (ΓSpecIso R).inv) =
    (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ))).comp (CommRingCat.Hom.hom (ΓSpecIso R).inv)

Tactic:
]

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

Goal state before:
pp: case mp
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
h :
  HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
⊢ ∃ x ∈ {s | s ∈ q.asIdeal},
    (algebraMap (A⁰_ f) (Localization.Away f)) x = Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩

Tactic:
]

Goal state after:
case mp
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
h :
  HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
⊢ ∃ x ∈ {s | s ∈ q.asIdeal},
    (algebraMap (A⁰_ f) (Localization.Away f)) x = Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
y : NumDenSameDeg 𝒜 x
n : ℕ
⊢ Localization.mk ↑(y ^ n).num ⟨↑(y ^ n).den, ⋯⟩ = Localization.mk (↑y.num ^ n) (⟨↑y.den, ⋯⟩ ^ n)

Tactic:
]

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
y : NumDenSameDeg 𝒜 x
n : ℕ
⊢ Localization.mk ↑(y ^ n).num ⟨↑(y ^ n).den, ⋯⟩ = Localization.mk (↑y.num ^ n) (⟨↑y.den, ⋯⟩ ^ n)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case mpr
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
h :
  ∃ x ∈ {s | s ∈ q.asIdeal},
    (algebraMap (A⁰_ f) (Localization.Away f)) x = Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩
⊢ HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal

Tactic:
]

Goal state after:
case mpr
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
h :
  ∃ x ∈ {s | s ∈ q.asIdeal},
    (algebraMap (A⁰_ f) (Localization.Away f)) x = Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩
⊢ HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
x : A⁰_ f
hx : (algebraMap (A⁰_ f) (Localization.Away f)) x = Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩
h : x ∈ q.asIdeal
⊢ Localization.mk ↑{ deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    HomogeneousLocalization.val x

Tactic:
]

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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
x : A⁰_ f
hx : (algebraMap (A⁰_ f) (Localization.Away f)) x = Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩
h : x ∈ q.asIdeal
⊢ Localization.mk ↑{ deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    HomogeneousLocalization.val x
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝¹ : CommRing A
inst✝ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
f : HomogeneousLocalization 𝒜 x
⊢ IsLocalization.mk' (at x) (f.den * f.num) ⟨f.den, ⋯⟩ = (algebraMap A (at x)) f.num

Tactic:
]

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝¹ : CommRing A
inst✝ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
f : HomogeneousLocalization 𝒜 x
⊢ IsLocalization.mk' (at x) (f.den * f.num) ⟨f.den, ⋯⟩ = (algebraMap A (at x)) f.num
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
x : A⁰_ f
hx : (algebraMap (A⁰_ f) (Localization.Away f)) x = Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩
h : x ∈ q.asIdeal
⊢ (algebraMap (A⁰_ f) (Localization.Away f)) x = HomogeneousLocalization.val x

Tactic:
]

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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
x : A⁰_ f
hx : (algebraMap (A⁰_ f) (Localization.Away f)) x = Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩
h : x ∈ q.asIdeal
⊢ (algebraMap (A⁰_ f) (Localization.Away f)) x = HomogeneousLocalization.val x
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
𝒜 : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq0 : ∃ c, ↑c * (↑f.num * b) = ↑c * ↑(⟨↑f.den, ⋯⟩ * s)
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)

Tactic:
]

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
𝒜 : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq0 : ∃ c, ↑c * (↑f.num * b) = ↑c * ↑(⟨↑f.den, ⋯⟩ * s)
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)
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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ f ^ n ∈ 𝒜 (n * m)

Tactic:
]

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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ f ^ n ∈ 𝒜 (n * m)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
𝒜 : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
c : ↥𝔭.primeCompl
hc : ↑c * (↑f.num * b) = ↑c * (↑f.den * ↑s)
this : ↑f.num ∉ 𝔭
⊢ Localization.mk ↑(f * { deg := f.deg, num := f.den, den := f.num, den_mem := this }).num
      ⟨↑(f * { deg := f.deg, num := f.den, den := f.num, den_mem := this }).den, ⋯⟩ =
    val 1

Tactic:
]

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
𝒜 : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
c : ↥𝔭.primeCompl
hc : ↑c * (↑f.num * b) = ↑c * (↑f.den * ↑s)
this : ↑f.num ∉ 𝔭
⊢ Localization.mk ↑(f * { deg := f.deg, num := f.den, den := f.num, den_mem := this }).num
      ⟨↑(f * { deg := f.deg, num := f.den, den := f.num, den_mem := this }).den, ⋯⟩ =
    val 1
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
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ (proj 𝒜 n) a ^ m ∈ 𝒜 (m • n)

Tactic:
]

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
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ (proj 𝒜 n) a ^ m ∈ 𝒜 (m • n)
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
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ f ^ n ∈ 𝒜 (n * m)

Tactic:
]

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
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ f ^ n ∈ 𝒜 (n * m)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case pos
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : f ^ k = 0
⊢ 0 = 0

Tactic:
]

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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
⊢ f ^ n ∈ 𝒜 (n * m)

Tactic:
]

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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
⊢ f ^ n ∈ 𝒜 (n * m)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case neg
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k + k) • m),
    (algebraMap A (at Submonoid.powers f)) x = (algebraMap A (at Submonoid.powers f)) (f ^ (k' - k) * num z)

Tactic:
]

Goal state after:
case neg
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k + k) • m),
    (algebraMap A (at Submonoid.powers f)) x = (algebraMap A (at Submonoid.powers f)) (f ^ (k' - k) * num z)
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
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
⊢ (HomogeneousLocalization.mk { deg := m * n, num := ⟨a, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ^ m ∈ q.asIdeal) =
    (HomogeneousLocalization.mk { deg := m * (n * m), num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ (n * m), ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal)

Tactic:
]

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
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
⊢ (HomogeneousLocalization.mk { deg := m * n, num := ⟨a, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ^ m ∈ q.asIdeal) =
    (HomogeneousLocalization.mk { deg := m * (n * m), num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ (n * m), ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case neg
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k) • m + deg z),
    (algebraMap A (at Submonoid.powers f)) x = (algebraMap A (at Submonoid.powers f)) (f ^ (k' - k) • num z)

Tactic:
]

Goal state after:
case neg
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k) • m + deg z),
    (algebraMap A (at Submonoid.powers f)) x = (algebraMap A (at Submonoid.powers f)) (f ^ (k' - k) • num z)
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
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = ↑z.den
this✝ : f ^ n ≠ 0
this : n • m = z.deg
⊢ ↑z.num ∈ 𝒜 z.deg

Tactic:
]

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
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = ↑z.den
this✝ : f ^ n ≠ 0
this : n • m = z.deg
⊢ ↑z.num ∈ 𝒜 z.deg
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ f ^ i ∈ 𝒜 (i * m)

Tactic:
]

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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ f ^ i ∈ 𝒜 (i * m)
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case refine_2
X✝ Y Z T : Scheme
M N K : X✝.Modules
φ : M ⟶ N
U✝ V✝ : X✝.Opens
X : Scheme
U V : X.Opens
f : V ⟶ U
this✝⁴ :
  (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥↑V) (Opens.grothendieckTopology ↑U.carrier)
this✝³ :
  Functor.IsDenseSubsite (Opens.grothendieckTopology ↥U) ((Opens.grothendieckTopology ↥X).over U)
    (Opens.overEquivalence U).inverse
this✝² : (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥V) (Opens.grothendieckTopology ↥↑U)
this✝¹ :
  ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
this✝ :
  (Opens.overEquivalence U).symm.functor.IsContinuous (Opens.grothendieckTopology ↥↑U)
    ((Opens.grothendieckTopology ↥X).over U)
this :
  (Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
W : (TopologicalSpace.Opens ↥V)ᵒᵖ
x : ↑(((Opens.sheafRestrict V).obj X.ringCatSheaf).obj.obj W)
⊢ (ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯))) x = (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x

Tactic:
]

Goal state after:
case refine_2
X✝ Y Z T : Scheme
M N K : X✝.Modules
φ : M ⟶ N
U✝ V✝ : X✝.Opens
X : Scheme
U V : X.Opens
f : V ⟶ U
this✝⁴ :
  (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥↑V) (Opens.grothendieckTopology ↑U.carrier)
this✝³ :
  Functor.IsDenseSubsite (Opens.grothendieckTopology ↥U) ((Opens.grothendieckTopology ↥X).over U)
    (Opens.overEquivalence U).inverse
this✝² : (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥V) (Opens.grothendieckTopology ↥↑U)
this✝¹ :
  ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
this✝ :
  (Opens.overEquivalence U).symm.functor.IsContinuous (Opens.grothendieckTopology ↥↑U)
    ((Opens.grothendieckTopology ↥X).over U)
this :
  (Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
W : (TopologicalSpace.Opens ↥V)ᵒᵖ
x : ↑(((Opens.sheafRestrict V).obj X.ringCatSheaf).obj.obj W)
⊢ (ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯))) x = (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) 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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ (proj 𝒜 i) b ^ m ∈ 𝒜 (m • i)

Tactic:
]

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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ (proj 𝒜 i) b ^ m ∈ 𝒜 (m • i)
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
⊢ (proj 𝒜 i) a ^ m ∈ 𝒜 (m • i)

Tactic:
]

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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
⊢ (proj 𝒜 i) a ^ m ∈ 𝒜 (m • i)