awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : Localization.AtPrime.IsLiesOverAlgebra p q
q' : Ideal (p.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S p : (a : (↑(p.primesOver S) : Type u_2)) → PrimeSpectrum (p.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x) q ⋯))
hq' : q = Ideal.comap (F := S →+* p.ResidueField ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q'
this_1 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) q'
this : q'.IsMaximal
x : R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [IsScalarTower.algebraMap_apply R S q.ResidueField]

Premises used: Ideal.ResidueField, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : Localization.AtPrime.IsLiesOverAlgebra p q
q' : Ideal (p.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S p : (a : (↑(p.primesOver S) : Type u_2)) → PrimeSpectrum (p.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x) q ⋯))
hq' : q = Ideal.comap (F := S →+* p.ResidueField ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q'
this_1 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) q'
this : q'.IsMaximal
x : S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [IsScalarTower.algebraMap_apply R S q.ResidueField]

Premises used: Ideal.ResidueField, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
inst_1 : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
inr :
  ∀
    (this :
      ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R[X]) [inst_2 : P.IsPrime] (H : Algebra.WeaklyQuasiFiniteAt R P)
        (hR : IsField R), False)
    (hR : ¬IsField R), False
wlog :
  ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R[X]) [inst_2 : P.IsPrime] (H : Algebra.WeaklyQuasiFiniteAt R P)
    (hR : IsField R), False
⊢ False

Tactic:
wlog hR : IsField R

Premises used: IsField
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
inst_1 : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R[X]) [inst_2 : P.IsPrime] (H : Algebra.WeaklyQuasiFiniteAt R P)
    (hR : IsField R), False
hR : ¬IsField R
p : Ideal R := Ideal.under R P
inr :
  ∀ (Q : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber R[X]))
    (hQ :
      (Equiv.symm (PrimeSpectrum.preimageEquivFiber R R[X] { asIdeal := p, isPrime := ⋯ }) :
            (a : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber R[X])) →
              (↑(PrimeSpectrum.comap (algebraMap R R[X]) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_1))
          Q =
        Subtype.mk (p := fun (x : PrimeSpectrum R[X]) ↦
          Membership.mem (γ := Set (PrimeSpectrum R[X]))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R R[X]))
              {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
            x)
          { asIdeal := P, isPrime := inst_1 : PrimeSpectrum R[X] } ⋯),
    False
⊢ False

Tactic:
obtain ⟨Q, hQ⟩ := (PrimeSpectrum.preimageEquivFiber R R[X]
        ⟨p, inferInstance⟩).symm.surjective ⟨⟨P, ‹_›⟩, rfl⟩

Premises used: PrimeSpectrum.mk, inferInstance, PrimeSpectrum.preimageEquivFiber, Polynomial, Subtype.mk, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
inst_1 : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R[X]) [inst_2 : P.IsPrime] (H : Algebra.WeaklyQuasiFiniteAt R P)
    (hR : IsField R), False
hR : ¬IsField R
p : Ideal R := Ideal.under R P
Q : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber R[X])
hQ :
  (Equiv.symm (PrimeSpectrum.preimageEquivFiber R R[X] { asIdeal := p, isPrime := ⋯ }) :
        (a : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber R[X])) →
          (↑(PrimeSpectrum.comap (algebraMap R R[X]) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_1))
      Q =
    Subtype.mk (p := fun (x : PrimeSpectrum R[X]) ↦
      Membership.mem (γ := Set (PrimeSpectrum R[X]))
        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R R[X]))
          {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
        x)
      { asIdeal := P, isPrime := inst_1 : PrimeSpectrum R[X] } ⋯
⊢ Algebra.WeaklyQuasiFiniteAt p.ResidueField Q.asIdeal

Tactic:
have inst : Algebra.WeaklyQuasiFiniteAt p.ResidueField Q.asIdeal :=
      .baseChange P Q.asIdeal congr($(hQ.symm).1.1)
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
inst_1 : CommRing R
P : Ideal R[X]
inst_2 : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R[X]) [inst_3 : P.IsPrime] (H : Algebra.WeaklyQuasiFiniteAt R P)
    (hR : IsField R), False
hR : ¬IsField R
p : Ideal R := Ideal.under R P
Q : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber R[X])
hQ :
  (Equiv.symm (PrimeSpectrum.preimageEquivFiber R R[X] { asIdeal := p, isPrime := ⋯ }) :
        (a : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber R[X])) →
          (↑(PrimeSpectrum.comap (algebraMap R R[X]) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_1))
      Q =
    Subtype.mk (p := fun (x : PrimeSpectrum R[X]) ↦
      Membership.mem (γ := Set (PrimeSpectrum R[X]))
        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R R[X]))
          {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
        x)
      { asIdeal := P, isPrime := inst_2 : PrimeSpectrum R[X] } ⋯
inst : Algebra.WeaklyQuasiFiniteAt p.ResidueField Q.asIdeal
⊢ False

Tactic:
this (Q.asIdeal.comap (polyEquivTensor' R p.ResidueField).toRingHom)
      inferInstance (Field.toIsField _)

Premises used: Ideal.ResidueField, Field.toIsField, inferInstance, polyEquivTensor', RingEquiv.toRingHom, AlgEquiv.toRingEquiv, Ideal.comap, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
inst_1 : CommRing R
P : Ideal R[X]
inst_2 : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R[X]) [inst_3 : P.IsPrime] (H : Algebra.WeaklyQuasiFiniteAt R P)
    (hR : IsField R), False
hR : ¬IsField R
p : Ideal R := Ideal.under R P
Q : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber R[X])
hQ :
  (Equiv.symm (PrimeSpectrum.preimageEquivFiber R R[X] { asIdeal := p, isPrime := ⋯ }) :
        (a : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber R[X])) →
          (↑(PrimeSpectrum.comap (algebraMap R R[X]) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_1))
      Q =
    Subtype.mk (p := fun (x : PrimeSpectrum R[X]) ↦
      Membership.mem (γ := Set (PrimeSpectrum R[X]))
        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R R[X]))
          {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
        x)
      { asIdeal := P, isPrime := inst_2 : PrimeSpectrum R[X] } ⋯
inst : Algebra.WeaklyQuasiFiniteAt p.ResidueField Q.asIdeal
⊢ False

Tactic:
exact this (Q.asIdeal.comap (polyEquivTensor' R p.ResidueField).toRingHom)
      inferInstance (Field.toIsField _)

Premises used: Ideal.ResidueField, Field.toIsField, inferInstance, polyEquivTensor', RingEquiv.toRingHom, AlgEquiv.toRingEquiv, Ideal.comap, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
P : Ideal R[X]
inst_2 : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
hR : IsField R
this : Field R := hR.toField
⊢ Module.Finite R R[X]

Tactic:
have := Module.Finite.of_injective
    (IsScalarTower.toAlgHom R R[X] (Localization.AtPrime P)).toLinearMap
    (IsLocalization.injective _ P.primeCompl_le_nonZeroDivisors)
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
P : Ideal R[X]
inst_2 : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
hR : IsField R
this_1 : Field R := hR.toField
this : Module.Finite R R[X]
⊢ False

Tactic:
transcendental_X R (Algebra.IsIntegral.isIntegral X).isAlgebraic

Premises used: Algebra.IsIntegral.isIntegral, Polynomial.transcendental_X, IsIntegral.isAlgebraic, Polynomial.X
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
P : Ideal R[X]
inst_2 : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
hR : IsField R
this_1 : Field R := hR.toField
this : Module.Finite R R[X]
⊢ False

Tactic:
exact transcendental_X R (Algebra.IsIntegral.isIntegral X).isAlgebraic

Premises used: Algebra.IsIntegral.isIntegral, Polynomial.transcendental_X, IsIntegral.isAlgebraic, Polynomial.X
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
inst_1 : P.IsPrime
⊢ ¬Algebra.QuasiFiniteAt R P

Tactic:
fun _ ↦ not_weaklyQuasiFiniteAt P inferInstance

Premises used: inferInstance, Polynomial.not_weaklyQuasiFiniteAt, Not
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
⊢ LT.lt (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
    (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P)

Tactic:
lt_of_le_of_ne (Ideal.map_le_iff_le_comap.mpr ?_) fun e ↦ ?_

Premises used: Iff.mpr, Ideal.map_le_iff_le_comap, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
refine_1 :
  LE.le (α := Ideal R) (Ideal.under R P)
    (Ideal.comap (F := R →+* R[X]) C (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P))
refine_2 :
  ∀
    (e :
      Eq (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
        (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P)),
    False
⊢ LT.lt (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
    (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P)

Tactic:
refine lt_of_le_of_ne (Ideal.map_le_iff_le_comap.mpr ?_) fun e ↦ ?_

Premises used: Iff.mpr, Ideal.map_le_iff_le_comap, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
refine_1 : LE.le (α := Ideal R) (Ideal.under R P) (Ideal.comap (F := R →+* S) (RingHom.comp (↑f : R[X] →+* S) C) P)
refine_1₁ :
  LE.le (α := Ideal R) (Ideal.under R P)
    (Ideal.comap (F := R →+* S)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R[X] →+* S) (algebraMap R R[X])) P)
refine_1₂ refine_1₃ : LE.le (α := Ideal R) (Ideal.under R P) (Ideal.under R P)
⊢ LE.le (α := Ideal R) (Ideal.under R P)
    (Ideal.comap (F := R →+* R[X]) C (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P))

Tactic:
rw [Ideal.comap_comap, ← algebraMap_eq, f.comp_algebraMap]

Premises used: AlgHom.comp_algebraMap, Polynomial.algebraMap_eq, Ideal.comap_comap
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
e :
  Eq (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
    (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P)
this_1 : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime (R := R[X]) (Ideal.under R[X] P)) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) (Ideal.under R[X] P)
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime (R := R[X]) (Ideal.under R[X] P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R[X] P) P
this : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
⊢ Module.Finite.{u_1, u_2} (Ideal.ResidueField (Ideal.under R P)) P.ResidueField

Tactic:
have : Module.Finite (Ideal.under R P).ResidueField P.ResidueField :=
    Algebra.WeaklyQuasiFiniteAt.finite_residueField ..
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
e :
  Eq (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
    (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P)
this_1 : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime (R := R[X]) (Ideal.under R[X] P)) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) (Ideal.under R[X] P)
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime (R := R[X]) (Ideal.under R[X] P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R[X] P) P
this_3 : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
this : Module.Finite.{u_1, u_2} (Ideal.ResidueField (Ideal.under R P)) P.ResidueField
⊢ Module.Finite.{u_1, u_1} (Ideal.ResidueField (Ideal.under R P)) (Ideal.ResidueField (R := R[X]) (Ideal.under R[X] P))

Tactic:
have : Module.Finite (P.under R).ResidueField (P.under R[X]).ResidueField :=
    .of_injective (IsScalarTower.toAlgHom _ _ P.ResidueField).toLinearMap
      (algebraMap (P.under R[X]).ResidueField P.ResidueField).injective
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
e :
  Eq (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
    (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P)
this_1 : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime (R := R[X]) (Ideal.under R[X] P)) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) (Ideal.under R[X] P)
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime (R := R[X]) (Ideal.under R[X] P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R[X] P) P
this_3 : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
this_4 : Module.Finite.{u_1, u_2} (Ideal.ResidueField (Ideal.under R P)) P.ResidueField
this :
  Module.Finite.{u_1, u_1} (Ideal.ResidueField (Ideal.under R P)) (Ideal.ResidueField (R := R[X]) (Ideal.under R[X] P))
⊢ Module.Finite.{u_1, u_1} (Ideal.ResidueField (Ideal.under R P)) (RatFunc (Ideal.ResidueField (Ideal.under R P)))

Tactic:
have : Module.Finite (P.under R).ResidueField (RatFunc (P.under R).ResidueField) :=
    .of_surjective (residueFieldMapCAlgEquiv _ (P.under _) e.symm).toLinearMap
      (residueFieldMapCAlgEquiv _ (P.under _) e.symm).surjective
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
e :
  Eq (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
    (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P)
this_1 : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime (R := R[X]) (Ideal.under R[X] P)) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) (Ideal.under R[X] P)
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime (R := R[X]) (Ideal.under R[X] P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R[X] P) P
this_3 : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
this_4 : Module.Finite.{u_1, u_2} (Ideal.ResidueField (Ideal.under R P)) P.ResidueField
this_5 :
  Module.Finite.{u_1, u_1} (Ideal.ResidueField (Ideal.under R P)) (Ideal.ResidueField (R := R[X]) (Ideal.under R[X] P))
this : Module.Finite.{u_1, u_1} (Ideal.ResidueField (Ideal.under R P)) (RatFunc (Ideal.ResidueField (Ideal.under R P)))
⊢ False

Tactic:
RatFunc.transcendental_X (K := (P.under R).ResidueField)
    (Algebra.IsIntegral.isIntegral _).isAlgebraic

Premises used: Algebra.IsIntegral.isIntegral, RatFunc.transcendental_X, IsIntegral.isAlgebraic
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
e :
  Eq (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
    (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P)
this_1 : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime (R := R[X]) (Ideal.under R[X] P)) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) (Ideal.under R[X] P)
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime (R := R[X]) (Ideal.under R[X] P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R[X] P) P
this_3 : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
this_4 : Module.Finite.{u_1, u_2} (Ideal.ResidueField (Ideal.under R P)) P.ResidueField
this_5 :
  Module.Finite.{u_1, u_1} (Ideal.ResidueField (Ideal.under R P)) (Ideal.ResidueField (R := R[X]) (Ideal.under R[X] P))
this : Module.Finite.{u_1, u_1} (Ideal.ResidueField (Ideal.under R P)) (RatFunc (Ideal.ResidueField (Ideal.under R P)))
⊢ False

Tactic:
exact RatFunc.transcendental_X (K := (P.under R).ResidueField)
    (Algebra.IsIntegral.isIntegral _).isAlgebraic

Premises used: Algebra.IsIntegral.isIntegral, RatFunc.transcendental_X, IsIntegral.isAlgebraic
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.QuasiFiniteAt R P
⊢ LT.lt (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
    (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P)

Tactic:
map_under_lt_comap_of_weaklyQuasiFiniteAt f P

Premises used: Polynomial.map_under_lt_comap_of_weaklyQuasiFiniteAt
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
H : LE.le (α := Ideal R[X]) (RingHom.ker f) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
p : Ideal R := Ideal.under R P
rw :
  LE.le (α := Ideal R[X]) (RingHom.ker f)
    (Ideal.comap (F := R[X] →+* p.ResidueField[X]) (mapRingHom (algebraMap R p.ResidueField)) ⊥)
⊢ Eq (α := Ideal p.ResidueField[X])
    (Ideal.map (F := R[X] →+* p.ResidueField[X]) (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker f)) ⊥

Tactic:
rw [← le_bot_iff, Ideal.map_le_iff_le_comap]

Premises used: le_bot_iff, Ideal.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
H : LE.le (α := Ideal R[X]) (RingHom.ker f) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
p : Ideal R := Ideal.under R P
x : R[X]
hx : Membership.mem (γ := Submodule R[X] R[X]) (RingHom.ker f) x
⊢ Membership.mem (γ := Submodule R[X] R[X])
    (Ideal.comap (F := R[X] →+* p.ResidueField[X]) (mapRingHom (algebraMap R p.ResidueField)) ⊥) x

Tactic:
simpa [Polynomial.ext_iff, Ideal.mem_map_C_iff] using H hx

Premises used: Polynomial.ext_iff, Ideal.mem_map_C_iff
-- Module: Mathlib.RingTheory.QuasiFinite.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
H : LE.le (α := Ideal R[X]) (RingHom.ker f) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
p : Ideal R := Ideal.under R P
⊢ Eq (α := Ideal p.ResidueField[X])
    (Ideal.map (F := R[X] →+* p.ResidueField[X]) (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker f)) ⊥

Tactic:
have H' : (RingHom.ker f).map (mapRingHom (algebraMap R p.ResidueField)) = ⊥ := by
    rw [← le_bot_iff, Ideal.map_le_iff_le_comap]
    intro x hx
    simpa [Polynomial.ext_iff, Ideal.mem_map_C_iff] using H hx