awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
⊢ f.QuasiFinite

Tactic:
⟨fun P _ ↦ ?_⟩

Premises used: Algebra.QuasiFinite.mk, RingHom.QuasiFinite
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
refine : ∀ (P : Ideal R) (x : P.IsPrime), Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber S)
⊢ f.QuasiFinite

Tactic:
refine ⟨fun P _ ↦ ?_⟩
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
P : Ideal R
h : P.IsPrime
r : ↥s
⊢ Algebra.QuasiFinite R (Localization.Away (↑r : S))

Tactic:
have : Algebra.QuasiFinite R (Localization.Away r.1) := quasiFinite_algebraMap.mp (H r)
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
P : Ideal R
h : P.IsPrime
r : ↥s
this : Algebra.QuasiFinite R (Localization.Away (↑r : S))
⊢ Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber (Localization.Away (↑r : S)))

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
P : Ideal R
h : P.IsPrime
⊢ ∀ (r : ↥s), Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber (Localization.Away (↑r : S)))

Tactic:
have (r : s) : Module.Finite P.ResidueField (P.Fiber (Localization.Away r.1)) := by
    have : Algebra.QuasiFinite R (Localization.Away r.1) := quasiFinite_algebraMap.mp (H r)
    infer_instance
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f_1 : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f_1)
algInst : Algebra R S := f_1.toAlgebra
P : Ideal R
h : P.IsPrime
this : ∀ (r : ↥s), Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber (Localization.Away (↑r : S)))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away (↑r : S)) :=
  fun (r : ↥s) ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away (↑r : S)))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away (↑r : S)) :=
  Pi.algHom P.ResidueField (fun (r : ↥s) ↦ P.Fiber (Localization.Away (↑r : S))) φ
⊢ IsNoetherian.{u_6, u_6} P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away (↑r : S)))

Tactic:
have : IsNoetherian P.ResidueField (Π r : s, (P.Fiber (Localization.Away r.1))) :=
    isNoetherian_of_isNoetherianRing_of_finite ..
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f_1 : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f_1)
algInst : Algebra R S := f_1.toAlgebra
P : Ideal R
h : P.IsPrime
this_1 : ∀ (r : ↥s), Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber (Localization.Away (↑r : S)))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away (↑r : S)) :=
  fun (r : ↥s) ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away (↑r : S)))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away (↑r : S)) :=
  Pi.algHom P.ResidueField (fun (r : ↥s) ↦ P.Fiber (Localization.Away (↑r : S))) φ
this : IsNoetherian.{u_6, u_6} P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
suffices :
  Function.Injective (α := P.Fiber S) (β := (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    (⇑f : (a : P.Fiber S) → (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
⊢ Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber S)

Tactic:
suffices Function.Injective f from .of_injective f.toLinearMap this
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f_1 : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f_1)
algInst : Algebra R S := f_1.toAlgebra
P : Ideal R
h : P.IsPrime
this_1 : ∀ (r : ↥s), Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber (Localization.Away (↑r : S)))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away (↑r : S)) :=
  fun (r : ↥s) ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away (↑r : S)))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away (↑r : S)) :=
  Pi.algHom P.ResidueField (fun (r : ↥s) ↦ P.Fiber (Localization.Away (↑r : S))) φ
this : IsNoetherian.{u_6, u_6} P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
rw :
  ∀ (a : P.Fiber S),
    Eq (α := (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
        ((f : (a : P.Fiber S) → (r : ↥s) → P.Fiber (Localization.Away (↑r : S))) a :
          (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
        (0 : (r : ↥s) → P.Fiber (Localization.Away (↑r : S))) →
      a = 0
⊢ Function.Injective (α := P.Fiber S) (β := (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    (⇑f : (a : P.Fiber S) → (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f_1 : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f_1)
algInst : Algebra R S := f_1.toAlgebra
P : Ideal R
h : P.IsPrime
this_1 : ∀ (r : ↥s), Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber (Localization.Away (↑r : S)))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away (↑r : S)) :=
  fun (r : ↥s) ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away (↑r : S)))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away (↑r : S)) :=
  Pi.algHom P.ResidueField (fun (r : ↥s) ↦ P.Fiber (Localization.Away (↑r : S))) φ
this : IsNoetherian.{u_6, u_6} P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
a : P.Fiber S
ha :
  Eq (α := (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    ((f : (a : P.Fiber S) → (r : ↥s) → P.Fiber (Localization.Away (↑r : S))) a :
      (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    (0 : (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
apply :
  ∀ (J : Ideal (P.Fiber S)) (hJ : J.IsMaximal),
    Eq (α := Localization.AtPrime J)
      ((algebraMap (P.Fiber S) (Localization.AtPrime J) : (a : P.Fiber S) → Localization.AtPrime J) a :
        Localization.AtPrime J)
      (0 : Localization.AtPrime J)
⊢ a = 0

Tactic:
apply eq_zero_of_localization _ fun J hJ ↦ ?_

Premises used: eq_zero_of_localization
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f_1 : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f_1)
algInst : Algebra R S := f_1.toAlgebra
P : Ideal R
h : P.IsPrime
this_1 : ∀ (r : ↥s), Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber (Localization.Away (↑r : S)))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away (↑r : S)) :=
  fun (r : ↥s) ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away (↑r : S)))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away (↑r : S)) :=
  Pi.algHom P.ResidueField (fun (r : ↥s) ↦ P.Fiber (Localization.Away (↑r : S))) φ
this : IsNoetherian.{u_6, u_6} P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
a : P.Fiber S
ha :
  Eq (α := (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    ((f : (a : P.Fiber S) → (r : ↥s) → P.Fiber (Localization.Away (↑r : S))) a :
      (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    (0 : (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
I : (↑(P.primesOver S) : Type u_6) :=
  (OrderIso.symm (PrimeSpectrum.primesOverOrderIsoFiber R S P) :
      (a : PrimeSpectrum (P.Fiber S)) → (↑(P.primesOver S) : Type u_6))
    { asIdeal := J, isPrime := ⋯ }
⊢ ¬(↑s : Set S) ⊆ (↑(↑I : Ideal S) : Set S)

Tactic:
have : ¬ (s : Set S) ⊆ I.1 := fun h ↦
    Ideal.IsPrime.ne_top' (top_le_iff.mp (hs.symm.trans_le (Ideal.span_le.mpr h)))
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f_1 : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f_1)
algInst : Algebra R S := f_1.toAlgebra
P : Ideal R
h : P.IsPrime
this_1 : ∀ (r : ↥s), Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber (Localization.Away (↑r : S)))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away (↑r : S)) :=
  fun (r : ↥s) ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away (↑r : S)))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away (↑r : S)) :=
  Pi.algHom P.ResidueField (fun (r : ↥s) ↦ P.Fiber (Localization.Away (↑r : S))) φ
this_2 : IsNoetherian.{u_6, u_6} P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
a : P.Fiber S
ha :
  Eq (α := (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    ((f : (a : P.Fiber S) → (r : ↥s) → P.Fiber (Localization.Away (↑r : S))) a :
      (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    (0 : (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
I : (↑(P.primesOver S) : Type u_6) :=
  (OrderIso.symm (PrimeSpectrum.primesOverOrderIsoFiber R S P) :
      (a : PrimeSpectrum (P.Fiber S)) → (↑(P.primesOver S) : Type u_6))
    { asIdeal := J, isPrime := ⋯ }
this : ¬(↑s : Set S) ⊆ (↑(↑I : Ideal S) : Set S)
obtain :
  ∀ (r : S) (hrs : r ∈ (↑s : Set S)) (hrI : r ∉ (↑(↑I : Ideal S) : Set S)),
    Eq (α := Localization.AtPrime J)
      ((algebraMap (P.Fiber S) (Localization.AtPrime J) : (a : P.Fiber S) → Localization.AtPrime J) a :
        Localization.AtPrime J)
      (0 : Localization.AtPrime J)
⊢ Eq (α := Localization.AtPrime J)
    ((algebraMap (P.Fiber S) (Localization.AtPrime J) : (a : P.Fiber S) → Localization.AtPrime J) a :
      Localization.AtPrime J)
    (0 : Localization.AtPrime J)

Tactic:
obtain ⟨r, hrs, hrI⟩ := Set.not_subset.mp this

Premises used: Set.not_subset, Iff.mp
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f_1 : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f_1)
algInst : Algebra R S := f_1.toAlgebra
P : Ideal R
h : P.IsPrime
this_1 : ∀ (r : ↥s), Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber (Localization.Away (↑r : S)))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away (↑r : S)) :=
  fun (r : ↥s) ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away (↑r : S)))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away (↑r : S)) :=
  Pi.algHom P.ResidueField (fun (r : ↥s) ↦ P.Fiber (Localization.Away (↑r : S))) φ
this_2 : IsNoetherian.{u_6, u_6} P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
a : P.Fiber S
ha :
  Eq (α := (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    ((f : (a : P.Fiber S) → (r : ↥s) → P.Fiber (Localization.Away (↑r : S))) a :
      (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    (0 : (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
I : (↑(P.primesOver S) : Type u_6) :=
  (OrderIso.symm (PrimeSpectrum.primesOverOrderIsoFiber R S P) :
      (a : PrimeSpectrum (P.Fiber S)) → (↑(P.primesOver S) : Type u_6))
    { asIdeal := J, isPrime := ⋯ }
this : ¬(↑s : Set S) ⊆ (↑(↑I : Ideal S) : Set S)
r : S
hrs : r ∈ (↑s : Set S)
hrI : r ∉ (↑(↑I : Ideal S) : Set S)
⊢ LE.le (α := Submonoid S) (Submonoid.powers r)
    (Submonoid.comap (F := S →+* P.Fiber S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) J.primeCompl)

Tactic:
simpa [Submonoid.powers_le] using hrI

Premises used: Submonoid.powers_le
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f_1 : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f_1)
algInst : Algebra R S := f_1.toAlgebra
P : Ideal R
h : P.IsPrime
this_1 : ∀ (r : ↥s), Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber (Localization.Away (↑r : S)))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away (↑r : S)) :=
  fun (r : ↥s) ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away (↑r : S)))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away (↑r : S)) :=
  Pi.algHom P.ResidueField (fun (r : ↥s) ↦ P.Fiber (Localization.Away (↑r : S))) φ
this_2 : IsNoetherian.{u_6, u_6} P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
a : P.Fiber S
ha :
  Eq (α := (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    ((f : (a : P.Fiber S) → (r : ↥s) → P.Fiber (Localization.Away (↑r : S))) a :
      (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    (0 : (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
I : (↑(P.primesOver S) : Type u_6) :=
  (OrderIso.symm (PrimeSpectrum.primesOverOrderIsoFiber R S P) :
      (a : PrimeSpectrum (P.Fiber S)) → (↑(P.primesOver S) : Type u_6))
    { asIdeal := J, isPrime := ⋯ }
this : ¬(↑s : Set S) ⊆ (↑(↑I : Ideal S) : Set S)
r : S
hrs : r ∈ (↑s : Set S)
hrI : r ∉ (↑(↑I : Ideal S) : Set S)
⊢ ∀ (r_1 : R),
    Eq (α := Localization.AtPrime J)
      (OneHom.toFun (M := Localization.Away r)
          ((↑(↑(IsLocalization.map (T := J.primeCompl) (Localization.AtPrime J)
                      (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ⋯) :
                  Localization.Away r →* Localization.AtPrime J) :
              OneHom (Localization.Away r) (Localization.AtPrime J)) :
            OneHom (Localization.Away r) (Localization.AtPrime J))
          ((algebraMap R (Localization.Away r) : (a : R) → Localization.Away r) r_1 : Localization.Away r) :
        Localization.AtPrime J)
      ((algebraMap R (Localization.AtPrime J) : (a : R) → Localization.AtPrime J) r_1 : Localization.AtPrime J)

Tactic:
simp [IsScalarTower.algebraMap_apply R S (Localization.Away r),
        -Algebra.TensorProduct.algebraMap_apply,
        ← IsScalarTower.algebraMap_apply R _ (Localization.AtPrime J)]

Premises used: Algebra.TensorProduct.algebraMap_apply, Localization.AtPrime, Localization.Away, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f_1 : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f_1)
algInst : Algebra R S := f_1.toAlgebra
P : Ideal R
h_1 : P.IsPrime
this_1 : ∀ (r : ↥s), Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber (Localization.Away (↑r : S)))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away (↑r : S)) :=
  fun (r : ↥s) ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away (↑r : S)))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away (↑r : S)) :=
  Pi.algHom P.ResidueField (fun (r : ↥s) ↦ P.Fiber (Localization.Away (↑r : S))) φ
this_2 : IsNoetherian.{u_6, u_6} P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
a : P.Fiber S
ha :
  Eq (α := (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    ((f : (a : P.Fiber S) → (r : ↥s) → P.Fiber (Localization.Away (↑r : S))) a :
      (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    (0 : (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
I : (↑(P.primesOver S) : Type u_6) :=
  (OrderIso.symm (PrimeSpectrum.primesOverOrderIsoFiber R S P) :
      (a : PrimeSpectrum (P.Fiber S)) → (↑(P.primesOver S) : Type u_6))
    { asIdeal := J, isPrime := ⋯ }
this : ¬(↑s : Set S) ⊆ (↑(↑I : Ideal S) : Set S)
r : S
hrs : r ∈ (↑s : Set S)
hrI : r ∉ (↑(↑I : Ideal S) : Set S)
ψ : P.Fiber (Localization.Away r) →ₐ[P.ResidueField] Localization.AtPrime J :=
  Algebra.TensorProduct.lift (Algebra.ofId P.ResidueField (Localization.AtPrime J))
    {
      toRingHom :=
        IsLocalization.map (T := J.primeCompl) (Localization.AtPrime J)
          (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ⋯,
      commutes' := ⋯ }
    ⋯
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f_1 : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f_1)
algInst : Algebra R S := f_1.toAlgebra
P : Ideal R
h : P.IsPrime
this_1 : ∀ (r : ↥s), Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber (Localization.Away (↑r : S)))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away (↑r : S)) :=
  fun (r : ↥s) ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away (↑r : S)))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away (↑r : S)) :=
  Pi.algHom P.ResidueField (fun (r : ↥s) ↦ P.Fiber (Localization.Away (↑r : S))) φ
this_2 : IsNoetherian.{u_6, u_6} P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
a : P.Fiber S
ha :
  Eq (α := (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    ((f : (a : P.Fiber S) → (r : ↥s) → P.Fiber (Localization.Away (↑r : S))) a :
      (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    (0 : (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
I : (↑(P.primesOver S) : Type u_6) :=
  (OrderIso.symm (PrimeSpectrum.primesOverOrderIsoFiber R S P) :
      (a : PrimeSpectrum (P.Fiber S)) → (↑(P.primesOver S) : Type u_6))
    { asIdeal := J, isPrime := ⋯ }
this : ¬(↑s : Set S) ⊆ (↑(↑I : Ideal S) : Set S)
r : S
hrs : r ∈ (↑s : Set S)
hrI : r ∉ (↑(↑I : Ideal S) : Set S)
ψ : P.Fiber (Localization.Away r) →ₐ[P.ResidueField] Localization.AtPrime J :=
  Algebra.TensorProduct.lift (Algebra.ofId P.ResidueField (Localization.AtPrime J))
    {
      toRingHom :=
        IsLocalization.map (T := J.primeCompl) (Localization.AtPrime J)
          (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ⋯,
      commutes' := ⋯ }
    ⋯
x : S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [φ, ψ]
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f_1 : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f_1)
algInst : Algebra R S := f_1.toAlgebra
P : Ideal R
h : P.IsPrime
this_1 : ∀ (r : ↥s), Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber (Localization.Away (↑r : S)))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away (↑r : S)) :=
  fun (r : ↥s) ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away (↑r : S)))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away (↑r : S)) :=
  Pi.algHom P.ResidueField (fun (r : ↥s) ↦ P.Fiber (Localization.Away (↑r : S))) φ
this_2 : IsNoetherian.{u_6, u_6} P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
a : P.Fiber S
ha :
  Eq (α := (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    ((f : (a : P.Fiber S) → (r : ↥s) → P.Fiber (Localization.Away (↑r : S))) a :
      (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    (0 : (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
I : (↑(P.primesOver S) : Type u_6) :=
  (OrderIso.symm (PrimeSpectrum.primesOverOrderIsoFiber R S P) :
      (a : PrimeSpectrum (P.Fiber S)) → (↑(P.primesOver S) : Type u_6))
    { asIdeal := J, isPrime := ⋯ }
this : ¬(↑s : Set S) ⊆ (↑(↑I : Ideal S) : Set S)
r : S
hrs : r ∈ (↑s : Set S)
hrI : r ∉ (↑(↑I : Ideal S) : Set S)
ψ : P.Fiber (Localization.Away r) →ₐ[P.ResidueField] Localization.AtPrime J :=
  Algebra.TensorProduct.lift (Algebra.ofId P.ResidueField (Localization.AtPrime J))
    {
      toRingHom :=
        IsLocalization.map (T := J.primeCompl) (Localization.AtPrime J)
          (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ⋯,
      commutes' := ⋯ }
    ⋯
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have hψ : ψ.comp (φ ⟨r, hrs⟩) = IsScalarTower.toAlgHom _ _ _ := by ext; simp [φ, ψ]