mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case inr.refine_1
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
⊢ p.leadingCoeff ∈ (algebraMap R Rₘ).range

pp: case inr.refine_2
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
⊢ (p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))).Monic

Tactic:
· rw [hp₁.leadingCoeff]
    exact one_mem _

Goal state after:
case inr.refine_2
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
⊢ (p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))).Monic
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
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ ∀ [h : Subsingleton (N ⊗[R] M)], Subsingleton N

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ ∀ [h : Subsingleton (N ⊗[R] M)], Subsingleton N
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
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ Subsingleton (N ⊗[R] M) → Subsingleton N

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ Subsingleton (N ⊗[R] M) → Subsingleton N
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
x✝² : Flat R M
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
⊢ ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝² : Flat R M
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
⊢ ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N
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
x✝² : Flat R M
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
⊢ ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝² : Flat R M
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
⊢ ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

pp: case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ¬Function.Injective ⇑(algebraMap R A)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
;

Goal state after:
case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ¬Function.Injective ⇑(algebraMap R A)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ¬∀ (a : R), (algebraMap R A) a = 0 → a = 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
;

Goal state after:
case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ¬∀ (a : R), (algebraMap R A) a = 0 → a = 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • 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_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : FaithfullyFlat R M
⊢ Subsingleton (M ⊗[R] N) ↔ Subsingleton N

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : FaithfullyFlat R M
⊢ Subsingleton (M ⊗[R] N) ↔ Subsingleton N
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_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : FaithfullyFlat R N
⊢ Subsingleton (M ⊗[R] N) ↔ Subsingleton M

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : FaithfullyFlat R N
⊢ Subsingleton (M ⊗[R] N) ↔ Subsingleton M
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
p : R[X]
monic : p.Monic
hy : ¬IsNilpotent 0
h✝ : IsIntegral R (0 • z)
eval0 : eval₂ (algebraMap R A) (0 • z) p = 0
h : (p.comp (C 0 * X)).coeff p.natDegree = coeff 0 p.natDegree
⊢ False

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
p : R[X]
monic : p.Monic
hy : ¬IsNilpotent 0
h✝ : IsIntegral R (0 • z)
eval0 : eval₂ (algebraMap R A) (0 • z) p = 0
h : (p.comp (C 0 * X)).coeff p.natDegree = coeff 0 p.natDegree
⊢ False
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)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
E : Submodule R N3 := R ∙ l23 (l12 n1)
hE : Nontrivial ↥E
eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0
c : ↥E ⊗[R] M →₀ R
b : ⦃a : ↥E ⊗[R] M⦄ → a ∈ ↑c.support → ↥E
a : ⦃a : ↥E ⊗[R] M⦄ → a ∈ ↑c.support → M
hy : ∀ ⦃a_1 : ↥E ⊗[R] M⦄ (a_2 : a_1 ∈ ↑c.support), b a_2 ⊗ₜ[R] a a_2 = a_1
r : ⦃a : ↥E ⊗[R] M⦄ → a ∈ c.support → R := fun a ha ↦ ⋯.choose
hr : ∀ ⦃i : ↥E ⊗[R] M⦄ (hi : i ∈ c.support), b hi = r hi • ⟨l23 (l12 n1), ⋯⟩
⊢ (c.sum fun mi r ↦ r • mi) = 0

Tactic:
refine Finset.sum_eq_zero fun i hi => show c i • i = 0 from
      (Module.Flat.rTensor_preserves_injective_linearMap (M := M) E.subtype <|
              Submodule.injective_subtype E) ?_

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)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
E : Submodule R N3 := R ∙ l23 (l12 n1)
hE : Nontrivial ↥E
eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0
c : ↥E ⊗[R] M →₀ R
b : ⦃a : ↥E ⊗[R] M⦄ → a ∈ ↑c.support → ↥E
a : ⦃a : ↥E ⊗[R] M⦄ → a ∈ ↑c.support → M
hy : ∀ ⦃a_1 : ↥E ⊗[R] M⦄ (a_2 : a_1 ∈ ↑c.support), b a_2 ⊗ₜ[R] a a_2 = a_1
r : ⦃a : ↥E ⊗[R] M⦄ → a ∈ c.support → R := fun a ha ↦ ⋯.choose
hr : ∀ ⦃i : ↥E ⊗[R] M⦄ (hi : i ∈ c.support), b hi = r hi • ⟨l23 (l12 n1), ⋯⟩
i : ↥E ⊗[R] M
hi : i ∈ c.support
⊢ (LinearMap.rTensor M E.subtype) (c i • i) = (LinearMap.rTensor M E.subtype) 0
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff (p.natDegree * (C y * X).natDegree) = 0
hy0 : y ≠ 0
⊢ 1 ≠ 0

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff (p.natDegree * (C y * X).natDegree) = 0
hy0 : y ≠ 0
⊢ 1 ≠ 0
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ map f I = ⊤ → I = ⊤

pp: case mpr
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ I = ⊤ → map f I = ⊤

Tactic:
;

Goal state after:
case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ map f I = ⊤ → I = ⊤

case mpr
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ I = ⊤ → map f I = ⊤
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case mpr
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf₂ : f.IsIntegral
hf₁ : RingHom.ker f ≤ ⊤
⊢ map f ⊤ = ⊤

Tactic:
;

Goal state after:
case mpr
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf₂ : f.IsIntegral
hf₁ : RingHom.ker f ≤ ⊤
⊢ map f ⊤ = ⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ Nonempty (PrimeSpectrum R) ↔ Nontrivial R

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ Nonempty (PrimeSpectrum R) ↔ Nontrivial R
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

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

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ ∀ (a : PrimeSpectrum R), f ∈ ⨅ (_ : a ∈ t), a.asIdeal ↔ a ∈ t → f ∈ a.asIdeal
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case add
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
y : ↥l23.ker ⊗[R] M
hy : ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = y
x : ↥(Submodule.inclusion complex).range ⊗[R] M
⊢ ∃ a,
    (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a =
      (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) x + y

Tactic:
;

Goal state after:
case add
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
y : ↥l23.ker ⊗[R] M
hy : ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = y
x : ↥(Submodule.inclusion complex).range ⊗[R] M
⊢ ∃ a,
    (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a =
      (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) x + y
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
⊢ vanishingIdeal t ⊔ vanishingIdeal t' ≤ vanishingIdeal (t ∩ t')

Tactic:
intro r

Goal state after:
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
r : R
⊢ r ∈ vanishingIdeal t ⊔ vanishingIdeal t' → r ∈ vanishingIdeal (t ∩ t')
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
x✝ : R
⊢ ((algebraMap S (TensorProduct R S A)).comp (algebraMap R S)) x✝ =
    ((↑Algebra.TensorProduct.includeRight).comp (algebraMap R A)) x✝

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
p : R[X]
h : p ≠ 0
eval0 : (aeval a) p = 0
x✝ : R
⊢ ((algebraMap S (TensorProduct R S A)).comp (algebraMap R S)) x✝ =
    ((↑Algebra.TensorProduct.includeRight).comp (algebraMap R A)) x✝
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 (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: R : Type u
inst✝ : CommSemiring R
r : R
hr : IsUnit r
s : Set R
x✝ : PrimeSpectrum R
⊢ x✝ ∈ zeroLocus (r • s) ↔ x✝ ∈ zeroLocus s

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
r : R
hr : IsUnit r
s : Set R
x✝ : PrimeSpectrum R
⊢ x✝ ∈ zeroLocus (r • s) ↔ x✝ ∈ zeroLocus s
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.lTensor M l12) ⇑(LinearMap.lTensor M l23)
x✝¹ : M
x✝ : N1
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor M l12 ∘ₗ ↑(TensorProduct.comm R M N1))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R M N2) ∘ₗ LinearMap.lTensor M l12)) x✝¹) x✝

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.lTensor M l12) ⇑(LinearMap.lTensor M l23)
x✝¹ : M
x✝ : N1
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor M l12 ∘ₗ ↑(TensorProduct.comm R M N1))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R M N2) ∘ₗ LinearMap.lTensor M l12)) x✝¹) x✝
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.lTensor M l12) ⇑(LinearMap.lTensor M l23)
x✝¹ : M
x✝ : N2
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor M l23 ∘ₗ ↑(TensorProduct.comm R M N2))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R M N3) ∘ₗ LinearMap.lTensor M l23)) x✝¹) x✝

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.lTensor M l12) ⇑(LinearMap.lTensor M l23)
x✝¹ : M
x✝ : N2
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor M l23 ∘ₗ ↑(TensorProduct.comm R M N2))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R M N3) ∘ₗ LinearMap.lTensor M l23)) x✝¹) x✝
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
h : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
hf : LinearMap.lTensor M f = 0
this : Function.Exact ⇑f ⇑LinearMap.id
x : N
⊢ f x = 0 x

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
h : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
hf : LinearMap.lTensor M f = 0
this : Function.Exact ⇑f ⇑LinearMap.id
x : N
⊢ f x = 0 x
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
h✝ : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
h : LinearMap.lTensor M f = 0
n : N
m : M
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor M f)) n) m = ((AlgebraTensorModule.curry 0) n) m

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
h✝ : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
h : LinearMap.lTensor M f = 0
n : N
m : M
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor M f)) n) m = ((AlgebraTensorModule.curry 0) n) m
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
h✝ : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
h : LinearMap.rTensor M f = 0
m : M
n : N
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor M f)) m) n = ((AlgebraTensorModule.curry 0) m) n

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
h✝ : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
h : LinearMap.rTensor M f = 0
m : M
n : N
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor M f)) m) n = ((AlgebraTensorModule.curry 0) m) n
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case mp
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
⊢ 1 ⊗ₜ[R] m = 0 → m = 0

pp: case mpr
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
⊢ m = 0 → 1 ⊗ₜ[R] m = 0

Tactic:
;

Goal state after:
case mp
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
⊢ 1 ⊗ₜ[R] m = 0 → m = 0

case mpr
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
⊢ m = 0 → 1 ⊗ₜ[R] m = 0
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case mpr
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
⊢ 1 ⊗ₜ[R] 0 = 0

Tactic:
;

Goal state after:
case mpr
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
⊢ 1 ⊗ₜ[R] 0 = 0
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
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst✝ : NoZeroDivisors S
h : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
⊢ Algebra.IsAlgebraic R[X] S[X]

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
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst✝ : NoZeroDivisors S
h : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
⊢ Algebra.IsAlgebraic R[X] S[X]
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
z : A
z' : S
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst✝ : NoZeroDivisors S
h : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)

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
z : A
z' : S
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst✝ : NoZeroDivisors S
h : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)