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')
⊢ f =
    AlgHom.comp (AlgHom.restrictScalars R g)
      (AlgHom.comp (↑(TensorProduct.comm R S R') : S ⊗[R] R' →ₐ[R] R' ⊗[R] S) (IsScalarTower.toAlgHom R S (S ⊗[R] R')))

Tactic:
have : f = (g.restrictScalars R).comp ((Algebra.TensorProduct.comm _ _ _).toAlgHom.comp
        (IsScalarTower.toAlgHom _ _ _)) := by 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')
this :
  f =
    AlgHom.comp (AlgHom.restrictScalars R g)
      (AlgHom.comp (↑(TensorProduct.comm R S R') : S ⊗[R] R' →ₐ[R] R' ⊗[R] S) (IsScalarTower.toAlgHom R S (S ⊗[R] R')))
simp :
  RingHom.IsIntegral
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(AlgHom.restrictScalars R g) : R' ⊗[R] S →+* S')
        (↑(↑(TensorProduct.comm R S R') : S ⊗[R] R' →ₐ[R] R' ⊗[R] S) : S ⊗[R] R' →+* R' ⊗[R] S))
      (↑(IsScalarTower.toAlgHom R S (S ⊗[R] R')) : S →+* S ⊗[R] R'))
⊢ f.IsIntegral

Tactic:
simp only [this, AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom, ← RingHom.comp_assoc]

Premises used: AlgHom.comp_toRingHom, RingHom.comp_assoc, AlgHom.toRingHom_eq_coe
-- 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')
this :
  f =
    AlgHom.comp (AlgHom.restrictScalars R g)
      (AlgHom.comp (↑(TensorProduct.comm R S R') : S ⊗[R] R' →ₐ[R] R' ⊗[R] S) (IsScalarTower.toAlgHom R S (S ⊗[R] R')))
⊢ RingHom.IsIntegral
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(AlgHom.restrictScalars R g) : R' ⊗[R] S →+* S')
        (↑(↑(TensorProduct.comm R S R') : S ⊗[R] R' →ₐ[R] R' ⊗[R] S) : S ⊗[R] R' →+* R' ⊗[R] S))
      (↑(IsScalarTower.toAlgHom R S (S ⊗[R] R')) : S →+* S ⊗[R] R'))

Tactic:
.trans _ _ (algebraMap_isIntegral_iff.mpr inferInstance) ?_

Premises used: Iff.mpr, algebraMap_isIntegral_iff, inferInstance, RingHom.IsIntegral.trans
-- 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')
this :
  f =
    AlgHom.comp (AlgHom.restrictScalars R g)
      (AlgHom.comp (↑(TensorProduct.comm R S R') : S ⊗[R] R' →ₐ[R] R' ⊗[R] S) (IsScalarTower.toAlgHom R S (S ⊗[R] R')))
refine :
  RingHom.IsIntegral
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(AlgHom.restrictScalars R g) : R' ⊗[R] S →+* S')
      (↑(↑(TensorProduct.comm R S R') : S ⊗[R] R' →ₐ[R] R' ⊗[R] S) : S ⊗[R] R' →+* R' ⊗[R] S))
⊢ RingHom.IsIntegral
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(AlgHom.restrictScalars R g) : R' ⊗[R] S →+* S')
        (↑(↑(TensorProduct.comm R S R') : S ⊗[R] R' →ₐ[R] R' ⊗[R] S) : S ⊗[R] R' →+* R' ⊗[R] S))
      (↑(IsScalarTower.toAlgHom R S (S ⊗[R] R')) : S →+* S ⊗[R] R'))

Tactic:
refine .trans _ _ (algebraMap_isIntegral_iff.mpr inferInstance) ?_
-- 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')
this :
  f =
    AlgHom.comp (AlgHom.restrictScalars R g)
      (AlgHom.comp (↑(TensorProduct.comm R S R') : S ⊗[R] R' →ₐ[R] R' ⊗[R] S) (IsScalarTower.toAlgHom R S (S ⊗[R] R')))
⊢ RingHom.IsIntegral
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(AlgHom.restrictScalars R g) : R' ⊗[R] S →+* S')
      (↑(↑(TensorProduct.comm R S R') : S ⊗[R] R' →ₐ[R] R' ⊗[R] S) : S ⊗[R] R' →+* R' ⊗[R] S))

Tactic:
RingHom.isIntegral_of_surjective _
      (hf₁.comp (Algebra.TensorProduct.comm _ _ _).surjective)

Premises used: Algebra.TensorProduct.comm, RingHom.isIntegral_of_surjective, Function.Surjective.comp, AlgEquiv.surjective
-- 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')
this :
  f =
    AlgHom.comp (AlgHom.restrictScalars R g)
      (AlgHom.comp (↑(TensorProduct.comm R S R') : S ⊗[R] R' →ₐ[R] R' ⊗[R] S) (IsScalarTower.toAlgHom R S (S ⊗[R] R')))
⊢ RingHom.IsIntegral
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(AlgHom.restrictScalars R g) : R' ⊗[R] S →+* S')
      (↑(↑(TensorProduct.comm R S R') : S ⊗[R] R' →ₐ[R] R' ⊗[R] S) : S ⊗[R] R' →+* R' ⊗[R] S))

Tactic:
exact RingHom.isIntegral_of_surjective _
      (hf₁.comp (Algebra.TensorProduct.comm _ _ _).surjective)

Premises used: RingHom.isIntegral_of_surjective, Function.Surjective.comp
-- 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')
⊢ 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)
-- 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:
.of_map (f := IsScalarTower.toAlgHom R' S' L) (FaithfulSMul.algebraMap_injective S' L) ?_

Premises used: IsStronglyTranscendental.of_map, FaithfulSMul.algebraMap_injective
-- 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
refine :
  IsStronglyTranscendental.{u_6, u_5} R' (S := L)
    ((IsScalarTower.toAlgHom R' S' L : (a : S') → L) ((f : (a : S) → S') x : S') : L)
⊢ IsStronglyTranscendental.{u_6, u_7} R' (S := S') ((f : (a : S) → S') x : S')

Tactic:
refine .of_map (f := IsScalarTower.toAlgHom R' S' L) (FaithfulSMul.algebraMap_injective S' L) ?_
-- 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
dsimp :
  IsStronglyTranscendental.{u_6, u_5} R' (S := L) ((algebraMap S' L : (a : S') → L) ((f : (a : S) → S') x : S') : L)
⊢ IsStronglyTranscendental.{u_6, u_5} R' (S := L)
    ((IsScalarTower.toAlgHom R' S' L : (a : S') → L) ((f : (a : S) → S') x : S') : L)

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

Tactic:
rw [show algebraMap S' L (f x) = algebraMap _ _ x from congr($hf₂ x)]

Premises used: congrArg, id, DFunLike.coe