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

Goal state before:
pp: case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff + r
hr : map (algebraMap R K) r = 0
hm : m = 0
⊢ IsUnit g

Tactic:
]

Goal state after:
case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff + r
hr : map (algebraMap R K) r = 0
hm : m = 0
⊢ IsUnit g
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
m : ℕ
hm✝ : m ≤ p
hm : m = 0
a : R
hg_div : C a ∣ f
hgP : a ∉ P
map_dvd_pow_q : map (algebraMap R K) (C a) ∣ map (algebraMap R K) q ^ p
hf : Associated (map (algebraMap R K) (C a)) (map (algebraMap R K) q ^ m)
r : R[X] := C a - C (C a).leadingCoeff * q ^ m
hg : C a = C (C a).leadingCoeff + r
hr : map (algebraMap R K) r = 0
this : (C a).natDegree = 0
⊢ C a ∣ f

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
m : ℕ
hm✝ : m ≤ p
hm : m = 0
a : R
hg_div : C a ∣ f
hgP : a ∉ P
map_dvd_pow_q : map (algebraMap R K) (C a) ∣ map (algebraMap R K) q ^ p
hf : Associated (map (algebraMap R K) (C a)) (map (algebraMap R K) q ^ m)
r : R[X] := C a - C (C a).leadingCoeff * q ^ m
hg : C a = C (C a).leadingCoeff + r
hr : map (algebraMap R K) r = 0
this : (C a).natDegree = 0
⊢ C a ∣ f
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree + ∑ i, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree + ∑ i, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff + r
hr : map (algebraMap R K) r = 0
hm : m = 0
hg' : ¬g.natDegree = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
φ : ℕ → R
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = (algebraMap R S) p * (-1 * ∑ i, (algebraMap R S) (φ ↑i) * x ^ ↑i)

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
φ : ℕ → R
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = (algebraMap R S) p * (-1 * ∑ i, (algebraMap R S) (φ ↑i) * x ^ ↑i)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : (aeval x) f = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : (aeval x) f = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : (aeval x) f = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
y : S
hy : y ∈ R[x]
H : (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
⊢ x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k = x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : f.IsRoot x
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ x ^ f.natDegree * x ^ k ∈ 𝓟

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : f.IsRoot x
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ x ^ f.natDegree * x ^ k ∈ 𝓟
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : x ^ f.natDegree + ∑ i, f.coeff ↑i * x ^ ↑i = 0
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ x ^ f.natDegree ∈ 𝓟

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : x ^ f.natDegree + ∑ i, f.coeff ↑i * x ^ ↑i = 0
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ x ^ f.natDegree ∈ 𝓟
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : x ^ f.natDegree + ∑ i, f.coeff ↑i * x ^ ↑i = 0
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ ∑ i, f.coeff ↑i * x ^ ↑i ∈ 𝓟

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : x ^ f.natDegree + ∑ i, f.coeff ↑i * x ^ ↑i = 0
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ ∑ i, f.coeff ↑i * x ^ ↑i ∈ 𝓟
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: A : Type u_2
inst✝² : CommRing A
C : Type u_5
inst✝¹ : SetLike C A
inst✝ : SubringClass C A
S : C
⊢ (∀ {x : A}, IsIntegral (↥S) x → ∃ y, (algebraMap (↥S) A) y = x) ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S

Tactic:
]

Goal state after:
A : Type u_2
inst✝² : CommRing A
C : Type u_5
inst✝¹ : SetLike C A
inst✝ : SubringClass C A
S : C
⊢ (∀ {x : A}, IsIntegral (↥S) x → ∃ y, (algebraMap (↥S) A) y = x) ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: A : Type u_2
inst✝² : CommRing A
C : Type u_5
inst✝¹ : SetLike C A
inst✝ : SubringClass C A
S : C
⊢ IsIntegrallyClosedIn (↥S) A ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S

Tactic:
rw [isIntegrallyClosedIn_iff, and_iff_right (FaithfulSMul.algebraMap_injective _ _)]
  exact congr(∀ _ _, _ ∈ $Subtype.range_val)

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: A : Type u_2
inst✝³ : CommRing A
C : Type u_5
inst✝² : SetLike C A
inst✝¹ : SubringClass C A
S : C
inst✝ : IsFractionRing (↥S) A
⊢ (∀ {x : A}, IsIntegral (↥S) x → ∃ y, (algebraMap (↥S) A) y = x) ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S

Tactic:
]

Goal state after:
A : Type u_2
inst✝³ : CommRing A
C : Type u_5
inst✝² : SetLike C A
inst✝¹ : SubringClass C A
S : C
inst✝ : IsFractionRing (↥S) A
⊢ (∀ {x : A}, IsIntegral (↥S) x → ∃ y, (algebraMap (↥S) A) y = x) ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: A : Type u_2
inst✝³ : CommRing A
C : Type u_5
inst✝² : SetLike C A
inst✝¹ : SubringClass C A
S : C
T : Subring A
inst✝ : IsIntegrallyClosedIn (↥T) A
⊢ (∀ (a : A) (b : a ∈ S), (algebraMap (↥S) A) ⟨a, b⟩ ∈ T) ↔ ∀ ⦃x : A⦄, x ∈ ofClass S → x ∈ T

Tactic:
]

Goal state after:
A : Type u_2
inst✝³ : CommRing A
C : Type u_5
inst✝² : SetLike C A
inst✝¹ : SubringClass C A
S : C
T : Subring A
inst✝ : IsIntegrallyClosedIn (↥T) A
⊢ (∀ (a : A) (b : a ∈ S), (algebraMap (↥S) A) ⟨a, b⟩ ∈ T) ↔ ∀ ⦃x : A⦄, x ∈ ofClass S → x ∈ T
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (aeval x) f = 0
hmo : f.Monic
this : x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
⊢ x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k ∈ Ideal.map (algebraMap R S) 𝓟

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (aeval x) f = 0
hmo : f.Monic
this : x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
⊢ x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k ∈ Ideal.map (algebraMap R S) 𝓟
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n✝ : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n✝ + s
hs : map (algebraMap R K) s = 0
hn0 : n✝ = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n✝ = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
⊢ r.coeff x.1 * s.coeff x.2 ∈ P * P

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n✝ : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n✝ + s
hs : map (algebraMap R K) s = 0
hn0 : n✝ = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n✝ = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
⊢ r.coeff x.1 * s.coeff x.2 ∈ P * P
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (Polynomial.map (algebraMap R S) f).IsRoot x
hmo : f.Monic
⊢ x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (Polynomial.map (algebraMap R S) f).IsRoot x
hmo : f.Monic
⊢ x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : IsIntegrallyClosedIn R A
x : A
hx : x ∈ integralClosure R A
⊢ ∃ y, (algebraMap R A) y = x

Tactic:
]

Goal state after:
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : IsIntegrallyClosedIn R A
x : A
hx : x ∈ integralClosure R A
⊢ ∃ y, (algebraMap R A) y = x
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < (p.scaleRoots x).natDegree
⊢ p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < (p.scaleRoots x).natDegree
⊢ p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : 0 < p.natDegree - n✝
⊢ p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : 0 < p.natDegree - n✝
⊢ p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ y ^ (p.scaleRoots x).natDegree ∈ span {x}

Tactic:
]

Goal state after:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ y ^ (p.scaleRoots x).natDegree ∈ span {x}
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_4
K : Type u_5
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : FaithfulSMul R K
inst✝ : IsIntegrallyClosedIn R K
this : IsDomain R
f : FractionRing R →ₐ[R] K := IsFractionRing.liftAlgHom ⋯
⊢ ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, (algebraMap R (FractionRing R)) y = x

Tactic:
]

Goal state after:
R : Type u_4
K : Type u_5
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : FaithfulSMul R K
inst✝ : IsIntegrallyClosedIn R K
this : IsDomain R
f : FractionRing R →ₐ[R] K := IsFractionRing.liftAlgHom ⋯
⊢ ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, (algebraMap R (FractionRing R)) y = x
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), f a = 0 ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ (p.scaleRoots x).IsRoot y

Tactic:
]

Goal state after:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), f a = 0 ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ (p.scaleRoots x).IsRoot y
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), f a = 0 ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
this : eval y (p.scaleRoots x) = 0
⊢ (p.scaleRoots x).IsRoot y

Tactic:
]

Goal state after:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), f a = 0 ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
this : eval y (p.scaleRoots x) = 0
⊢ (p.scaleRoots x).IsRoot y
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case hr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n✝ : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n✝ + s
hs : map (algebraMap R K) s = 0
hn0 : n✝ = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n✝ = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case refine_1
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : CommRing U
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : Algebra R U
inst✝⁵ : Algebra S U
inst✝⁴ : Algebra T U
inst✝³ : IsScalarTower S T U
inst✝² : IsScalarTower R T U
inst✝¹ : IsIntegralClosure S R T
inst✝ : IsIntegrallyClosedIn T U
⊢ Function.Injective ⇑((algebraMap T U).comp (algebraMap S T))

Tactic:
]

Goal state after:
case refine_1
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : CommRing U
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : Algebra R U
inst✝⁵ : Algebra S U
inst✝⁴ : Algebra T U
inst✝³ : IsScalarTower S T U
inst✝² : IsScalarTower R T U
inst✝¹ : IsIntegralClosure S R T
inst✝ : IsIntegrallyClosedIn T U
⊢ Function.Injective ⇑((algebraMap T U).comp (algebraMap S T))
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: case inr
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
h₂ : f.natDegree < n
⊢ 0 ∈ 𝓟

Tactic:
]

Goal state after:
case inr
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
h₂ : f.natDegree < n
⊢ 0 ∈ 𝓟
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case refine_2.refine_1
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : CommRing U
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : Algebra R U
inst✝⁵ : Algebra S U
inst✝⁴ : Algebra T U
inst✝³ : IsScalarTower S T U
inst✝² : IsScalarTower R T U
inst✝¹ : IsIntegralClosure S R T
inst✝ : IsIntegrallyClosedIn T U
x : T
h : IsIntegral R x
⊢ ∃ y, (algebraMap S U) y = (algebraMap T U) x

Tactic:
]

Goal state after:
case refine_2.refine_1
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : CommRing U
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : Algebra R U
inst✝⁵ : Algebra S U
inst✝⁴ : Algebra T U
inst✝³ : IsScalarTower S T U
inst✝² : IsScalarTower R T U
inst✝¹ : IsIntegralClosure S R T
inst✝ : IsIntegrallyClosedIn T U
x : T
h : IsIntegral R x
⊢ ∃ y, (algebraMap S U) y = (algebraMap T U) x
Module: Mathlib.Algebra.GCDMonoid.IntegrallyClosed

Goal state before:
pp: case right
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : GCDMonoid R
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ mk' A (y' * x) ⟨y, hy⟩ = (algebraMap R A) x'

Tactic:
]

Goal state after:
case right
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : GCDMonoid R
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ mk' A (y' * x) ⟨y, hy⟩ = (algebraMap R A) x'
Module: Mathlib.Algebra.GCDMonoid.IntegrallyClosed

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
a✝ : GCDMonoid R
x y : R
hg : IsUnit (gcd x y)
he : X * (algebraMap R (FractionRing R)) y = (algebraMap R (FractionRing R)) x
⊢ (algebraMap R (FractionRing R)) x = (algebraMap R (FractionRing R)) x

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case refine_2.refine_2
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : CommRing U
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : Algebra R U
inst✝⁵ : Algebra S U
inst✝⁴ : Algebra T U
inst✝³ : IsScalarTower S T U
inst✝² : IsScalarTower R T U
inst✝¹ : IsIntegralClosure S R T
inst✝ : IsIntegrallyClosedIn T U
x : S
⊢ IsIntegral R ((algebraMap T U) ((algebraMap S T) x))

Tactic:
]

Goal state after:
case refine_2.refine_2
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : CommRing U
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : Algebra R U
inst✝⁵ : Algebra S U
inst✝⁴ : Algebra T U
inst✝³ : IsScalarTower S T U
inst✝² : IsScalarTower R T U
inst✝¹ : IsIntegralClosure S R T
inst✝ : IsIntegrallyClosedIn T U
x : S
⊢ IsIntegral R ((algebraMap T U) ((algebraMap S T) x))