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_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_5 : WeaklyQuasiFiniteAt R (S := ↥R') (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' :=
  MvPolynomial.aeval fun (i : Fin n) ↦
    Subtype.mk (p := fun (x : S) ↦ x ∈ R') ((f : (a : MvPolynomial (Fin (n + 1)) R) → S) (MvPolynomial.X i.succ)) ⋯
this : ZariskisMainProperty R (S := ↥R') (Ideal.under (↥R') p)
succ : ⊤ ≤ R'.saturation (Submonoid.powers r) ⋯
⊢ Eq (α := Subalgebra (↥R') S)
    (Subalgebra.saturation ⊥
        (Submonoid.powers ((algebraMap (↥R') S : (a : ↥R') → S) (Subtype.mk (p := fun (x : S) ↦ x ∈ R') r hrR'))) ⋯ :
      Subalgebra (↥R') S)
    (⊤ : Subalgebra (↥R') S)

Tactic:
suffices ⊤ ≤ R'.saturation (.powers r) (by simpa [Submonoid.powers_le]) by
      simpa [SetLike.le_def, Subalgebra.smul_def, Submonoid.mem_powers_iff,
        SetLike.ext_iff, Algebra.mem_bot] using this
-- 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_5 : WeaklyQuasiFiniteAt R (S := ↥R') (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' :=
  MvPolynomial.aeval fun (i : Fin n) ↦
    Subtype.mk (p := fun (x : S) ↦ x ∈ R') ((f : (a : MvPolynomial (Fin (n + 1)) R) → S) (MvPolynomial.X i.succ)) ⋯
this : ZariskisMainProperty R (S := ↥R') (Ideal.under (↥R') p)
succ : (↑s : Set S) ⊆ (↑(R'.saturation (Submonoid.powers r) ⋯) : Set S)
⊢ ⊤ ≤ R'.saturation (Submonoid.powers r) ⋯

Tactic:
rw [← hs, Algebra.adjoin_le_iff]

Premises used: Algebra.adjoin_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_5 : WeaklyQuasiFiniteAt R (S := ↥R') (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' :=
  MvPolynomial.aeval fun (i : Fin n) ↦
    Subtype.mk (p := fun (x : S) ↦ x ∈ R') ((f : (a : MvPolynomial (Fin (n + 1)) R) → S) (MvPolynomial.X i.succ)) ⋯
this : ZariskisMainProperty R (S := ↥R') (Ideal.under (↥R') p)
x : S
hx : x ∈ (↑s : Set S)
⊢ x ∈ (↑(R'.saturation (Submonoid.powers r) ⋯) : Set S)

Tactic:
⟨_, ⟨s.sup m, rfl⟩, Algebra.subset_adjoin ?_⟩

Premises used: Set.Mem, Algebra.subset_adjoin, setOf, And.intro, Exists.intro, Finset.sup, rfl
-- 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_5 : WeaklyQuasiFiniteAt R (S := ↥R') (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' :=
  MvPolynomial.aeval fun (i : Fin n) ↦
    Subtype.mk (p := fun (x : S) ↦ x ∈ R') ((f : (a : MvPolynomial (Fin (n + 1)) R) → S) (MvPolynomial.X i.succ)) ⋯
this : ZariskisMainProperty R (S := ↥R') (Ideal.under (↥R') p)
x : S
hx : x ∈ (↑s : Set S)
succ :
  (fun (x : ℕ) ↦ r ^ x) (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 (Submonoid.powers r) ⋯) : Set S)

Tactic:
refine ⟨_, ⟨s.sup m, rfl⟩, 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_5 : WeaklyQuasiFiniteAt R (S := ↥R') (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' :=
  MvPolynomial.aeval fun (i : Fin n) ↦
    Subtype.mk (p := fun (x : S) ↦ x ∈ R') ((f : (a : MvPolynomial (Fin (n + 1)) R) → S) (MvPolynomial.X i.succ)) ⋯
this : ZariskisMainProperty R (S := ↥R') (Ideal.under (↥R') p)
x : S
hx : x ∈ (↑s : Set S)
⊢ (fun (x : ℕ) ↦ r ^ x) (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:
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
obtain :
  ∀ (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)),
    ZariskisMainProperty R p
⊢ ZariskisMainProperty R p

Tactic:
obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp ‹_›

Premises used: Iff.mp, Algebra.FiniteType.iff_quotient_mvPolynomial''
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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)
⊢ Small.{u, v} S

Tactic:
have : Small.{u} S := small_of_surjective hf
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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
⊢ ZariskisMainProperty R
    (Ideal.comap (F := RingHom.{u, v} (Shrink.{u, v} S) S)
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (Shrink.algEquiv R S))) p)

Tactic:
have := ZariskisMainProperty.of_algHom_mvPolynomial (p.comap (Shrink.algEquiv R S).toRingHom)
    ((Shrink.algEquiv R S).symm.toAlgHom.comp f)
    (.of_surjective _ <| (Shrink.algEquiv R S).symm.surjective.comp hf)
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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)
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)
⊢ ZariskisMainProperty R p

Tactic:
rw [zariskisMainProperty_iff'] at this ⊢

Premises used: Algebra.zariskisMainProperty_iff'
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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)
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)
⊢ ∃ r ∉ p, ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
obtain ⟨r, hr, H⟩ := this
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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)

Tactic:
⟨Shrink.algEquiv R S r, hr, fun x ↦ ?_⟩

Premises used: Shrink.algEquiv, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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)
refine :
  ∀ (x : S),
    ∃ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((Shrink.algEquiv R S : (a : Shrink.{u, v} S) → S) r : S) m * x)
⊢ ∃ r ∉ p, ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
refine ⟨Shrink.algEquiv R S r, hr, fun x ↦ ?_⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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
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)
⊢ ∃ (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)

Premises used: AlgEquiv.symm, Shrink.algEquiv, DFunLike.coe
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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 : ℕ
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))
⊢ IsIntegral R (HPow.hPow (α := S) ((Shrink.algEquiv R S : (a : Shrink.{u, v} S) → S) r : S) m * x)

Tactic:
simpa [-Shrink.algEquiv_apply, -Shrink.algEquiv_symm_apply]
    using hm.map (Shrink.algEquiv R S).toAlgHom

Premises used: AlgEquiv.toAlgHom, Shrink.algEquiv_apply, IsIntegral.map, Shrink.algEquiv, Shrink.algEquiv_symm_apply
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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 : ℕ
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:
exact ⟨m, by simpa [-Shrink.algEquiv_apply, -Shrink.algEquiv_symm_apply]
    using hm.map (Shrink.algEquiv R S).toAlgHom⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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 : QuasiFiniteAt R p
⊢ ZariskisMainProperty R p

Tactic:
.of_finiteType_of_weaklyQuasiFiniteAt _

Premises used: Algebra.ZariskisMainProperty.of_finiteType_of_weaklyQuasiFiniteAt
-- 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
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))
⊢ ∃ (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)

Premises used: Algebra.FiniteType.out
-- 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)) ⊤
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))
⊢ ∃ (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

Premises used: Algebra.zariskisMainProperty_iff, Iff.mp
-- 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 ∈ t

Tactic:
simp [t]