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

Goal state before:
pp: case refine_2.refine_1
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)
s : Finset ι' := {x | 0 < dv x}
this :
  Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai,
          ∃ (hai : ∑ i, ai i • (dv ∘ Subtype.val) i = a • d) (_ : ∀ (i : ↥s), ai i ≤ d),
            Away.mk 𝒜 hf a (∏ i, (v ∘ Subtype.val) i ^ ai i) ⋯ = x} =
    ⊤
a : ℕ
ai : ↥s → ℕ
hai : ∑ x ∈ s.attach, ai x • (dv ∘ Subtype.val) x = a • d
h : ∀ (i : ↥s), ai i ≤ d
⊢ ∑ i, (fun i ↦ if hi : i ∈ s then ai ⟨i, hi⟩ else 0) i • dv i = a • d

Tactic:
simpa using

Goal state after:
case refine_2.refine_1
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)
s : Finset ι' := {x | 0 < dv x}
this :
  Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai,
          ∃ (hai : ∑ i, ai i • (dv ∘ Subtype.val) i = a • d) (_ : ∀ (i : ↥s), ai i ≤ d),
            Away.mk 𝒜 hf a (∏ i, (v ∘ Subtype.val) i ^ ai i) ⋯ = x} =
    ⊤
a : ℕ
ai : ↥s → ℕ
hai : ∑ x ∈ s.attach, ai x • (dv ∘ Subtype.val) x = a • d
h : ∀ (i : ↥s), ai i ≤ d
⊢ (∑ x, if h : x ∈ s then ai ⟨x, ⋯⟩ * dv x else 0) = a * d
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case neg
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, ⋯⟩, 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 := ⟨0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal

Tactic:
simpa using

Goal state after:
case neg
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, ⋯⟩, 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 := ⟨0, ⋯⟩, 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
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
a : A
ha : a ∈ asIdeal f_deg hm q
j : ℕ
h : i = j
⊢ HomogeneousLocalization.mk
      { deg := m * i, num := ⟨(proj 𝒜 i) ↑(((decompose 𝒜) a) i) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
simpa using

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 : ℕ
a : A
ha : a ∈ asIdeal f_deg hm q
j : ℕ
h : i = j
⊢ HomogeneousLocalization.mk { deg := m * i, num := ⟨↑(((decompose 𝒜) a) i) ^ 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
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
a : A
ha : a ∈ asIdeal f_deg hm q
j : ℕ
h : ¬i = j
⊢ HomogeneousLocalization.mk
      { deg := m * j, num := ⟨(proj 𝒜 j) ↑(((decompose 𝒜) a) i) ^ m, ⋯⟩, den := ⟨f ^ j, ⋯⟩, den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
simpa using

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 : ℕ
a : A
ha : a ∈ asIdeal f_deg hm q
j : ℕ
h : ¬i = j
⊢ HomogeneousLocalization.mk { deg := m * j, num := ⟨0, ⋯⟩, den := ⟨f ^ j, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
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 : ℕ
ai : ↥s → ℕ
hai : ∑ i, ai i • dx i = a • d
hai' : ∀ (i : ↥s), ai i ≤ d
⊢ ∀ (x : ↥s), ai x = 0 x

Tactic:
simpa using

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 := Away.mk 𝒜 hf 1 1 ⋯
a : ℕ
ai : ↥s → ℕ
hai : ∑ i, ai i • dx i = a • d
hai' : ∀ (i : ↥s), ai i ≤ d
⊢ ∀ (a : A) (b : a ∈ s), ai ⟨a, b⟩ = 0
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : Algebra.IsIntegral ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
hRS : R.toSubring ≤ S.toSubring
| maximalIdeal ↥(ofPrime S.toSubring Q).toSubring

Tactic:
← IsLocalization.AtPrime.map_eq_maximalIdeal Q

Goal state after:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : Algebra.IsIntegral ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
hRS : R.toSubring ≤ S.toSubring
| Ideal.map (algebraMap ↥S.toSubring ↥(ofPrime S.toSubring Q).toSubring) Q
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case e'_4
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
⊢ ↑(((decompose 𝒜) y) n) ^ m = 0

Tactic:
decompose_of_mem_ne 𝒜 _ hn.symm,

Goal state after:
case e'_4
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
⊢ 0 ^ m = 0

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
⊢ y ∈ 𝒜 ny
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
this : IsUnit ((Subring.inclusion ⋯) ⟨x⁻¹, h⟩)
x' : ↥R.toLocalSubring.toSubring
hx' : ⟨x⁻¹, h⟩ * x' = 1
⊢ ↑x' = x

Tactic:
simpa using

Goal state after:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
this : IsUnit ((Subring.inclusion ⋯) ⟨x⁻¹, h⟩)
x' : ↥R.toLocalSubring.toSubring
hx' : ⟨x⁻¹, h⟩ * x' = 1
⊢ ↑x' = x
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
this✝ : Invertible x := invertibleOfNonzero hx0
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : R.toSubring < S.toSubring
p : Polynomial ↥R.toSubring
hp : p.leadingCoeff - 1 ∈ maximalIdeal ↥R.toSubring
hpx : (Polynomial.aeval ⅟x) p = 0
h : ¬IsUnit p.leadingCoeff
⊢ False

Tactic:
simpa using

Goal state after:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
this✝ : Invertible x := invertibleOfNonzero hx0
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : R.toSubring < S.toSubring
p : Polynomial ↥R.toSubring
hp : p.leadingCoeff - 1 ∈ maximalIdeal ↥R.toSubring
hpx : (Polynomial.aeval ⅟x) p = 0
h : ¬IsUnit p.leadingCoeff
⊢ False
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
this✝ : Invertible x := invertibleOfNonzero hx0
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : R.toSubring < S.toSubring
p : Polynomial ↥R.toSubring
hp : p.leadingCoeff - 1 ∈ maximalIdeal ↥R.toSubring
hpx : (Polynomial.aeval ⅟x) p = 0
H : IsUnit p.leadingCoeff
⊢ Polynomial.eval₂ (algebraMap (↥R.toSubring) K) x⁻¹ (Polynomial.C ↑H.unit⁻¹ * p) = 0

Tactic:
simpa using

Goal state after:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
this✝ : Invertible x := invertibleOfNonzero hx0
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : R.toSubring < S.toSubring
p : Polynomial ↥R.toSubring
hp : p.leadingCoeff - 1 ∈ maximalIdeal ↥R.toSubring
hpx : (Polynomial.aeval ⅟x) p = 0
H : IsUnit p.leadingCoeff
⊢ p = 0 ∨ Polynomial.eval₂ (algebraMap (↥R.toSubring) K) x⁻¹ p = 0
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: case refine_1.refine_1
K : Type u_3
inst✝ : Field K
A✝ : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A✝
H : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x ↦ ↑x)
a : K
ha : a ∈ ⨆ i, (↑i).toSubring
b : K
hb : b ∈ ⨆ i, (↑i).toSubring
e : ⟨a, ha⟩ + ⟨b, hb⟩ = 1
A : { a // a ∈ s }
haA : a ∈ (↑A).toSubring
B : { a // a ∈ s }
hbB : b ∈ (↑B).toSubring
C : { a // a ∈ s }
hCA : (toSubring ∘ fun x ↦ ↑x) A ≤ (toSubring ∘ fun x ↦ ↑x) C
hCB : (toSubring ∘ fun x ↦ ↑x) B ≤ (toSubring ∘ fun x ↦ ↑x) C
⊢ IsUnit ⟨a, ⋯⟩ → IsUnit ⟨a, ha⟩

pp: case refine_1.refine_2
K : Type u_3
inst✝ : Field K
A✝ : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A✝
H : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x ↦ ↑x)
a : K
ha : a ∈ ⨆ i, (↑i).toSubring
b : K
hb : b ∈ ⨆ i, (↑i).toSubring
e : ⟨a, ha⟩ + ⟨b, hb⟩ = 1
A : { a // a ∈ s }
haA : a ∈ (↑A).toSubring
B : { a // a ∈ s }
hbB : b ∈ (↑B).toSubring
C : { a // a ∈ s }
hCA : (toSubring ∘ fun x ↦ ↑x) A ≤ (toSubring ∘ fun x ↦ ↑x) C
hCB : (toSubring ∘ fun x ↦ ↑x) B ≤ (toSubring ∘ fun x ↦ ↑x) C
⊢ IsUnit ⟨b, ⋯⟩ → IsUnit ⟨b, hb⟩

Tactic:
· exact fun h ↦ h.map (Subring.inclusion (le_iSup (fun i : s ↦ i.1.toSubring) C))

Goal state after:
case refine_1.refine_2
K : Type u_3
inst✝ : Field K
A✝ : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A✝
H : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x ↦ ↑x)
a : K
ha : a ∈ ⨆ i, (↑i).toSubring
b : K
hb : b ∈ ⨆ i, (↑i).toSubring
e : ⟨a, ha⟩ + ⟨b, hb⟩ = 1
A : { a // a ∈ s }
haA : a ∈ (↑A).toSubring
B : { a // a ∈ s }
hbB : b ∈ (↑B).toSubring
C : { a // a ∈ s }
hCA : (toSubring ∘ fun x ↦ ↑x) A ≤ (toSubring ∘ fun x ↦ ↑x) C
hCB : (toSubring ∘ fun x ↦ ↑x) B ≤ (toSubring ∘ fun x ↦ ↑x) C
⊢ IsUnit ⟨b, ⋯⟩ → IsUnit ⟨b, hb⟩
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: case refine_1.refine_2
K : Type u_3
inst✝ : Field K
A✝ : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A✝
H : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x ↦ ↑x)
a : K
ha : a ∈ ⨆ i, (↑i).toSubring
b : K
hb : b ∈ ⨆ i, (↑i).toSubring
e : ⟨a, ha⟩ + ⟨b, hb⟩ = 1
A : { a // a ∈ s }
haA : a ∈ (↑A).toSubring
B : { a // a ∈ s }
hbB : b ∈ (↑B).toSubring
C : { a // a ∈ s }
hCA : (toSubring ∘ fun x ↦ ↑x) A ≤ (toSubring ∘ fun x ↦ ↑x) C
hCB : (toSubring ∘ fun x ↦ ↑x) B ≤ (toSubring ∘ fun x ↦ ↑x) C
⊢ IsUnit ⟨b, ⋯⟩ → IsUnit ⟨b, hb⟩

Tactic:
· exact fun h ↦ h.map (Subring.inclusion (le_iSup (fun i : s ↦ i.1.toSubring) C))

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

Goal state before:
pp: case e'_4
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
⊢ ↑(((decompose 𝒜) x) n) ^ m = 0

Tactic:
decompose_of_mem_ne 𝒜 _ hn.symm,

Goal state after:
case e'_4
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
⊢ 0 ^ m = 0

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
⊢ x ∈ 𝒜 nx
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝¹ : Field K
x : K
R : Subring K
hxR : x ∉ R
inst✝ : IsIntegrallyClosedIn (↥R) K
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R) K := (↥R)[x⁻¹]
xinv : ↥B.toSubring := ⟨x⁻¹, ⋯⟩
eq : Ideal.span {xinv} = ⊤
p : (↥R)[X]
hp : p.leadingCoeff - 1 ∈ ⊥
hpx : (aeval ⅟x⁻¹) p = 0
⊢ p.Monic

Tactic:
simpa using

Goal state after:
K : Type u_3
inst✝¹ : Field K
x : K
R : Subring K
hxR : x ∉ R
inst✝ : IsIntegrallyClosedIn (↥R) K
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R) K := (↥R)[x⁻¹]
xinv : ↥B.toSubring := ⟨x⁻¹, ⋯⟩
eq : Ideal.span {xinv} = ⊤
p : (↥R)[X]
hp : p.leadingCoeff - 1 ∈ ⊥
hpx : (aeval ⅟x⁻¹) p = 0
⊢ p.leadingCoeff = 1
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝¹ : Field K
x : K
R : LocalSubring K
hxR : x ∉ R.toSubring
inst✝ : IsIntegrallyClosedIn (↥R.toSubring) K
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := ⟨x⁻¹, ⋯⟩
eq : Ideal.map (algebraMap ↥R.toSubring ↥B) (maximalIdeal ↥R.toSubring) + Ideal.span {xinv} = ⊤
p : (↥R.toSubring)[X]
hp : p.leadingCoeff - 1 ∈ maximalIdeal ↥R.toSubring
hpx : (aeval ⅟x⁻¹) p = 0
h : ¬IsUnit p.leadingCoeff
⊢ False

Tactic:
simpa using

Goal state after:
K : Type u_3
inst✝¹ : Field K
x : K
R : LocalSubring K
hxR : x ∉ R.toSubring
inst✝ : IsIntegrallyClosedIn (↥R.toSubring) K
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := ⟨x⁻¹, ⋯⟩
eq : Ideal.map (algebraMap ↥R.toSubring ↥B) (maximalIdeal ↥R.toSubring) + Ideal.span {xinv} = ⊤
p : (↥R.toSubring)[X]
hp : p.leadingCoeff - 1 ∈ maximalIdeal ↥R.toSubring
hpx : (aeval ⅟x⁻¹) p = 0
h : ¬IsUnit p.leadingCoeff
⊢ False
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h
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)) := ⋯
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
i j : ι
m : ℕ
hm :
  (f * (g i * g j)) ^ m •
      ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i) -
        (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t j)) =
    0
⊢ (fun x ↦ (g i * g j) ^ m • x) ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ m • t i)) =
    (fun x ↦ (g i * g j) ^ m • x) ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ m • t j))

Tactic:
simpa using

Goal state after:
case h
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)
i j : ι
m : ℕ
hm :
  (f * (g i * g j)) ^ m •
      ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i) -
        (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t j)) =
    0
⊢ (f * (g i * g j)) ^ m • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i) =
    (f * (g i * g j)) ^ m • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t j)
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝¹ : Field K
x : K
R : LocalSubring K
hxR : x ∉ R.toSubring
inst✝ : IsIntegrallyClosedIn (↥R.toSubring) K
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := ⟨x⁻¹, ⋯⟩
eq : Ideal.map (algebraMap ↥R.toSubring ↥B) (maximalIdeal ↥R.toSubring) + Ideal.span {xinv} = ⊤
p : (↥R.toSubring)[X]
hp : p.leadingCoeff - 1 ∈ maximalIdeal ↥R.toSubring
hpx : (aeval ⅟x⁻¹) p = 0
H : IsUnit p.leadingCoeff
⊢ eval₂ (algebraMap (↥R.toSubring) K) x (C ↑H.unit⁻¹ * p) = 0

Tactic:
simpa using

Goal state after:
K : Type u_3
inst✝¹ : Field K
x : K
R : LocalSubring K
hxR : x ∉ R.toSubring
inst✝ : IsIntegrallyClosedIn (↥R.toSubring) K
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := ⟨x⁻¹, ⋯⟩
eq : Ideal.map (algebraMap ↥R.toSubring ↥B) (maximalIdeal ↥R.toSubring) + Ideal.span {xinv} = ⊤
p : (↥R.toSubring)[X]
hp : p.leadingCoeff - 1 ∈ maximalIdeal ↥R.toSubring
hpx : (aeval ⅟x⁻¹) p = 0
H : IsUnit p.leadingCoeff
⊢ p = 0 ∨ eval₂ (algebraMap (↥R.toSubring) K) x p = 0
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
V : ValuationSubring K := { toSubring := (algebraMap R K).range, mem_or_inv_mem' := ⋯ }
this : LocalSubring.range g ≤ V.toLocalSubring
x : S
y : R
hy : (algebraMap R K) y = g x
⊢ ↑((g.rangeRestrict.comp f) y) = ↑⟨g x, ⋯⟩

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
V : ValuationSubring K := { toSubring := (algebraMap R K).range, mem_or_inv_mem' := ⋯ }
this : LocalSubring.range g ≤ V.toLocalSubring
x : S
y : R
hy : (algebraMap R K) y = g x
⊢ g (f y) = g 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
t : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ⇑(ConcreteCategory.hom (toSpec 𝒜 f).base) ⁻¹' ↑(sbo HomogeneousLocalization.mk t) =
    ↑((Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (pbo ↑t.num))

Tactic:
by
  convert! (ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen f t)
  exact funext fun _ => toSpec_base_apply_eq _ _

Goal state after:
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:
· exact hx ▸ hfg

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: 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
⊢ Existence f'

Tactic:
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.Sites.Small

Goal state before:
pp: case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.I₀
h : V ⟶ 𝒰.X k
hcomp : h ≫ 𝒰.f k = f
this : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S
⊢ ∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯

Tactic:
refine ⟨(𝒰.X k).asOver S, Over.homMk h (by simp [← hcomp, this]), (𝒰.f k).asOver S, ⟨k⟩, ?_⟩

Goal state after:
case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.I₀
h : V ⟶ 𝒰.X k
hcomp : h ≫ 𝒰.f k = f
this : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S
⊢ Over.homMk h ⋯ ≫ Hom.asOver (𝒰.f k) S = Over.homMk f ⋯