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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
hx : (aeval ((algebraMap R[X] J.ResidueField) X)) x = 0
r : R[X]
hr : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hb0 : (Ideal.Quotient.mk I) s ∈ (R ⧸ I)⁰
hb :
  map (algebraMap (R ⧸ I) I.ResidueField) (IsLocalization.integerNormalization (R ⧸ I)⁰ x) = (Ideal.Quotient.mk I) s • x
⊢ s ∉ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : QuasiFinite R (Localization.AtPrime p ⧸ Ideal.map (algebraMap R (Localization.AtPrime p)) (Ideal.under R p))
q : Ideal T
inst✝ : q.IsPrime
f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q
hf : Function.Surjective ⇑f
x : R
hx : x ∈ Ideal.under R p
hx' : x ∉ Ideal.under R q
this✝ : IsLocalHom f.toRingHom
this : IsUnit (IsLocalization.mk' (Localization.AtPrime q) ((algebraMap R T) x) 1)
⊢ IsUnit (f.toRingHom ((algebraMap R (Localization.AtPrime p)) x))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
hx : (aeval ((algebraMap R[X] J.ResidueField) X)) x = 0
r : R[X]
hr : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
⊢ ∃ s ∉ I, map (algebraMap R I.ResidueField) r = s • x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : QuasiFinite R (Localization.AtPrime p ⧸ Ideal.map (algebraMap R (Localization.AtPrime p)) (Ideal.under R p))
q : Ideal T
inst✝ : q.IsPrime
f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q
hf : Function.Surjective ⇑f
x : R
hx : x ∈ Ideal.under R p
hx' : x ∉ Ideal.under R q
this : IsLocalHom f.toRingHom
⊢ IsUnit (f.toRingHom ((algebraMap R (Localization.AtPrime p)) x))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : QuasiFinite R (Localization.AtPrime p ⧸ Ideal.map (algebraMap R (Localization.AtPrime p)) (Ideal.under R p))
q : Ideal T
inst✝ : q.IsPrime
f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q
hf : Function.Surjective ⇑f
x : R
hx : x ∈ Ideal.under R p
hx' : x ∉ Ideal.under R q
this✝ : IsLocalHom f.toRingHom
this : IsUnit ((algebraMap R (Localization.AtPrime p)) x)
⊢ IsUnit (IsLocalization.mk' (Localization.AtPrime p) ((algebraMap R S) x) 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
α β : Type w
e : α ≃ β
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial β S
H : (algebraMap (MvPolynomial β R) (MvPolynomial β S)).IsIntegralElem f
n : β →₀ ℕ
⊢ (((rename ⇑e).comp (algebraMap (MvPolynomial α R) (MvPolynomial α S))).comp (rename ⇑e.symm).toRingHom).IsIntegralElem
    ((rename ⇑e).toRingHom ((rename ⇑e.symm) f))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : QuasiFinite R (Localization.AtPrime p ⧸ Ideal.map (algebraMap R (Localization.AtPrime p)) (Ideal.under R p))
q : Ideal T
inst✝ : q.IsPrime
f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q
hf : Function.Surjective ⇑f
⊢ Ideal.map (algebraMap R (Localization.AtPrime p)) (Ideal.under R p) ≤
    Ideal.comap f.toRingHom (Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
hx : (aeval ((algebraMap R[X] J.ResidueField) X)) x = 0
r : R[X]
hr✝ : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hs : s ∉ I
hr : map (algebraMap R I.ResidueField) r = s • x
⊢ r ∈ J

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
r : R[X]
hr✝ : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hs : s ∉ I
hr : map (algebraMap R I.ResidueField) r = s • x
hx : r ∈ J
⊢ (algebraMap R I.ResidueField) s ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : WeaklyQuasiFiniteAt R p
q : Ideal T
inst✝ : q.IsPrime
f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q
hf : Function.Surjective ⇑f
⊢ WeaklyQuasiFiniteAt R q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : WeaklyQuasiFiniteAt R p
q : Ideal T
inst✝ : q.IsPrime
f : S →ₐ[R] T
hf : f.SurjectiveOnStalks
hq : p = Ideal.comap f q
⊢ WeaklyQuasiFiniteAt R q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
p✝ : Ideal R
q : Ideal S
inst✝² : q.IsPrime
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : T ≃ₐ[R] S
⊢ p = Ideal.comap (↑f.symm) (Ideal.comap f.toRingEquiv.toRingHom p)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
⊢ constantCoeff = (isEmptyAlgEquiv S PEmpty.{?u.342 + 1}).toRingEquiv.toRingHom

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁵ : q.IsPrime
inst✝⁴ : p.IsPrime
inst✝³ : q.LiesOver p
inst✝² : WeaklyQuasiFiniteAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
⊢ Module.Finite p.ResidueField q.ResidueField

Tactic:
let r := q.map (Ideal.Quotient.mk ((q.under R).map (algebraMap R S)))

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁵ : q.IsPrime
inst✝⁴ : p.IsPrime
inst✝³ : q.LiesOver p
inst✝² : WeaklyQuasiFiniteAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
r : Ideal (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R q)) :=
  Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R q))) q
⊢ Module.Finite p.ResidueField q.ResidueField
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁵ : q.IsPrime
inst✝⁴ : p.IsPrime
inst✝³ : q.LiesOver p
inst✝² : WeaklyQuasiFiniteAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
r : Ideal (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R q)) :=
  Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R q))) q
⊢ q = q ⊔ Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R q))) ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁵ : q.IsPrime
inst✝⁴ : p.IsPrime
inst✝³ : q.LiesOver p
inst✝² : WeaklyQuasiFiniteAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
⊢ Module.Finite p.ResidueField q.ResidueField

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: S : Type u_2
inst✝⁴ : CommRing S
q : Ideal S
inst✝³ : q.IsPrime
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : WeaklyQuasiFiniteAt K q
⊢ Module.Finite K (Localization.AtPrime q)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : WeaklyQuasiFiniteAt R Q
⊢ RingHom.ker (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) ≤ P

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : WeaklyQuasiFiniteAt R Q
this : (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P).IsPrime
⊢ Ideal.under R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P) =
    Ideal.under R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) Q)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst✝ : Fintype α
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial (Option α) S
H : (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f
n : Option α →₀ ℕ
⊢ (((optionEquivLeft S α).symm.toRingEquiv.toRingHom.comp
            (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S)))).comp
        (optionEquivLeft R α).toRingEquiv.toRingHom).IsIntegralElem
    ((optionEquivLeft S α).symm.toRingEquiv.toRingHom ((optionEquivLeft S α) f))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : WeaklyQuasiFiniteAt R Q
⊢ P = Q

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
⊢ IsIntegral (MvPolynomial σ R) f ↔ ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
inst✝ : P.IsPrime
⊢ ¬Algebra.WeaklyQuasiFiniteAt R P

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
φ : A ⊗[R] S →ₐ[A] (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₁ : Function.Surjective ⇑φ
⊢ RingHom.ker φ.toRingHom = Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Algebra.WeaklyQuasiFiniteAt R P
⊢ Ideal.map C (Ideal.under R P) < Ideal.comap (↑f) P

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Algebra.WeaklyQuasiFiniteAt R P
H : RingHom.ker f ≤ Ideal.map C (Ideal.under R P)
algInst✝ : Algebra R[X] S := f.toAlgebra
p : Ideal R := Ideal.under R P
⊢ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker f) = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Algebra.WeaklyQuasiFiniteAt R P
⊢ ¬RingHom.ker f ≤ Ideal.map C (Ideal.under R P)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
φ : A ⊗[R] S →ₐ[A] (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₁ : Function.Surjective ⇑φ
hφ₂ : RingHom.ker φ.toRingHom = Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)
hφ₃ :
  φ.comp TensorProduct.includeRight.toRingHom =
    TensorProduct.includeRight.comp (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p)))
this : (Ideal.map φ.toRingHom q).IsPrime
⊢ Function.Surjective ⇑φ.toRingHom

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
⊢ J.ResidueField ≃ₐ[I.ResidueField] RatFunc I.ResidueField

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
p : R[X]
⊢ (residueFieldMapCAlgEquiv I J hJ) ((algebraMap R[X] J.ResidueField) p) =
    (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (map (algebraMap R I.ResidueField) p)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
⊢ (residueFieldMapCAlgEquiv I J hJ) ((residueFieldMapCAlgEquiv I J hJ).symm RatFunc.X) =
    (residueFieldMapCAlgEquiv I J hJ) ((algebraMap R[X] J.ResidueField) X)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
I : Ideal R
inst✝⁵ : I.IsPrime
J : Ideal R[X]
inst✝⁴ : J.IsPrime
inst✝³ : J.LiesOver I
inst✝² : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra I J
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
p : Ideal R
inst✝ : p.IsPrime
⊢ (AlgHom.restrictScalars R (aeval (1 ⊗ₜ[R] f X))).comp (mapAlgHom (Algebra.ofId R p.ResidueField)) =
    Algebra.TensorProduct.includeRight.comp f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
φ : A ⊗[R] S →ₐ[A] (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₁ : Function.Surjective ⇑φ
hφ₂ : RingHom.ker φ.toRingHom = Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)
hφ₃ :
  φ.comp TensorProduct.includeRight.toRingHom =
    TensorProduct.includeRight.comp (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p)))
this : (Ideal.map φ.toRingHom q).IsPrime
⊢ Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) p =
    Ideal.comap TensorProduct.includeRight.toRingHom (Ideal.map φ.toRingHom q)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
I : Ideal R
inst✝⁵ : I.IsPrime
J : Ideal R[X]
inst✝⁴ : J.IsPrime
inst✝³ : J.LiesOver I
inst✝² : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra I J
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
p : Ideal R
inst✝ : p.IsPrime
this :
  (AlgHom.restrictScalars R (aeval (1 ⊗ₜ[R] f X))).comp (mapAlgHom (Algebra.ofId R p.ResidueField)) =
    Algebra.TensorProduct.includeRight.comp f
⊢ RingHom.ker ↑f ≤ RingHom.ker (Algebra.TensorProduct.includeRight.comp f)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
φ : A ⊗[R] S →ₐ[A] (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₁ : Function.Surjective ⇑φ
hφ₂ : RingHom.ker φ.toRingHom = Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)
hφ₃ :
  φ.comp TensorProduct.includeRight.toRingHom =
    TensorProduct.includeRight.comp (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p)))
this✝¹ : (Ideal.map φ.toRingHom q).IsPrime
this✝ : QuasiFiniteAt (A ⧸ Ideal.under A q) (Ideal.map φ.toRingHom q)
this : QuasiFiniteAt A (Ideal.map φ.toRingHom q)
⊢ RingHom.ker φ = Ideal.map (↑AlgEquiv.refl) (Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
I : Ideal R
inst✝⁵ : I.IsPrime
J : Ideal R[X]
inst✝⁴ : J.IsPrime
inst✝³ : J.LiesOver I
inst✝² : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra I J
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
p : Ideal R
inst✝ : p.IsPrime
⊢ p.Fiber S ≃ₐ[p.ResidueField] p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
p : Ideal R
inst✝ : p.IsPrime
a : p.ResidueField
b : R[X]
⊢ (fiberEquivQuotient f hf p) (a ⊗ₜ[R] f b) =
    (Ideal.Quotient.mk (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)))
      (C a * map (algebraMap R p.ResidueField) b)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : WeaklyQuasiFiniteAt R p
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
⊢ WeaklyQuasiFiniteAt A q

Tactic:
by

Goal state after: