mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
inst✝ : IsScalarTower R A B
f : R[X]
hf : (map (algebraMap R A) f).Splits
⊢ Multiset.map (⇑(algebraMap A B)) (map (algebraMap R A) f).roots =
    Multiset.map (⇑(algebraMap A B)) (map (algebraMap R A) f).roots

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
inst✝ : IsScalarTower R A B
f : R[X]
hf : (map (algebraMap R A) f).Splits
⊢ f.rootSet B = f.rootSet B

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f g : R[X]
hp : f.Splits
hp0 : f ≠ 0
hq : f.roots ≤ g.roots
⊢ (Multiset.map (fun x ↦ X - C x) f.roots).prod ∣ g

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Field R
f g : R[X]
hp : f.Splits
hp0 : f ≠ 0
hq : f.roots ≤ g.roots
⊢ (Multiset.map (fun x ↦ X - C x) f.roots).prod ∣ g
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
⊢ ∀ (n : ℕ),
    (p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))).coeff n ∈ Set.range ⇑(algebraMap R Rₘ)

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
⊢ ∀ (n : ℕ),
    (p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))).coeff n ∈ Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Ring B
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R ↑p.coeffs
this : Module.Finite R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
⊢ eval₂ (algebraMap A B) x (Polynomial.map (algebraMap (↥S) A) p') = 0

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Ring B
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R ↑p.coeffs
this : Module.Finite R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
⊢ eval₂ (algebraMap A B) x (Polynomial.map (algebraMap (↥S) A) p') = 0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
⊢ f = f

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
this : f = (f.comp (C a * X + C b)).comp (C a⁻¹ * (X - C b))
⊢ ((f.comp (C a * X + C b)).comp (C a⁻¹ * (X - C b))).Splits

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
this : f = (f.comp (C a * X + C b)).comp (C a⁻¹ * (X - C b))
⊢ ((f.comp (C a * X + C b)).comp (C a⁻¹ * (X - C b))).Splits
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
this : f = (f.comp (C a * X + C b)).comp (C a⁻¹ * (X - C b))
⊢ 1 ≤ 1

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : n = p.natDegree
⊢ p.leadingCoeff ∈ Set.range ⇑(algebraMap R Rₘ)

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : n = p.natDegree
⊢ p.leadingCoeff ∈ Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Ring B
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R ↑p.coeffs
this✝ : Module.Finite R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
hSx : IsIntegral (↥S) x
Sx : Submodule (↥S) B := Subalgebra.toSubmodule (↥S)[x]
MSx : Module ↥S ↥Sx := SMulMemClass.toModule Sx
this : Module.Finite ↥S ↥Sx
⊢ Module.Finite R ↥(Subalgebra.toSubmodule (Subalgebra.restrictScalars R (↥S)[x]))

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Ring B
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R ↑p.coeffs
this✝ : Module.Finite R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
hSx : IsIntegral (↥S) x
Sx : Submodule (↥S) B := Subalgebra.toSubmodule (↥S)[x]
MSx : Module ↥S ↥Sx := SMulMemClass.toModule Sx
this : Module.Finite ↥S ↥Sx
⊢ Module.Finite R ↥(Subalgebra.toSubmodule (Subalgebra.restrictScalars R (↥S)[x]))
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
z : R
hz : z ∈ f.roots
⊢ f.leadingCoeff * (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase z)).prod =
    f.leadingCoeff * (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase z)).prod

pp: case ha
R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
z : R
hz : z ∈ f.roots
⊢ x - z ≠ 0

Tactic:
]

Goal state after:
case ha
R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
z : R
hz : z ∈ f.roots
⊢ x - z ≠ 0
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing T
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsTorsionFree S T
inst✝¹ : Nontrivial T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ (algebraMap R T).IsIntegral

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing T
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsTorsionFree S T
inst✝¹ : Nontrivial T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ (algebraMap R T).IsIntegral
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
x : T
h : (g.comp f).IsIntegralElem x
p : R[X]
hp : p.Monic
hp' : eval₂ g x (Polynomial.map f p) = 0
⊢ eval₂ g x (Polynomial.map f p) = 0

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
x : T
h : (g.comp f).IsIntegralElem x
p : R[X]
hp : p.Monic
hp' : eval₂ g x (Polynomial.map f p) = 0
⊢ eval₂ g x (Polynomial.map f p) = 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ (algebraMap R Rₘ) (↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n - 1)) *
      ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) * p.coeff n) ∈
    Set.range ⇑(algebraMap R Rₘ)

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ (algebraMap R Rₘ) (↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n - 1)) *
      ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) * p.coeff n) ∈
    Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ (algebraMap R T).IsIntegral

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ (algebraMap R T).IsIntegral
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
⊢ (Multiset.map (fun z ↦ 1 / (x - z)) f.roots).sum = (Multiset.map (fun z ↦ 1 / (x - z)) f.roots).sum

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
⊢ 2 - 1 = 1

Tactic:
]

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

Goal state before:
pp: case neg.a
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ ↑(commonDenom M p.support p.coeff) • p.coeff n ∈ (algebraMap R Rₘ).range

Tactic:
]

Goal state after:
case neg.a
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ ↑(commonDenom M p.support p.coeff) • p.coeff n ∈ (algebraMap R Rₘ).range
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
h : (f /ₘ (X - C x)).natDegree = 1
⊢ (X - C x).Splits ∧ (f /ₘ (X - C x)).Splits

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
h : (f /ₘ (X - C x)).natDegree = 1
⊢ (X - C x).Splits ∧ (f /ₘ (X - C x)).Splits
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : p.coeff n = 0
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : p.coeff n = 0
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
hf0 : ¬f = 0
u : R[X]ˣ
hu : (factors f).prod * ↑u = f
⊢ ((factors f).prod * ↑u).Splits

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝ : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
hf0 : ¬f = 0
u : R[X]ˣ
hu : (factors f).prod * ↑u = f
⊢ ((factors f).prod * ↑u).Splits
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : p.coeff n = 0
⊢ 0 ∈ Set.range ⇑(algebraMap R Rₘ)

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : p.coeff n = 0
⊢ 0 ∈ Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective ⇑f
a : R
ha : IsUnit (f a)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (⅟↑ha.unit⁻¹) p.reverse = 0
⊢ eval₂ f (f a) p.reverse = 0

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective ⇑f
a : R
ha : IsUnit (f a)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (⅟↑ha.unit⁻¹) p.reverse = 0
⊢ eval₂ f (f a) p.reverse = 0
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
k : Type u_6
inst✝² : Field k
inst✝¹ : Algebra R k
inst✝ : Algebra.IsIntegral R k
this : ⊥.IsMaximal
⊢ IsField (R ⧸ Ideal.comap (algebraMap R k) ⊥)

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
k : Type u_6
inst✝² : Field k
inst✝¹ : Algebra R k
inst✝ : Algebra.IsIntegral R k
this : ⊥.IsMaximal
⊢ IsField (R ⧸ Ideal.comap (algebraMap R k) ⊥)
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r p.divX * r + f (p.coeff 0) ∈ I
⊢ p.coeff 0 ∈ comap f I

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r p.divX * r + f (p.coeff 0) ∈ I
⊢ p.coeff 0 ∈ comap f I
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
⊢ (Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤) ↔ Flat R M ∧ ∀ (I : Ideal R), I ≠ ⊤ → I • ⊤ ≠ ⊤

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤) ↔ Flat R M ∧ ∀ (I : Ideal R), I ≠ ⊤ → I • ⊤ ≠ ⊤
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case pos
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := (R ∙ n).annihilator
I_ne_top : n = 0
⊢ Nontrivial (N ⊗[R] M)

Tactic:
]

Goal state after:
case pos
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := (R ∙ n).annihilator
I_ne_top : n = 0
⊢ Nontrivial (N ⊗[R] M)
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_3
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, (p * X).coeff i ≠ 0 ∧ (p * X).coeff i ∈ comap f I

Tactic:
]

Goal state after:
case refine_3
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, (p * X).coeff i ≠ 0 ∧ (p * X).coeff i ∈ comap f I
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case inr.refine_3
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' : R[X]
hp'₁ : Polynomial.map (algebraMap R Rₘ) p' = p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))
hp'₂ : p'.Monic
⊢ eval₂ (algebraMap Rₘ S) ((algebraMap Rₘ S) ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff)) * x)
      (p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))) =
    0

Tactic:
]

Goal state after:
case inr.refine_3
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' : R[X]
hp'₁ : Polynomial.map (algebraMap R Rₘ) p' = p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))
hp'₂ : p'.Monic
⊢ eval₂ (algebraMap Rₘ S) ((algebraMap Rₘ S) ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff)) * x)
      (p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))) =
    0
Module: Mathlib.RingTheory.Ideal.GoingUp

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

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ P ⊔ comap (mapRingHom (Quotient.mk (comap C P))) ⊥ = P
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
⊢ 1 ∈ (algebraMap R Rₘ).range

Tactic:
]

Goal state after:
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
⊢ 1 ∈ (algebraMap R Rₘ).range
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), C x ∈ P → x = 0
m : ↥P
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ comap C P = ⊥

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), C x ∈ P → x = 0
m : ↥P
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ comap C P = ⊥
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case neg
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := (R ∙ n).annihilator
I_ne_top : ¬I = ⊤
inc : R ⧸ I →ₗ[R] N := Submodule.liftQ I ((LinearMap.lsmul R N).flip n) ⋯
injective_inc : Function.Injective ⇑inc
ne_top : I • ⊤ ≠ ⊤
rid : Subsingleton (N ⊗[R] M)
⊢ Subsingleton (M ⧸ I • ⊤)

Tactic:
]

Goal state after:
case neg
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := (R ∙ n).annihilator
I_ne_top : ¬I = ⊤
inc : R ⧸ I →ₗ[R] N := Submodule.liftQ I ((LinearMap.lsmul R N).flip n) ⋯
injective_inc : Function.Injective ⇑inc
ne_top : I • ⊤ ≠ ⊤
rid : Subsingleton (N ⊗[R] M)
⊢ Subsingleton (M ⧸ I • ⊤)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
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.Monic

Tactic:
]

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.Monic