awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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))

Tactic:
⟨Algebra.adjoin R t, fg_adjoin_of_finite ?_ ?_, ?_⟩

Premises used: Algebra.adjoin, fg_adjoin_of_finite, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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
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))
⊢ ∃ (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:
refine ⟨Algebra.adjoin R t, fg_adjoin_of_finite ?_ ?_, ?_⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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 : Set.Finite.{u_2} (α := S) {x : S | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
⊢ t.Finite

Tactic:
simp only [t, Set.finite_insert]

Premises used: Set.finite_insert
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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 ⋯
⊢ Set.Finite.{u_2} (α := S) {x : S | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}

Tactic:
s.finite_toSet.image (fun x ↦ r ^ m x * x)

Premises used: HMul.hMul, setOf, Set.Finite.image, HPow.hPow, Set.image, Finset.finite_toSet
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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 ⋯
⊢ Set.Finite.{u_2} (α := S) {x : S | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}

Tactic:
exact s.finite_toSet.image (fun x ↦ r ^ m x * x)

Premises used: HMul.hMul, Set.Finite.image, HPow.hPow, Finset.finite_toSet
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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)) ⊤
m : (x : S) → ℕ
a : S
hrp : a ∉ p
hr : IsIntegral R a
hm : ∀ (x : S), IsIntegral R (a ^ m x * x)
t : Set S := insert a {x : S | ∃ x_1 ∈ s, a ^ 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) a ⋯
⊢ IsIntegral R a

Tactic:
hr
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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
⊢ IsIntegral R (r ^ m x * x)

Tactic:
hm _
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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)) ⊤
m : (x : S) → ℕ
a : S
hrp : a ∉ p
hr : IsIntegral R a
hm : ∀ (x : S), IsIntegral R (a ^ m x * x)
t : Set S := insert a {x : S | ∃ x_1 ∈ s, a ^ 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) a ⋯
⊢ IsIntegral R a

Tactic:
exacts [hr, hm _]
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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))

Tactic:
⟨r', hrp,
    IsLocalization.map_injective_of_injective _ _ _ Subtype.val_injective, ?_⟩

Premises used: IsLocalization.map_injective_of_injective, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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_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'))
⊢ ∃ (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 ⟨r', hrp,
    IsLocalization.map_injective_of_injective _ _ _ Subtype.val_injective, ?_⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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 ⋯
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)
⊢ 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:
rw [← Algebra.map_top, ← hs, Subalgebra.map_le, Algebra.adjoin_le_iff]

Premises used: Subalgebra.map_le, Algebra.adjoin_le_iff, Algebra.map_top
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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)
this :
  ∃ (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)
⊢ 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)

Tactic:
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]

Premises used: IsLocalization.map_mk', IsLocalization.mk'_surjective, Function.Surjective.forall, Function.Surjective.exists, Subalgebra.val, map_pow, Subtype.ext_iff, IsLocalization.mk'_eq_iff_eq_mul, map_mul, IsLocalization.Away.map, Submonoid.powers, Submonoid.mem_powers_iff, Localization.awayMapₐ, IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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)
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)
⊢ 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)

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]
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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)
⊢ ∃ (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:
⟨_, Algebra.subset_adjoin (Set.mem_insert_of_mem _ ⟨x, hx, mul_comm _ _⟩),
      m x, pow_mem r'.2 _, 1, rfl⟩

Premises used: Algebra.subset_adjoin, Set.mem_insert_of_mem, And.intro, Exists.intro, pow_mem, mul_comm, OfNat.ofNat, rfl, Subtype.property
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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)
⊢ ∃ (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:
exact ⟨_, Algebra.subset_adjoin (Set.mem_insert_of_mem _ ⟨x, hx, mul_comm _ _⟩),
      m x, pow_mem r'.2 _, 1, rfl⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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'))

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⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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)
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)
              ⋯) :
          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

Tactic:
obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq
    (.powers ((Algebra.adjoin R t).val.toRingHom r')) x

Premises used: Subalgebra.val, Algebra.adjoin, AlgHom.toRingHom, Submonoid.powers, DFunLike.coe, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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 : S
n : ℕ
y : Localization.Away r'
hy :
  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'))
        y :
      Localization.Away (M := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))
    ((AlgHom.toRingHom
            (IsScalarTower.toAlgHom R S
              (Localization.Away (M := S) ((Subalgebra.val (adjoin R t) : (a : ↥(adjoin R t)) → S) r' : S))) :
          (a : S) → Localization.Away (((adjoin R t).val : (a : ↥(adjoin R t)) → S) r'))
        x :
      Localization.Away (M := S) ((Subalgebra.val (adjoin R t) : (a : ↥(adjoin R t)) → S) r' : S))
⊢ ∃ (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)
            ⋯) :
        Localization.Away (M := S) ((AlgHom.toRingHom (Subalgebra.val (adjoin R t)) : (a : ↥(adjoin R t)) → S) r' : S))

Tactic:
⟨y * Localization.Away.invSelf _ ^ n, ?_⟩

Premises used: HMul.hMul, Localization.Away.invSelf, HPow.hPow, Exists.intro