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
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 }
suffices : WeaklyQuasiFiniteAt R' Q
⊢ False

Tactic:
suffices WeaklyQuasiFiniteAt R' Q from
    not_isStronglyTranscendental_of_weaklyQuasiFiniteAt_of_isIntegrallyClosed H₂ Q H₁
-- 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
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 }
rw : P = Ideal.comap (g.comp (AlgHom.toRingHom TensorProduct.includeRight)) Q
⊢ P = Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) (Ideal.comap g.toRingHom Q)

Tactic:
rw [Ideal.comap_comap]

Premises used: Ideal.comap_comap
-- 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
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 }
⊢ { asIdeal := P, isPrime := inst_27 : PrimeSpectrum S }.asIdeal =
    (PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime }).asIdeal

Tactic:
congr(($hQ.symm).1)

Premises used: congrArg, id, Eq.symm, PrimeSpectrum.asIdeal
-- 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
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 }
h :
  Ideal.comap (g.comp (AlgHom.toRingHom TensorProduct.includeRight)) Q =
    (PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S' }).asIdeal
⊢ P = Ideal.comap (g.comp (AlgHom.toRingHom TensorProduct.includeRight)) Q

Tactic:
convert! congr(($hQ.symm).1)
-- 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
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 }
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
⊢ Ideal.comap (g.comp (AlgHom.toRingHom TensorProduct.includeRight)) Q =
    (PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S' }).asIdeal

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
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 }
x_1 : S
⊢ Membership.mem (γ := Ideal S) (Ideal.comap (g.comp (AlgHom.toRingHom TensorProduct.includeRight)) Q) x_1 ↔
    x_1 ∈ (PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S' }).asIdeal

Tactic:
simp [g]
-- 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
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' (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]
-- 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
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_9 : 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 }
this : WeaklyQuasiFiniteAt R' (Ideal.comap g.toRingHom Q)
⊢ WeaklyQuasiFiniteAt R' Q

Tactic:
.of_surjectiveOnStalks (Q.comap g.toRingHom) _ g
    (RingHom.surjectiveOnStalks_of_surjective hf₁) rfl

Premises used: RingHom.surjectiveOnStalks_of_surjective, AlgHom.toRingHom, Ideal.comap, Algebra.WeaklyQuasiFiniteAt.of_surjectiveOnStalks, 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
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_9 : 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 }
this : WeaklyQuasiFiniteAt R' (Ideal.comap g.toRingHom Q)
⊢ WeaklyQuasiFiniteAt R' Q

Tactic:
exact .of_surjectiveOnStalks (Q.comap g.toRingHom) _ g
    (RingHom.surjectiveOnStalks_of_surjective hf₁) 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 : 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
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
⊢ ¬IsStronglyTranscendental R x

Tactic:
wlog hS : IsDomain S ∧ FaithfulSMul R S

Premises used: IsDomain, FaithfulSMul
-- 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 : 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
inr : ∀ (p : Ideal S) (hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p) (hpP : p ≤ P), False
⊢ False

Tactic:
obtain ⟨p, hp, hpP⟩ := Ideal.exists_minimalPrimes_le (J := P) bot_le

Premises used: Ideal.exists_minimalPrimes_le, bot_le
-- 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 : 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
⊢ p.IsPrime

Tactic:
have inst := hp.1.1
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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
⊢ RingHom.ker (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) ≤ P

Tactic:
simpa