awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.OpenImmersion (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
f : R →+* S
g : S →+* T
hg : g.IsStandardOpenImmersion
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.IsStandardOpenImmersion R S
algebraizeInst_1 : Algebra.IsStandardOpenImmersion S T
r : R
hr : IsLocalization.Away r S
⊢ (g.comp f).IsStandardOpenImmersion
have obtain : ∀ (s : S) (hs : IsLocalization.Away s T), (g.comp f).IsStandardOpenImmersion
Tactic: obtain ⟨s, hs⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.OpenImmersion (goal)
Goal:
⊢ IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardOpenImmersion
have refine : ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  IsStandardOpenImmersion (algebraMap R T) →
    IsStandardOpenImmersion (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
Tactic: refine .mk respectsIso ?_
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.OpenImmersion (goal)
Goal:
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : IsStandardOpenImmersion (algebraMap R T)
⊢ IsStandardOpenImmersion (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
have rw : ∀ (h : Algebra.IsStandardOpenImmersion R T), Algebra.IsStandardOpenImmersion S (TensorProduct R S T)
Tactic: rw [isStandardOpenImmersion_algebraMap] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ QuasiFinite (algebraMap R S) ↔ Algebra.QuasiFinite R S
have rw : Algebra.QuasiFinite R S ↔ Algebra.QuasiFinite R S
Tactic: rw [RingHom.QuasiFinite, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Algebra.QuasiFinite R S ↔ Algebra.QuasiFinite R S
⊢ QuasiFinite (algebraMap R S) ↔ Algebra.QuasiFinite R S
have rw₁ : Algebra.QuasiFinite R S ↔ Algebra.QuasiFinite R S
Tactic: rw [RingHom.QuasiFinite, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (hypothesis)
Goal:
T : Type u_3
inst : CommRing T
R : Type u_4
S : Type u_5
inst_1 : CommRing R
inst_2 : CommRing S
f : S →+* T
g : R →+* S
hf : f.QuasiFinite
hg : g.QuasiFinite
⊢ (f.comp g).QuasiFinite
have algebraizeInst : Algebra.QuasiFinite S T
Tactic: algebraize [f, g, (f.comp g)]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (hypothesis)
Goal:
T : Type u_3
inst : CommRing T
R : Type u_4
S : Type u_5
inst_1 : CommRing R
inst_2 : CommRing S
f : S →+* T
g : R →+* S
hf : f.QuasiFinite
hg : g.QuasiFinite
algebraizeInst : Algebra.QuasiFinite S T
⊢ (f.comp g).QuasiFinite
have algebraizeInst₁ : Algebra.QuasiFinite R S
Tactic: algebraize [f, g, (f.comp g)]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (hypothesis)
Goal:
T : Type u_3
inst : CommRing T
R : Type u_4
S : Type u_5
inst_1 : CommRing R
inst_2 : CommRing S
f : S →+* T
g : R →+* S
h : (f.comp g).QuasiFinite
⊢ f.QuasiFinite
have algebraizeInst : Algebra.QuasiFinite R T
Tactic: algebraize [f, g, (f.comp g)]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (hypothesis)
Goal:
T : Type u_3
inst : CommRing T
S : Type u_5
inst_1 : CommRing S
f : S →+* T
hf : f.Finite
⊢ f.QuasiFinite
have algebraizeInst : Module.Finite S T
Tactic: algebraize [f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (goal)
Goal:
⊢ IsStableUnderBaseChange.{u_6} fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ QuasiFinite
have refine : ∀ ⦃R S T : Type u_6⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  QuasiFinite (algebraMap R T) → QuasiFinite (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
Tactic: refine .mk respectsIso ?_
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (goal)
Goal:
R S T : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
H : QuasiFinite (algebraMap R T)
⊢ QuasiFinite (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
have rw : ∀ (H : Algebra.QuasiFinite R T), Algebra.QuasiFinite S (TensorProduct R S T)
Tactic: rw [quasiFinite_algebraMap] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (goal)
Goal:
⊢ OfLocalizationSpanTarget.{u_6} fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ QuasiFinite
have rw : OfLocalizationFiniteSpanTarget.{u_6} fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ QuasiFinite
Tactic: rw [RingHom.ofLocalizationSpanTarget_iff_finite]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (goal)
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
have refine : ∀ (P : Ideal R) (x : P.IsPrime), Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber S)
Tactic: refine ⟨fun P _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (hypothesis)
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)))
have this : Algebra.QuasiFinite R (Localization.Away (↑r : S))
Tactic: have : Algebra.QuasiFinite R (Localization.Away r.1) := quasiFinite_algebraMap.mp (H r)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (hypothesis)
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
⊢ Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber S)
have this : ∀ (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
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (hypothesis)
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))) φ
⊢ Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber S)
have this₁ : 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 ..
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (goal)
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)))
⊢ Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber S)
have 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)))
Tactic: suffices Function.Injective f from .of_injective f.toLinearMap this
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (goal)
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)))
⊢ 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)))
have 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
Tactic: rw [injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (goal)
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)))
⊢ a = 0
have 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)
Tactic: apply eq_zero_of_localization _ fun J hJ ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (hypothesis)
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 := ⋯ }
⊢ 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)
have this₁ : ¬(↑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)))
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (goal)
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)
⊢ 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)
have 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)
Tactic: obtain ⟨r, hrs, hrI⟩ := Set.not_subset.mp this
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (goal)
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)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (hypothesis)
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' := ⋯ }
    ⋯
⊢ 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)
have hψ : 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 [φ, ψ]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (hypothesis)
Goal:
R : Type u_6
S : Type u_7
T : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
hf : f.IsIntegral
g : S →+* T
hg_1 : g.IsStandardOpenImmersion
hg : (g.comp f).FiniteType
⊢ (g.comp f).QuasiFinite
have algebraizeInst : let algInst := f.toAlgebra;
Algebra.IsIntegral R S
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (hypothesis)
Goal:
R : Type u_6
S : Type u_7
T : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
hf : f.IsIntegral
g : S →+* T
hg_1 : g.IsStandardOpenImmersion
hg : (g.comp f).FiniteType
algebraizeInst :
  let algInst := f.toAlgebra;
  Algebra.IsIntegral R S
⊢ (g.comp f).QuasiFinite
have algebraizeInst₁ : Algebra.IsStandardOpenImmersion S T
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (hypothesis)
Goal:
R : Type u_6
S : Type u_7
T : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
hf : f.IsIntegral
g : S →+* T
hg_1 : g.IsStandardOpenImmersion
hg : (g.comp f).FiniteType
algebraizeInst :
  let algInst := f.toAlgebra;
  Algebra.IsIntegral R S
algebraizeInst₁ : Algebra.IsStandardOpenImmersion S T
⊢ (g.comp f).QuasiFinite
have algebraizeInst₂ : Algebra.FiniteType R T
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.QuasiFinite (goal)
Goal:
R : Type u_6
S : Type u_7
T : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
hf : f.IsIntegral
g : S →+* T
hg_1 : g.IsStandardOpenImmersion
hg : (g.comp f).FiniteType
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.IsIntegral R S
algebraizeInst_1 : Algebra.IsStandardOpenImmersion S T
algebraizeInst_2 : Algebra.FiniteType R T
⊢ (g.comp f).QuasiFinite
have obtain : ∀ (s : S) (hs : IsLocalization.Away s T), (g.comp f).QuasiFinite
Tactic: obtain ⟨s, hs⟩ := Algebra.IsStandardOpenImmersion.exists_away S T