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 : QuasiFinite R S
I : Ideal R
pos : ∀ (h : I.IsPrime), Set.Finite (α := Ideal S) (I.primesOver S)
neg : ∀ (h : ¬I.IsPrime), Set.Finite (α := Ideal S) (I.primesOver S)
⊢ Set.Finite (α := Ideal S) (I.primesOver S)

Tactic:
by_cases h : I.IsPrime

Premises used: Ideal.IsPrime
-- 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 : QuasiFinite R S
I : Ideal R
h : I.IsPrime
⊢ Set.Finite (α := Ideal S) (I.primesOver S)

Tactic:
((finite_comap_preimage_singleton ⟨I, h⟩).image PrimeSpectrum.asIdeal).subset ?_

Premises used: PrimeSpectrum.mk, Set.Finite.subset, Set.Finite.image, Algebra.QuasiFinite.finite_comap_preimage_singleton, PrimeSpectrum.asIdeal
-- 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 : QuasiFinite R S
I : Ideal R
h : I.IsPrime
pos :
  Subset (α := Set (Ideal S)) (I.primesOver S)
    (PrimeSpectrum.asIdeal ''
      Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        {{ asIdeal := I, isPrime := h : PrimeSpectrum R }})
⊢ Set.Finite (α := Ideal S) (I.primesOver S)

Tactic:
refine ((finite_comap_preimage_singleton ⟨I, h⟩).image PrimeSpectrum.asIdeal).subset ?_

Premises used: PrimeSpectrum.mk, Set.Finite.subset, Set.Finite.image, Algebra.QuasiFinite.finite_comap_preimage_singleton, PrimeSpectrum.asIdeal
-- 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 : QuasiFinite R S
I : Ideal R
h : I.IsPrime
⊢ Subset (α := Set (Ideal S)) (I.primesOver S)
    (PrimeSpectrum.asIdeal ''
      Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        {{ asIdeal := I, isPrime := h : PrimeSpectrum R }})

Tactic:
fun J hJ ↦ ⟨⟨_, hJ.1⟩, PrimeSpectrum.ext hJ.2.1.symm, rfl⟩

Premises used: PrimeSpectrum.mk, PrimeSpectrum.ext, Set.Mem, setOf, Set.Subset, And.left, And.intro, Ideal.LiesOver.over, Exists.intro, Set.image, Eq.symm, rfl
-- 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 : QuasiFinite R S
I : Ideal R
h : I.IsPrime
⊢ Subset (α := Set (Ideal S)) (I.primesOver S)
    (PrimeSpectrum.asIdeal ''
      Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        {{ asIdeal := I, isPrime := h : PrimeSpectrum R }})

Tactic:
exact fun J hJ ↦ ⟨⟨_, hJ.1⟩, PrimeSpectrum.ext hJ.2.1.symm, rfl⟩
-- 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 : QuasiFinite R S
I : Ideal R
h : ¬I.IsPrime
⊢ Set.Finite.{u_2} (α := Ideal S) ∅

Tactic:
Set.finite_empty

Premises used: Set.finite_empty
-- 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 : QuasiFinite R S
I : Ideal R
h : ¬I.IsPrime
h₁ : Eq (α := Set (Ideal S)) (I.primesOver S) ∅
⊢ Set.Finite (α := Ideal S) (I.primesOver S)

Tactic:
convert! Set.finite_empty

Premises used: Set.finite_empty
-- 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 : QuasiFinite R S
I : Ideal R
h : ¬I.IsPrime
h₁ : ∀ (this : Set.Nonempty (α := Ideal S) (I.primesOver S)), False
⊢ Eq (α := Set (Ideal S)) (I.primesOver S) ∅

Tactic:
by_contra!
-- 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 : QuasiFinite R S
I : Ideal R
h : ¬I.IsPrime
this : Set.Nonempty (α := Ideal S) (I.primesOver S)
h₁ : ∀ (J : Ideal S) (h₁ : J.IsPrime) (h : ¬Ideal.IsPrime (Ideal.under R J)), False
⊢ False

Tactic:
obtain ⟨J, h₁, ⟨rfl⟩⟩ := this

Premises used: rfl
-- 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 : QuasiFinite R S
J : Ideal S
h₁ : J.IsPrime
h : ¬Ideal.IsPrime (Ideal.under R J)
⊢ False

Tactic:
h inferInstance

Premises used: inferInstance
-- 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 : QuasiFinite R S
J : Ideal S
h₁ : J.IsPrime
h : ¬Ideal.IsPrime (Ideal.under R J)
⊢ False

Tactic:
exact h inferInstance

Premises used: inferInstance
-- 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 : QuasiFinite R S
s : Set (PrimeSpectrum R)
hs : s.Finite
⊢ Set.Finite (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S) ⁻¹' s)

Tactic:
hs.preimage' fun _ _ ↦ finite_comap_preimage_singleton _

Premises used: Algebra.QuasiFinite.finite_comap_preimage_singleton, Set.Finite.preimage'
-- 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 : QuasiFinite R S
P : PrimeSpectrum R
⊢ IsDiscrete (X := PrimeSpectrum S) (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {P})

Tactic:
⟨(PrimeSpectrum.preimageHomeomorphFiber R S P).symm.discreteTopology⟩

Premises used: PrimeSpectrum.preimageHomeomorphFiber, IsDiscrete.mk, Homeomorph.symm, Homeomorph.discreteTopology
-- 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 : QuasiFinite R S
s : Set (PrimeSpectrum R)
hs : IsDiscrete s
⊢ IsDiscrete (X := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S) ⁻¹' s)

Tactic:
hs.preimage' (PrimeSpectrum.continuous_comap _).continuousOn
    fun _ ↦ isDiscrete_comap_preimage_singleton _

Premises used: Continuous.continuousOn, Algebra.QuasiFinite.isDiscrete_comap_preimage_singleton, PrimeSpectrum.continuous_comap, IsDiscrete.preimage'
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : QuasiFinite R S
A : Type u_4
inst_8 : CommRing A
inst_9 : Algebra R A
⊢ QuasiFinite A (A ⊗[R] S)

Tactic:
⟨fun P hP ↦ ?_⟩

Premises used: Algebra.QuasiFinite.mk
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : QuasiFinite R S
A : Type u_4
inst_8 : CommRing A
inst_9 : Algebra R A
refine : ∀ (P : Ideal A) (hP : P.IsPrime), Module.Finite P.ResidueField (P.Fiber (A ⊗[R] S))
⊢ QuasiFinite A (A ⊗[R] S)

Tactic:
refine ⟨fun P hP ↦ ?_⟩
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : QuasiFinite R S
A : Type u_4
inst_8 : CommRing A
inst_9 : Algebra R A
P : Ideal A
hP : P.IsPrime
p : Ideal R := Ideal.under R P
this : Algebra.{u_1, u_4} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
e : P.Fiber (A ⊗[R] S) ≃ₐ[P.ResidueField] P.ResidueField ⊗[p.ResidueField] p.Fiber S :=
  AlgEquiv.trans (A₂ := TensorProduct.{u_1, u_4, u_2} R P.ResidueField S)
    (TensorProduct.cancelBaseChange R A P.ResidueField P.ResidueField S :
      P.ResidueField ⊗[A] (A ⊗[R] S) ≃ₐ[P.ResidueField] TensorProduct.{u_1, u_4, u_2} R P.ResidueField S)
    (AlgEquiv.symm (TensorProduct.cancelBaseChange R p.ResidueField P.ResidueField P.ResidueField S) :
      TensorProduct.{u_1, u_4, u_2} R P.ResidueField S ≃ₐ[P.ResidueField]
        P.ResidueField ⊗[p.ResidueField] (p.ResidueField ⊗[R] S))
⊢ Module.Finite P.ResidueField (P.Fiber (A ⊗[R] S))

Tactic:
.of_surjective e.symm.toLinearMap e.symm.surjective

Premises used: Module.Finite.of_surjective, AlgEquiv.symm, AlgEquiv.toLinearMap, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : QuasiFinite R S
A : Type u_4
inst_8 : CommRing A
inst_9 : Algebra R A
P : Ideal A
hP : P.IsPrime
p : Ideal R := Ideal.under R P
this : Algebra.{u_1, u_4} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
e : P.Fiber (A ⊗[R] S) ≃ₐ[P.ResidueField] P.ResidueField ⊗[p.ResidueField] p.Fiber S :=
  AlgEquiv.trans (A₂ := TensorProduct.{u_1, u_4, u_2} R P.ResidueField S)
    (TensorProduct.cancelBaseChange R A P.ResidueField P.ResidueField S :
      P.ResidueField ⊗[A] (A ⊗[R] S) ≃ₐ[P.ResidueField] TensorProduct.{u_1, u_4, u_2} R P.ResidueField S)
    (AlgEquiv.symm (TensorProduct.cancelBaseChange R p.ResidueField P.ResidueField P.ResidueField S) :
      TensorProduct.{u_1, u_4, u_2} R P.ResidueField S ≃ₐ[P.ResidueField]
        P.ResidueField ⊗[p.ResidueField] (p.ResidueField ⊗[R] S))
⊢ Module.Finite P.ResidueField (P.Fiber (A ⊗[R] S))

Tactic:
exact .of_surjective e.symm.toLinearMap e.symm.surjective
-- 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 : QuasiFinite R S
inst_4 : IsArtinianRing R
inst_5 : IsLocalRing R
e : Ideal.Fiber (maximalIdeal R) S ≃ₐ[R]
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :=
  AlgEquiv.trans
    (TensorProduct.congr
        (AlgEquiv.symm
          (AlgEquiv.ofBijective (Ideal.Quotient.liftₐ (maximalIdeal R) (ofId R (Ideal.ResidueField (maximalIdeal R))) ⋯)
            ⋯))
        AlgEquiv.refl :
      Ideal.ResidueField (maximalIdeal R) ⊗[R] S ≃ₐ[R] HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S)
    (AlgEquiv.trans (TensorProduct.comm R (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)) S)
        (AlgEquiv.restrictScalars R (AlgEquiv.symm (TensorProduct.quotIdealMapEquivTensorQuot S (maximalIdeal R)))) :
      HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S ≃ₐ[R]
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
⊢ Module.Finite.{u_1, u_2} R
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))

Tactic:
have : Module.Finite R (S ⧸ (maximalIdeal R).map (algebraMap R S)) :=
    have : Module.Finite R ((maximalIdeal R).Fiber S) :=
      .trans (maximalIdeal R).ResidueField _
    .of_surjective e.toLinearMap e.surjective
-- 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 : QuasiFinite R S
inst_4 : IsArtinianRing R
inst_5 : IsLocalRing R
e : Ideal.Fiber (maximalIdeal R) S ≃ₐ[R]
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :=
  AlgEquiv.trans
    (TensorProduct.congr
        (AlgEquiv.symm
          (AlgEquiv.ofBijective (Ideal.Quotient.liftₐ (maximalIdeal R) (ofId R (Ideal.ResidueField (maximalIdeal R))) ⋯)
            ⋯))
        AlgEquiv.refl :
      Ideal.ResidueField (maximalIdeal R) ⊗[R] S ≃ₐ[R] HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S)
    (AlgEquiv.trans (TensorProduct.comm R (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)) S)
        (AlgEquiv.restrictScalars R (AlgEquiv.symm (TensorProduct.quotIdealMapEquivTensorQuot S (maximalIdeal R)))) :
      HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S ≃ₐ[R]
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
this :
  Module.Finite.{u_1, u_2} R
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
⊢ Module.Finite R S

Tactic:
Module.finite_of_surjective_of_ker_le_nilradical (Ideal.Quotient.mkₐ R
    ((maximalIdeal R).map (algebraMap R S))) Ideal.Quotient.mk_surjective ?_ ?_

Premises used: Algebra.algebraMap, IsLocalRing.maximalIdeal, Ideal.map, Ideal.Quotient.mk_surjective, Ideal.Quotient.mkₐ, Module.finite_of_surjective_of_ker_le_nilradical
-- 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 : QuasiFinite R S
inst_4 : IsArtinianRing R
inst_5 : IsLocalRing R
e : Ideal.Fiber (maximalIdeal R) S ≃ₐ[R]
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :=
  AlgEquiv.trans
    (TensorProduct.congr
        (AlgEquiv.symm
          (AlgEquiv.ofBijective (Ideal.Quotient.liftₐ (maximalIdeal R) (ofId R (Ideal.ResidueField (maximalIdeal R))) ⋯)
            ⋯))
        AlgEquiv.refl :
      Ideal.ResidueField (maximalIdeal R) ⊗[R] S ≃ₐ[R] HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S)
    (AlgEquiv.trans (TensorProduct.comm R (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)) S)
        (AlgEquiv.restrictScalars R (AlgEquiv.symm (TensorProduct.quotIdealMapEquivTensorQuot S (maximalIdeal R)))) :
      HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S ≃ₐ[R]
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
this :
  Module.Finite.{u_1, u_2} R
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
refine_1 :
  LE.le (α := Ideal S)
    (RingHom.ker (F :=
      S →ₐ[R] HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
      (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))))
    (nilradical S)
refine_2 :
  Ideal.FG
    (RingHom.ker (F :=
      S →ₐ[R] HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
      (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))))
⊢ Module.Finite R S

Tactic:
refine Module.finite_of_surjective_of_ker_le_nilradical (Ideal.Quotient.mkₐ R
    ((maximalIdeal R).map (algebraMap R S))) Ideal.Quotient.mk_surjective ?_ ?_

Premises used: Algebra.algebraMap, IsLocalRing.maximalIdeal, Ideal.map, Ideal.Quotient.mk_surjective, Ideal.Quotient.mkₐ, Module.finite_of_surjective_of_ker_le_nilradical
-- 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 : QuasiFinite R S
inst_4 : IsArtinianRing R
inst_5 : IsLocalRing R
e : Ideal.Fiber (maximalIdeal R) S ≃ₐ[R]
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :=
  AlgEquiv.trans
    (TensorProduct.congr
        (AlgEquiv.symm
          (AlgEquiv.ofBijective (Ideal.Quotient.liftₐ (maximalIdeal R) (ofId R (Ideal.ResidueField (maximalIdeal R))) ⋯)
            ⋯))
        AlgEquiv.refl :
      Ideal.ResidueField (maximalIdeal R) ⊗[R] S ≃ₐ[R] HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S)
    (AlgEquiv.trans (TensorProduct.comm R (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)) S)
        (AlgEquiv.restrictScalars R (AlgEquiv.symm (TensorProduct.quotIdealMapEquivTensorQuot S (maximalIdeal R)))) :
      HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S ≃ₐ[R]
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
this :
  Module.Finite.{u_1, u_2} R
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
⊢ LE.le (α := Ideal S)
    (RingHom.ker (F :=
      S →ₐ[R] HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
      (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))))
    (nilradical S)

Tactic:
Ideal.mk_ker.trans_le ?_

Premises used: Set.Mem, Eq.trans_le, Ideal.mk_ker
-- 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 : QuasiFinite R S
inst_4 : IsArtinianRing R
inst_5 : IsLocalRing R
e : Ideal.Fiber (maximalIdeal R) S ≃ₐ[R]
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :=
  AlgEquiv.trans
    (TensorProduct.congr
        (AlgEquiv.symm
          (AlgEquiv.ofBijective (Ideal.Quotient.liftₐ (maximalIdeal R) (ofId R (Ideal.ResidueField (maximalIdeal R))) ⋯)
            ⋯))
        AlgEquiv.refl :
      Ideal.ResidueField (maximalIdeal R) ⊗[R] S ≃ₐ[R] HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S)
    (AlgEquiv.trans (TensorProduct.comm R (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)) S)
        (AlgEquiv.restrictScalars R (AlgEquiv.symm (TensorProduct.quotIdealMapEquivTensorQuot S (maximalIdeal R)))) :
      HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S ≃ₐ[R]
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
this :
  Module.Finite.{u_1, u_2} R
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
refine_1 :
  LE.le (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R) : Ideal S) (nilradical S : Ideal S)
⊢ LE.le (α := Ideal S)
    (RingHom.ker (F :=
      S →ₐ[R] HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
      (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))))
    (nilradical S)

Tactic:
refine Ideal.mk_ker.trans_le ?_

Premises used: Eq.trans_le, Ideal.mk_ker
-- 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 : QuasiFinite R S
inst_4 : IsArtinianRing R
inst_5 : IsLocalRing R
e : Ideal.Fiber (maximalIdeal R) S ≃ₐ[R]
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :=
  AlgEquiv.trans
    (TensorProduct.congr
        (AlgEquiv.symm
          (AlgEquiv.ofBijective (Ideal.Quotient.liftₐ (maximalIdeal R) (ofId R (Ideal.ResidueField (maximalIdeal R))) ⋯)
            ⋯))
        AlgEquiv.refl :
      Ideal.ResidueField (maximalIdeal R) ⊗[R] S ≃ₐ[R] HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S)
    (AlgEquiv.trans (TensorProduct.comm R (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)) S)
        (AlgEquiv.restrictScalars R (AlgEquiv.symm (TensorProduct.quotIdealMapEquivTensorQuot S (maximalIdeal R)))) :
      HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S ≃ₐ[R]
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
this :
  Module.Finite.{u_1, u_2} R
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
refine_1 : LE.le (α := Ideal R) (nilradical R) (Ideal.comap (F := R →+* S) (algebraMap R S) (nilradical S))
⊢ LE.le (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R) : Ideal S) (nilradical S : Ideal S)

Tactic:
rw [Ideal.map_le_iff_le_comap, ← Ring.KrullDimLE.nilradical_eq_maximalIdeal]

Premises used: Ring.KrullDimLE.nilradical_eq_maximalIdeal, Ideal.map_le_iff_le_comap
-- 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 : QuasiFinite R S
inst_4 : IsArtinianRing R
inst_5 : IsLocalRing R
e : Ideal.Fiber (maximalIdeal R) S ≃ₐ[R]
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :=
  AlgEquiv.trans
    (TensorProduct.congr
        (AlgEquiv.symm
          (AlgEquiv.ofBijective (Ideal.Quotient.liftₐ (maximalIdeal R) (ofId R (Ideal.ResidueField (maximalIdeal R))) ⋯)
            ⋯))
        AlgEquiv.refl :
      Ideal.ResidueField (maximalIdeal R) ⊗[R] S ≃ₐ[R] HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S)
    (AlgEquiv.trans (TensorProduct.comm R (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)) S)
        (AlgEquiv.restrictScalars R (AlgEquiv.symm (TensorProduct.quotIdealMapEquivTensorQuot S (maximalIdeal R)))) :
      HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S ≃ₐ[R]
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
this :
  Module.Finite.{u_1, u_2} R
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
⊢ LE.le (α := Ideal R) (nilradical R) (Ideal.comap (F := R →+* S) (algebraMap R S) (nilradical S))

Tactic:
fun x hx ↦ IsNilpotent.map hx _

Premises used: Algebra.algebraMap, Set.Mem, setOf, IsNilpotent.map, Set.preimage, Set.singleton, IsNilpotent
-- 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 : QuasiFinite R S
inst_4 : IsArtinianRing R
inst_5 : IsLocalRing R
e : Ideal.Fiber (maximalIdeal R) S ≃ₐ[R]
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :=
  AlgEquiv.trans
    (TensorProduct.congr
        (AlgEquiv.symm
          (AlgEquiv.ofBijective (Ideal.Quotient.liftₐ (maximalIdeal R) (ofId R (Ideal.ResidueField (maximalIdeal R))) ⋯)
            ⋯))
        AlgEquiv.refl :
      Ideal.ResidueField (maximalIdeal R) ⊗[R] S ≃ₐ[R] HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S)
    (AlgEquiv.trans (TensorProduct.comm R (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)) S)
        (AlgEquiv.restrictScalars R (AlgEquiv.symm (TensorProduct.quotIdealMapEquivTensorQuot S (maximalIdeal R)))) :
      HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S ≃ₐ[R]
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
this :
  Module.Finite.{u_1, u_2} R
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
⊢ LE.le (α := Ideal R) (nilradical R) (Ideal.comap (F := R →+* S) (algebraMap R S) (nilradical S))

Tactic:
exact fun x hx ↦ IsNilpotent.map hx _

Premises used: IsNilpotent.map
-- 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 : QuasiFinite R S
inst_4 : IsArtinianRing R
inst_5 : IsLocalRing R
e : Ideal.Fiber (maximalIdeal R) S ≃ₐ[R]
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :=
  AlgEquiv.trans
    (TensorProduct.congr
        (AlgEquiv.symm
          (AlgEquiv.ofBijective (Ideal.Quotient.liftₐ (maximalIdeal R) (ofId R (Ideal.ResidueField (maximalIdeal R))) ⋯)
            ⋯))
        AlgEquiv.refl :
      Ideal.ResidueField (maximalIdeal R) ⊗[R] S ≃ₐ[R] HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S)
    (AlgEquiv.trans (TensorProduct.comm R (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)) S)
        (AlgEquiv.restrictScalars R (AlgEquiv.symm (TensorProduct.quotIdealMapEquivTensorQuot S (maximalIdeal R)))) :
      HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R) ⊗[R] S ≃ₐ[R]
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
this :
  Module.Finite.{u_1, u_2} R
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
refine_2 : Ideal.FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))
⊢ Ideal.FG
    (RingHom.ker (F :=
      S →ₐ[R] HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
      (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))))

Tactic:
rw [← RingHom.ker_coe_toRingHom, Ideal.Quotient.mkₐ_ker]

Premises used: Ideal.Quotient.mkₐ_ker, RingHom.ker_coe_toRingHom