awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
inst_8 : p.IsPrime
inst_9 : q.IsPrime
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_12 : Algebra.IsIntegral A B
this_1 : Algebra.IsIntegral.{u_2, u_3} (A ⧸ p) (B ⧸ q)
this_2 : Algebra.{u_2, u_3} (A ⧸ p) q.ResidueField :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ q) q.ResidueField)
      (algebraMap (A ⧸ p) (B ⧸ q)))
this_3 : IsScalarTower.{u_2, u_3, u_3} (A ⧸ p) (B ⧸ q) q.ResidueField
this_4 : Algebra.IsAlgebraic.{u_2, u_3} (A ⧸ p) q.ResidueField
this : IsScalarTower.{u_2, u_2, u_3} (A ⧸ p) p.ResidueField q.ResidueField
⊢ Algebra.IsAlgebraic.{u_2, u_3} p.ResidueField q.ResidueField

Tactic:
.extendScalars (Ideal.injective_algebraMap_quotient_residueField p)

Premises used: Algebra.IsAlgebraic.extendScalars, Ideal.injective_algebraMap_quotient_residueField
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
inst_8 : p.IsPrime
inst_9 : q.IsPrime
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_12 : Algebra.IsIntegral A B
this_1 : Algebra.IsIntegral.{u_2, u_3} (A ⧸ p) (B ⧸ q)
this_2 : Algebra.{u_2, u_3} (A ⧸ p) q.ResidueField :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ q) q.ResidueField)
      (algebraMap (A ⧸ p) (B ⧸ q)))
this_3 : IsScalarTower.{u_2, u_3, u_3} (A ⧸ p) (B ⧸ q) q.ResidueField
this_4 : Algebra.IsAlgebraic.{u_2, u_3} (A ⧸ p) q.ResidueField
this : IsScalarTower.{u_2, u_2, u_3} (A ⧸ p) p.ResidueField q.ResidueField
⊢ Algebra.IsAlgebraic.{u_2, u_3} p.ResidueField q.ResidueField

Tactic:
refine .extendScalars (Ideal.injective_algebraMap_quotient_residueField p)
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
Goal:
R_1 : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R_1
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R_1 A
inst_4 : Algebra A B
inst_5 : Algebra R_1 B
inst_6 : IsScalarTower R_1 A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
R : Type u_4
k : Type u_5
inst_8 : CommRing R
inst_9 : IsLocalRing R
inst_10 : Field k
inst_11 : Algebra R k
inst_12 : Algebra.IsIntegral R k
⊢ ∀ (a : R),
    Membership.mem (γ := Ideal R) (maximalIdeal R : Ideal R) a →
      Eq.{u_5 + 1} (α := k) (((algebraMap R k : R →+* k) : (a : R) → k) a : k) (0 : k)

Tactic:
simp [← eq_maximalIdeal (Algebra.ker_algebraMap_isMaximal_of_isIntegral R k)]

Premises used: Algebra.ker_algebraMap_isMaximal_of_isIntegral, IsLocalRing.eq_maximalIdeal
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
Goal:
R_1 : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R_1
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R_1 A
inst_4 : Algebra A B
inst_5 : Algebra R_1 B
inst_6 : IsScalarTower R_1 A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
R : Type u_4
k : Type u_5
inst_8 : CommRing R
inst_9 : IsLocalRing R
inst_10 : Field k
inst_11 : Algebra R k
inst_12 : Algebra.IsIntegral R k
⊢ IsScalarTower R (ResidueField R) k

Tactic:
.of_algebraMap_eq fun _ ↦ rfl

Premises used: IsScalarTower.of_algebraMap_eq, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
Goal:
R_1 : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R_1
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R_1 A
inst_4 : Algebra A B
inst_5 : Algebra R_1 B
inst_6 : IsScalarTower R_1 A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
R : Type u_4
k : Type u_5
inst_8 : CommRing R
inst_9 : IsLocalRing R
inst_10 : Field k
inst_11 : Algebra R k
inst_12 : Module.Finite R k
rw : Eq (α := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥) (RingHom.ker (F := R →+* k) (algebraMap R k))
rw₁ rw₂ :
  Eq (α := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥)
⊢ Eq (α := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥) (maximalIdeal R)

Tactic:
rw [← eq_maximalIdeal (Algebra.ker_algebraMap_isMaximal_of_isIntegral R k), RingHom.ker]

Premises used: Algebra.ker_algebraMap_isMaximal_of_isIntegral, IsLocalRing.eq_maximalIdeal, RingHom.ker
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
Goal:
R_1 : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R_1
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R_1 A
inst_4 : Algebra A B
inst_5 : Algebra R_1 B
inst_6 : IsScalarTower R_1 A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
R : Type u_4
k : Type u_5
inst_8 : CommRing R
inst_9 : IsLocalRing R
inst_10 : Field k
inst_11 : Algebra R k
inst_12 : Module.Finite R k
h :
  ∀ (x : R),
    Eq.{u_5 + 1} (α := k)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (ResidueField R) k)
                (↑(Ideal.quotEquivOfEq ⋯) : R ⧸ Ideal.comap (algebraMap R k) ⊥ →+* ResidueField R))
              (Ideal.Quotient.mk (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥)) :
            (a : R) → k)
          x :
        k)
      ((RingHom.comp (β := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥))
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(RingEquiv.quotientBot k) : k ⧸ ⊥ →+* k)
                (algebraMap (HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥))
                  (HasQuotient.Quotient k (B := Ideal k) ⊥)))
              (Ideal.Quotient.mk (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥)) :
            (a : R) → k)
          x :
        k)
⊢ Eq (α := RingHom.{u_4, u_5} (HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥)) k)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (ResidueField R) k)
      (↑(Ideal.quotEquivOfEq ⋯) : R ⧸ Ideal.comap (algebraMap R k) ⊥ →+* ResidueField R))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(RingEquiv.quotientBot k) : k ⧸ ⊥ →+* k)
      (algebraMap (HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥))
        (HasQuotient.Quotient k (B := Ideal k) ⊥)))

Tactic:
ext
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
Goal:
R_1 : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R_1
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R_1 A
inst_4 : Algebra A B
inst_5 : Algebra R_1 B
inst_6 : IsScalarTower R_1 A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
R : Type u_4
k : Type u_5
inst_8 : CommRing R
inst_9 : IsLocalRing R
inst_10 : Field k
inst_11 : Algebra R k
inst_12 : Module.Finite R k
x : R
⊢ Eq.{u_5 + 1} (α := k)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (ResidueField R) k)
              (↑(Ideal.quotEquivOfEq ⋯) : R ⧸ Ideal.comap (algebraMap R k) ⊥ →+* ResidueField R))
            (Ideal.Quotient.mk (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥)) :
          (a : R) → k)
        x :
      k)
    ((RingHom.comp (β := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥))
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(RingEquiv.quotientBot k) : k ⧸ ⊥ →+* k)
              (algebraMap (HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥))
                (HasQuotient.Quotient k (B := Ideal k) ⊥)))
            (Ideal.Quotient.mk (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥)) :
          (a : R) → k)
        x :
      k)

Tactic:
rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
inst_3 : I.IsPrime
J : Ideal R[X]
inst_4 : J.IsPrime
inst_5 : J.LiesOver I
inst_6 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
refine_1 :
  J ≤
    RingHom.ker (F := R[X] →+* RatFunc I.ResidueField)
      (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
        (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
refine_2 :
  J.primeCompl ≤
    Submonoid.comap (F := R[X] →+* RatFunc I.ResidueField)
      (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
        (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
      (IsUnit.submonoid (RatFunc I.ResidueField))
⊢ J.ResidueField →+* RatFunc I.ResidueField

Tactic:
refine Ideal.ResidueField.lift _
        ((algebraMap I.ResidueField[X] _).comp (mapRingHom (algebraMap _ _))) ?_ ?_

Premises used: Algebra.algebraMap, Ideal.ResidueField, Polynomial, RingHom.comp, Ideal.ResidueField.lift
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
inst_3 : I.IsPrime
J : Ideal R[X]
inst_4 : J.IsPrime
inst_5 : J.LiesOver I
inst_6 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
⊢ J ≤
    RingHom.ker (F := R[X] →+* RatFunc I.ResidueField)
      (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
        (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))

Tactic:
simp [hJ, Ideal.map_le_iff_le_comap, RingHom.comap_ker _ C, mapRingHom_comp_C,
        RingHom.ker_comp_of_injective, C_injective,
        FaithfulSMul.algebraMap_injective I.ResidueField[X] (RatFunc I.ResidueField)]

Premises used: Polynomial.C, RingHom.comap_ker, Ideal.ResidueField, Polynomial, Polynomial.mapRingHom_comp_C, Ideal.map_le_iff_le_comap, RingHom.ker_comp_of_injective, RatFunc, FaithfulSMul.algebraMap_injective, Polynomial.C_injective
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
inst_3 : I.IsPrime
J : Ideal R[X]
inst_4 : J.IsPrime
inst_5 : J.LiesOver I
inst_6 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
x : R[X]
hx : x ∉ J
this : ∃ (i : ℕ), x.coeff i ∉ I
⊢ Membership.mem (γ := Submonoid R[X])
    (Submonoid.comap (F := R[X] →+* RatFunc I.ResidueField)
      (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
        (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
      (IsUnit.submonoid (RatFunc I.ResidueField)))
    x

Tactic:
simpa [IsUnit.mem_submonoid_iff, Polynomial.ext_iff]

Premises used: Polynomial.ext_iff, IsUnit.mem_submonoid_iff
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
inst_3 : I.IsPrime
J : Ideal R[X]
inst_4 : J.IsPrime
inst_5 : J.LiesOver I
inst_6 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
x : R[X]
hx : x ∉ J
refine_2 : ∃ (i : ℕ), x.coeff i ∉ I
⊢ Membership.mem (γ := Submonoid R[X])
    (Submonoid.comap (F := R[X] →+* RatFunc I.ResidueField)
      (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
        (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
      (IsUnit.submonoid (RatFunc I.ResidueField)))
    x

Tactic:
suffices ∃ i, x.coeff i ∉ I by simpa [IsUnit.mem_submonoid_iff, Polynomial.ext_iff]
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
inst_3 : I.IsPrime
J : Ideal R[X]
inst_4 : J.IsPrime
inst_5 : J.LiesOver I
inst_6 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
x : R[X]
hx : x ∉ J
refine_2 : ∀ (hx : ∀ (i : ℕ), x.coeff i ∈ I), x ∈ J
⊢ ∃ (i : ℕ), x.coeff i ∉ I

Tactic:
contrapose! hx
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
inst_3 : I.IsPrime
J : Ideal R[X]
inst_4 : J.IsPrime
inst_5 : J.LiesOver I
inst_6 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
x : R[X]
hx : ∀ (i : ℕ), x.coeff i ∈ I
refine_2 : Membership.mem (γ := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I) x
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : ∀ (n : ℕ), x.coeff n ∈ I
⊢ x ∈ J

Tactic:
rwa [hJ, Ideal.mem_map_C_iff]

Premises used: Ideal.mem_map_C_iff
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
inst_3 : I.IsPrime
J : Ideal R[X]
inst_4 : J.IsPrime
inst_5 : J.LiesOver I
inst_6 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
      (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
    ⋯ ⋯
H :
  ∀ (x : R),
    Eq (α := RatFunc I.ResidueField)
      ((@RingHom.comp _ I.ResidueField _ _ Semiring.toNonAssocSemiring _
              (f.comp (algebraMap I.ResidueField J.ResidueField)) (algebraMap R I.ResidueField) :
            (a : R) → RatFunc I.ResidueField)
          x :
        RatFunc I.ResidueField)
      ((@RingHom.comp _ I.ResidueField _ _ Semiring.toNonAssocSemiring _
              (algebraMap I.ResidueField (RatFunc I.ResidueField)) (algebraMap R I.ResidueField) :
            (a : R) → RatFunc I.ResidueField)
          x :
        RatFunc I.ResidueField)
⊢ Eq (α := I.ResidueField →+* RatFunc I.ResidueField) (f.comp (algebraMap I.ResidueField J.ResidueField))
    (algebraMap I.ResidueField (RatFunc I.ResidueField))

Tactic:
ext
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
inst_3 : I.IsPrime
J : Ideal R[X]
inst_4 : J.IsPrime
inst_5 : J.LiesOver I
inst_6 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
      (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
    ⋯ ⋯
x : R
⊢ Eq (α := RatFunc I.ResidueField)
    ((@RingHom.comp _ I.ResidueField _ _ Semiring.toNonAssocSemiring _
            (f.comp (algebraMap I.ResidueField J.ResidueField)) (algebraMap R I.ResidueField) :
          (a : R) → RatFunc I.ResidueField)
        x :
      RatFunc I.ResidueField)
    ((@RingHom.comp _ I.ResidueField _ _ Semiring.toNonAssocSemiring _
            (algebraMap I.ResidueField (RatFunc I.ResidueField)) (algebraMap R I.ResidueField) :
          (a : R) → RatFunc I.ResidueField)
        x :
      RatFunc I.ResidueField)

Tactic:
simp [f, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R R[X] J.ResidueField]

Premises used: Ideal.ResidueField, Polynomial, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
inst_3 : I.IsPrime
J : Ideal R[X]
inst_4 : J.IsPrime
inst_5 : J.LiesOver I
inst_6 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
      (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
    ⋯ ⋯
⊢ Eq (α := I.ResidueField →+* RatFunc I.ResidueField) (f.comp (algebraMap I.ResidueField J.ResidueField))
    (algebraMap I.ResidueField (RatFunc I.ResidueField))

Tactic:
haveI hf : f.comp (algebraMap I.ResidueField _) = algebraMap _ _ := by
    ext
    simp [f, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R R[X] J.ResidueField]
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
inst_3 : I.IsPrime
J : Ideal R[X]
inst_4 : J.IsPrime
inst_5 : J.LiesOver I
inst_6 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
      (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
    ⋯ ⋯
hf :
  Eq (α := I.ResidueField →+* RatFunc I.ResidueField) (f.comp (algebraMap I.ResidueField J.ResidueField))
    (algebraMap I.ResidueField (RatFunc I.ResidueField))
refine_1 :
  ∀ (x : I.ResidueField[X]),
    Membership.mem (γ := Submonoid I.ResidueField[X]) I.ResidueField[X]⁰ x →
      Membership.mem (γ := Submonoid I.ResidueField[X])
        (Submonoid.comap (F := I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField)
          (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
            I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField)
          J.ResidueField⁰)
        x
refine_2 :
  Eq (α := RatFunc I.ResidueField →ₐ[I.ResidueField] RatFunc I.ResidueField)
    (AlgHom.comp { toRingHom := f, commutes' := ⋯ }
      (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X)) ⋯))
    (AlgHom.id I.ResidueField (RatFunc I.ResidueField))
refine_3 :
  Eq (α := J.ResidueField →ₐ[I.ResidueField] J.ResidueField)
    (AlgHom.comp (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X)) ⋯)
        { toRingHom := f, commutes' := ⋯ } :
      J.ResidueField →ₐ[I.ResidueField] J.ResidueField)
    (AlgHom.id I.ResidueField J.ResidueField : J.ResidueField →ₐ[I.ResidueField] J.ResidueField)
⊢ J.ResidueField ≃ₐ[I.ResidueField] RatFunc I.ResidueField

Tactic:
refine .ofAlgHom ⟨f, fun r ↦ congr($hf r)⟩
      (RatFunc.liftAlgHom (aeval (algebraMap R[X] _ X)) fun x ↦ ?_) ?_ ?_
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
inst_3 : I.IsPrime
J : Ideal R[X]
inst_4 : J.IsPrime
inst_5 : J.LiesOver I
inst_6 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
      (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
    ⋯ ⋯
hf :
  Eq (α := I.ResidueField →+* RatFunc I.ResidueField) (f.comp (algebraMap I.ResidueField J.ResidueField))
    (algebraMap I.ResidueField (RatFunc I.ResidueField))
x : I.ResidueField[X]
this :
  Function.Injective.{u_1 + 1, u_1 + 1} (α := I.ResidueField[X]) (β := J.ResidueField)
    (⇑(aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
          I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField) :
      (a : I.ResidueField[X]) → J.ResidueField)
⊢ Membership.mem (γ := Submonoid I.ResidueField[X]) I.ResidueField[X]⁰ x →
    Membership.mem (γ := Submonoid I.ResidueField[X])
      (Submonoid.comap (F := I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField)
        (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
          I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField)
        J.ResidueField⁰)
      x

Tactic:
simp [← this.eq_iff]

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
inst_3 : I.IsPrime
J : Ideal R[X]
inst_4 : J.IsPrime
inst_5 : J.LiesOver I
inst_6 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
      (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
    ⋯ ⋯
hf :
  Eq (α := I.ResidueField →+* RatFunc I.ResidueField) (f.comp (algebraMap I.ResidueField J.ResidueField))
    (algebraMap I.ResidueField (RatFunc I.ResidueField))
x : I.ResidueField[X]
refine_1 :
  Function.Injective.{u_1 + 1, u_1 + 1} (α := I.ResidueField[X]) (β := J.ResidueField)
    (⇑(aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
          I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField) :
      (a : I.ResidueField[X]) → J.ResidueField)
⊢ Membership.mem (γ := Submonoid I.ResidueField[X]) I.ResidueField[X]⁰ x →
    Membership.mem (γ := Submonoid I.ResidueField[X])
      (Submonoid.comap (F := I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField)
        (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
          I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField)
        J.ResidueField⁰)
      x

Tactic:
suffices Function.Injective (aeval (R := I.ResidueField) (algebraMap R[X] J.ResidueField X)) by
      simp [← this.eq_iff]
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
inst_3 : I.IsPrime
J : Ideal R[X]
inst_4 : J.IsPrime
inst_5 : J.LiesOver I
inst_6 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
      (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
    ⋯ ⋯
hf :
  Eq (α := I.ResidueField →+* RatFunc I.ResidueField) (f.comp (algebraMap I.ResidueField J.ResidueField))
    (algebraMap I.ResidueField (RatFunc I.ResidueField))
x : I.ResidueField[X]
refine_1 :
  ∀ (a : I.ResidueField[X]),
    Eq (α := J.ResidueField)
        (((aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
                I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField) :
              (a : I.ResidueField[X]) → J.ResidueField)
            a :
          J.ResidueField)
        (0 : J.ResidueField) →
      a = 0
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := I.ResidueField[X]) (β := J.ResidueField)
    (⇑(aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
          I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField) :
      (a : I.ResidueField[X]) → J.ResidueField)

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero