mathlib-initiative/mathlib-tactics huggingface dataset:
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 : y ^ p.natDegree = 0
hy0 : y ≠ 0
⊢ False

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
⊢ (C y * X).natDegree ≠ 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 : y ^ p.natDegree = 0
hy0 : y ≠ 0
⊢ False
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
⊢ (C y * X).natDegree ≠ 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
⊢ (C y * X).natDegree ≠ 0
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_2
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
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P
⊢ comap (Quotient.mk (comap (algebraMap R S) I)) (map (Quotient.mk (comap (algebraMap R S) I)) P) = P

Tactic:
·

Goal state after:
case refine_2
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
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P
⊢ comap (Quotient.mk (comap (algebraMap R S) I)) (map (Quotient.mk (comap (algebraMap R S) I)) P) = P
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ q'.Monic

pp: case refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ eval₂ (algebraMap R S) t q' = 0

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ q'.Monic
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ q'.natDegree ≤ q.natDegree + N

pp: case refine_1.refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ q'.coeff (q.natDegree + N) = 1

Tactic:
·

Goal state after:
case refine_1.refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ q'.natDegree ≤ q.natDegree + N
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case inl
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : ↑n ≠ 0
h : ↑n • x = (algebraMap S K) s
⊢ ∃ m s, m ≠ 0 ∧ m • x = (algebraMap S K) s

pp: case inr
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : -↑n ≠ 0
h : -↑n • x = (algebraMap S K) s
⊢ ∃ m s, m ≠ 0 ∧ m • x = (algebraMap S K) s

Tactic:
·

Goal state after:
case inl
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : ↑n ≠ 0
h : ↑n • x = (algebraMap S K) s
⊢ ∃ m s, m ≠ 0 ∧ m • x = (algebraMap S K) s
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case inr
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : -↑n ≠ 0
h : -↑n • x = (algebraMap S K) s
⊢ ∃ m s, m ≠ 0 ∧ m • x = (algebraMap S K) s

Tactic:
·

Goal state after:
case inr
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : -↑n ≠ 0
h : -↑n • x = (algebraMap S K) s
⊢ ∃ m s, m ≠ 0 ∧ m • x = (algebraMap S K) s
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
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ I = ⊤ → map f I = ⊤

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 = ⊤

Tactic:
·

Goal state after:
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.Localization.Integral

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ q'.coeff (q.natDegree + N) = 1

Tactic:
·

Goal state after:
case refine_1.refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ q'.coeff (q.natDegree + N) = 1
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos.inl
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✝ : Subsingleton R
⊢ IsAlgebraic R a

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
⊢ IsAlgebraic R a

Tactic:
·

Goal state after:
case pos.inl
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✝ : Subsingleton R
⊢ IsAlgebraic R a
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ (if q.natDegree ≤ q.natDegree + N then (q.coeff q.natDegree).coeff ((revAt N) (q.natDegree + N - q.natDegree))
    else 0) =
    1

pp: case refine_1.refine_2.h₀
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ ∀ b ∈ q.support,
    b ≠ q.natDegree → (if b ≤ q.natDegree + N then (q.coeff b).coeff ((revAt N) (q.natDegree + N - b)) else 0) = 0

pp: case refine_1.refine_2.h₁
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ q.natDegree ∉ q.support →
    (if q.natDegree ≤ q.natDegree + N then (q.coeff q.natDegree).coeff ((revAt N) (q.natDegree + N - q.natDegree))
      else 0) =
      0

Tactic:
·

Goal state after:
case refine_1.refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ (if q.natDegree ≤ q.natDegree + N then (q.coeff q.natDegree).coeff ((revAt N) (q.natDegree + N - q.natDegree))
    else 0) =
    1
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_1.refine_2.h₀
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ ∀ b ∈ q.support,
    b ≠ q.natDegree → (if b ≤ q.natDegree + N then (q.coeff b).coeff ((revAt N) (q.natDegree + N - b)) else 0) = 0

pp: case refine_1.refine_2.h₁
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ q.natDegree ∉ q.support →
    (if q.natDegree ≤ q.natDegree + N then (q.coeff q.natDegree).coeff ((revAt N) (q.natDegree + N - q.natDegree))
      else 0) =
      0

Tactic:
·

Goal state after:
case refine_1.refine_2.h₀
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ ∀ b ∈ q.support,
    b ≠ q.natDegree → (if b ≤ q.natDegree + N then (q.coeff b).coeff ((revAt N) (q.natDegree + N - b)) else 0) = 0
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case refine_1
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 ⋯
⊢ p ≠ 0

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 ⋯
⊢ (aeval a) p = 0

Tactic:
·

Goal state after:
case refine_1
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 ⋯
⊢ p ≠ 0
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommSemiring R
x✝ : Nonempty (PrimeSpectrum R)
p : PrimeSpectrum R
h : 0 = 1
⊢ p.asIdeal = ⊤

pp: case refine_2
R : Type u
inst✝ : CommSemiring R
h : Nontrivial R
⊢ Nonempty (PrimeSpectrum R)

Tactic:
·

Goal state after:
case refine_1
R : Type u
inst✝ : CommSemiring R
x✝ : Nonempty (PrimeSpectrum R)
p : PrimeSpectrum R
h : 0 = 1
⊢ p.asIdeal = ⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

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

Tactic:
·

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

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

pp: case right
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Function.Surjective (primeSpectrumProdOfSum R S)

Tactic:
·

Goal state after:
case left
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Function.Injective (primeSpectrumProdOfSum R S)
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case left.inl.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal R
hI : I.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h : I = I' ∧ True
⊢ Sum.inl { asIdeal := I, isPrime := hI } = Sum.inl { asIdeal := I', isPrime := hI' }

pp: case left.inl.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal R
hI : I.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h : I = ⊤ ∧ ⊤ = J'
⊢ Sum.inl { asIdeal := I, isPrime := hI } = Sum.inr { asIdeal := J', isPrime := hJ' }

pp: case left.inr.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h : ⊤ = I' ∧ J = ⊤
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inl { asIdeal := I', isPrime := hI' }

pp: case left.inr.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h : True ∧ J = J'
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inr { asIdeal := J', isPrime := hJ' }

Tactic:
·

Goal state after:
case left.inl.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal R
hI : I.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h : I = I' ∧ True
⊢ Sum.inl { asIdeal := I, isPrime := hI } = Sum.inl { asIdeal := I', isPrime := hI' }
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case left.inl.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal R
hI : I.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h : I = ⊤ ∧ ⊤ = J'
⊢ Sum.inl { asIdeal := I, isPrime := hI } = Sum.inr { asIdeal := J', isPrime := hJ' }

pp: case left.inr.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h : ⊤ = I' ∧ J = ⊤
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inl { asIdeal := I', isPrime := hI' }

pp: case left.inr.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h : True ∧ J = J'
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inr { asIdeal := J', isPrime := hJ' }

Tactic:
·

Goal state after:
case left.inl.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal R
hI : I.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h : I = ⊤ ∧ ⊤ = J'
⊢ Sum.inl { asIdeal := I, isPrime := hI } = Sum.inr { asIdeal := J', isPrime := hJ' }
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case left.inr.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h : ⊤ = I' ∧ J = ⊤
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inl { asIdeal := I', isPrime := hI' }

pp: case left.inr.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h : True ∧ J = J'
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inr { asIdeal := J', isPrime := hJ' }

Tactic:
·

Goal state after:
case left.inr.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h : ⊤ = I' ∧ J = ⊤
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inl { asIdeal := I', isPrime := hI' }
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case left.inr.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h : True ∧ J = J'
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inr { asIdeal := J', isPrime := hJ' }

Tactic:
·

Goal state after:
case left.inr.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h : True ∧ J = J'
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inr { asIdeal := J', isPrime := hJ' }
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

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

Tactic:
·

Goal state after:
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: case right.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : Ideal R
hp : p.IsPrime
hI : (p.prod ⊤).IsPrime
⊢ ∃ a, primeSpectrumProdOfSum R S a = { asIdeal := p.prod ⊤, isPrime := hI }

pp: case right.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : Ideal S
hp : p.IsPrime
hI : (⊤.prod p).IsPrime
⊢ ∃ a, primeSpectrumProdOfSum R S a = { asIdeal := ⊤.prod p, isPrime := hI }

Tactic:
·

Goal state after:
case right.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : Ideal R
hp : p.IsPrime
hI : (p.prod ⊤).IsPrime
⊢ ∃ a, primeSpectrumProdOfSum R S a = { asIdeal := p.prod ⊤, isPrime := hI }
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case right.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : Ideal S
hp : p.IsPrime
hI : (⊤.prod p).IsPrime
⊢ ∃ a, primeSpectrumProdOfSum R S a = { asIdeal := ⊤.prod p, isPrime := hI }

Tactic:
·

Goal state after:
case right.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : Ideal S
hp : p.IsPrime
hI : (⊤.prod p).IsPrime
⊢ ∃ a, primeSpectrumProdOfSum R S a = { asIdeal := ⊤.prod p, isPrime := hI }