awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
let₃ let₄ : ∀ (this : Fintype (PrimeSpectrum R)), Module.Finite R S
⊢ Module.Finite R S
have let₅ : ∀ (this : Fintype (PrimeSpectrum R))
  (this : ∀ (p : PrimeSpectrum R), Module.Finite R (Localization (M := R) p.asIdeal.primeCompl ⊗[R] S)),
  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
-- 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
inst_8 : QuasiFinite S T
⊢ QuasiFinite R T
have refine : ∀ (P : Ideal R) (hP : P.IsPrime), Module.Finite P.ResidueField (P.Fiber T)
Tactic: refine ⟨fun P hP ↦ ?_⟩
-- 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
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
⊢ QuasiFinite S T
have refine : ∀ (P : Ideal S) (hP : P.IsPrime),
  Function.Surjective (α := P.ResidueField) (β := P.Fiber T)
    (⇑(Algebra.linearMap P.ResidueField (P.Fiber T)) : (a : P.ResidueField) → P.Fiber T)
Tactic: refine ⟨fun P hP ↦ .of_surjective (Algebra.linearMap P.ResidueField (P.Fiber T)) ?_⟩
-- 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
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
⊢ Function.Surjective (α := P.ResidueField) (β := P.Fiber T)
    (⇑(Algebra.linearMap P.ResidueField (P.Fiber T)) : (a : P.ResidueField) → P.Fiber T)
have rw : {t : P.ResidueField ⊗[S] T | ∃ (m : P.ResidueField) (n : T), m ⊗ₜ[S] n = t} ⊆
  (↑(LinearMap.range (M := P.ResidueField)
        ((↑S :
            {S_1 M : Type u_2} →
              {M₂ : Type (max u_2 u_3)} →
                [inst : Semiring S] →
                  [inst_9 : Semiring S_1] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module S M] →
                          [inst_13 : Module S M₂] →
                            [inst_14 : Module S_1 M] →
                              [inst_15 : Module S_1 M₂] →
                                [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
          (Algebra.linearMap P.ResidueField (P.Fiber T)))) :
    Set (P.ResidueField ⊗[S] T))
Tactic: rw [← LinearMap.coe_restrictScalars (R := S), ← LinearMap.range_eq_top,
      ← top_le_iff, ← TensorProduct.span_tmul_eq_top, Submodule.span_le]
-- 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
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : T
⊢ p ⊗ₜ[S] s ∈
    (↑(LinearMap.range (M := P.ResidueField)
          ((↑S :
              {S_1 M : Type u_2} →
                {M₂ : Type (max u_2 u_3)} →
                  [inst : Semiring S] →
                    [inst_9 : Semiring S_1] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [inst_14 : Module S_1 M] →
                                [inst_15 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (Algebra.linearMap P.ResidueField (P.Fiber T)))) :
      Set (P.ResidueField ⊗[S] T))
have obtain : ∀ (s : S) (t : ↥M),
  p ⊗ₜ[S] IsLocalization.mk' T s t ∈
    (↑(LinearMap.range (M := P.ResidueField)
          ((↑S :
              {S_1 M : Type u_2} →
                {M₂ : Type (max u_2 u_3)} →
                  [inst : Semiring S] →
                    [inst_9 : Semiring S_1] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [inst_14 : Module S_1 M] →
                                [inst_15 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (Algebra.linearMap P.ResidueField (P.Fiber T)))) :
      Set (P.ResidueField ⊗[S] T))
Tactic: obtain ⟨s, t, rfl⟩ := IsLocalization.exists_mk'_eq M s
Cleared hypotheses: s
-- 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
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
⊢ p ⊗ₜ[S] IsLocalization.mk' T s t ∈
    (↑(LinearMap.range (M := P.ResidueField)
          ((↑S :
              {S_1 M : Type u_2} →
                {M₂ : Type (max u_2 u_3)} →
                  [inst : Semiring S] →
                    [inst_9 : Semiring S_1] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [inst_14 : Module S_1 M] →
                                [inst_15 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (Algebra.linearMap P.ResidueField (P.Fiber T)))) :
      Set (P.ResidueField ⊗[S] T))
have h : Eq (α := P.Fiber T)
  (((↑S :
            {S_1 M : Type u_2} →
              {M₂ : Type (max u_2 u_3)} →
                [inst : Semiring S] →
                  [inst_9 : Semiring S_1] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module S M] →
                          [inst_13 : Module S M₂] →
                            [inst_14 : Module S_1 M] →
                              [inst_15 : Module S_1 M₂] →
                                [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
          (Algebra.linearMap P.ResidueField (P.Fiber T)) :
        (a : P.ResidueField) → P.Fiber T)
      (HDiv.hDiv (β := P.ResidueField) (s • p)
        ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField)) :
    P.Fiber T)
  (p ⊗ₜ[S] IsLocalization.mk' T s t : P.ResidueField ⊗[S] T)
Tactic: use s • p / algebraMap _ _ t.1
-- 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
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
⊢ Eq (α := P.Fiber T)
    (((↑S :
              {S_1 M : Type u_2} →
                {M₂ : Type (max u_2 u_3)} →
                  [inst : Semiring S] →
                    [inst_9 : Semiring S_1] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [inst_14 : Module S_1 M] →
                                [inst_15 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (Algebra.linearMap P.ResidueField (P.Fiber T)) :
          (a : P.ResidueField) → P.Fiber T)
        (HDiv.hDiv (β := P.ResidueField) (s • p)
          ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField)) :
      P.Fiber T)
    (p ⊗ₜ[S] IsLocalization.mk' T s t : P.ResidueField ⊗[S] T)
have h : Eq (α := P.ResidueField ⊗[S] T)
  ((fun (x : P.ResidueField ⊗[S] T) ↦
      HMul.hMul (β := P.ResidueField ⊗[S] T) x
        ((TensorProduct.includeRight : (a : T) → P.ResidueField ⊗[S] T) ((algebraMap S T : (a : S) → T) (↑t : S)) :
          P.ResidueField ⊗[S] T))
    (((↑S :
            {S_1 M : Type u_2} →
              {M₂ : Type (max u_2 u_3)} →
                [inst : Semiring S] →
                  [inst_9 : Semiring S_1] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module S M] →
                          [inst_13 : Module S M₂] →
                            [inst_14 : Module S_1 M] →
                              [inst_15 : Module S_1 M₂] →
                                [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
          (Algebra.linearMap P.ResidueField (P.Fiber T)) :
        (a : P.ResidueField) → P.Fiber T)
      (HDiv.hDiv (β := P.ResidueField) (s • p)
        ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField))))
  ((fun (x : P.ResidueField ⊗[S] T) ↦
      HMul.hMul (β := P.ResidueField ⊗[S] T) x
        ((TensorProduct.includeRight : (a : T) → P.ResidueField ⊗[S] T) ((algebraMap S T : (a : S) → T) (↑t : S)) :
          P.ResidueField ⊗[S] T))
    (p ⊗ₜ[S] IsLocalization.mk' T s t))
Tactic: apply ((IsLocalization.map_units T t).map
      Algebra.TensorProduct.includeRight).mul_left_injective
-- 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
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
ht :
  ¬Eq (α := P.ResidueField) ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField)
      (0 : P.ResidueField)
⊢ Eq (α := P.ResidueField ⊗[S] T)
    ((fun (x : P.ResidueField ⊗[S] T) ↦
        HMul.hMul (β := P.ResidueField ⊗[S] T) x
          ((TensorProduct.includeRight : (a : T) → P.ResidueField ⊗[S] T) ((algebraMap S T : (a : S) → T) (↑t : S)) :
            P.ResidueField ⊗[S] T))
      (((↑S :
              {S_1 M : Type u_2} →
                {M₂ : Type (max u_2 u_3)} →
                  [inst : Semiring S] →
                    [inst_9 : Semiring S_1] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [inst_14 : Module S_1 M] →
                                [inst_15 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (Algebra.linearMap P.ResidueField (P.Fiber T)) :
          (a : P.ResidueField) → P.Fiber T)
        (HDiv.hDiv (β := P.ResidueField) (s • p)
          ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField))))
    ((fun (x : P.ResidueField ⊗[S] T) ↦
        HMul.hMul (β := P.ResidueField ⊗[S] T) x
          ((TensorProduct.includeRight : (a : T) → P.ResidueField ⊗[S] T) ((algebraMap S T : (a : S) → T) (↑t : S)) :
            P.ResidueField ⊗[S] T))
      (p ⊗ₜ[S] IsLocalization.mk' T s t))
have trans : Eq (α := P.ResidueField ⊗[S] T)
  ((fun (x : P.ResidueField ⊗[S] T) ↦
      HMul.hMul (β := P.ResidueField ⊗[S] T) x
        ((TensorProduct.includeRight : (a : T) → P.ResidueField ⊗[S] T) ((algebraMap S T : (a : S) → T) (↑t : S)) :
          P.ResidueField ⊗[S] T))
    (((↑S :
            {S_1 M : Type u_2} →
              {M₂ : Type (max u_2 u_3)} →
                [inst : Semiring S] →
                  [inst_9 : Semiring S_1] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module S M] →
                          [inst_13 : Module S M₂] →
                            [inst_14 : Module S_1 M] →
                              [inst_15 : Module S_1 M₂] →
                                [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
          (Algebra.linearMap P.ResidueField (P.Fiber T)) :
        (a : P.ResidueField) → P.Fiber T)
      (HDiv.hDiv (β := P.ResidueField) (s • p)
        ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField))))
  ((s • p) ⊗ₜ[S] 1)
Tactic: trans (s • p) ⊗ₜ[S] 1
-- 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
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
ht :
  ¬Eq (α := P.ResidueField) ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField)
      (0 : P.ResidueField)
⊢ Eq (α := P.ResidueField ⊗[S] T) ((s • p) ⊗ₜ[S] 1)
    ((fun (x : P.ResidueField ⊗[S] T) ↦
        HMul.hMul (β := P.ResidueField ⊗[S] T) x
          ((TensorProduct.includeRight : (a : T) → P.ResidueField ⊗[S] T) ((algebraMap S T : (a : S) → T) (↑t : S)) :
            P.ResidueField ⊗[S] T))
      (p ⊗ₜ[S] IsLocalization.mk' T s t))
have dsimp : Eq (α := P.ResidueField ⊗[S] T) ((s • p) ⊗ₜ[S] 1)
  ((p * 1) ⊗ₜ[S] HMul.hMul (β := T) (IsLocalization.mk' T s t) ((algebraMap S T : (a : S) → T) (↑t : S) : T))
Tactic: dsimp
-- 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 T
⊢ QuasiFinite S T
have refine : ∀ (P : Ideal S) (hP : P.IsPrime), Module.Finite P.ResidueField (P.Fiber T)
Tactic: refine ⟨fun P hP ↦ ?_⟩
-- 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 T
P : Ideal S
hP : P.IsPrime
f : TensorProduct.{u_1, u_2, u_3} R P.ResidueField T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
⊢ Function.Surjective (α := TensorProduct.{u_1, u_2, u_3} R P.ResidueField T) (β := P.Fiber T)
    (⇑f : (a : P.ResidueField ⊗[R] T) → P.Fiber T)
have rw : {t : P.ResidueField ⊗[S] T | ∃ (m : P.ResidueField) (n : T), m ⊗ₜ[S] n = t} ⊆
  (↑(LinearMap.range (AlgHom.toLinearMap (AlgHom.restrictScalars S f))) : Set (P.ResidueField ⊗[S] T))
Tactic: rw [← AlgHom.coe_restrictScalars' (R := S), ← AlgHom.coe_toLinearMap, ← LinearMap.range_eq_top,
      ← top_le_iff, ← TensorProduct.span_tmul_eq_top, Submodule.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
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 T
P : Ideal S
hP : P.IsPrime
f : TensorProduct.{u_1, u_2, u_3} R P.ResidueField T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
⊢ Module.Finite P.ResidueField (P.Fiber T)
have hf : Function.Surjective (α := TensorProduct.{u_1, u_2, u_3} R P.ResidueField T) (β := P.Fiber T)
  (⇑f : (a : P.ResidueField ⊗[R] T) → P.Fiber T)
Tactic: have hf : Function.Surjective f := by
    rw [← AlgHom.coe_restrictScalars' (R := S), ← AlgHom.coe_toLinearMap, ← LinearMap.range_eq_top,
      ← top_le_iff, ← TensorProduct.span_tmul_eq_top, Submodule.span_le]
    rintro _ ⟨a, b, rfl⟩
    exact ⟨a ⊗ₜ b, by simp [f]⟩
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
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 T
P : Ideal S
hP : P.IsPrime
f : TensorProduct.{u_1, u_2, u_3} R P.ResidueField T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
hf :
  Function.Surjective (α := TensorProduct.{u_1, u_2, u_3} R P.ResidueField T) (β := P.Fiber T)
    (⇑f : (a : P.ResidueField ⊗[R] T) → P.Fiber T)
⊢ Module.Finite P.ResidueField (P.Fiber T)
have this : Module.Finite P.ResidueField (TensorProduct.{u_1, u_2, u_3} R P.ResidueField T)
Tactic: have : Module.Finite P.ResidueField (P.ResidueField ⊗[R] T) := .of_quasiFinite
-- 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 : QuasiFinite R S
f : S →ₐ[R] T
H :
  ∀ (x : T),
    ∃ (s : S),
      IsUnit.{u_3} (M := T) ((f : (a : S) → T) s : T) ∧ HMul.hMul (β := T) x ((f : (a : S) → T) s : T) ∈ f.range
φ : AlgHom.{u_1, u_2, u_3} R (Localization (Submonoid.comap f (IsUnit.submonoid T))) T :=
  IsLocalization.liftAlgHom (M := Submonoid.comap f (IsUnit.submonoid T)) (f := f) ⋯
⊢ QuasiFinite R T
have suffices : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Localization (Submonoid.comap f (IsUnit.submonoid T))) (β := T)
  (⇑φ : (a : Localization (Submonoid.comap f (IsUnit.submonoid T))) → T)
Tactic: suffices Function.Surjective φ from .of_surjective_algHom φ 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 : QuasiFinite R S
f : S →ₐ[R] T
H :
  ∀ (x : T),
    ∃ (s : S),
      IsUnit.{u_3} (M := T) ((f : (a : S) → T) s : T) ∧ HMul.hMul (β := T) x ((f : (a : S) → T) s : T) ∈ f.range
φ : AlgHom.{u_1, u_2, u_3} R (Localization (Submonoid.comap f (IsUnit.submonoid T))) T :=
  IsLocalization.liftAlgHom (M := Submonoid.comap f (IsUnit.submonoid T)) (f := f) ⋯
x : T
⊢ ∃ (a : Localization (Submonoid.comap f (IsUnit.submonoid T))),
    (φ : (a : Localization (Submonoid.comap f (IsUnit.submonoid T))) → T) a = x
have obtain : ∀ (s : S) (hs : IsUnit.{u_3} (M := T) ((f : (a : S) → T) s : T)) (t : S)
  (ht : (f.toRingHom : (a : S) → T) t = HMul.hMul (β := T) x ((f : (a : S) → T) s : T)),
  ∃ (a : Localization (Submonoid.comap f (IsUnit.submonoid T))),
    (φ : (a : Localization (Submonoid.comap f (IsUnit.submonoid T))) → T) a = x
Tactic: obtain ⟨s, hs, t, ht⟩ := H x
-- 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 : QuasiFinite R S
f : S →ₐ[R] T
H :
  ∀ (x : T),
    ∃ (s : S),
      IsUnit.{u_3} (M := T) ((f : (a : S) → T) s : T) ∧ HMul.hMul (β := T) x ((f : (a : S) → T) s : T) ∈ f.range
φ : AlgHom.{u_1, u_2, u_3} R (Localization (Submonoid.comap f (IsUnit.submonoid T))) T :=
  IsLocalization.liftAlgHom (M := Submonoid.comap f (IsUnit.submonoid T)) (f := f) ⋯
x : T
s : S
hs : IsUnit.{u_3} (M := T) ((f : (a : S) → T) s : T)
t : S
ht : (f.toRingHom : (a : S) → T) t = HMul.hMul (β := T) x ((f : (a : S) → T) s : T)
⊢ ∃ (a : Localization (Submonoid.comap f (IsUnit.submonoid T))),
    (φ : (a : Localization (Submonoid.comap f (IsUnit.submonoid T))) → T) a = x
have refine : (φ : (a : Localization (Submonoid.comap f (IsUnit.submonoid T))) → T)
    (IsLocalization.mk' (M := Submonoid.comap f (IsUnit.submonoid T))
      (Localization (Submonoid.comap f (IsUnit.submonoid T))) t
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.comap f (IsUnit.submonoid T)) x) s
        hs)) =
  x
Tactic: refine ⟨IsLocalization.mk' (M := (IsUnit.submonoid T).comap f) _ t ⟨s, hs⟩, ?_⟩
-- 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 : FiniteType R S
⊢ QuasiFinite R S ↔
    ∀ (x : PrimeSpectrum R),
      Set.Finite (α := PrimeSpectrum S) (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {x})
have refine : ∀
  (H :
    ∀ (x : PrimeSpectrum R),
      Set.Finite (α := PrimeSpectrum S)
        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {x}))
  (P : Ideal R) (x : P.IsPrime), Module.Finite P.ResidueField (P.Fiber S)
Tactic: refine ⟨fun H _ ↦ finite_comap_preimage_singleton _, fun H ↦ ⟨fun P _ ↦ ?_⟩⟩
-- 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 : FiniteType R S
H :
  ∀ (x : PrimeSpectrum R),
    Set.Finite (α := PrimeSpectrum S) (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {x})
P : Ideal R
h : P.IsPrime
⊢ Module.Finite P.ResidueField (P.Fiber S)
have rw : IsNoetherianRing (P.Fiber S) ∧ Ring.KrullDimLE 0 (P.Fiber S)
Tactic: rw [Module.finite_iff_isArtinianRing, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero]
-- 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 : FiniteType R S
H :
  ∀ (x : PrimeSpectrum R),
    Set.Finite (α := PrimeSpectrum S) (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {x})
P : Ideal R
h : P.IsPrime
⊢ IsNoetherianRing (P.Fiber S) ∧ Ring.KrullDimLE 0 (P.Fiber S)
have this : IsJacobsonRing (P.Fiber S)
Tactic: have : IsJacobsonRing (P.Fiber S) := isJacobsonRing_of_finiteType (A := P.ResidueField)