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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
obtain :
  ∀ (r : R[X]) (hr : (φ : (a : R[X]) → S) r = HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t),
    ∃ (q : R[X]), IsIntegral R (HSub.hSub (β := S) t ((φ : (a : R[X]) → S) q : S))
⊢ ∃ (q : R[X]), IsIntegral R (HSub.hSub (β := S) t ((φ : (a : R[X]) → S) q : S))

Tactic:
obtain ⟨r, hr : φ r = _⟩ := hp
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
r : R[X]
hr : (φ : (a : R[X]) → S) r = HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t
inl :
  ∀ (hpm : Monic.{u_1} (R := R) 1) (hr : (φ : (a : R[X]) → S) r = HMul.hMul (α := S) ((φ : (a : R[X]) → S) 1 : S) t),
    ∃ (q : R[X]), IsIntegral R (HSub.hSub (β := S) t ((φ : (a : R[X]) → S) q : S))
inr : ∀ (hp1 : p ≠ 1), ∃ (q : R[X]), IsIntegral R (HSub.hSub (β := S) t ((φ : (a : R[X]) → S) q : S))
⊢ ∃ (q : R[X]), IsIntegral R (HSub.hSub (β := S) t ((φ : (a : R[X]) → S) q : S))

Tactic:
obtain rfl | hp1 := eq_or_ne p 1

Premises used: eq_or_ne, OfNat.ofNat, 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
φ : R[X] →ₐ[R] S
t : S
ht : φ.IsIntegralElem t
r : R[X]
hpm : Monic.{u_1} (R := R) 1
hr : (φ : (a : R[X]) → S) r = HMul.hMul (α := S) ((φ : (a : R[X]) → S) 1 : S) t
⊢ IsIntegral R (HSub.hSub (β := S) t ((φ : (a : R[X]) → S) r : S))

Tactic:
simp_all [isIntegral_zero]

Premises used: isIntegral_zero
-- 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
φ : R[X] →ₐ[R] S
t : S
ht : φ.IsIntegralElem t
r : R[X]
hpm : Monic.{u_1} (R := R) 1
hr : (φ : (a : R[X]) → S) r = HMul.hMul (α := S) ((φ : (a : R[X]) → S) 1 : S) t
⊢ ∃ (q : R[X]), IsIntegral R (HSub.hSub (β := S) t ((φ : (a : R[X]) → S) q : S))

Tactic:
exact ⟨r, by simp_all [isIntegral_zero]⟩
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
r : R[X]
hr : (φ : (a : R[X]) → S) r = HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t
hp1 : p ≠ 1
⊢ HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) (HSub.hSub (β := S) t ((φ : (a : R[X]) → S) (r /ₘ p) : S)) =
    (φ : (a : R[X]) → S) (r %ₘ p)

Tactic:
simp [mul_sub, ← hr, sub_eq_iff_eq_add, ← map_mul, ← map_add, r.modByMonic_add_div]

Premises used: mul_sub, map_add, map_mul, sub_eq_iff_eq_add, Polynomial.modByMonic_add_div
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
r : R[X]
hr : (φ : (a : R[X]) → S) r = HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t
hp1 : p ≠ 1
⊢ ∃ (q : R[X]), IsIntegral R (HSub.hSub (β := S) t ((φ : (a : R[X]) → S) q : S))

Tactic:
exact ⟨_, isIntegral_of_isIntegralElem_of_monic_of_natDegree_lt φ (t - φ (r /ₘ p)) p (r %ₘ p)
    (ht.sub _ φ.isIntegralElem_map) hpm (natDegree_modByMonic_lt _ hpm hp1)
    (by simp [mul_sub, ← hr, sub_eq_iff_eq_add, ← map_mul, ← map_add, r.modByMonic_add_div])⟩
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
set :
  let a := p.leadingCoeff;
  ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))
⊢ ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (p.leadingCoeff ^ n • t) ((φ : (a : R[X]) → S) q : S))

Tactic:
set a := p.leadingCoeff

Premises used: Polynomial.leadingCoeff
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
⊢ ∀ (x : R),
    Eq.{u_2 + 1} (α := S') (((algebraMap R S' : R →+* S') : (a : R) → S') x : S')
      (((algebraMap R' S' : R' →+* S') : (a : R') → S') ((algebraMap R R' : (a : R) → R') x) : S')

Tactic:
simp +zetaDelta [RingHom.algebraMap_toAlgebra, IsLocalization.Away.map, ← algebraMap_apply R S]

Premises used: IsLocalization.Away.map, RingHom.algebraMap_toAlgebra, IsScalarTower.algebraMap_apply
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
⊢ IsScalarTower R R' S'

Tactic:
have : IsScalarTower R R' S' := .of_algebraMap_eq (by
    simp +zetaDelta [RingHom.algebraMap_toAlgebra, IsLocalization.Away.map, ← algebraMap_apply R S])
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
⊢ IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')

Tactic:
have ha : IsUnit (algebraMap R R' a) := IsLocalization.Away.algebraMap_isUnit a
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
h₁ :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S')
      (((RingHom.comp
                (RingHom.comp
                  (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
                  (mapRingHom (algebraMap R R')))
                C :
              R →+* S') :
            (a : R) → S')
          x :
        S')
      (((RingHom.comp (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S)) C :
              R →+* S') :
            (a : R) → S')
          x :
        S')
h₂ :
  Eq.{u_2 + 1} (α := S')
    (((RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
              (mapRingHom (algebraMap R R')) :
            RingHom.{u_1, u_2} R[X] S') :
          (a : R[X]) → S')
        X :
      S')
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
            RingHom.{u_1, u_2} R[X] S') :
          (a : R[X]) → S')
        X :
      S')
⊢ Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')

Tactic:
ext
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
x : R
⊢ Eq.{u_2 + 1} (α := S')
    (((RingHom.comp
              (RingHom.comp
                (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
                (mapRingHom (algebraMap R R')))
              C :
            R →+* S') :
          (a : R) → S')
        x :
      S')
    (((RingHom.comp (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S)) C :
            R →+* S') :
          (a : R) → S')
        x :
      S')

Tactic:
simp [-Polynomial.algebraMap_apply, ← Polynomial.algebraMap_eq, ← algebraMap_apply]

Premises used: Polynomial.algebraMap_apply, IsScalarTower.algebraMap_apply, Polynomial.algebraMap_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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
⊢ Eq.{u_2 + 1} (α := S')
    (((RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
              (mapRingHom (algebraMap R R')) :
            RingHom.{u_1, u_2} R[X] S') :
          (a : R[X]) → S')
        X :
      S')
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
            RingHom.{u_1, u_2} R[X] S') :
          (a : R[X]) → S')
        X :
      S')

Tactic:
simp [-Polynomial.algebraMap_apply, ← Polynomial.algebraMap_eq, ← algebraMap_apply]

Premises used: Polynomial.algebraMap_apply, IsScalarTower.algebraMap_apply, Polynomial.algebraMap_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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
⊢ Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')

Tactic:
have H : (aeval ((algebraMap S S') (φ X))).toRingHom.comp (mapRingHom (algebraMap R R')) =
    (algebraMap S S').comp φ := by ext <;>
      simp [-Polynomial.algebraMap_apply, ← Polynomial.algebraMap_eq, ← algebraMap_apply]
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
obtain :
  ∀ (q : R[X][X]) (hqm : q.Monic) (hq : eval₂ φ.toRingHom t q = 0),
    RingHom.IsIntegralElem.{u_1, u_2} (R := R'[X]) (A := S')
      (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))) :
        RingHom.{u_1, u_2} R'[X] S')
      ((algebraMap S S' : (a : S) → S') t : S')
⊢ RingHom.IsIntegralElem.{u_1, u_2} (R := R'[X]) (A := S')
    (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))) :
      RingHom.{u_1, u_2} R'[X] S')
    ((algebraMap S S' : (a : S) → S') t : S')

Tactic:
obtain ⟨q, hqm, hq⟩ := ht
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R[X][X]
hqm : q.Monic
hq : eval₂ φ.toRingHom t q = 0
⊢ RingHom.IsIntegralElem.{u_1, u_2} (R := R'[X]) (A := S')
    (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))) :
      RingHom.{u_1, u_2} R'[X] S')
    ((algebraMap S S' : (a : S) → S') t : S')

Tactic:
⟨q.map (mapRingHom (algebraMap _ _)), hqm.map _, ?_⟩

Premises used: Algebra.algebraMap, RingHom.IsIntegralElem, Polynomial.mapRingHom, And.intro, Exists.intro, Polynomial.map, Polynomial.Monic.map
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R[X][X]
hqm : q.Monic
hq : eval₂ φ.toRingHom t q = 0
refine :
  Eq (α := S')
    (eval₂ (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        ((algebraMap S S' : (a : S) → S') t) (map (mapRingHom (algebraMap R R')) q) :
      S')
    (0 : S')
⊢ RingHom.IsIntegralElem.{u_1, u_2} (R := R'[X]) (A := S')
    (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))) :
      RingHom.{u_1, u_2} R'[X] S')
    ((algebraMap S S' : (a : S) → S') t : S')

Tactic:
refine ⟨q.map (mapRingHom (algebraMap _ _)), hqm.map _, ?_⟩
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R[X][X]
hqm : q.Monic
hq : eval₂ φ.toRingHom t q = 0
rw :
  Eq (α := S')
    (eval₂
        (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
          (mapRingHom (algebraMap R R')))
        ((algebraMap S S' : (a : S) → S') t) q :
      S')
    (0 : S')
rw₁ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S))
      ((algebraMap S S' : (a : S) → S') t) q =
    0
rw₂ : Eq (α := S') ((algebraMap S S' : (a : S) → S') (eval₂ (↑φ : R[X] →+* S) t q) : S') (0 : S')
rw₃ : Eq (α := S') ((algebraMap S S' : (a : S) → S') (eval₂ φ.toRingHom t q) : S') (0 : S')
rw₄ : Eq (α := S') ((algebraMap S S' : (a : S) → S') 0) 0
rw₅ rw₆ : Eq.{u_2 + 1} (α := S') 0 0
⊢ Eq (α := S')
    (eval₂ (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        ((algebraMap S S' : (a : S) → S') t) (map (mapRingHom (algebraMap R R')) q) :
      S')
    (0 : S')

Tactic:
rw [eval₂_map, H, ← hom_eval₂, ← AlgHom.toRingHom_eq_coe, hq, map_zero]

Premises used: Polynomial.hom_eval₂, map_zero, Polynomial.eval₂_map, AlgHom.toRingHom_eq_coe
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
⊢ Nontrivial R'

Tactic:
nontriviality R'
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
h : Nontrivial R'
⊢ (HMul.hMul (α := R'[X]) ((C : (a_1 : R') → R'[X]) (↑ha.unit⁻¹ : R') : R'[X]) (map (algebraMap R R') p)).Monic

Tactic:
simp [Monic, leadingCoeff_C_mul_of_isUnit,
        leadingCoeff_map_of_leadingCoeff_ne_zero _ ha.ne_zero, a]

Premises used: Polynomial.leadingCoeff_C_mul_of_isUnit, Polynomial.Monic, Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero, IsUnit.ne_zero
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
obtain :
  ∀ (r : R[X]) (hr : (φ : (a : R[X]) → S) r = HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t),
    Membership.mem (γ := Subalgebra R' S')
      (AlgHom.range (A := R'[X]) (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))) : Subalgebra R' S')
      (HMul.hMul (α := S') (β := S')
        (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S')
            (HMul.hMul (α := R'[X]) ((C : (a_1 : R') → R'[X]) (↑ha.unit⁻¹ : R') : R'[X]) (map (algebraMap R R') p)) :
          S')
        ((algebraMap S S' : (a : S) → S') t : S'))
⊢ Membership.mem (γ := Subalgebra R' S')
    (AlgHom.range (A := R'[X]) (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))) : Subalgebra R' S')
    (HMul.hMul (α := S') (β := S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S')
          (HMul.hMul (α := R'[X]) ((C : (a_1 : R') → R'[X]) (↑ha.unit⁻¹ : R') : R'[X]) (map (algebraMap R R') p)) :
        S')
      ((algebraMap S S' : (a : S) → S') t : S'))

Tactic:
obtain ⟨r, hr : φ r = _⟩ := hp