awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : WeaklyQuasiFiniteAt R p
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
this_1 : Small.{u, v} S
this :
  ZariskisMainProperty R
    (Ideal.comap (F := RingHom.{u, v} (Shrink.{u, v} S) S)
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (Shrink.algEquiv R S))) p)
⊢ ZariskisMainProperty R p
have rw : ∀
  (this :
    ∃
      r ∉
        Ideal.comap (F := RingHom.{u, v} (Shrink.{u, v} S) S)
          (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (Shrink.algEquiv R S))) p,
      ∀ (x : Shrink.{u, v} S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)),
  ∃ r ∉ p, ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
Tactic: rw [zariskisMainProperty_iff'] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : WeaklyQuasiFiniteAt R p
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
this_1 : Small.{u, v} S
this :
  ∃
    r ∉
      Ideal.comap (F := RingHom.{u, v} (Shrink.{u, v} S) S)
        (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (Shrink.algEquiv R S))) p,
    ∀ (x : Shrink.{u, v} S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
⊢ ∃ r ∉ p, ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
have obtain : ∀ (r : Shrink.{u, v} S)
  (hr :
    r ∉
      Ideal.comap (F := RingHom.{u, v} (Shrink.{u, v} S) S)
        (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (Shrink.algEquiv R S))) p)
  (H : ∀ (x : Shrink.{u, v} S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)),
  ∃ r ∉ p, ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
Tactic: obtain ⟨r, hr, H⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : WeaklyQuasiFiniteAt R p
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
this : Small.{u, v} S
r : Shrink.{u, v} S
hr :
  r ∉
    Ideal.comap (F := RingHom.{u, v} (Shrink.{u, v} S) S)
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (Shrink.algEquiv R S))) p
H : ∀ (x : Shrink.{u, v} S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
⊢ ∃ r ∉ p, ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
have refine : ∀ (x : S), ∃ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((Shrink.algEquiv R S : (a : Shrink.{u, v} S) → S) r : S) m * x)
Tactic: refine ⟨Shrink.algEquiv R S r, hr, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : WeaklyQuasiFiniteAt R p
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
this : Small.{u, v} S
r : Shrink.{u, v} S
hr :
  r ∉
    Ideal.comap (F := RingHom.{u, v} (Shrink.{u, v} S) S)
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (Shrink.algEquiv R S))) p
H : ∀ (x : Shrink.{u, v} S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
x : S
⊢ ∃ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((Shrink.algEquiv R S : (a : Shrink.{u, v} S) → S) r : S) m * x)
have obtain : ∀ (m : ℕ)
  (hm :
    IsIntegral R
      (HMul.hMul (β := Shrink.{u, v} S) (r ^ m)
        ((AlgEquiv.symm (Shrink.algEquiv R S) : (a : S) → Shrink.{u, v} S) x : Shrink.{u, v} S))),
  ∃ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((Shrink.algEquiv R S : (a : Shrink.{u, v} S) → S) r : S) m * x)
Tactic: obtain ⟨m, hm⟩ := H ((Shrink.algEquiv R S).symm x)
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (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
p : Ideal S
H : ZariskisMainProperty R p
⊢ ∃ (S' : Subalgebra R S),
    Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S') ∧
      ∃ (r : ↥S'),
        (↑r : S) ∉ p ∧
          Function.Bijective (α := Localization.Away r) (β :=
            Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
            (⇑(Localization.awayMap S'.val.toRingHom r) :
              (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
have obtain : ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤),
  ∃ (S' : Subalgebra R S),
    Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S') ∧
      ∃ (r : ↥S'),
        (↑r : S) ∉ p ∧
          Function.Bijective (α := Localization.Away r) (β :=
            Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
            (⇑(Localization.awayMap S'.val.toRingHom r) :
              (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
Tactic: obtain ⟨s, hs⟩ := Algebra.FiniteType.out (R := R) (A := S)
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (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
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
⊢ ∃ (S' : Subalgebra R S),
    Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S') ∧
      ∃ (r : ↥S'),
        (↑r : S) ∉ p ∧
          Function.Bijective (α := Localization.Away r) (β :=
            Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
            (⇑(Localization.awayMap S'.val.toRingHom r) :
              (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
have choose : ∀ (r : S) (hrp : r ∉ p) (hr : IsIntegral R r) (m : (x : S) → ℕ) (hm : ∀ (x : S), IsIntegral R (r ^ m x * x)),
  ∃ (S' : Subalgebra R S),
    Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S') ∧
      ∃ (r : ↥S'),
        (↑r : S) ∉ p ∧
          Function.Bijective (α := Localization.Away r) (β :=
            Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
            (⇑(Localization.awayMap S'.val.toRingHom r) :
              (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
Tactic: choose r hrp hr m hm using zariskisMainProperty_iff.mp H
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (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
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x : S | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (adjoin R t) x) r ⋯
⊢ ∃ (S' : Subalgebra R S),
    Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S') ∧
      ∃ (r : ↥S'),
        (↑r : S) ∉ p ∧
          Function.Bijective (α := Localization.Away r) (β :=
            Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
            (⇑(Localization.awayMap S'.val.toRingHom r) :
              (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
have refine_1 : t.Finite
Tactic: refine ⟨Algebra.adjoin R t, fg_adjoin_of_finite ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (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
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x : S | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (adjoin R t) x) r ⋯
refine_1 : t.Finite
⊢ ∃ (S' : Subalgebra R S),
    Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S') ∧
      ∃ (r : ↥S'),
        (↑r : S) ∉ p ∧
          Function.Bijective (α := Localization.Away r) (β :=
            Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
            (⇑(Localization.awayMap S'.val.toRingHom r) :
              (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
have refine_2 : ∀ x ∈ t, IsIntegral R x
Tactic: refine ⟨Algebra.adjoin R t, fg_adjoin_of_finite ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (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
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x : S | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (adjoin R t) x) r ⋯
refine_1 : t.Finite
refine_2 : ∀ x ∈ t, IsIntegral R x
⊢ ∃ (S' : Subalgebra R S),
    Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S') ∧
      ∃ (r : ↥S'),
        (↑r : S) ∉ p ∧
          Function.Bijective (α := Localization.Away r) (β :=
            Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
            (⇑(Localization.awayMap S'.val.toRingHom r) :
              (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
have refine_3 : ∃ (r : ↥(adjoin R t)),
  (↑r : S) ∉ p ∧
    Function.Bijective (α := Localization.Away r) (β :=
      Localization.Away (M := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r : S))
      (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (adjoin R t))) r) :
        (a : Localization.Away r) → Localization.Away (((adjoin R t).val.toRingHom : (a : ↥(adjoin R t)) → S) r))
Tactic: refine ⟨Algebra.adjoin R t, fg_adjoin_of_finite ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (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
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x : S | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (adjoin R t) x) r ⋯
⊢ t.Finite
have refine_1 : Set.Finite.{u_2} (α := S) {x : S | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
Tactic: simp only [t, Set.finite_insert]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (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
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x : S | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (adjoin R t) x) r ⋯
⊢ ∃ (r : ↥(adjoin R t)),
    (↑r : S) ∉ p ∧
      Function.Bijective (α := Localization.Away r) (β :=
        Localization.Away (M := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r : S))
        (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (adjoin R t))) r) :
          (a : Localization.Away r) → Localization.Away (((adjoin R t).val.toRingHom : (a : ↥(adjoin R t)) → S) r))
have refine_3 : Function.Surjective (α := Localization.Away r') (β :=
  Localization.Away (M := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
  (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (adjoin R t))) r') :
    (a : Localization.Away r') → Localization.Away (((adjoin R t).val.toRingHom : (a : ↥(adjoin R t)) → S) r'))
Tactic: refine ⟨r', hrp,
    IsLocalization.map_injective_of_injective _ _ _ Subtype.val_injective, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (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
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x : S | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (adjoin R t) x) r ⋯
⊢ LE.le (α :=
    Subalgebra R (Localization.Away (M := S) ((Subalgebra.val (adjoin R t) : (a : ↥(adjoin R t)) → S) r' : S)))
    (AlgHom.range
      (IsScalarTower.toAlgHom R S
        (Localization.Away (M := S) ((Subalgebra.val (adjoin R t) : (a : ↥(adjoin R t)) → S) r' : S))))
    (AlgHom.range (Localization.awayMapₐ (Subalgebra.val (adjoin R t)) r'))
have rw : (↑s : Set S) ⊆
  (↑(Subalgebra.comap (B := Localization.Away (M := S) ((Subalgebra.val (adjoin R t) : (a : ↥(adjoin R t)) → S) r' : S))
        (IsScalarTower.toAlgHom R S
          (Localization.Away (M := S) ((Subalgebra.val (adjoin R t) : (a : ↥(adjoin R t)) → S) r' : S)))
        (AlgHom.range (Localization.awayMapₐ (Subalgebra.val (adjoin R t)) r'))) :
    Set S)
Tactic: rw [← Algebra.map_top, ← hs, Subalgebra.map_le, Algebra.adjoin_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (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
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x : S | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (adjoin R t) x) r ⋯
x : S
hx : x ∈ (↑s : Set S)
⊢ x ∈
    (↑(Subalgebra.comap (B :=
          Localization.Away (M := S) ((Subalgebra.val (adjoin R t) : (a : ↥(adjoin R t)) → S) r' : S))
          (IsScalarTower.toAlgHom R S
            (Localization.Away (M := S) ((Subalgebra.val (adjoin R t) : (a : ↥(adjoin R t)) → S) r' : S)))
          (AlgHom.range (Localization.awayMapₐ (Subalgebra.val (adjoin R t)) r'))) :
      Set S)
have suffices : ∃ (a : S),
  Membership.mem (γ := Subalgebra R S) (adjoin R t) a ∧
    ∃ (n : ℕ), Membership.mem (γ := Subalgebra R S) (adjoin R t) (r ^ n) ∧ ∃ (k : ℕ), r ^ k * a = r ^ k * (x * r ^ n)
Tactic: suffices ∃ a ∈ Algebra.adjoin R t, ∃ n, r ^ n ∈ Algebra.adjoin R t ∧
        ∃ k, r ^ k * a = r ^ k * (x * r ^ n) by
      simpa [(IsLocalization.mk'_surjective (.powers r')).exists,
        (IsLocalization.mk'_surjective (.powers r)).forall, Localization.awayMapₐ,
        IsLocalization.Away.map, IsLocalization.map_mk', Submonoid.mem_powers_iff,
        Subtype.ext_iff, IsLocalization.mk'_eq_iff_eq_mul, ← map_mul, ← map_pow,
        IsLocalization.eq_iff_exists (.powers r), Subalgebra.val]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (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
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x : S | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (adjoin R t) x) r ⋯
⊢ Function.Surjective (α := Localization.Away r') (β :=
    Localization.Away (M := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
    (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (adjoin R t))) r') :
      (a : Localization.Away r') → Localization.Away (((adjoin R t).val.toRingHom : (a : ↥(adjoin R t)) → S) r'))
have this : LE.le (α := Subalgebra R (Localization.Away (M := S) ((Subalgebra.val (adjoin R t) : (a : ↥(adjoin R t)) → S) r' : S)))
  (AlgHom.range
    (IsScalarTower.toAlgHom R S
      (Localization.Away (M := S) ((Subalgebra.val (adjoin R t) : (a : ↥(adjoin R t)) → S) r' : S))))
  (AlgHom.range (Localization.awayMapₐ (Subalgebra.val (adjoin R t)) r'))
Tactic: have : (IsScalarTower.toAlgHom R S _).range ≤
      (Localization.awayMapₐ (Algebra.adjoin R t).val r').range := by
    rw [← Algebra.map_top, ← hs, Subalgebra.map_le, Algebra.adjoin_le_iff]
    intro x hx
    suffices ∃ a ∈ Algebra.adjoin R t, ∃ n, r ^ n ∈ Algebra.adjoin R t ∧
        ∃ k, r ^ k * a = r ^ k * (x * r ^ n) by
      simpa [(IsLocalization.mk'_surjective (.powers r')).exists,
        (IsLocalization.mk'_surjective (.powers r)).forall, Localization.awayMapₐ,
        IsLocalization.Away.map, IsLocalization.map_mk', Submonoid.mem_powers_iff,
        Subtype.ext_iff, IsLocalization.mk'_eq_iff_eq_mul, ← map_mul, ← map_pow,
        IsLocalization.eq_iff_exists (.powers r), Subalgebra.val]
    exact ⟨_, Algebra.subset_adjoin (Set.mem_insert_of_mem _ ⟨x, hx, mul_comm _ _⟩),
      m x, pow_mem r'.2 _, 1, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (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
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x : S | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (adjoin R t) x) r ⋯
this :
  LE.le (α :=
    Subalgebra R (Localization.Away (M := S) ((Subalgebra.val (adjoin R t) : (a : ↥(adjoin R t)) → S) r' : S)))
    (AlgHom.range
      (IsScalarTower.toAlgHom R S
        (Localization.Away (M := S) ((Subalgebra.val (adjoin R t) : (a : ↥(adjoin R t)) → S) r' : S))))
    (AlgHom.range (Localization.awayMapₐ (Subalgebra.val (adjoin R t)) r'))
x : Localization.Away (M := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S)
⊢ ∃ (a : Localization.Away r'),
    (Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (adjoin R t))) r' :
          (a : Localization.Away r') → Localization.Away (((adjoin R t).val.toRingHom : (a : ↥(adjoin R t)) → S) r'))
        a =
      x
have refine_3 : ∀ (x : S) (n : ℕ),
  ∃ (a : Localization.Away r'),
    Eq (α :=
      Localization.Away (M := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
      ((Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (adjoin R t))) r' :
            (a : Localization.Away r') → Localization.Away (((adjoin R t).val.toRingHom : (a : ↥(adjoin R t)) → S) r'))
          a :
        Localization.Away (M := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
      (IsLocalization.mk'
          (Localization.Away (M := S)
            ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
          x
          (Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S)
              (Submonoid.powers ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r') :
                Submonoid S)
              x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S)
                  x)
              n)
            sorry) :
        Localization.Away (M := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
Tactic: obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq
    (.powers ((Algebra.adjoin R t).val.toRingHom r')) x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (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
p : Ideal S
inst_4 : p.IsPrime
H : ZariskisMainProperty R p
⊢ QuasiFiniteAt R p
have obtain : ∀ (S' : Subalgebra R S)
  (hS' : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S'))
  (r : ↥S') (hrp : (↑r : S) ∉ p)
  (H :
    Function.Bijective (α := Localization.Away r) (β :=
      Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
      (⇑(Localization.awayMap S'.val.toRingHom r) :
        (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))),
  QuasiFiniteAt R p
Tactic: obtain ⟨S', hS', r, hrp, H⟩ := H.exists_fg_and_exists_notMem_and_awayMap_bijective _
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (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
p : Ideal S
inst_4 : p.IsPrime
H_1 : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrp : (↑r : S) ∉ p
H :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
⊢ QuasiFiniteAt R p
have this : Module.Finite.{u_1, u_2} R ↥S'
Tactic: have : Module.Finite R S' := ⟨(Submodule.fg_top _).mpr hS'⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (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
p : Ideal S
inst_4 : p.IsPrime
H_1 : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrp : (↑r : S) ∉ p
H :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this : Module.Finite.{u_1, u_2} R ↥S'
⊢ QuasiFiniteAt R p
have this₁ : QuasiFinite.{u_1, u_2} R (Localization.Away r)
Tactic: have : Algebra.QuasiFinite R (Localization.Away r) :=
    .trans _ S' _