awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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')
⊢ False
have hf₄ : f.IsIntegral
Tactic: have hf₄ : f.IsIntegral := by
    have : f = (g.restrictScalars R).comp ((Algebra.TensorProduct.comm _ _ _).toAlgHom.comp
        (IsScalarTower.toAlgHom _ _ _)) := by ext; simp [g]
    simp only [this, AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom, ← RingHom.comp_assoc]
    refine .trans _ _ (algebraMap_isIntegral_iff.mpr inferInstance) ?_
    exact RingHom.isIntegral_of_surjective _
      (hf₁.comp (Algebra.TensorProduct.comm _ _ _).surjective)
-- 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
⊢ IsStronglyTranscendental.{u_6, u_7} R' (S := S') ((f : (a : S) → S') x : S')
have refine : IsStronglyTranscendental.{u_6, u_5} R' (S := L)
  ((IsScalarTower.toAlgHom R' S' L : (a : S') → L) ((f : (a : S) → S') x : S') : L)
Tactic: refine .of_map (f := IsScalarTower.toAlgHom R' S' L) (FaithfulSMul.algebraMap_injective S' L) ?_
-- 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
⊢ IsStronglyTranscendental.{u_6, u_5} R' (S := L)
    ((IsScalarTower.toAlgHom R' S' L : (a : S') → L) ((f : (a : S) → S') x : S') : L)
have dsimp : IsStronglyTranscendental.{u_6, u_5} R' (S := L) ((algebraMap S' L : (a : S') → L) ((f : (a : S) → S') x : S') : L)
Tactic: dsimp
-- 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
⊢ IsStronglyTranscendental.{u_6, u_5} R' (S := L) ((algebraMap S' L : (a : S') → L) ((f : (a : S) → S') x : S') : L)
have rw : IsStronglyTranscendental.{u_6, u_5} R' (S := L) ((algebraMap S L : (a : S) → L) x : L)
Tactic: rw [show algebraMap S' L (f x) = algebraMap _ _ x from congr($hf₂ x)]
-- 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
⊢ False
have H₁ : 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)
-- 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')
⊢ RingHom.Finite.{u_6, u_7} (A := R'[X]) (B := S') (AlgHom.toRingHom (R := R') (aeval ((f : (a : S) → S') x)))
have 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')))
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
-- 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')
⊢ 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')))
have 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')
Tactic: ext
-- 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 :
  ∀ (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')
⊢ 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')))
have 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')
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')
⊢ False
have H₂ : 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]
-- 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)))
⊢ False
have obtain : ∀ (Q : Ideal S') (isPrime : Q.IsPrime)
  (hQ :
    PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S' } =
      { asIdeal := P, isPrime := inst_27 }),
  False
Tactic: obtain ⟨⟨Q, _⟩, hQ⟩ := hf₄.comap_surjective hf₃ ⟨P, ‹_›⟩