awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ span {a}
⊢ Membership.mem (γ := Submodule R R) (span {x * y}) i
have hasup : a ∈ I ⊔ span {a}
Tactic: have hasup : a ∈ I ⊔ span {a} := mem_sup_right (mem_span_singleton_self a)
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ span {a}
hasup : a ∈ I ⊔ span {a}
⊢ Membership.mem (γ := Submodule R R) (span {x * y}) i
have hisup₁ : ∃ (a : R), a * x = i
Tactic: rw [hx, mem_span_singleton'] at hisup hasup
Cleared hypotheses: hisup, hasup
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ span {a}
hasup : a ∈ I ⊔ span {a}
hisup₁ : ∃ (a : R), a * x = i
⊢ Membership.mem (γ := Submodule R R) (span {x * y}) i
have hasup₁ : ∃ (a_1 : R), a_1 * x = a
Tactic: rw [hx, mem_span_singleton'] at hisup hasup
Cleared hypotheses: hisup, hasup
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}
i : R
hi : i ∈ I
hisup : ∃ (a : R), a * x = i
hasup : ∃ (a_1 : R), a_1 * x = a
⊢ Membership.mem (γ := Submodule R R) (span {x * y}) i
have refine_1 : ∀ (u : R) (hi : u * x ∈ I), Membership.mem (γ := Submodule R R) (span {x * y}) (u * x)
Tactic: obtain ⟨u, rfl⟩ := hisup
Cleared hypotheses: i, hi, hisup
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}
hasup : ∃ (a_1 : R), a_1 * x = a
u : R
hi : u * x ∈ I
⊢ Membership.mem (γ := Submodule R R) (span {x * y}) (u * x)
have refine_1 : ∀ (v : R) (hx : I ⊔ span {v * x} = span {x}) (hy : Submodule.colon I (↑(span {v * x}) : Set R) = span {y}),
  Membership.mem (γ := Submodule R R) (span {x * y}) (u * x)
Tactic: obtain ⟨v, rfl⟩ := hasup
Cleared hypotheses: a, hx, hy, hasup
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y u : R
hi : u * x ∈ I
v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I (↑(span {v * x}) : Set R) = span {y}
⊢ ∃ (z : R), z * y = u
have rw : u * x * v ∈ I
Tactic: rw [← mem_span_singleton', ← hy, mem_colon_span_singleton, mul_comm v, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y u : R
hi : u * x ∈ I
v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I (↑(span {v * x}) : Set R) = span {y}
⊢ Membership.mem (γ := Submodule R R) (span {x * y}) (u * x)
have refine_1 : ∀ (z : R) (hi : z * y * x ∈ I), Membership.mem (γ := Submodule R R) (span {x * y}) (z * y * x)
Tactic: obtain ⟨z, rfl⟩ : ∃ z, z * y = u := by
        rw [← mem_span_singleton', ← hy, mem_colon_span_singleton, mul_comm v, ← mul_assoc]
        exact mul_mem_right _ _ hi
Cleared hypotheses: u, hi
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I (↑(span {v * x}) : Set R) = span {y}
z : R
hi : z * y * x ∈ I
⊢ z * (x * y) = z * y * x
have rw : z * (x * y) = z * (y * x)
Tactic: rw [mul_assoc, mul_comm y]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I (↑(span {v * x}) : Set R) = span {y}
z : R
hi : z * y * x ∈ I
rw : z * (x * y) = z * (y * x)
⊢ z * (x * y) = z * y * x
have rw₁ : z * (x * y) = z * (x * y)
Tactic: rw [mul_assoc, mul_comm y]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}
⊢ span {x * y} ≤ I
have refine_2 : I * span {y} ≤ I ∧ y * a ∈ I
Tactic: rw [← span_singleton_mul_span_singleton, ← hx, Ideal.sup_mul, sup_le_iff,
        span_singleton_mul_span_singleton, mul_comm a, span_singleton_le_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (goal)
Goal:
R : Type u_1
inst : CommSemiring R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
⊢ IsPrincipalIdealRing R
have refine : ∀ (I : Ideal R) (hI : ¬Submodule.IsPrincipal I), ¬IsPrincipalIdealRing R
Tactic: refine ⟨isOka_isPrincipal.forall_of_forall_prime (fun I hI ↦ exists_maximal_not_isPrincipal ?_) H⟩
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (goal)
Goal:
R : Type u_1
inst : CommSemiring R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
I : Ideal R
hI : ¬Submodule.IsPrincipal I
⊢ ¬IsPrincipalIdealRing R
have rw : ∃ (x : Ideal R), ¬Submodule.IsPrincipal x
Tactic: rw [isPrincipalIdealRing_iff, not_forall]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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
⊢ Set.Finite (α := Ideal S) (I.primesOver S)
have pos : ∀ (h : I.IsPrime), Set.Finite (α := Ideal S) (I.primesOver S)
Tactic: by_cases h : I.IsPrime
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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)
⊢ Set.Finite (α := Ideal S) (I.primesOver S)
have neg : ∀ (h : ¬I.IsPrime), Set.Finite (α := Ideal S) (I.primesOver S)
Tactic: by_cases h : I.IsPrime
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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)
have 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 }})
Tactic: refine ((finite_comap_preimage_singleton ⟨I, h⟩).image PrimeSpectrum.asIdeal).subset ?_
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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)
have h₁ : Eq (α := Set (Ideal S)) (I.primesOver S) ∅
Tactic: convert! Set.finite_empty
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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
⊢ Eq (α := Set (Ideal S)) (I.primesOver S) ∅
have h₁ : ∀ (this : Set.Nonempty (α := Ideal S) (I.primesOver S)), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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)
⊢ False
have h₁ : ∀ (J : Ideal S) (h₁ : J.IsPrime) (h : ¬Ideal.IsPrime (Ideal.under R J)), False
Tactic: obtain ⟨J, h₁, ⟨rfl⟩⟩ := this
Cleared hypotheses: I, h, this
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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)
have refine : ∀ (P : Ideal A) (hP : P.IsPrime), Module.Finite P.ResidueField (P.Fiber (A ⊗[R] S))
Tactic: refine ⟨fun P hP ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
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 R S
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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
have 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)
Tactic: refine Module.finite_of_surjective_of_ker_le_nilradical (Ideal.Quotient.mkₐ R
    ((maximalIdeal R).map (algebraMap R S))) Ideal.Quotient.mk_surjective ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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)
⊢ Module.Finite R S
have 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))))
Tactic: refine Module.finite_of_surjective_of_ker_le_nilradical (Ideal.Quotient.mkₐ R
    ((maximalIdeal R).map (algebraMap R S))) Ideal.Quotient.mk_surjective ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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)
have refine_1 : LE.le (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R) : Ideal S) (nilradical S : Ideal S)
Tactic: refine Ideal.mk_ker.trans_le ?_
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R) : Ideal S) (nilradical S : Ideal S)
have refine_1 : LE.le (α := Ideal R) (nilradical R) (Ideal.comap (F := R →+* S) (algebraMap R S) (nilradical S))
Tactic: rw [Ideal.map_le_iff_le_comap, ← Ring.KrullDimLE.nilradical_eq_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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)))
⊢ 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))))
have refine_2 : Ideal.FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))
Tactic: rw [← RingHom.ker_coe_toRingHom, Ideal.Quotient.mkₐ_ker]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsArtinianRing R
inst_4 : QuasiFinite R S
e : R ≃ₐ[R] PrimeSpectrum.PiLocalization R :=
  AlgEquiv.ofBijective (IsScalarTower.toAlgHom R R (PrimeSpectrum.PiLocalization R)) ⋯
⊢ Module.Finite R S
have have : ∀ (this : Fintype (PrimeSpectrum R)), Module.Finite R S
Tactic: have : Fintype (PrimeSpectrum R) := .ofFinite _
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsArtinianRing R
inst_4 : QuasiFinite R S
e : R ≃ₐ[R] PrimeSpectrum.PiLocalization R :=
  AlgEquiv.ofBijective (IsScalarTower.toAlgHom R R (PrimeSpectrum.PiLocalization R)) ⋯
this : Fintype (PrimeSpectrum R)
e' : S ≃ₐ[R] (p : PrimeSpectrum R) → Localization (M := R) p.asIdeal.primeCompl ⊗[R] S :=
  AlgEquiv.trans (A₂ := S ⊗[R] R) (AlgEquiv.symm (TensorProduct.rid R R S) : S ≃ₐ[R] S ⊗[R] R)
    (AlgEquiv.trans (A₂ := S ⊗[R] PrimeSpectrum.PiLocalization R)
        (TensorProduct.congr AlgEquiv.refl e : S ⊗[R] R ≃ₐ[R] S ⊗[R] PrimeSpectrum.PiLocalization R)
        (AlgEquiv.trans
            (TensorProduct.piRight R R S fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl :
              S ⊗[R] ((i : PrimeSpectrum R) → Localization (M := R) i.asIdeal.primeCompl) ≃ₐ[R]
                (i : PrimeSpectrum R) → S ⊗[R] Localization (M := R) i.asIdeal.primeCompl)
            (AlgEquiv.piCongrRight (A₁ := fun (i : PrimeSpectrum R) ↦ S ⊗[R] Localization (M := R) i.asIdeal.primeCompl)
                (A₂ := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl ⊗[R] S)
                fun (x : PrimeSpectrum R) ↦ TensorProduct.comm R S (Localization (M := R) x.asIdeal.primeCompl) :
              ((i : PrimeSpectrum R) → S ⊗[R] Localization (M := R) i.asIdeal.primeCompl) ≃ₐ[R]
                (i : PrimeSpectrum R) → Localization (M := R) i.asIdeal.primeCompl ⊗[R] S) :
          S ⊗[R] ((i : PrimeSpectrum R) → Localization (M := R) i.asIdeal.primeCompl) ≃ₐ[R]
            (p : PrimeSpectrum R) → Localization (M := R) p.asIdeal.primeCompl ⊗[R] S) :
      S ⊗[R] R ≃ₐ[R] (p : PrimeSpectrum R) → Localization (M := R) p.asIdeal.primeCompl ⊗[R] S)
⊢ Module.Finite R S
have this₁ : ∀ (p : PrimeSpectrum R), Module.Finite R (Localization (M := R) p.asIdeal.primeCompl ⊗[R] S)
Tactic: have (p : PrimeSpectrum R) : Module.Finite R (Localization p.asIdeal.primeCompl ⊗[R] S) :=
    have : Module.Finite R (Localization.AtPrime p.asIdeal) :=
      .of_surjective (Algebra.linearMap _ _)
        (IsArtinianRing.localization_surjective p.asIdeal.primeCompl _)
    have : Module.Finite (Localization.AtPrime p.asIdeal)
      (Localization.AtPrime p.asIdeal ⊗[R] S) := finite_of_isArtinianRing_of_isLocalRing
    .trans (Localization.AtPrime p.asIdeal) _
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsArtinianRing R
inst_4 : QuasiFinite R S
let let₁ let₂ : Module.Finite R S
⊢ Module.Finite R S
have let₃ : ∀ (this : Fintype (PrimeSpectrum R)), Module.Finite R S
Tactic: classical
  let e : R ≃ₐ[R] PrimeSpectrum.PiLocalization R :=
    .ofBijective (IsScalarTower.toAlgHom _ _ _)
      (PrimeSpectrum.discreteTopology_iff_toPiLocalization_bijective.mp inferInstance)
  have : Fintype (PrimeSpectrum R) := .ofFinite _
  let e' : S ≃ₐ[R] Π p : PrimeSpectrum R, Localization p.asIdeal.primeCompl ⊗[R] S :=
    (Algebra.TensorProduct.rid R R S).symm.trans <| (Algebra.TensorProduct.congr .refl e).trans <|
      (Algebra.TensorProduct.piRight _ _ _ _).trans <| AlgEquiv.piCongrRight
      fun _ ↦ Algebra.TensorProduct.comm _ _ _
  have (p : PrimeSpectrum R) : Module.Finite R (Localization p.asIdeal.primeCompl ⊗[R] S) :=
    have : Module.Finite R (Localization.AtPrime p.asIdeal) :=
      .of_surjective (Algebra.linearMap _ _)
        (IsArtinianRing.localization_surjective p.asIdeal.primeCompl _)
    have : Module.Finite (Localization.AtPrime p.asIdeal)
      (Localization.AtPrime p.asIdeal ⊗[R] S) := finite_of_isArtinianRing_of_isLocalRing
    .trans (Localization.AtPrime p.asIdeal) _
  exact .of_surjective e'.symm.toLinearMap e'.symm.surjective