mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
⊢ scaleRoots 1 r = 1

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
n✝ : ℕ
⊢ (scaleRoots 1 r).coeff n✝ = coeff 1 n✝
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.integralNormalization.support ⊆ p.support

Tactic:
intro
  simp +contextual [sum_def, integralNormalization, coeff_monomial, mem_support_iff]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r s : R
⊢ p.scaleRoots (r * s) = (p.scaleRoots r).scaleRoots s

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r s : R
n✝ : ℕ
⊢ (p.scaleRoots (r * s)).coeff n✝ = ((p.scaleRoots r).scaleRoots s).coeff n✝
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
⊢ f.integralNormalization.support = f.support

Tactic:
nontriviality R using Subsingleton.eq_zero (α := R[X])
  have : IsDomain R := {}
  by_cases hf : f = 0; · simp [hf]
  ext i
  refine ⟨fun h => support_integralNormalization_subset h, ?_⟩
  simp only [integralNormalization_coeff, mem_support_iff]
  intro hfi
  split_ifs with hi <;> simp [hf, hfi]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.MvPolynomial

Goal state before:
pp: R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
e : σ →₀ ℕ
s : S
n : N
d : σ →₀ ℕ
⊢ coeff d (rTensorAlgEquiv (s ⊗ₜ[R] (monomial e) n)) = if e = d then s ⊗ₜ[R] n else 0

Tactic:
by
  simp [tmul_ite]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.MvPolynomial

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ (AlgHom.restrictScalars R ↑(algebraTensorAlgEquiv R A).symm).comp (mapAlgHom (Algebra.ofId R A)) =
    Algebra.TensorProduct.includeRight

Tactic:
ext

Goal state after:
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
i✝ : σ
⊢ ((AlgHom.restrictScalars R ↑(algebraTensorAlgEquiv R A).symm).comp (mapAlgHom (Algebra.ofId R A))) (X i✝) =
    Algebra.TensorProduct.includeRight (X i✝)
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ rootMultiplicity (r * a) (((X - C a) ^ rootMultiplicity a p).scaleRoots r * q.scaleRoots r) = rootMultiplicity a p

pp: case inr.inr.h
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ ((X - C a) ^ rootMultiplicity a p).leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
pow_scaleRoots',

Goal state after:
case inr.inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ rootMultiplicity (r * a) ((X - C a).scaleRoots r ^ rootMultiplicity a p * q.scaleRoots r) = rootMultiplicity a p

case inr.inr.hp
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ (X - C a).leadingCoeff ^ rootMultiplicity a p ≠ 0

case inr.inr.h
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ ((X - C a) ^ rootMultiplicity a p).leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
⊢ ((Algebra.TensorProduct.lift ((IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]).comp includeLeft)
            (mapAlgHom M includeRight) ⋯).comp
        rTensorEquivAlgEquiv.invFun).toLinearMap =
    (AlgHom.id A (A ⊗[R] B)[M]).toLinearMap

Tactic:
ext

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
x✝¹ : M
x✝ : B
a✝ : M
⊢ (((AlgebraTensorModule.curry
              (((Algebra.TensorProduct.lift ((IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]).comp includeLeft)
                        (mapAlgHom M includeRight) ⋯).comp
                    rTensorEquivAlgEquiv.invFun).toLinearMap ∘ₗ
                lsingle x✝¹))
            1)
          x✝).coeff
      a✝ =
    (((AlgebraTensorModule.curry ((AlgHom.id A (A ⊗[R] B)[M]).toLinearMap ∘ₗ lsingle x✝¹)) 1) x✝).coeff a✝
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
⊢ ((AlgHom.restrictScalars R
            (rTensorEquivAlgEquiv.invFun.comp
              (Algebra.TensorProduct.lift ((IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]).comp includeLeft)
                (mapAlgHom M includeRight) ⋯))).comp
        includeRight).toLinearMap =
    ((AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))).comp includeRight).toLinearMap

Tactic:
ext

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
x✝¹ : M
x✝ : B
⊢ (((AlgHom.restrictScalars R
                (rTensorEquivAlgEquiv.invFun.comp
                  (Algebra.TensorProduct.lift ((IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]).comp includeLeft)
                    (mapAlgHom M includeRight) ⋯))).comp
            includeRight).toLinearMap ∘ₗ
        lsingle x✝¹)
      x✝ =
    (((AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))).comp includeRight).toLinearMap ∘ₗ lsingle x✝¹) x✝
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : CommMonoid M
a : A
p : R[M]
⊢ (scalarTensorEquiv R A) (a ⊗ₜ[R] p) = a • (mapAlgHom M (ofId R A)) p

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
A : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : CommMonoid M
a : A
p : R[M]
a✝ : M
⊢ ((scalarTensorEquiv R A) (a ⊗ₜ[R] p)).coeff a✝ = (a • (mapAlgHom M (ofId R A)) p).coeff a✝
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝ : CommSemiring R
m : M
r₁ : R
n : N
r₂ : R
⊢ (tensorEquiv R) (single m r₁ ⊗ₜ[R] single n r₂) = single (m, n) (r₁ * r₂)

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝ : CommSemiring R
m : M
r₁ : R
n : N
r₂ : R
a✝ : M × N
⊢ ((tensorEquiv R) (single m r₁ ⊗ₜ[R] single n r₂)).coeff a✝ = (single (m, n) (r₁ * r₂)).coeff a✝
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hR : IsField R
x : S
hx : x ≠ 0
this : Field R := hR.toField
⊢ ∃ b, x * b = 1

Tactic:
obtain ⟨y, rfl⟩ := (Algebra.IsIntegral.isIntegral (R := R) x).isUnit hx

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hR : IsField R
this : Field R := hR.toField
y : Sˣ
hx : ↑y ≠ 0
⊢ ∃ b, ↑y * b = 1
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : A ≃ₐ[R] S
y : S
⊢ (∃ x ∈ integralClosure R A, ↑f x = y) ↔ y ∈ integralClosure R S

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
A : Type u_2
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : A ≃ₐ[R] S
y : S
⊢ (∃ x ∈ integralClosure R A, ↑f x = y) → y ∈ integralClosure R S

case mpr
R : Type u_1
A : Type u_2
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : A ≃ₐ[R] S
y : S
⊢ y ∈ integralClosure R S → ∃ x ∈ integralClosure R A, ↑f x = y
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : f (p.coeff 0) = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
⊢ C 0 = 0

Tactic:
C_eq_zero

Goal state after:
case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : f (p.coeff 0) = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: A : Type u_3
K : Type u_4
C : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
⊢ IsAlgebraic A x ↔ IsAlgebraic K x

Tactic:
constructor

Goal state after:
case mp
A : Type u_3
K : Type u_4
C : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
⊢ IsAlgebraic A x → IsAlgebraic K x

case mpr
A : Type u_3
K : Type u_4
C : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
⊢ IsAlgebraic K x → IsAlgebraic A x
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case mp.refine_2
A : Type u_3
K : Type u_4
C : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : (aeval x) p = 0
⊢ (aeval x) (Polynomial.map (algebraMap A K) p) = 0

Tactic:
exact (Polynomial.aeval_map_algebraMap K _ _).trans px

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
⊢ g ∈ S[(Ideal.Quotient.mkₐ S I) X] ↔ g ∈ ⊤

Tactic:
constructor

Goal state after:
case mp
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
⊢ g ∈ S[(Ideal.Quotient.mkₐ S I) X] → g ∈ ⊤

case mpr
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
⊢ g ∈ ⊤ → g ∈ S[(Ideal.Quotient.mkₐ S I) X]
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case a.e'_3.a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this : g = (Multiset.map (fun x ↦ X - C x) g.roots).prod
x : R
hx : x ∈ s
x✝ : R
a✝ : x✝ ∈ g.roots
⊢ HSub.hSub x = eval x ∘ fun x ↦ X - C x

Tactic:
ext

Goal state after:
case a.e'_3.a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this : g = (Multiset.map (fun x ↦ X - C x) g.roots).prod
x : R
hx : x ∈ s
x✝¹ : R
a✝ : x✝¹ ∈ g.roots
x✝ : R
⊢ x - x✝ = (eval x ∘ fun x ↦ X - C x) x✝
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_3.refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
a✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : p.coeff i ≠ 0
mem : p.coeff i ∈ comap f I
⊢ (p * X).coeff (i + 1) ∈ comap f I

Tactic:
simpa [hi] using mem

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ ((Quotient.mk (map (mapRingHom (Quotient.mk (comap C P))) P)).comp C).comp (Quotient.mk (comap C P)) =
    (quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯).comp
      ((Quotient.mk P).comp C)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
x✝ : R
⊢ (((Quotient.mk (map (mapRingHom (Quotient.mk (comap C P))) P)).comp C).comp (Quotient.mk (comap C P))) x✝ =
    ((quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯).comp
        ((Quotient.mk P).comp C))
      x✝
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra.IsIntegral R A
I : Ideal A
inst✝ : I.IsPrime
⊢ I ∈ (map (algebraMap R A) (under R I)).minimalPrimes

Tactic:
refine ⟨⟨inferInstance, map_comap_le⟩, fun r ⟨hr, hpr⟩ hrq ↦ ?_⟩

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra.IsIntegral R A
I : Ideal A
inst✝ : I.IsPrime
r : Ideal A
x✝ : (fun q ↦ q.IsPrime ∧ map (algebraMap R A) (under R I) ≤ q) r
hrq : r ≤ I
hr : r.IsPrime
hpr : map (algebraMap R A) (under R I) ≤ r
⊢ I ≤ r
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
inst✝ : IsReduced R
x✝ : ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)
w✝ : R
hy : w✝ ≠ 0
int : IsIntegral R (w✝ • z)
⊢ ¬IsNilpotent w✝

Tactic:
isNilpotent_iff_eq_zero

Goal state after:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
z : A
inst✝ : IsReduced R
x✝ : ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)
w✝ : R
hy : w✝ ≠ 0
int : IsIntegral R (w✝ • z)
⊢ ¬w✝ = 0
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hIP : comap (algebraMap R S) I ≤ P
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q = P

Tactic:
have ⟨P', hP, hP', hP''⟩ := exists_ideal_comap_le_prime P I hIP
  obtain ⟨Q, hQ, hQ', hQ''⟩ := exists_ideal_over_prime_of_isIntegral_of_isPrime P P' hP''
  exact ⟨Q, hP.trans hQ, hQ', hQ''⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: 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 = ⊤

Tactic:
constructor

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.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
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✝
⊢ ¬IsNilpotent r

Tactic:
isNilpotent_iff_eq_zero

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
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✝
⊢ ¬r = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Function.Bijective (primeSpectrumProdOfSum R S)

Tactic:
constructor

Goal state after:
case left
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Function.Injective (primeSpectrumProdOfSum R S)

case right
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Function.Surjective (primeSpectrumProdOfSum R S)
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ zeroLocus ↑I = ∅ ↔ I = ⊤

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ zeroLocus ↑I = ∅ → I = ⊤

case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ I = ⊤ → zeroLocus ↑I = ∅
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
⊢ (algebraMap S (TensorProduct R S A)).comp (algebraMap R S) =
    (↑Algebra.TensorProduct.includeRight).comp (algebraMap R A)

Tactic:
ext

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
r : R
hr : IsUnit r
s : Set R
⊢ zeroLocus (r • s) = zeroLocus s

Tactic:
ext

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)
⊢ LinearMap.rTensor M l12 ∘ₗ ↑(TensorProduct.comm R M N1) = ↑(TensorProduct.comm R M N2) ∘ₗ LinearMap.lTensor M l12

Tactic:
ext

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.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}.prod ≤ M

Tactic:
Multiset.prod_singleton

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
⊢ { asIdeal := M, isPrime := h_prM }.asIdeal ≤ 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
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)
⊢ LinearMap.rTensor M l23 ∘ₗ ↑(TensorProduct.comm R M N2) = ↑(TensorProduct.comm R M N3) ∘ₗ LinearMap.lTensor M l23

Tactic:
ext

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.Localization.Integral

Goal state before:
pp: 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
⊢ (∀ (x : S), IsAlgebraic R x) ↔ ∀ (x : K), IsAlgebraic R x

Tactic:
constructor

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
⊢ (∀ (x : S), IsAlgebraic R x) → ∀ (x : K), IsAlgebraic R x

case mpr
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
⊢ (∀ (x : K), IsAlgebraic R x) → ∀ (x : S), IsAlgebraic R x