awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
R' : Subalgebra R S :=
  adjoin R
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)
⊢ r ∈
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)

Tactic:
simp
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
R' : Subalgebra R S :=
  adjoin R
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)
⊢ r ∈ R'

Tactic:
have hrR' : r ∈ R' := Algebra.subset_adjoin (by simp)
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this_4 : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
R' : Subalgebra R S :=
  adjoin R
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)
hrR' : r ∈ R'
this : Algebra (Localization.AtPrime (R := ↥R') (Ideal.under (↥R') p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R') p) p
⊢ Function.Bijective (α := Localization.AtPrime (R := ↥R') (Ideal.under (↥R') p)) (β := Localization.AtPrime p)
    (⇑(IsScalarTower.toAlgHom R (Localization.AtPrime (R := ↥R') (Ideal.under (↥R') p)) (Localization.AtPrime p)) :
      (a : Localization.AtPrime (Ideal.under (↥R') p)) → Localization.AtPrime p)

Tactic:
Localization.localRingHom_bijective_of_saturated_inf_eq_top _ ?_ _

Premises used: Subsemiring.mk', Subsemiring.closure, Set.Mem, setOf, Localization.localRingHom_bijective_of_saturated_inf_eq_top
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this_4 : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
R' : Subalgebra R S :=
  adjoin R
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)
hrR' : r ∈ R'
this : Algebra (Localization.AtPrime (R := ↥R') (Ideal.under (↥R') p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R') p) p
rw : (↑s : Set S) ⊆ (↑(R'.saturation (p.primeCompl ⊓ R'.toSubmonoid) ⋯) : Set S)
⊢ R'.saturation (p.primeCompl ⊓ R'.toSubmonoid) ⋯ = ⊤

Tactic:
rw [← top_le_iff, ← hs, Algebra.adjoin_le_iff]

Premises used: Algebra.adjoin_le_iff, top_le_iff
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this_4 : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
R' : Subalgebra R S :=
  adjoin R
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)
hrR' : r ∈ R'
this : Algebra (Localization.AtPrime (R := ↥R') (Ideal.under (↥R') p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R') p) p
x : S
hx : x ∈ (↑s : Set S)
⊢ r ∈ p.primeCompl ⊓ R'.toSubmonoid

Tactic:
⟨hrp, hrR'⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this_4 : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
R' : Subalgebra R S :=
  adjoin R
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)
hrR' : r ∈ R'
this : Algebra (Localization.AtPrime (R := ↥R') (Ideal.under (↥R') p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R') p) p
x : S
hx : x ∈ (↑s : Set S)
⊢ r ∈ p.primeCompl ⊓ R'.toSubmonoid

Tactic:
exact ⟨hrp, hrR'⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this_4 : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
R' : Subalgebra R S :=
  adjoin R
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)
hrR' : r ∈ R'
this : Algebra (Localization.AtPrime (R := ↥R') (Ideal.under (↥R') p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R') p) p
x : S
hx : x ∈ (↑s : Set S)
refine :
  r ^ s.sup m * x ∈
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)
⊢ x ∈ (↑(R'.saturation (p.primeCompl ⊓ R'.toSubmonoid) ⋯) : Set S)

Tactic:
refine ⟨r ^ (s.sup m), pow_mem (by exact ⟨hrp, hrR'⟩) _, Algebra.subset_adjoin ?_⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this_4 : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
R' : Subalgebra R S :=
  adjoin R
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)
hrR' : r ∈ R'
this : Algebra (Localization.AtPrime (R := ↥R') (Ideal.under (↥R') p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R') p) p
x : S
hx : x ∈ (↑s : Set S)
⊢ r ^ s.sup m * x ∈
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)

Tactic:
simp [Set.smul_mem_smul_set hx, ← smul_eq_mul]

Premises used: smul_eq_mul, Set.smul_mem_smul_set
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this_4 : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
R' : Subalgebra R S :=
  adjoin R
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)
hrR' : r ∈ R'
this : Algebra (Localization.AtPrime (R := ↥R') (Ideal.under (↥R') p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R') p) p
e : Localization.AtPrime (R := ↥R') (Ideal.under (↥R') p) ≃ₐ[R] Localization.AtPrime p :=
  AlgEquiv.ofBijective
    (IsScalarTower.toAlgHom R (Localization.AtPrime (R := ↥R') (Ideal.under (↥R') p)) (Localization.AtPrime p)) ⋯
⊢ WeaklyQuasiFiniteAt R (S := ↥R') (Ideal.under (↥R') p)

Tactic:
.of_algHom_localization _ _ e.symm.toAlgHom e.symm.surjective

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, Algebra.WeaklyQuasiFiniteAt.of_algHom_localization, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this_4 : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
R' : Subalgebra R S :=
  adjoin R
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)
hrR' : r ∈ R'
this : Algebra (Localization.AtPrime (R := ↥R') (Ideal.under (↥R') p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R') p) p
e : Localization.AtPrime (R := ↥R') (Ideal.under (↥R') p) ≃ₐ[R] Localization.AtPrime p :=
  AlgEquiv.ofBijective
    (IsScalarTower.toAlgHom R (Localization.AtPrime (R := ↥R') (Ideal.under (↥R') p)) (Localization.AtPrime p)) ⋯
⊢ WeaklyQuasiFiniteAt R (S := ↥R') (Ideal.under (↥R') p)

Tactic:
exact .of_algHom_localization _ _ e.symm.toAlgHom e.symm.surjective
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
R' : Subalgebra R S :=
  adjoin R
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)
hrR' : r ∈ R'
⊢ WeaklyQuasiFiniteAt R (S := ↥R') (Ideal.under (↥R') p)

Tactic:
have : Algebra.WeaklyQuasiFiniteAt R (p.under R') := by
      let := Localization.AtPrime.algebraOfLiesOver (p.under R') p
      let e : Localization.AtPrime (p.under R') ≃ₐ[R] Localization.AtPrime p :=
        .ofBijective (IsScalarTower.toAlgHom _ _ _) <| by
          refine Localization.localRingHom_bijective_of_saturated_inf_eq_top _ ?_ _
          rw [← top_le_iff, ← hs, Algebra.adjoin_le_iff]
          intro x hx
          refine ⟨r ^ (s.sup m), pow_mem (by exact ⟨hrp, hrR'⟩) _, Algebra.subset_adjoin ?_⟩
          simp [Set.smul_mem_smul_set hx, ← smul_eq_mul]
      exact .of_algHom_localization _ _ e.symm.toAlgHom e.symm.surjective
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this_4 : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
R' : Subalgebra R S :=
  adjoin R
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)
hrR' : r ∈ R'
this : WeaklyQuasiFiniteAt R (S := ↥R') (Ideal.under (↥R') p)
i : Fin n
⊢ Membership.mem (α := S)
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)
    ((f : (a : MvPolynomial (Fin (n + 1)) R) → S) (MvPolynomial.X i.succ) : S)

Tactic:
simp