Module: Mathlib.RingTheory.LocalRing.ResidueField.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
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
⊢ RingHom.ker f.toRingHom ≤
    RingHom.ker
      ((Ideal.Quotient.mkₐ R (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))).comp
          (mapAlgHom (Algebra.ofId R p.ResidueField))).toRingHom

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)))
            ?refine_1)
          ⋯).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)))
          ?refine_1)
        ⋯) =
    AlgHom.id p.ResidueField (p.Fiber S)

Tactic:
· simp [AlgHom.comp_toRingHom, ← RingHom.comap_ker, ← Ideal.map_le_iff_le_comap]

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

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))

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)