awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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 i • t) ^ (n * k + n))
have 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))
Tactic: rw [_root_.smul_pow, pow_add, add_comm, pow_add, mul_smul_mul_comm, hi]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)))
have 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
Tactic: refine Ideal.Quotient.mk_surjective.forall.mpr fun u p e ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
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
⊢ 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
have e₁ : 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
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ 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
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
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
⊢ False
have this : IsDomain R
Tactic: have : IsDomain R := (FaithfulSMul.algebraMap_injective R S).isDomain
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
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
⊢ False
have hf' : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ False
have 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
Tactic: generalize hf : aeval (R := R) x = f at *
Cleared hypotheses: hx', hf'
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
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)
⊢ False
have hx₁ : IsStronglyTranscendental.{u_1, u_2} R (S := S) ((f : (a : R[X]) → S) X : S)
Tactic: obtain rfl : f X = x := by simp [← hf]
Cleared hypotheses: x, hx, hf
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
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)
⊢ False
have hf₁ : aeval ((f : (a : R[X]) → S) X) = f
Tactic: obtain rfl : f X = x := by simp [← hf]
Cleared hypotheses: x, hx, hf
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
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
⊢ False
have this₁ : IsScalarTower R R[X] S
Tactic: have := IsScalarTower.of_algebraMap_eq' f.comp_algebraMap.symm
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
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
⊢ False
have this₁ : Module.Finite.{u_1, u_2} R[X] S
Tactic: have : Module.Finite R[X] S := RingHom.finite_algebraMap.mpr hx'
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
have rw : ∀ (a : R[X]), Eq.{u_2 + 1} (α := S) ((algebraMap R[X] S : (a : R[X]) → S) a : S) (0 : S) → a = 0
Tactic: rw [faithfulSMul_iff_algebraMap_injective, injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ p = 0
have by_contra : ∀ (hp' : ¬p = 0), False
Tactic: by_contra hp'
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ Eq.{u_2 + 1} (α := S) (((aeval ((f : (a : R[X]) → S) X) : R[X] →ₐ[R] S) : (a : R[X]) → S) p : S) (0 : S)
have rwa : Eq.{u_2 + 1} (α := S) ((f : (a : R[X]) → S) ((aeval X : (a : R[X]) → R[X]) p : R[X]) : S) (0 : S)
Tactic: rwa [aeval_algHom_apply, aeval_X_left_apply]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ Eq.{u_2 + 1} (α := S) (((aeval ((f : (a : R[X]) → S) X) : R[X] →ₐ[R] S) : (a : R[X]) → S) p : S) (0 : S)
have rwa₁ : Eq.{u_2 + 1} (α := S) ((f : (a : R[X]) → S) p : S) (0 : S)
Tactic: rwa [aeval_algHom_apply, aeval_X_left_apply]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
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
⊢ False
have this₁ : 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]⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
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
⊢ False
have this₁ : 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 _ _
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ False
have 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
Tactic: obtain ⟨Q, hQ, _, ⟨e⟩⟩ := Ideal.exists_ideal_lt_liesOver_of_lt (S := S) P this
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
have refine : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R P)
Tactic: refine hQ.ne (Algebra.WeaklyQuasiFiniteAt.eq_of_le_of_under_eq (R := R) hQ.le ?_)
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R P)
have rw : Eq (α := Ideal R) (Ideal.under R (B := R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))) (Ideal.under R P)
Tactic: rw [← Ideal.under_under (B := R[X]), ← e]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ Eq (α := Ideal R) (Ideal.under R (B := R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))) (Ideal.under R P)
have h : ∀ (x : R),
  Membership.mem (γ := Ideal R) (Ideal.under R (B := R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))) x ↔
    Membership.mem (γ := Ideal R) (Ideal.under R P) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_4
L : Type u_5
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : IsScalarTower R K L
inst_10 : IsScalarTower R S L
inst_11 : IsFractionRing R K
inst_12 : IsFractionRing S L
R' : Type u_6
S' : Type u_7
inst_13 : CommRing R'
inst_14 : CommRing S'
inst_15 : Algebra R R'
inst_16 : Algebra R' S'
inst_17 : Algebra R S'
inst_18 : Algebra S' L
inst_19 : Algebra R' L
inst_20 : IsScalarTower R' S' L
inst_21 : Algebra R' K
inst_22 : IsScalarTower R' K L
inst_23 : IsScalarTower R R' S'
inst_24 : FaithfulSMul S' L
inst_25 : IsIntegralClosure R' R K
inst_26 : IsScalarTower R R' K
f : S →ₐ[R] S'
hf₁ :
  Function.Surjective (α := R' ⊗[R] S) (β := S')
    (⇑(TensorProduct.lift (ofId R' S') f ⋯ : R' ⊗[R] S →ₐ[R'] S') : (a : R' ⊗[R] S) → S')
hf₂ : Eq (α := S →+* L) (RingHom.comp (algebraMap S' L) f.toRingHom) (algebraMap S L)
x : S
hx' : AlgHom.Finite.{u_1, u_1, u_2} (R := R) (A := R[X]) (aeval x)
P : Ideal S
inst_27 : P.IsPrime
inst_28 : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
⊢ False
have this : IsDomain S'
Tactic: have := (FaithfulSMul.algebraMap_injective S' L).isDomain