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
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.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))

Tactic:
Ideal.FG.map (IsNoetherian.noetherian _) _

Premises used: Ideal.FG.map, IsNoetherian.noetherian
-- 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)))
⊢ Ideal.FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))

Tactic:
exact Ideal.FG.map (IsNoetherian.noetherian _) _

Premises used: Ideal.FG.map, IsNoetherian.noetherian
-- 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 : IsArtinianRing R
inst_4 : QuasiFinite R S
e : R ≃ₐ[R] PrimeSpectrum.PiLocalization R :=
  AlgEquiv.ofBijective (IsScalarTower.toAlgHom R R (PrimeSpectrum.PiLocalization R)) ⋯
have : ∀ (this : Fintype (PrimeSpectrum R)), Module.Finite R S
⊢ Module.Finite R S

Tactic:
have : Fintype (PrimeSpectrum R) := .ofFinite _
-- 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 : 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)
⊢ ∀ (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) _
-- 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 : IsArtinianRing R
inst_4 : QuasiFinite R S
e : R ≃ₐ[R] PrimeSpectrum.PiLocalization R :=
  AlgEquiv.ofBijective (IsScalarTower.toAlgHom R R (PrimeSpectrum.PiLocalization R)) ⋯
this_1 : 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)
this : ∀ (p : PrimeSpectrum R), Module.Finite R (Localization (M := R) p.asIdeal.primeCompl ⊗[R] S)
⊢ Module.Finite 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
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_1 : 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)
this : ∀ (p : PrimeSpectrum R), Module.Finite R (Localization (M := R) p.asIdeal.primeCompl ⊗[R] S)
⊢ Module.Finite 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 : IsArtinianRing R
inst_4 : QuasiFinite R S
let let₁ let₂ : Module.Finite R S
let₃ let₄ : ∀ (this : Fintype (PrimeSpectrum R)), Module.Finite R S
let₅ :
  ∀ (this : Fintype (PrimeSpectrum R))
    (this : ∀ (p : PrimeSpectrum R), Module.Finite R (Localization (M := R) p.asIdeal.primeCompl ⊗[R] S)),
    Module.Finite 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
-- 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 : IsArtinianRing R
⊢ QuasiFinite R S ↔ Module.Finite R S

Tactic:
⟨fun _ ↦ .of_quasiFinite, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, Module.Finite.of_quasiFinite
-- 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
inst_8 : QuasiFinite S T
⊢ QuasiFinite R T

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
inst_8 : QuasiFinite S T
refine : ∀ (P : Ideal R) (hP : P.IsPrime), Module.Finite P.ResidueField (P.Fiber T)
⊢ QuasiFinite R T

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 : QuasiFinite R S
f : S →ₐ[R] T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
⊢ QuasiFinite R T

Tactic:
let := f.toRingHom.toAlgebra
  let := IsScalarTower.of_algebraMap_eq' f.comp_algebraMap.symm
  have : Module.Finite S T := .of_surjective (Algebra.linearMap _ _) hf
  trans R S T

Premises used: Module.Finite.of_surjective, AlgHom.comp_algebraMap, Algebra.linearMap, IsScalarTower.of_algebraMap_eq', Algebra.QuasiFinite.trans, AlgHom.toRingHom, Eq.symm, RingHom.toAlgebra
-- 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
I : Ideal S
inst_7 : QuasiFinite R S
⊢ QuasiFinite.{u_1, u_2} R (S ⧸ I)

Tactic:
of_surjective_algHom (Ideal.Quotient.mkₐ _ _) Ideal.Quotient.mk_surjective

Premises used: Algebra.QuasiFinite.of_surjective_algHom, Ideal.Quotient.mk_surjective, Ideal.Quotient.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
e : S ≃ₐ[R] T
⊢ QuasiFinite R S ↔ QuasiFinite R T

Tactic:
⟨fun _ ↦ .of_surjective_algHom e.toAlgHom e.surjective,
    fun _ ↦ .of_surjective_algHom e.symm.toAlgHom e.symm.surjective⟩

Premises used: Algebra.QuasiFinite.of_surjective_algHom, AlgEquiv.toAlgHom, AlgEquiv.symm, Iff.intro, 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
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
⊢ QuasiFinite S T

Tactic:
⟨fun P hP ↦ .of_surjective (Algebra.linearMap P.ResidueField (P.Fiber T)) ?_⟩

Premises used: Module.Finite.of_surjective, Ideal.ResidueField, Algebra.QuasiFinite.mk, Algebra.linearMap, Ideal.Fiber
-- 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
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
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)
⊢ QuasiFinite S T

Tactic:
refine ⟨fun P hP ↦ .of_surjective (Algebra.linearMap P.ResidueField (P.Fiber T)) ?_⟩
-- 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
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
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))
⊢ Function.Surjective (α := P.ResidueField) (β := P.Fiber T)
    (⇑(Algebra.linearMap P.ResidueField (P.Fiber T)) : (a : P.ResidueField) → P.Fiber T)

Tactic:
rw [← LinearMap.coe_restrictScalars (R := S), ← LinearMap.range_eq_top,
      ← top_le_iff, ← TensorProduct.span_tmul_eq_top, Submodule.span_le]

Premises used: TensorProduct.span_tmul_eq_top, LinearMap.coe_restrictScalars, LinearMap.range_eq_top, top_le_iff, Submodule.span_le
-- 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
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : T
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))
⊢ 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))

Tactic:
obtain ⟨s, t, rfl⟩ := IsLocalization.exists_mk'_eq M s

Premises used: rfl, IsLocalization.exists_mk'_eq
-- 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
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
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)
⊢ 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:
use s • p / algebraMap _ _ t.1

Premises used: Algebra.algebraMap, Subtype.val, DFunLike.coe