mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
⊢ Function.Surjective ⇑(TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id)

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
⊢ Function.Surjective ⇑(TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id)
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos.inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h✝ : Nontrivial R
r : R
hr : r ≠ 0
w✝ : S
e : (algebraMap R S) r = s * w✝
⊢ IsIntegral R (w✝ • s • a)

Tactic:
]

Goal state after:
case pos.inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h✝ : Nontrivial R
r : R
hr : r ≠ 0
w✝ : S
e : (algebraMap R S) r = s * w✝
⊢ IsIntegral R (w✝ • s • a)
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : (aeval a) p = 0
hRS : FaithfulSMul R S
⊢ IsAlgebraic R a

Tactic:
]

Goal state after:
case pos
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : (aeval a) p = 0
hRS : FaithfulSMul R S
⊢ IsAlgebraic R a
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
B : Type u_2
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst✝¹ : P.LiesOver p
hpm : (Ideal.under A P).IsMaximal
inst✝ : P.IsPrime
⊢ P.IsMaximal

Tactic:
]

Goal state after:
A : Type u_1
inst✝⁵ : CommRing A
B : Type u_2
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst✝¹ : P.LiesOver p
hpm : (Ideal.under A P).IsMaximal
inst✝ : P.IsPrime
⊢ P.IsMaximal
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case tmul
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : l23 x = 0
mem : x ⊗ₜ[R] m ∈ (LinearMap.rTensor M l12).range
⊢ ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = ⟨x, hx⟩ ⊗ₜ[R] m

Tactic:
]

Goal state after:
case tmul
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : l23 x = 0
mem : x ⊗ₜ[R] m ∈ (LinearMap.rTensor M l12).range
⊢ ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = ⟨x, hx⟩ ⊗ₜ[R] m
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
B : Type u_2
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst✝¹ : P.LiesOver p
inst✝ : P.IsMaximal
⊢ (Ideal.under A P).IsMaximal

Tactic:
]

Goal state after:
A : Type u_1
inst✝⁵ : CommRing A
B : Type u_2
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst✝¹ : P.LiesOver p
inst✝ : P.IsMaximal
⊢ (Ideal.under A P).IsMaximal
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ (∀ (i : PrimeSpectrum R), f ∈ ⨅ (_ : i ∈ t), i.asIdeal) ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asIdeal}

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ (∀ (i : PrimeSpectrum R), f ∈ ⨅ (_ : i ∈ t), i.asIdeal) ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asIdeal}
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
x : PrimeSpectrum R
⊢ x ∈ t → f ∈ x.asIdeal ↔ x ∈ t → f ∈ x.asIdeal

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ (∀ x ∈ t, f ∈ x.asIdeal) ↔ ∀ x ∈ t, f ∈ x.asIdeal

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R
⊢ (∀ x ∈ zeroLocus ↑I, f ∈ x.asIdeal) ↔ ∀ p ∈ {J | I ≤ J ∧ J.IsPrime}, f ∈ p

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R
⊢ (∀ x ∈ zeroLocus ↑I, f ∈ x.asIdeal) ↔ ∀ p ∈ {J | I ≤ J ∧ J.IsPrime}, f ∈ p
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ ⨅ x, x.asIdeal = iInf asIdeal

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ J ≤ I.radical ↔ J ≤ I.radical

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p✝ : S[X]
hp : p✝ ≠ 0
eval0 : (aeval a) p✝ = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p✝.coeff p✝.support, IsIntegral R (r • z)
p : (↥(integralClosure R S).toSubring)[X] := (r • p✝).toSubring (integralClosure R S).toSubring ⋯
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R
⊢ g ∈ (Ideal.span {f}).radical ↔ g ∈ (Ideal.span {f}).radical

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case tmul
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : l23 x = 0
y : N1 ⊗[R] M
hy : (LinearMap.rTensor M l12) y = x ⊗ₜ[R] m
⊢ (LinearMap.rTensor M l12) y = (LinearMap.rTensor M l12) y

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ Set.univ = Set.univ

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
⊢ ∀ (x : PrimeSpectrum R), x ∉ zeroLocus s

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
⊢ ∀ (x : PrimeSpectrum R), x ∉ zeroLocus s
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
⊢ False

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
⊢ False
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : x.asIdeal.IsPrime
⊢ 1 ∈ x.asIdeal

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : x.asIdeal.IsPrime
⊢ 1 ∈ x.asIdeal
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: A : Type u_3
inst✝⁹ : CommRing A
L : Type u_5
inst✝⁸ : Field L
inst✝⁷ : Algebra A L
C : Type u_6
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : Algebra.IsAlgebraic A L
inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
h : (algebraMap A C) x = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ s = ∅ ↔ s = ∅

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ s ⊆ ↑(nilradical R) ↔ s ⊆ ↑(nilradical R)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: A : Type u_3
inst✝⁹ : CommRing A
L : Type u_5
inst✝⁸ : Field L
inst✝⁷ : Algebra A L
C : Type u_6
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : Algebra.IsAlgebraic A L
inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
⊢ (algebraMap A L) x * z = (algebraMap A L) x * z

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s s' : Set R
⊢ zeroLocus s ∪ zeroLocus s' = zeroLocus ↑(Ideal.span s) ∪ zeroLocus ↑(Ideal.span s')

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s s' : Set R
⊢ zeroLocus s ∪ zeroLocus s' = zeroLocus ↑(Ideal.span s) ∪ zeroLocus ↑(Ideal.span s')
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
s : S
a : A
ha : IsAlgebraic R a
inst✝ : FaithfulSMul R S
⊢ IsAlgebraic S (s • 1 ⊗ₜ[R] a)

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
s : S
a : A
ha : IsAlgebraic R a
inst✝ : FaithfulSMul R S
⊢ IsAlgebraic S (s • 1 ⊗ₜ[R] a)
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
r : R
⊢ (∃ y ∈ vanishingIdeal t, ∃ z ∈ vanishingIdeal t', y + z = r) → ∀ x ∈ t ∩ t', r ∈ x.asIdeal

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
r : R
⊢ (∃ y ∈ vanishingIdeal t, ∃ z ∈ vanishingIdeal t', y + z = r) → ∀ x ∈ t ∩ t', r ∈ x.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
s : S
a : A
ha : IsAlgebraic R a
inst✝ : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : (aeval a) p = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R
I : PrimeSpectrum R
⊢ f ∉ ↑I.asIdeal ↔ f ∉ I.asIdeal

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R
I : PrimeSpectrum R
⊢ f ∉ ↑I.asIdeal ↔ f ∉ I.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus s = zeroLocus s

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus (insert 0 (s \ {0})) = zeroLocus (insert 0 s)

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus (insert 0 (s \ {0})) = zeroLocus (insert 0 s)
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : CommSemiring R
m : Ideal R
inst✝ : m.IsMaximal
I : PrimeSpectrum R
h : I ∈ zeroLocus ↑m
⊢ I ∈ {{ asIdeal := m, isPrime := ⋯ }}

Tactic:
simp only [mem_zeroLocus, SetLike.coe_subset_coe] at h

Goal state after:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
m : Ideal R
inst✝ : m.IsMaximal
I : PrimeSpectrum R
h : m ≤ I.asIdeal
⊢ I ∈ {{ asIdeal := m, isPrime := ⋯ }}
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : M.IsPrime
⊢ { asIdeal := M, isPrime := h_prM }.asIdeal ≤ M

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : M = ⊤
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ ⊤

Tactic:
]

Goal state after:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : M = ⊤
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ ⊤
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R (rb • ra • a + ra • rb • b)

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R (rb • ra • a + ra • rb • b)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑0 ⇑(LinearMap.lTensor M f) ↔ Function.Exact ⇑0 ⇑f

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑0 ⇑(LinearMap.lTensor M f) ↔ Function.Exact ⇑0 ⇑f
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
z : R
hz : z ∉ M
m_eq : M = M + R ∙ z
⊢ z ∈ M + R ∙ z

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
z : R
hz : z ∉ M
m_eq : M = M + R ∙ z
⊢ z ∈ M + R ∙ z
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑(LinearMap.lTensor M f) ⇑0 ↔ Function.Exact ⇑f ⇑0

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑(LinearMap.lTensor M f) ⇑0 ↔ Function.Exact ⇑f ⇑0
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M

Tactic:
]

Goal state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ R[y]
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
this : IsAlgebraic R (r • z)
⊢ IsAlgebraic R z

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ R[y]
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
this : IsAlgebraic R (r • z)
⊢ IsAlgebraic R z
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ M * (M + R ∙ y) + (R ∙ x) * (M + R ∙ y) ≤ M

Tactic:
]

Goal state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ M * (M + R ∙ y) + (R ∙ x) * (M + R ∙ y) ≤ M
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case mp
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
x : K
this✝¹ : Nontrivial S := MulActionWithZero.nontrivial S K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
⊢ IsIntegral (FractionRing R) x

Tactic:
]

Goal state after:
case mp
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
x : K
this✝¹ : Nontrivial S := MulActionWithZero.nontrivial S K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
⊢ IsIntegral (FractionRing R) x
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (R ∙ x) * M + (R ∙ x) * (R ∙ y) ≤ M

Tactic:
]

Goal state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (R ∙ x) * M + (R ∙ x) * (R ∙ y) ≤ M