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
⊢ IsStronglyTranscendental.{u_6, u_5} R' (S := L) ((algebraMap S L : (a : S) → L) x : L)

Tactic:
((hx.of_isLocalization S⁰).of_isLocalization_left R⁰).restrictScalars (S := K)

Premises used: IsStronglyTranscendental.of_isLocalization_left, nonZeroDivisors, IsStronglyTranscendental.restrictScalars, IsStronglyTranscendental.of_isLocalization
-- 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
⊢ IsStronglyTranscendental.{u_6, u_5} R' (S := L) ((algebraMap S L : (a : S) → L) x : L)

Tactic:
exact ((hx.of_isLocalization S⁰).of_isLocalization_left R⁰).restrictScalars (S := K)

Premises used: IsStronglyTranscendental.of_isLocalization_left, nonZeroDivisors, IsStronglyTranscendental.restrictScalars, IsStronglyTranscendental.of_isLocalization
-- 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
⊢ IsStronglyTranscendental.{u_6, u_7} R' (S := S') ((f : (a : S) → S') x : S')

Tactic:
have H₁ : IsStronglyTranscendental R' (f x) := by
    refine .of_map (f := IsScalarTower.toAlgHom R' S' L) (FaithfulSMul.algebraMap_injective S' L) ?_
    dsimp
    rw [show algebraMap S' L (f x) = algebraMap _ _ x from congr($hf₂ x)]
    exact ((hx.of_isLocalization S⁰).of_isLocalization_left R⁰).restrictScalars (S := K)
-- 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')
⊢ (RingHom.comp (β := R' ⊗[R] R[X])
      (g.comp (AlgHom.toRingHom (TensorProduct.map (AlgHom.id R R') (aeval x) : R' ⊗[R] R[X] →ₐ[R] R' ⊗[R] S)))
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (polyEquivTensor R R')))).Finite

Tactic:
((RingHom.Finite.of_surjective g.toRingHom hf₁).comp
            (RingHom.Finite.tensorProductMap (f := AlgHom.id R R') (RingEquiv.refl _).finite
              hx')).comp
        (polyEquivTensor R R').toRingEquiv.finite

Premises used: RingEquiv.refl, RingHom.Finite.comp, polyEquivTensor, RingHom.Finite.of_surjective, AlgHom.toRingHom, RingEquiv.finite, AlgEquiv.toRingEquiv, RingHom.Finite.tensorProductMap
-- 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 :
  AlgHom.toRingHom (R := R') (aeval ((f : (a : S) → S') x)) =
    RingHom.comp (β := R' ⊗[R] R[X])
      (g.comp (AlgHom.toRingHom (TensorProduct.map (AlgHom.id R R') (aeval x) : R' ⊗[R] R[X] →ₐ[R] R' ⊗[R] S)))
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (polyEquivTensor R R')))
⊢ RingHom.Finite.{u_6, u_7} (A := R'[X]) (B := S') (AlgHom.toRingHom (R := R') (aeval ((f : (a : S) → S') x)))

Tactic:
convert!
      ((RingHom.Finite.of_surjective g.toRingHom hf₁).comp
            (RingHom.Finite.tensorProductMap (f := AlgHom.id R R') (RingEquiv.refl _).finite
              hx')).comp
        (polyEquivTensor R R').toRingEquiv.finite using 1

Premises used: RingEquiv.refl, RingHom.Finite.comp, polyEquivTensor, RingHom.Finite.of_surjective, AlgHom.toRingHom, RingEquiv.finite, AlgEquiv.toRingEquiv, RingHom.Finite.tensorProductMap
-- 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 :
  ∀ (x_1 : R'),
    Eq.{u_7 + 1} (α := S')
      (((RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((f : (a : S) → S') x))) C : R' →+* S') : (a : R') → S') x_1 :
        S')
      (((RingHom.comp (β := R' ⊗[R] R[X])
                  (g.comp
                    (AlgHom.toRingHom (TensorProduct.map (AlgHom.id R R') (aeval x) : R' ⊗[R] R[X] →ₐ[R] R' ⊗[R] S)))
                  (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (polyEquivTensor R R')))).comp
              C :
            (a : R') → S')
          x_1 :
        S')
h₁ :
  Eq.{u_7 + 1} (α := S')
    (((AlgHom.toRingHom (R := R') (aeval ((f : (a : S) → S') x)) : RingHom.{u_6, u_7} R'[X] S') : (a : R'[X]) → S') X :
      S')
    ((RingHom.comp (β := R' ⊗[R] R[X])
            (g.comp (AlgHom.toRingHom (TensorProduct.map (AlgHom.id R R') (aeval x) : R' ⊗[R] R[X] →ₐ[R] R' ⊗[R] S)))
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (polyEquivTensor R R'))) :
          (a : R'[X]) → S')
        X :
      S')
⊢ AlgHom.toRingHom (R := R') (aeval ((f : (a : S) → S') x)) =
    RingHom.comp (β := R' ⊗[R] R[X])
      (g.comp (AlgHom.toRingHom (TensorProduct.map (AlgHom.id R R') (aeval x) : R' ⊗[R] R[X] →ₐ[R] R' ⊗[R] S)))
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (polyEquivTensor R R')))

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')
x_1 : R'
⊢ Eq.{u_7 + 1} (α := S')
    (((RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((f : (a : S) → S') x))) C : R' →+* S') : (a : R') → S') x_1 :
      S')
    (((RingHom.comp (β := R' ⊗[R] R[X])
                (g.comp
                  (AlgHom.toRingHom (TensorProduct.map (AlgHom.id R R') (aeval x) : R' ⊗[R] R[X] →ₐ[R] R' ⊗[R] S)))
                (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (polyEquivTensor R R')))).comp
            C :
          (a : R') → S')
        x_1 :
      S')

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')
⊢ Eq.{u_7 + 1} (α := S')
    (((AlgHom.toRingHom (R := R') (aeval ((f : (a : S) → S') x)) : RingHom.{u_6, u_7} R'[X] S') : (a : R'[X]) → S') X :
      S')
    ((RingHom.comp (β := R' ⊗[R] R[X])
            (g.comp (AlgHom.toRingHom (TensorProduct.map (AlgHom.id R R') (aeval x) : R' ⊗[R] R[X] →ₐ[R] R' ⊗[R] S)))
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (polyEquivTensor R R'))) :
          (a : R'[X]) → S')
        X :
      S')

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')
⊢ RingHom.Finite.{u_6, u_7} (A := R'[X]) (B := S') (AlgHom.toRingHom (R := R') (aeval ((f : (a : S) → S') x)))

Tactic:
have H₂ : (aeval (R := R') (f x)).toRingHom.Finite := by
    convert!
      ((RingHom.Finite.of_surjective g.toRingHom hf₁).comp
            (RingHom.Finite.tensorProductMap (f := AlgHom.id R R') (RingEquiv.refl _).finite
              hx')).comp
        (polyEquivTensor R R').toRingEquiv.finite using 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 : 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)))
obtain :
  ∀ (Q : Ideal S') (isPrime : Q.IsPrime)
    (hQ :
      PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S' } =
        { asIdeal := P, isPrime := inst_27 }),
    False
⊢ False

Tactic:
obtain ⟨⟨Q, _⟩, hQ⟩ := hf₄.comap_surjective hf₃ ⟨P, ‹_›⟩

Premises used: PrimeSpectrum.mk, RingHom.IsIntegral.comap_surjective