mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
i : ℕ
a : ↥(𝒜 i)
b : A
hb : b ∈ 𝒜 i
hb' : b ∉ (↑x).asHomogeneousIdeal
⊢ 1 ≤ m

Tactic:
by lia

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

Goal state before:
pp: case surj.refine_2
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
i : ℕ
a : ↥(𝒜 i)
b : A
hb : b ∈ 𝒜 i
hb' : b ∉ (↑x).asHomogeneousIdeal
⊢ HomogeneousLocalization.val
      (HomogeneousLocalization.mk { deg := i, num := a, den := ⟨b, hb⟩, den_mem := hb' } *
        (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))
          ↑(HomogeneousLocalization.mk { deg := i * m, num := ⟨↑a * b ^ (m - 1), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ },
                ⟨HomogeneousLocalization.mk { deg := i * m, num := ⟨b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ },
                  ⋯⟩).2) =
    HomogeneousLocalization.val
      ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))
        (HomogeneousLocalization.mk { deg := i * m, num := ⟨↑a * b ^ (m - 1), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ },
            ⟨HomogeneousLocalization.mk { deg := i * m, num := ⟨b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }, ⋯⟩).1)

Tactic:
·

Goal state after:
case surj.refine_2
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
i : ℕ
a : ↥(𝒜 i)
b : A
hb : b ∈ 𝒜 i
hb' : b ∉ (↑x).asHomogeneousIdeal
⊢ HomogeneousLocalization.val
      (HomogeneousLocalization.mk { deg := i, num := a, den := ⟨b, hb⟩, den_mem := hb' } *
        (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))
          ↑(HomogeneousLocalization.mk { deg := i * m, num := ⟨↑a * b ^ (m - 1), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ },
                ⟨HomogeneousLocalization.mk { deg := i * m, num := ⟨b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ },
                  ⋯⟩).2) =
    HomogeneousLocalization.val
      ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))
        (HomogeneousLocalization.mk { deg := i * m, num := ⟨↑a * b ^ (m - 1), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ },
            ⟨HomogeneousLocalization.mk { deg := i * m, num := ⟨b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }, ⋯⟩).1)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case exists_of_eq
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := ⋯
⊢ ∀ {x_1 y : A⁰_ f},
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) x_1 =
        (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) y →
      ∃ c, ↑c * x_1 = ↑c * y

Tactic:
·

Goal state after:
case exists_of_eq
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := ⋯
⊢ ∀ {x_1 y : A⁰_ f},
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) x_1 =
        (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) y →
      ∃ c, ↑c * x_1 = ↑c * y
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case pos
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : (f * g) ^ j = 0
⊢ ∃ a_1,
    (Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯) a_1 =
      HomogeneousLocalization.mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x_1 ↦ x ^ x_1) j, hb'⟩, den_mem := ⋯ }

pp: case neg
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ ∃ a_1,
    (Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯) a_1 =
      HomogeneousLocalization.mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x_1 ↦ x ^ x_1) j, hb'⟩, den_mem := ⋯ }

Tactic:
·

Goal state after:
case pos
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : (f * g) ^ j = 0
⊢ ∃ a_1,
    (Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯) a_1 =
      HomogeneousLocalization.mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x_1 ↦ x ^ x_1) j, hb'⟩, den_mem := ⋯ }
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case hxj
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 (j * (d + e))

pp: case hx
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ (fun x_1 ↦ x ^ x_1) j ≠ 0

Tactic:
·

Goal state after:
case hxj
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 (j * (d + e))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case hxj.convert_8
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ SetLike.GradedMonoid 𝒜

pp: case hxj.convert_12
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ x ∈ 𝒜 (d + e)

Tactic:
·

Goal state after:
case hxj.convert_8
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ SetLike.GradedMonoid 𝒜
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case hxj.convert_12
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ x ∈ 𝒜 (d + e)

Tactic:
·

Goal state after:
case hxj.convert_12
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ x ∈ 𝒜 (d + e)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case hx
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ (fun x_1 ↦ x ^ x_1) j ≠ 0

Tactic:
·

Goal state after:
case hx
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ (fun x_1 ↦ x ^ x_1) j ≠ 0
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case e'_4.zero
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
hf : f ∈ 𝒜 0
hd : 0 < 0
this : n = j * (0 + e)
⊢ j * (0 * (e + 1)) = j * (0 + e) + (j * (0 - 1)) • e

pp: case e'_4.succ
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n✝ : ℕ
hf : f ∈ 𝒜 (n✝ + 1)
hd : 0 < n✝ + 1
this : n = j * (n✝ + 1 + e)
⊢ j * ((n✝ + 1) * (e + 1)) = j * (n✝ + 1 + e) + (j * (n✝ + 1 - 1)) • e

Tactic:
·

Goal state after:
case e'_4.zero
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
hf : f ∈ 𝒜 0
hd : 0 < 0
this : n = j * (0 + e)
⊢ j * (0 * (e + 1)) = j * (0 + e) + (j * (0 - 1)) • e
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case e'_4.succ
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n✝ : ℕ
hf : f ∈ 𝒜 (n✝ + 1)
hd : 0 < n✝ + 1
this : n = j * (n✝ + 1 + e)
⊢ j * ((n✝ + 1) * (e + 1)) = j * (n✝ + 1 + e) + (j * (n✝ + 1 - 1)) • e

Tactic:
·

Goal state after:
case e'_4.succ
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n✝ : ℕ
hf : f ∈ 𝒜 (n✝ + 1)
hd : 0 < n✝ + 1
this : n = j * (n✝ + 1 + e)
⊢ j * ((n✝ + 1) * (e + 1)) = j * (n✝ + 1 + e) + (j * (n✝ + 1 - 1)) • e
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)), num := ⟨a * g ^ (j * (d - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩, den_mem := ⋯ }
⊢ g ^ (j * d) ∈ 𝒜 (j * (d * e))

Tactic:
convert SetLike.pow_mem_graded _ hg

Goal state after:
case e'_4
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)), num := ⟨a * g ^ (j * (d - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩, den_mem := ⋯ }
⊢ j * (d * e) = (j * d) • e
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case h.zero
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
hf : f ∈ 𝒜 0
hd : 0 < 0
this : n = j * (0 + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (0 * (e + 1)), num := ⟨a * g ^ (j * (0 - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (0 * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * 0), ⋯⟩, den_mem := ⋯ }
⊢ x ^ j * (a * g ^ (j * (0 - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * 0))) =
    x ^ (j * (e + 1)) * x ^ (j * 0) * a

pp: case h.succ
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n✝ : ℕ
hf : f ∈ 𝒜 (n✝ + 1)
hd : 0 < n✝ + 1
this : n = j * (n✝ + 1 + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * ((n✝ + 1) * (e + 1)), num := ⟨a * g ^ (j * (n✝ + 1 - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩,
    den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * ((n✝ + 1) * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * (n✝ + 1)), ⋯⟩, den_mem := ⋯ }
⊢ x ^ j * (a * g ^ (j * (n✝ + 1 - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * (n✝ + 1)))) =
    x ^ (j * (e + 1)) * x ^ (j * (n✝ + 1)) * a

Tactic:
·

Goal state after:
case h.zero
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
hf : f ∈ 𝒜 0
hd : 0 < 0
this : n = j * (0 + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (0 * (e + 1)), num := ⟨a * g ^ (j * (0 - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (0 * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * 0), ⋯⟩, den_mem := ⋯ }
⊢ x ^ j * (a * g ^ (j * (0 - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * 0))) =
    x ^ (j * (e + 1)) * x ^ (j * 0) * a
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case h.succ
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n✝ : ℕ
hf : f ∈ 𝒜 (n✝ + 1)
hd : 0 < n✝ + 1
this : n = j * (n✝ + 1 + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * ((n✝ + 1) * (e + 1)), num := ⟨a * g ^ (j * (n✝ + 1 - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩,
    den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * ((n✝ + 1) * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * (n✝ + 1)), ⋯⟩, den_mem := ⋯ }
⊢ x ^ j * (a * g ^ (j * (n✝ + 1 - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * (n✝ + 1)))) =
    x ^ (j * (e + 1)) * x ^ (j * (n✝ + 1)) * a

Tactic:
·

Goal state after:
case h.succ
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n✝ : ℕ
hf : f ∈ 𝒜 (n✝ + 1)
hd : 0 < n✝ + 1
this : n = j * (n✝ + 1 + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * ((n✝ + 1) * (e + 1)), num := ⟨a * g ^ (j * (n✝ + 1 - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩,
    den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * ((n✝ + 1) * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * (n✝ + 1)), ⋯⟩, den_mem := ⋯ }
⊢ x ^ j * (a * g ^ (j * (n✝ + 1 - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * (n✝ + 1)))) =
    x ^ (j * (e + 1)) * x ^ (j * (n✝ + 1)) * a
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case h.succ
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n✝ : ℕ
hf : f ∈ 𝒜 (n✝ + 1)
hd : 0 < n✝ + 1
this : n = j * (n✝ + 1 + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * ((n✝ + 1) * (e + 1)), num := ⟨a * g ^ (j * (n✝ + 1 - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩,
    den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * ((n✝ + 1) * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * (n✝ + 1)), ⋯⟩, den_mem := ⋯ }
⊢ x ^ j * (a * g ^ (j * (n✝ + 1 - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * (n✝ + 1)))) =
    x ^ (j * (e + 1)) * x ^ (j * (n✝ + 1)) * a

Tactic:
simp only [hx, add_tsub_cancel_right]
    ring

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h.refine_2
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
a : ToType ({ obj := M.presheaf, property := ⋯ }.obj.obj (op V))
ha : ∀ (i : ι), (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) a = f ^ K • t i
⊢ ∀ (i : ι),
    (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) a) =
      (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) (f ^ (N + K) • s)

Tactic:
·

Goal state after:
case h.refine_2
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
a : ToType ({ obj := M.presheaf, property := ⋯ }.obj.obj (op V))
ha : ∀ (i : ι), (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) a = f ^ K • t i
⊢ ∀ (i : ι),
    (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) a) =
      (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) (f ^ (N + K) • s)
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y Y' S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X},
    IsPullback f' g' g f → Existence g → Existence g'

Tactic:
intro Y' X X' Y Y'_to_Y f X'_to_X f' hP hf commSq

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
⊢ ⋯.HasLift
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case h₀
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f := ⋯
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
⊢ (Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ ⋯) ≫ X'_to_X = commSq.i₁ ≫ X'_to_X

pp: case h₁
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f := ⋯
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
⊢ (Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ ⋯) ≫ f' = commSq.i₁ ≫ f'

Tactic:
·

Goal state after:
case h₀
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f := ⋯
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
⊢ (Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ ⋯) ≫ X'_to_X = commSq.i₁ ≫ X'_to_X
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case h₁
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f := ⋯
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
⊢ (Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ ⋯) ≫ f' = commSq.i₁ ≫ f'

Tactic:
·

Goal state after:
case h₁
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f := ⋯
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
⊢ (Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ ⋯) ≫ f' = commSq.i₁ ≫ f'