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_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
k : ℕ
hk : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ (n * k) • t ^ n)
hpn : ¬p.leadingCoeff ^ n = 0
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)

Tactic:
⟨n * k + n, ?_⟩

Premises used: HMul.hMul, Set.Mem, setOf, HAdd.hAdd, Exists.intro
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
k : ℕ
hk : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ (n * k) • t ^ n)
hpn : ¬p.leadingCoeff ^ n = 0
neg : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) ((p.coeff i • t) ^ (n * k + n))
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)

Tactic:
refine ⟨n * k + n, ?_⟩
-- 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_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
k : ℕ
hk : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ (n * k) • t ^ n)
hpn : ¬p.leadingCoeff ^ n = 0
neg :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (p.coeff p.natDegree ^ (n * k) • t ^ n * p.coeff p.natDegree ^ n • t ^ (n * k))
⊢ Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) ((p.coeff i • t) ^ (n * k + n))

Tactic:
rw [_root_.smul_pow, pow_add, add_comm, pow_add, mul_smul_mul_comm, hi]

Premises used: pow_add, add_comm, smul_pow, mul_smul_mul_comm
-- 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_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
k : ℕ
hk : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ (n * k) • t ^ n)
hpn : ¬p.leadingCoeff ^ n = 0
⊢ Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (p.coeff p.natDegree ^ (n * k) • t ^ n * p.coeff p.natDegree ^ n • t ^ (n * k))

Tactic:
Ideal.mul_mem_right _ _ hk

Premises used: Set.Mem, setOf, Ideal.mul_mem_right
-- 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_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
k : ℕ
hk : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ (n * k) • t ^ n)
hpn : ¬p.leadingCoeff ^ n = 0
⊢ Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (p.coeff p.natDegree ^ (n * k) • t ^ n * p.coeff p.natDegree ^ n • t ^ (n * k))

Tactic:
exact Ideal.mul_mem_right _ _ hk

Premises used: Ideal.mul_mem_right
-- 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
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
x : S
hx : AlgHom.Finite.{u_1, u_1, u_2} (R := R) (A := R[X]) (aeval x)
⊢ IsStronglyTranscendental R (S := HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))
    ((Ideal.Quotient.mk (Ideal.radical (conductor R x)) : (a : S) → S ⧸ (conductor R x).radical) x :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))

Tactic:
Ideal.Quotient.mk_surjective.forall.mpr fun u p e ↦ ?_

Premises used: Iff.mpr, Function.Surjective.forall, Ideal.Quotient.mk_surjective, IsStronglyTranscendental
-- 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
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
x : S
hx : AlgHom.Finite.{u_1, u_1, u_2} (R := R) (A := R[X]) (aeval x)
refine :
  ∀ (u : S) (p : R[X])
    (e :
      HMul.hMul (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x))) (β :=
          HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))
          (((aeval ((Ideal.Quotient.mk (Ideal.radical (conductor R x)) : (a : S) → S ⧸ (conductor R x).radical) x) :
                  AlgHom.{u_1, u_1, u_2} R R[X]
                    (HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))) :
                (a : R[X]) → S ⧸ (conductor R x).radical)
              p :
            HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))
          ((Ideal.Quotient.mk (Ideal.radical (conductor R x)) : (a : S) → S ⧸ (conductor R x).radical) u :
            HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x))) =
        0),
    HMul.hMul (α := (HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))[X]) (β :=
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))[X])
        (map (algebraMap R (HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))) p)
        ((C : (a : S ⧸ (conductor R x).radical) → (S ⧸ (conductor R x).radical)[X])
            ((Ideal.Quotient.mk (Ideal.radical (conductor R x)) : (a : S) → S ⧸ (conductor R x).radical) u) :
          (HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))[X]) =
      0
⊢ IsStronglyTranscendental R (S := HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))
    ((Ideal.Quotient.mk (Ideal.radical (conductor R x)) : (a : S) → S ⧸ (conductor R x).radical) x :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))

Tactic:
refine Ideal.Quotient.mk_surjective.forall.mpr fun u p e ↦ ?_

Premises used: Iff.mpr, Function.Surjective.forall, Ideal.Quotient.mk_surjective
-- 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
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
x : S
hx : AlgHom.Finite.{u_1, u_1, u_2} (R := R) (A := R[X]) (aeval x)
u : S
p : R[X]
e :
  HMul.hMul (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x))) (β :=
      HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))
      (((aeval ((Ideal.Quotient.mk (Ideal.radical (conductor R x)) : (a : S) → S ⧸ (conductor R x).radical) x) :
              AlgHom.{u_1, u_1, u_2} R R[X] (HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))) :
            (a : R[X]) → S ⧸ (conductor R x).radical)
          p :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))
      ((Ideal.Quotient.mk (Ideal.radical (conductor R x)) : (a : S) → S ⧸ (conductor R x).radical) u :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x))) =
    0
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R x))
    (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u)

Tactic:
rw [← Ideal.Quotient.algebraMap_eq, aeval_algebraMap_apply, Ideal.Quotient.algebraMap_eq,
    ← map_mul, Ideal.Quotient.eq_zero_iff_mem] at e

Premises used: Ideal.Quotient.algebraMap_eq, Ideal.Quotient.eq_zero_iff_mem, map_mul, Polynomial.aeval_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
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
x : S
hx : AlgHom.Finite.{u_1, u_1, u_2} (R := R) (A := R[X]) (aeval x)
u : S
p : R[X]
e :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R x))
    (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u)
a :
  ∀ (i : ℕ),
    (HMul.hMul (α := (HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))[X]) (β :=
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))[X])
            (map (algebraMap R (HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))) p)
            ((C : (a : S ⧸ (conductor R x).radical) → (S ⧸ (conductor R x).radical)[X])
                ((Ideal.Quotient.mk (Ideal.radical (conductor R x)) : (a : S) → S ⧸ (conductor R x).radical) u) :
              (HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))[X])).coeff
        i =
      coeff 0 i
⊢ HMul.hMul (α := (HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))[X]) (β :=
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))[X])
      (map (algebraMap R (HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))) p)
      ((C : (a : S ⧸ (conductor R x).radical) → (S ⧸ (conductor R x).radical)[X])
          ((Ideal.Quotient.mk (Ideal.radical (conductor R x)) : (a : S) → S ⧸ (conductor R x).radical) u) :
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.radical (conductor R x)))[X]) =
    0

Tactic:
ext i
-- 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
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
x : S
hx : AlgHom.Finite.{u_1, u_1, u_2} (R := R) (A := R[X]) (aeval x)
u : S
p : R[X]
e :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R x))
    (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u)
i : ℕ
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((aeval x : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u)

Tactic:
simpa using e
-- 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 : FaithfulSMul R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
x : S
hx' : AlgHom.Finite.{u_1, u_1, u_2} (R := R) (A := R[X]) (aeval x)
P : Ideal S
inst_6 : P.IsPrime
inst_7 : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
⊢ IsDomain R

Tactic:
have : IsDomain R := (FaithfulSMul.algebraMap_injective R S).isDomain
-- 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 : FaithfulSMul R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
x : S
hx' : AlgHom.Finite.{u_1, u_1, u_2} (R := R) (A := R[X]) (aeval x)
P : Ideal S
inst_6 : P.IsPrime
inst_7 : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this : IsDomain R
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)

Tactic:
have hf' : Function.Injective (aeval (R := R) x) := (injective_iff_map_eq_zero _).mpr
    fun p hp ↦ not_not.mp fun hp' ↦ hx.transcendental ⟨p, hp', 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
inst_3 : FaithfulSMul R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
x : S
hx' : AlgHom.Finite.{u_1, u_1, u_2} (R := R) (A := R[X]) (aeval x)
P : Ideal S
inst_6 : P.IsPrime
inst_7 : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this : IsDomain R
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
generalize :
  ∀ (f : R[X] →ₐ[R] S) (hf : aeval x = f) (hx' : f.Finite)
    (hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)), False
⊢ False

Tactic:
generalize hf : aeval (R := R) x = f at *

Premises used: Polynomial.aeval
-- 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 : FaithfulSMul R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
x : S
P : Ideal S
inst_6 : P.IsPrime
inst_7 : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this : IsDomain R
f : R[X] →ₐ[R] S
hf : aeval x = f
hx' : f.Finite
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
⊢ (f : (a : R[X]) → S) X = x

Tactic:
simp [← hf]
-- 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 : FaithfulSMul R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
x : S
P : Ideal S
inst_6 : P.IsPrime
inst_7 : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this : IsDomain R
f : R[X] →ₐ[R] S
hf : aeval x = f
hx' : f.Finite
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
⊢ IsStronglyTranscendental.{u_1, u_2} R (S := S) ((f : (a : R[X]) → S) X : S)

Tactic:
obtain rfl : f X = x := by simp [← hf]

Premises used: Polynomial.X, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
x : S
P : Ideal S
inst_6 : P.IsPrime
inst_7 : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this : IsDomain R
f : R[X] →ₐ[R] S
hf : aeval x = f
hx' : f.Finite
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
hx₁ : IsStronglyTranscendental.{u_1, u_2} R (S := S) ((f : (a : R[X]) → S) X : S)
⊢ aeval ((f : (a : R[X]) → S) X) = f

Tactic:
obtain rfl : f X = x := by simp [← hf]

Premises used: Polynomial.X, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
P : Ideal S
inst_6 : P.IsPrime
inst_7 : WeaklyQuasiFiniteAt R P
this_1 : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
hx : IsStronglyTranscendental.{u_1, u_2} R (S := S) ((f : (a : R[X]) → S) X : S)
hf : aeval ((f : (a : R[X]) → S) X) = f
this : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
⊢ IsScalarTower R R[X] S

Tactic:
have := IsScalarTower.of_algebraMap_eq' f.comp_algebraMap.symm
-- 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 : FaithfulSMul R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
P : Ideal S
inst_6 : P.IsPrime
inst_7 : WeaklyQuasiFiniteAt R P
this_1 : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
hx : IsStronglyTranscendental.{u_1, u_2} R (S := S) ((f : (a : R[X]) → S) X : S)
hf : aeval ((f : (a : R[X]) → S) X) = f
this_2 : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
this : IsScalarTower R R[X] S
⊢ Module.Finite.{u_1, u_2} R[X] S

Tactic:
have : Module.Finite R[X] S := RingHom.finite_algebraMap.mpr hx'
-- 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 : FaithfulSMul R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
P : Ideal S
inst_6 : P.IsPrime
inst_7 : WeaklyQuasiFiniteAt R P
this_1 : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
hx : IsStronglyTranscendental.{u_1, u_2} R (S := S) ((f : (a : R[X]) → S) X : S)
hf : aeval ((f : (a : R[X]) → S) X) = f
this_2 : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
this_3 : IsScalarTower R R[X] S
this : Module.Finite.{u_1, u_2} R[X] S
rw : ∀ (a : R[X]), Eq.{u_2 + 1} (α := S) ((algebraMap R[X] S : (a : R[X]) → S) a : S) (0 : S) → a = 0
⊢ FaithfulSMul.{u_1, u_2} R[X] S

Tactic:
rw [faithfulSMul_iff_algebraMap_injective, injective_iff_map_eq_zero]

Premises used: faithfulSMul_iff_algebraMap_injective, injective_iff_map_eq_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
inst_3 : FaithfulSMul R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
P : Ideal S
inst_6 : P.IsPrime
inst_7 : WeaklyQuasiFiniteAt R P
this_1 : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
hx : IsStronglyTranscendental.{u_1, u_2} R (S := S) ((f : (a : R[X]) → S) X : S)
hf : aeval ((f : (a : R[X]) → S) X) = f
this_2 : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
this_3 : IsScalarTower R R[X] S
this : Module.Finite.{u_1, u_2} R[X] S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((algebraMap R[X] S : (a : R[X]) → S) p : S) (0 : S)
by_contra : ∀ (hp' : ¬p = 0), False
⊢ p = 0

Tactic:
by_contra 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
inst_3 : FaithfulSMul R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
P : Ideal S
inst_6 : P.IsPrime
inst_7 : WeaklyQuasiFiniteAt R P
this_1 : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
hx : IsStronglyTranscendental.{u_1, u_2} R (S := S) ((f : (a : R[X]) → S) X : S)
hf : aeval ((f : (a : R[X]) → S) X) = f
this_2 : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
this_3 : IsScalarTower R R[X] S
this : Module.Finite.{u_1, u_2} R[X] S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((algebraMap R[X] S : (a : R[X]) → S) p : S) (0 : S)
hp' : ¬p = 0
rwa : Eq.{u_2 + 1} (α := S) ((f : (a : R[X]) → S) ((aeval X : (a : R[X]) → R[X]) p : R[X]) : S) (0 : S)
rwa₁ rwa₂ rwa₃ rwa₄ : Eq.{u_2 + 1} (α := S) ((f : (a : R[X]) → S) p : S) (0 : S)
⊢ Eq.{u_2 + 1} (α := S) (((aeval ((f : (a : R[X]) → S) X) : R[X] →ₐ[R] S) : (a : R[X]) → S) p : S) (0 : S)

Tactic:
rwa [aeval_algHom_apply, aeval_X_left_apply]

Premises used: Polynomial.aeval_X_left_apply, Polynomial.aeval_algHom_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
inst_3 : FaithfulSMul R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
P : Ideal S
inst_6 : P.IsPrime
inst_7 : WeaklyQuasiFiniteAt R P
this_1 : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
hx : IsStronglyTranscendental.{u_1, u_2} R (S := S) ((f : (a : R[X]) → S) X : S)
hf : aeval ((f : (a : R[X]) → S) X) = f
this_2 : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
this_3 : IsScalarTower R R[X] S
this : Module.Finite.{u_1, u_2} R[X] S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((algebraMap R[X] S : (a : R[X]) → S) p : S) (0 : S)
hp' : ¬p = 0
⊢ False

Tactic:
exact hx.transcendental ⟨p, hp', by rwa [aeval_algHom_apply, aeval_X_left_apply]⟩

Premises used: IsStronglyTranscendental.transcendental, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
P : Ideal S
inst_6 : P.IsPrime
inst_7 : WeaklyQuasiFiniteAt R P
this_1 : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
hx : IsStronglyTranscendental.{u_1, u_2} R (S := S) ((f : (a : R[X]) → S) X : S)
hf : aeval ((f : (a : R[X]) → S) X) = f
this_2 : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
this_3 : IsScalarTower R R[X] S
this : Module.Finite.{u_1, u_2} R[X] S
⊢ FaithfulSMul.{u_1, u_2} R[X] S

Tactic:
have : FaithfulSMul R[X] S := by
    rw [faithfulSMul_iff_algebraMap_injective, injective_iff_map_eq_zero]
    intro p hp
    by_contra hp'
    exact hx.transcendental ⟨p, hp', by rwa [aeval_algHom_apply, aeval_X_left_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
inst_3 : FaithfulSMul R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
P : Ideal S
inst_6 : P.IsPrime
inst_7 : WeaklyQuasiFiniteAt R P
this_1 : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
hx : IsStronglyTranscendental.{u_1, u_2} R (S := S) ((f : (a : R[X]) → S) X : S)
hf : aeval ((f : (a : R[X]) → S) X) = f
this_2 : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
this_3 : IsScalarTower R R[X] S
this_4 : Module.Finite.{u_1, u_2} R[X] S
this : FaithfulSMul.{u_1, u_2} R[X] S
⊢ LT.lt (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P)) (Ideal.under R[X] P)

Tactic:
have : (P.under R).map C < P.under R[X] := map_under_lt_comap_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 : FaithfulSMul R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
P : Ideal S
inst_6 : P.IsPrime
inst_7 : WeaklyQuasiFiniteAt R P
this_1 : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
hx : IsStronglyTranscendental.{u_1, u_2} R (S := S) ((f : (a : R[X]) → S) X : S)
hf : aeval ((f : (a : R[X]) → S) X) = f
this_2 : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
this_3 : IsScalarTower R R[X] S
this_4 : Module.Finite.{u_1, u_2} R[X] S
this_5 : FaithfulSMul.{u_1, u_2} R[X] S
this : LT.lt (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P)) (Ideal.under R[X] P)
obtain :
  ∀ (Q : Ideal S) (hQ : Q < P),
    Q.IsPrime →
      ∀ (e : Eq (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P)) (Ideal.under R[X] Q)), False
⊢ False

Tactic:
obtain ⟨Q, hQ, _, ⟨e⟩⟩ := Ideal.exists_ideal_lt_liesOver_of_lt (S := S) P this

Premises used: Ideal.exists_ideal_lt_liesOver_of_lt
-- 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 : FaithfulSMul R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
P : Ideal S
inst_6 : P.IsPrime
inst_7 : WeaklyQuasiFiniteAt R P
this_1 : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
hx : IsStronglyTranscendental.{u_1, u_2} R (S := S) ((f : (a : R[X]) → S) X : S)
hf : aeval ((f : (a : R[X]) → S) X) = f
this_2 : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
this_3 : IsScalarTower R R[X] S
this_4 : Module.Finite.{u_1, u_2} R[X] S
this_5 : FaithfulSMul.{u_1, u_2} R[X] S
this : LT.lt (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P)) (Ideal.under R[X] P)
Q : Ideal S
hQ : Q < P
left : Q.IsPrime
e : Eq (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P)) (Ideal.under R[X] Q)
⊢ False

Tactic:
hQ.ne (Algebra.WeaklyQuasiFiniteAt.eq_of_le_of_under_eq (R := R) hQ.le ?_)

Premises used: Algebra.WeaklyQuasiFiniteAt.eq_of_le_of_under_eq, LT.lt.le, LT.lt.ne