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
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
this_1 : IsDomain S'
this_2 : IsDomain R
this_3 : Algebra.IsIntegral R R'
this_4 : FaithfulSMul R' K
this_5 : FaithfulSMul R R'
this_6 : FaithfulSMul R' L
this_7 : FaithfulSMul R' S'
this_8 : IsIntegrallyClosedIn R' K
this : IsIntegrallyClosed R'
g : R' ⊗[R] S →ₐ[R'] S' := TensorProduct.lift (ofId R' S') f ⋯
hf₃ : Function.Injective.{u_2 + 1, u_7 + 1} (α := S) (β := S') (⇑f : (a : S) → S')
hf₄ : f.IsIntegral
H₁ : IsStronglyTranscendental.{u_6, u_7} R' (S := S') ((f : (a : S) → S') x : S')
H₂ : RingHom.Finite.{u_6, u_7} (A := R'[X]) (B := S') (AlgHom.toRingHom (R := R') (aeval ((f : (a : S) → S') x)))
Q : Ideal S'
isPrime : Q.IsPrime
hQ :
  PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S' } =
    { asIdeal := P, isPrime := inst_27 }
⊢ False
have suffices : WeaklyQuasiFiniteAt R' Q
Tactic: suffices WeaklyQuasiFiniteAt R' Q from
    not_isStronglyTranscendental_of_weaklyQuasiFiniteAt_of_isIntegrallyClosed H₂ Q H₁
-- 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
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
this_1 : IsDomain S'
this_2 : IsDomain R
this_3 : Algebra.IsIntegral R R'
this_4 : FaithfulSMul R' K
this_5 : FaithfulSMul R R'
this_6 : FaithfulSMul R' L
this_7 : FaithfulSMul R' S'
this_8 : IsIntegrallyClosedIn R' K
this : IsIntegrallyClosed R'
g : R' ⊗[R] S →ₐ[R'] S' := TensorProduct.lift (ofId R' S') f ⋯
hf₃ : Function.Injective.{u_2 + 1, u_7 + 1} (α := S) (β := S') (⇑f : (a : S) → S')
hf₄ : f.IsIntegral
H₁ : IsStronglyTranscendental.{u_6, u_7} R' (S := S') ((f : (a : S) → S') x : S')
H₂ : RingHom.Finite.{u_6, u_7} (A := R'[X]) (B := S') (AlgHom.toRingHom (R := R') (aeval ((f : (a : S) → S') x)))
Q : Ideal S'
isPrime : Q.IsPrime
hQ :
  PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S' } =
    { asIdeal := P, isPrime := inst_27 }
⊢ P = Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) (Ideal.comap g.toRingHom Q)
have rw : P = Ideal.comap (g.comp (AlgHom.toRingHom TensorProduct.includeRight)) Q
Tactic: rw [Ideal.comap_comap]
-- 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
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
this_1 : IsDomain S'
this_2 : IsDomain R
this_3 : Algebra.IsIntegral R R'
this_4 : FaithfulSMul R' K
this_5 : FaithfulSMul R R'
this_6 : FaithfulSMul R' L
this_7 : FaithfulSMul R' S'
this_8 : IsIntegrallyClosedIn R' K
this : IsIntegrallyClosed R'
g : R' ⊗[R] S →ₐ[R'] S' := TensorProduct.lift (ofId R' S') f ⋯
hf₃ : Function.Injective.{u_2 + 1, u_7 + 1} (α := S) (β := S') (⇑f : (a : S) → S')
hf₄ : f.IsIntegral
H₁ : IsStronglyTranscendental.{u_6, u_7} R' (S := S') ((f : (a : S) → S') x : S')
H₂ : RingHom.Finite.{u_6, u_7} (A := R'[X]) (B := S') (AlgHom.toRingHom (R := R') (aeval ((f : (a : S) → S') x)))
Q : Ideal S'
isPrime : Q.IsPrime
hQ :
  PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S' } =
    { asIdeal := P, isPrime := inst_27 }
⊢ P = Ideal.comap (g.comp (AlgHom.toRingHom TensorProduct.includeRight)) Q
have h : Ideal.comap (g.comp (AlgHom.toRingHom TensorProduct.includeRight)) Q =
  (PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S' }).asIdeal
Tactic: convert! congr(($hQ.symm).1)
-- 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
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
this_1 : IsDomain S'
this_2 : IsDomain R
this_3 : Algebra.IsIntegral R R'
this_4 : FaithfulSMul R' K
this_5 : FaithfulSMul R R'
this_6 : FaithfulSMul R' L
this_7 : FaithfulSMul R' S'
this_8 : IsIntegrallyClosedIn R' K
this : IsIntegrallyClosed R'
g : R' ⊗[R] S →ₐ[R'] S' := TensorProduct.lift (ofId R' S') f ⋯
hf₃ : Function.Injective.{u_2 + 1, u_7 + 1} (α := S) (β := S') (⇑f : (a : S) → S')
hf₄ : f.IsIntegral
H₁ : IsStronglyTranscendental.{u_6, u_7} R' (S := S') ((f : (a : S) → S') x : S')
H₂ : RingHom.Finite.{u_6, u_7} (A := R'[X]) (B := S') (AlgHom.toRingHom (R := R') (aeval ((f : (a : S) → S') x)))
Q : Ideal S'
isPrime : Q.IsPrime
hQ :
  PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S' } =
    { asIdeal := P, isPrime := inst_27 }
⊢ Ideal.comap (g.comp (AlgHom.toRingHom TensorProduct.includeRight)) Q =
    (PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S' }).asIdeal
have h : ∀ (x : S),
  Membership.mem (γ := Ideal S) (Ideal.comap (g.comp (AlgHom.toRingHom TensorProduct.includeRight)) Q) x ↔
    x ∈ (PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S' }).asIdeal
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
this_1 : IsDomain S'
this_2 : IsDomain R
this_3 : Algebra.IsIntegral R R'
this_4 : FaithfulSMul R' K
this_5 : FaithfulSMul R R'
this_6 : FaithfulSMul R' L
this_7 : FaithfulSMul R' S'
this_8 : IsIntegrallyClosedIn R' K
this : IsIntegrallyClosed R'
g : R' ⊗[R] S →ₐ[R'] S' := TensorProduct.lift (ofId R' S') f ⋯
hf₃ : Function.Injective.{u_2 + 1, u_7 + 1} (α := S) (β := S') (⇑f : (a : S) → S')
hf₄ : f.IsIntegral
H₁ : IsStronglyTranscendental.{u_6, u_7} R' (S := S') ((f : (a : S) → S') x : S')
H₂ : RingHom.Finite.{u_6, u_7} (A := R'[X]) (B := S') (AlgHom.toRingHom (R := R') (aeval ((f : (a : S) → S') x)))
Q : Ideal S'
isPrime : Q.IsPrime
hQ :
  PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S' } =
    { asIdeal := P, isPrime := inst_27 }
⊢ WeaklyQuasiFiniteAt R' Q
have this₁ : WeaklyQuasiFiniteAt R' (Ideal.comap g.toRingHom Q)
Tactic: have : Algebra.WeaklyQuasiFiniteAt R' (Q.comap g.toRingHom) := .baseChange P _ <| by
    rw [Ideal.comap_comap]
    convert! congr(($hQ.symm).1)
    ext; simp [g]
-- 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 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_4 : P.IsPrime
inst_5 : WeaklyQuasiFiniteAt R P
⊢ ¬IsStronglyTranscendental R x
have inr : ∀
  (this :
    ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S] [IsReduced S]
      {x : S} (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
      [inst_9 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S),
      ¬IsStronglyTranscendental R x)
  (hS : ¬(IsDomain S ∧ FaithfulSMul R S)), ¬IsStronglyTranscendental R x
Tactic: wlog hS : IsDomain S ∧ FaithfulSMul R S
-- 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 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_4 : P.IsPrime
inst_5 : WeaklyQuasiFiniteAt R P
inr :
  ∀
    (this :
      ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S] [IsReduced S]
        {x : S} (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
        [inst_9 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S),
        ¬IsStronglyTranscendental R x)
    (hS : ¬(IsDomain S ∧ FaithfulSMul R S)), ¬IsStronglyTranscendental R x
⊢ ¬IsStronglyTranscendental R x
have wlog : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S] [IsReduced S] {x : S}
  (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S) [inst_9 : P.IsPrime]
  [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
Tactic: wlog hS : IsDomain S ∧ FaithfulSMul R S
Cleared hypotheses: R, S, inst, inst_1, inst_2, inst_3, x, hx', P, inst_4, inst_5
-- 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 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_4 : P.IsPrime
inst_5 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S] [IsReduced S] {x : S}
    (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_9 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
⊢ False
have inr : ∀ (p : Ideal S) (hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p) (hpP : p ≤ P), False
Tactic: obtain ⟨p, hp, hpP⟩ := Ideal.exists_minimalPrimes_le (J := P) bot_le
-- 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 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_4 : P.IsPrime
inst_5 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S] [IsReduced S] {x : S}
    (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_9 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
⊢ False
have inst : p.IsPrime
Tactic: have inst := hp.1.1
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_7 : CommRing S] [inst_8 : Algebra R S] [IsReduced S] {x : S}
    (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_10 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst : p.IsPrime
⊢ False
have inst₁ : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
Tactic: have inst : (P.map (Ideal.Quotient.mk p)).IsPrime :=
      Ideal.map_isPrime_of_surjective Ideal.Quotient.mk_surjective (by simpa)
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_8 : CommRing S] [inst_9 : Algebra R S] [IsReduced S] {x : S}
    (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_11 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
⊢ WeaklyQuasiFiniteAt.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p)) (S := S ⧸ p)
    (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
have suffices : WeaklyQuasiFiniteAt R (S := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
Tactic: suffices Algebra.WeaklyQuasiFiniteAt R (P.map (Ideal.Quotient.mk p)) from
        .of_restrictScalars R _ _
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_8 : CommRing S] [inst_9 : Algebra R S] [IsReduced S] {x : S}
    (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_11 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
⊢ WeaklyQuasiFiniteAt R (S := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
have refine : P = Ideal.comap (F := S →ₐ[R] S ⧸ p) (Ideal.Quotient.mkₐ R p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
Tactic: refine .of_surjectiveOnStalks P _ (Ideal.Quotient.mkₐ _ _)
        (RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective) ?_
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_8 : CommRing S] [inst_9 : Algebra R S] [IsReduced S] {x : S}
    (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_11 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
⊢ P = Ideal.comap (F := S →ₐ[R] S ⧸ p) (Ideal.Quotient.mkₐ R p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
have refine : P = P ⊔ Ideal.comap (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) ⊥
Tactic: refine .trans ?_ (Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective _).symm
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_8 : CommRing S] [inst_9 : Algebra R S] [IsReduced S] {x : S}
    (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_11 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
⊢ False
have inst₁ : WeaklyQuasiFiniteAt.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p)) (S := S ⧸ p)
  (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
Tactic: have inst : WeaklyQuasiFiniteAt (R ⧸ Ideal.under R p) (Ideal.map (Ideal.Quotient.mk p) P) := by
      suffices Algebra.WeaklyQuasiFiniteAt R (P.map (Ideal.Quotient.mk p)) from
        .of_restrictScalars R _ _
      refine .of_surjectiveOnStalks P _ (Ideal.Quotient.mkₐ _ _)
        (RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective) ?_
      refine .trans ?_ (Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective _).symm
      simpa [← RingHom.ker_eq_comap_bot]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_9 : CommRing S] [inst_10 : Algebra R S] [IsReduced S]
    {x : S} (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_12 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst_8 : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
inst :
  WeaklyQuasiFiniteAt.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p)) (S := S ⧸ p)
    (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
⊢ False
have inr : RingHom.Finite.{u_1, u_2} (A := (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))[X]) (B := S ⧸ p)
  (AlgHom.toRingHom (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))
    (aeval ((Ideal.Quotient.mk p : (a : S) → S ⧸ p) x)))
Tactic: refine this (R := R ⧸ p.under R) ?_ (P.map (Ideal.Quotient.mk p)) ⟨inferInstance, inferInstance⟩
      ((isStronglyTranscendental_mk_of_mem_minimalPrimes hx p hp).of_surjective_left
        Ideal.Quotient.mk_surjective)