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

Goal state before:
pp: case e'_5.hX
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 α →₀ ℕ
i : Option α
m : Option α →₀ ℕ
⊢ coeff m
      ((((optionEquivLeft S α).symm.toRingEquiv.toRingHom.comp
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S)))).comp
          (optionEquivLeft R α).toRingEquiv.toRingHom)
        (X i)) =
    coeff m ((algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)) (X i))

Tactic:
·

Goal state after:
case e'_5.hX
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 α →₀ ℕ
i : Option α
m : Option α →₀ ℕ
⊢ coeff m
      ((((optionEquivLeft S α).symm.toRingEquiv.toRingHom.comp
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S)))).comp
          (optionEquivLeft R α).toRingEquiv.toRingHom)
        (X i)) =
    coeff m ((algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)) (X i))
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case e'_6
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 ((optionEquivLeft S α) f) = f

Tactic:
·

Goal state after:
case e'_6
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 ((optionEquivLeft S α) f) = f
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
⊢ QuasiFiniteAt A (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q))) q)

Tactic:
let φ : A ⊗[R] S →ₐ[A] (A ⧸ q.under A) ⊗[R] (S ⧸ (p.under R).map (algebraMap R S)) :=
    Algebra.TensorProduct.map (Ideal.Quotient.mkₐ _ _) (Ideal.Quotient.mkₐ _ _)

Goal state after:
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)))
⊢ QuasiFiniteAt A (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q))) q)
Module: Mathlib.RingTheory.QuasiFinite.Polynomial

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
inst✝ : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R[X]) [inst_1 : P.IsPrime],
    Algebra.WeaklyQuasiFiniteAt R P → IsField R → False
hR : ¬IsField R
⊢ False

pp: R✝ : Type u_1
inst✝² : CommRing R✝
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
inst✝ : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
hR : IsField R
⊢ False

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
inst✝ : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R[X]) [inst_1 : P.IsPrime],
    Algebra.WeaklyQuasiFiniteAt R P → IsField R → False
hR : ¬IsField R
⊢ False
Module: Mathlib.RingTheory.QuasiFinite.Polynomial

Goal state before:
pp: case refine_1
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
algInst✝ : Algebra R[X] S := f.toAlgebra
⊢ Ideal.under R P ≤ Ideal.comap C (Ideal.comap (↑f) P)

pp: case refine_2
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
algInst✝ : Algebra R[X] S := f.toAlgebra
e : Ideal.map C (Ideal.under R P) = Ideal.comap (↑f) P
⊢ False

Tactic:
·

Goal state after:
case refine_1
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
algInst✝ : Algebra R[X] S := f.toAlgebra
⊢ Ideal.under R P ≤ Ideal.comap C (Ideal.comap (↑f) P)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_3
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)
⊢ (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField) X)) ⋯).comp { toRingHom := f, commutes' := ⋯ } =
    AlgHom.id I.ResidueField J.ResidueField

Tactic:
·

Goal state after:
case refine_3
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)
⊢ (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField) X)) ⋯).comp { toRingHom := f, commutes' := ⋯ } =
    AlgHom.id I.ResidueField J.ResidueField
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_3.h₁
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✝ : R
⊢ (((↑((RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField) X)) ⋯).comp
                  { toRingHom := f, commutes' := ⋯ })).comp
            (algebraMap R[X] J.ResidueField)).comp
        C)
      x✝ =
    (((↑(AlgHom.id I.ResidueField J.ResidueField)).comp (algebraMap R[X] J.ResidueField)).comp C) x✝

pp: case h₂
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 := ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
⊢ ((↑((RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField) X)) ⋯).comp { toRingHom := f, commutes' := ⋯ })).comp
        (algebraMap R[X] J.ResidueField))
      X =
    ((↑(AlgHom.id I.ResidueField J.ResidueField)).comp (algebraMap R[X] J.ResidueField)) X

Tactic:
·

Goal state after:
case refine_3.h₁
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✝ : R
⊢ (((↑((RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField) X)) ⋯).comp
                  { toRingHom := f, commutes' := ⋯ })).comp
            (algebraMap R[X] J.ResidueField)).comp
        C)
      x✝ =
    (((↑(AlgHom.id I.ResidueField J.ResidueField)).comp (algebraMap R[X] J.ResidueField)).comp C) x✝
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case h₂
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 := ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
⊢ ((↑((RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField) X)) ⋯).comp { toRingHom := f, commutes' := ⋯ })).comp
        (algebraMap R[X] J.ResidueField))
      X =
    ((↑(AlgHom.id I.ResidueField J.ResidueField)).comp (algebraMap R[X] J.ResidueField)) X

Tactic:
·

Goal state after:
case h₂
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 := ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
⊢ ((↑((RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField) X)) ⋯).comp { toRingHom := f, commutes' := ⋯ })).comp
        (algebraMap R[X] J.ResidueField))
      X =
    ((↑(AlgHom.id I.ResidueField J.ResidueField)).comp (algebraMap R[X] J.ResidueField)) X
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_2
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
⊢ ∀ a ∈ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f), (aeval (1 ⊗ₜ[R] f X)) a = 0

pp: case refine_3
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
⊢ (Algebra.TensorProduct.lift
          (Algebra.ofId p.ResidueField
            (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)))
          (f.liftOfSurjective hf
            ((Ideal.Quotient.mkₐ R (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))).comp
              (mapAlgHom (Algebra.ofId R p.ResidueField)))
            ⋯)
          ⋯).comp
      (Ideal.Quotient.liftₐ (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))
        (aeval (1 ⊗ₜ[R] f X)) ?refine_2) =
    AlgHom.id p.ResidueField (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))

pp: case refine_4
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
⊢ (Ideal.Quotient.liftₐ (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)) (aeval (1 ⊗ₜ[R] f X))
          ?refine_2).comp
      (Algebra.TensorProduct.lift
        (Algebra.ofId p.ResidueField
          (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)))
        (f.liftOfSurjective hf
          ((Ideal.Quotient.mkₐ R (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))).comp
            (mapAlgHom (Algebra.ofId R p.ResidueField)))
          ⋯)
        ⋯) =
    AlgHom.id p.ResidueField (p.Fiber S)

Tactic:
·

Goal state after:
case refine_2
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
⊢ ∀ a ∈ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f), (aeval (1 ⊗ₜ[R] f X)) a = 0
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_3
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
⊢ (Algebra.TensorProduct.lift
          (Algebra.ofId p.ResidueField
            (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)))
          (f.liftOfSurjective hf
            ((Ideal.Quotient.mkₐ R (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))).comp
              (mapAlgHom (Algebra.ofId R p.ResidueField)))
            ⋯)
          ⋯).comp
      (Ideal.Quotient.liftₐ (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))
        (aeval (1 ⊗ₜ[R] f X)) ⋯) =
    AlgHom.id p.ResidueField (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))

pp: case refine_4
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
⊢ (Ideal.Quotient.liftₐ (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)) (aeval (1 ⊗ₜ[R] f X))
          ⋯).comp
      (Algebra.TensorProduct.lift
        (Algebra.ofId p.ResidueField
          (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)))
        (f.liftOfSurjective hf
          ((Ideal.Quotient.mkₐ R (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))).comp
            (mapAlgHom (Algebra.ofId R p.ResidueField)))
          ⋯)
        ⋯) =
    AlgHom.id p.ResidueField (p.Fiber S)

Tactic:
·

Goal state after:
case refine_3
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
⊢ (Algebra.TensorProduct.lift
          (Algebra.ofId p.ResidueField
            (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)))
          (f.liftOfSurjective hf
            ((Ideal.Quotient.mkₐ R (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))).comp
              (mapAlgHom (Algebra.ofId R p.ResidueField)))
            ⋯)
          ⋯).comp
      (Ideal.Quotient.liftₐ (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))
        (aeval (1 ⊗ₜ[R] f X)) ⋯) =
    AlgHom.id p.ResidueField (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_4
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
⊢ (Ideal.Quotient.liftₐ (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)) (aeval (1 ⊗ₜ[R] f X))
          ⋯).comp
      (Algebra.TensorProduct.lift
        (Algebra.ofId p.ResidueField
          (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)))
        (f.liftOfSurjective hf
          ((Ideal.Quotient.mkₐ R (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))).comp
            (mapAlgHom (Algebra.ofId R p.ResidueField)))
          ⋯)
        ⋯) =
    AlgHom.id p.ResidueField (p.Fiber S)

Tactic:
·

Goal state after:
case refine_4
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
⊢ (Ideal.Quotient.liftₐ (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)) (aeval (1 ⊗ₜ[R] f X))
          ⋯).comp
      (Algebra.TensorProduct.lift
        (Algebra.ofId p.ResidueField
          (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)))
        (f.liftOfSurjective hf
          ((Ideal.Quotient.mkₐ R (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))).comp
            (mapAlgHom (Algebra.ofId R p.ResidueField)))
          ⋯)
        ⋯) =
    AlgHom.id p.ResidueField (p.Fiber S)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = Ideal.span {p}
this✝¹ : Algebra (R ⧸ P)[X] P.ResidueField[X] := (mapRingHom (algebraMap (R ⧸ P) P.ResidueField)).toAlgebra
this✝ : IsLocalization (Submonoid.map C (R ⧸ P)⁰) P.ResidueField[X]
this : p ∈ Ideal.map (algebraMap (R ⧸ P)[X] P.ResidueField[X]) (Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I)
s : ↥(Submonoid.map C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr : (mapRingHom (algebraMap R (R ⧸ P))) r ∈ Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I
e : p * map (algebraMap (R ⧸ P) P.ResidueField) ↑s = map (algebraMap R P.ResidueField) r
⊢ Ideal.span {map (algebraMap R P.ResidueField) r} ≤ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I

pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = Ideal.span {p}
this✝¹ : Algebra (R ⧸ P)[X] P.ResidueField[X] := (mapRingHom (algebraMap (R ⧸ P) P.ResidueField)).toAlgebra
this✝ : IsLocalization (Submonoid.map C (R ⧸ P)⁰) P.ResidueField[X]
this : p ∈ Ideal.map (algebraMap (R ⧸ P)[X] P.ResidueField[X]) (Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I)
s : ↥(Submonoid.map C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr : (mapRingHom (algebraMap R (R ⧸ P))) r ∈ Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I
e : p * map (algebraMap (R ⧸ P) P.ResidueField) ↑s = map (algebraMap R P.ResidueField) r
⊢ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I ≤ Ideal.span {map (algebraMap R P.ResidueField) r}

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = Ideal.span {p}
this✝¹ : Algebra (R ⧸ P)[X] P.ResidueField[X] := (mapRingHom (algebraMap (R ⧸ P) P.ResidueField)).toAlgebra
this✝ : IsLocalization (Submonoid.map C (R ⧸ P)⁰) P.ResidueField[X]
this : p ∈ Ideal.map (algebraMap (R ⧸ P)[X] P.ResidueField[X]) (Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I)
s : ↥(Submonoid.map C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr : (mapRingHom (algebraMap R (R ⧸ P))) r ∈ Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I
e : p * map (algebraMap (R ⧸ P) P.ResidueField) ↑s = map (algebraMap R P.ResidueField) r
⊢ Ideal.span {map (algebraMap R P.ResidueField) r} ≤ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I