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 : 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)) ⋯
⊢ φ.Finite

Tactic:
RingHom.finite_iff_isIntegral_and_finiteType.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, AlgHom.Finite, And.intro, RingHom.finite_iff_isIntegral_and_finiteType
-- 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)
φ : 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)) ⋯
refine_1 : φ.IsIntegral
refine_2 : φ.FiniteType
⊢ φ.Finite

Tactic:
refine RingHom.finite_iff_isIntegral_and_finiteType.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, And.intro, RingHom.finite_iff_isIntegral_and_finiteType
-- 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 : Algebra (MvPolynomial (Fin n) R) ↥R' := φ.toAlgebra
hC :
  ∀ (x : R),
    Eq (α := S)
      ((RingHom.comp (β := MvPolynomial (Fin n) R) (algebraMap (MvPolynomial (Fin n) R) S) MvPolynomial.C : (a : R) → S)
          x :
        S)
      ((RingHom.comp (β := MvPolynomial (Fin n) R)
              (@RingHom.comp _ ↥R' _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R') S)
                (algebraMap (MvPolynomial (Fin n) R) ↥R'))
              MvPolynomial.C :
            (a : R) → S)
          x :
        S)
hX :
  ∀ (i : Fin n),
    Eq (α := S) ((algebraMap (MvPolynomial (Fin n) R) S : (a : MvPolynomial (Fin n) R) → S) (MvPolynomial.X i) : S)
      ((@RingHom.comp _ ↥R' _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R') S)
              (algebraMap (MvPolynomial (Fin n) R) ↥R') :
            (a : MvPolynomial (Fin n) R) → S)
          (MvPolynomial.X i) :
        S)
⊢ Eq (α := MvPolynomial (Fin n) R →+* S) (algebraMap (MvPolynomial (Fin n) R) S)
    (@RingHom.comp _ ↥R' _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R') S)
      (algebraMap (MvPolynomial (Fin n) R) ↥R'))

Tactic:
ext
-- 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 : Algebra (MvPolynomial (Fin n) R) ↥R' := φ.toAlgebra
x : R
⊢ Eq (α := S)
    ((RingHom.comp (β := MvPolynomial (Fin n) R) (algebraMap (MvPolynomial (Fin n) R) S) MvPolynomial.C : (a : R) → S)
        x :
      S)
    ((RingHom.comp (β := MvPolynomial (Fin n) R)
            (@RingHom.comp _ ↥R' _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R') S)
              (algebraMap (MvPolynomial (Fin n) R) ↥R'))
            MvPolynomial.C :
          (a : R) → S)
        x :
      S)

Tactic:
simp [φ, (f'.toRingHom.comp C).algebraMap_toAlgebra, φ.algebraMap_toAlgebra, f',
            MvPolynomial.finSuccEquiv, MvPolynomial.optionEquivLeft]

Premises used: Polynomial.C, MvPolynomial.finSuccEquiv, RingHom.comp, AlgHom.toRingHom, RingHom.algebraMap_toAlgebra, MvPolynomial.optionEquivLeft
-- 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 : Algebra (MvPolynomial (Fin n) R) ↥R' := φ.toAlgebra
i : Fin n
⊢ Eq (α := S) ((algebraMap (MvPolynomial (Fin n) R) S : (a : MvPolynomial (Fin n) R) → S) (MvPolynomial.X i) : S)
    ((@RingHom.comp _ ↥R' _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R') S)
            (algebraMap (MvPolynomial (Fin n) R) ↥R') :
          (a : MvPolynomial (Fin n) R) → S)
        (MvPolynomial.X i) :
      S)

Tactic:
simp [φ, (f'.toRingHom.comp C).algebraMap_toAlgebra, φ.algebraMap_toAlgebra, f',
            MvPolynomial.finSuccEquiv, MvPolynomial.optionEquivLeft]

Premises used: Polynomial.C, MvPolynomial.finSuccEquiv, RingHom.comp, AlgHom.toRingHom, RingHom.algebraMap_toAlgebra, MvPolynomial.optionEquivLeft
-- 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 : Algebra (MvPolynomial (Fin n) R) ↥R' := φ.toAlgebra
⊢ IsScalarTower (MvPolynomial (Fin n) R) (↥R') S

Tactic:
have : IsScalarTower (MvPolynomial (Fin n) R) R' S := .of_algebraMap_eq' <| by
          ext <;> simp [φ, (f'.toRingHom.comp C).algebraMap_toAlgebra, φ.algebraMap_toAlgebra, f',
            MvPolynomial.finSuccEquiv, MvPolynomial.optionEquivLeft]
-- 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_6 : Algebra (MvPolynomial (Fin n) R) ↥R' := φ.toAlgebra
this : IsScalarTower (MvPolynomial (Fin n) R) (↥R') S
⊢ φ.IsIntegral

Tactic:
algebraMap_isIntegral_iff.mpr (integralClosure_eq_top_iff.mp ?_)

Premises used: Iff.mpr, integralClosure_eq_top_iff, algebraMap_isIntegral_iff, Iff.mp
-- 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_6 : Algebra (MvPolynomial (Fin n) R) ↥R' := φ.toAlgebra
this : IsScalarTower (MvPolynomial (Fin n) R) (↥R') S
refine_1 : Eq.{u + 1} (α := Subalgebra (MvPolynomial (Fin n) R) ↥R') (integralClosure (MvPolynomial (Fin n) R) ↥R') ⊤
⊢ φ.IsIntegral

Tactic:
refine algebraMap_isIntegral_iff.mpr (integralClosure_eq_top_iff.mp ?_)

Premises used: Iff.mpr, integralClosure_eq_top_iff, algebraMap_isIntegral_iff, Iff.mp
-- 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_6 : Algebra (MvPolynomial (Fin n) R) ↥R' := φ.toAlgebra
this : IsScalarTower (MvPolynomial (Fin n) R) (↥R') S
refine_1 :
  Eq (α := Subalgebra R ↥R')
    (Subalgebra.restrictScalars R (S := MvPolynomial (Fin n) R) (integralClosure (MvPolynomial (Fin n) R) ↥R'))
    (Subalgebra.restrictScalars R (S := MvPolynomial (Fin n) R) ⊤)
⊢ Eq.{u + 1} (α := Subalgebra (MvPolynomial (Fin n) R) ↥R') (integralClosure (MvPolynomial (Fin n) R) ↥R') ⊤

Tactic:
apply Subalgebra.restrictScalars_injective R

Premises used: Subalgebra.restrictScalars_injective
-- 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_6 : Algebra (MvPolynomial (Fin n) R) ↥R' := φ.toAlgebra
this : IsScalarTower (MvPolynomial (Fin n) R) (↥R') S
refine_1 :
  Subalgebra.map R'.val
      (Subalgebra.restrictScalars R (S := MvPolynomial (Fin n) R) (integralClosure (MvPolynomial (Fin n) R) ↥R')) =
    Subalgebra.map R'.val (Subalgebra.restrictScalars R (S := MvPolynomial (Fin n) R) ⊤)
⊢ Eq (α := Subalgebra R ↥R')
    (Subalgebra.restrictScalars R (S := MvPolynomial (Fin n) R) (integralClosure (MvPolynomial (Fin n) R) ↥R'))
    (Subalgebra.restrictScalars R (S := MvPolynomial (Fin n) R) ⊤)

Tactic:
rw [← (Subalgebra.map_injective (f := R'.val) Subtype.val_injective).eq_iff]

Premises used: Subtype.val_injective, Function.Injective.eq_iff, Subalgebra.map_injective