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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
h : Nontrivial.{u_2} ↥R₁
inr :
  (HMul.hMul (α := (↥R₁)[X]) (β := (↥R₁)[X])
        ((C : (a : ↥R₁) → (↥R₁)[X]) (Subtype.mk (p := fun (x : St) ↦ x ∈ R₁) t' ⋯) : (↥R₁)[X])
        (map (algebraMap R ↥R₁) r)).natDegree <
    natDegree.{u_2} (R := ↥R₁) (map (algebraMap R ↥R₁) p)
inr₁ :
  eval₂ (algebraMap (↥R₁) St) ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X))
      (map (algebraMap R ↥R₁) p -
        HMul.hMul (α := (↥R₁)[X]) (β := (↥R₁)[X])
          ((C : (a : ↥R₁) → (↥R₁)[X]) (Subtype.mk (p := fun (x : St) ↦ x ∈ R₁) t' ⋯) : (↥R₁)[X])
          (map (algebraMap R ↥R₁) r)) =
    0
⊢ IsIntegral ↥R₁ (A := St) ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)

Tactic:
refine ⟨p.map (algebraMap R R₁) - C ⟨t', Algebra.self_mem_adjoin_singleton R t'⟩ *
        r.map (algebraMap R R₁), (hpm.map _).sub_of_left (degree_lt_degree ?_), ?_⟩
-- 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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
h : Nontrivial.{u_2} ↥R₁
inr : r.natDegree < p.natDegree
⊢ (HMul.hMul (α := (↥R₁)[X]) (β := (↥R₁)[X])
        ((C : (a : ↥R₁) → (↥R₁)[X]) (Subtype.mk (p := fun (x : St) ↦ x ∈ R₁) t' ⋯) : (↥R₁)[X])
        (map (algebraMap R ↥R₁) r)).natDegree <
    natDegree.{u_2} (R := ↥R₁) (map (algebraMap R ↥R₁) p)

Tactic:
grw [natDegree_C_mul_le, natDegree_map_le, hpm.natDegree_map]

Premises used: Polynomial.natDegree_C_mul_le, Polynomial.Monic.natDegree_map, Polynomial.natDegree_map_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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
h : Nontrivial.{u_2} ↥R₁
⊢ r.natDegree < p.natDegree

Tactic:
assumption
-- 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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
h : Nontrivial.{u_2} ↥R₁
⊢ eval₂ (algebraMap (↥R₁) St) ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X))
      (map (algebraMap R ↥R₁) p -
        HMul.hMul (α := (↥R₁)[X]) (β := (↥R₁)[X])
          ((C : (a : ↥R₁) → (↥R₁)[X]) (Subtype.mk (p := fun (x : St) ↦ x ∈ R₁) t' ⋯) : (↥R₁)[X])
          (map (algebraMap R ↥R₁) r)) =
    0

Tactic:
simp [← aeval_def, aeval_algebraMap_apply, aeval_algHom_apply,
        ← hp, ← mul_assoc, ht't, mul_right_comm]

Premises used: mul_assoc, Polynomial.aeval_def, mul_right_comm, Polynomial.aeval_algHom_apply, Polynomial.aeval_algebraMap_apply
-- 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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
⊢ Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂

Tactic:
have : Algebra.IsIntegral R₁ R₂ := by
    cases subsingleton_or_nontrivial R₁
    · have := (algebraMap R₁ R₂).codomain_trivial; exact ⟨(Subsingleton.elim · 0 ▸ isIntegral_zero)⟩
    rw [← le_integralClosure_iff_isIntegral, Algebra.adjoin_le_iff, Set.singleton_subset_iff,
      SetLike.mem_coe, mem_integralClosure_iff]
    refine ⟨p.map (algebraMap R R₁) - C ⟨t', Algebra.self_mem_adjoin_singleton R t'⟩ *
        r.map (algebraMap R R₁), (hpm.map _).sub_of_left (degree_lt_degree ?_), ?_⟩
    · grw [natDegree_C_mul_le, natDegree_map_le, hpm.natDegree_map]; assumption
    · simp [← aeval_def, aeval_algebraMap_apply, aeval_algHom_apply,
        ← hp, ← mul_assoc, ht't, mul_right_comm]
-- 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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this_4 : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
⊢ IsIntegral ↥R₁ (A := St) ((algebraMap S St : (a : S) → St) t : St)

Tactic:
isIntegral_trans (A := R₂) (algebraMap S St t) ?_

Premises used: Algebra.algebraMap, isIntegral_trans, DFunLike.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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this_4 : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
refine : IsIntegral ↥R₂ (A := St) ((algebraMap S St : (a : S) → St) t : St)
⊢ IsIntegral ↥R₁ (A := St) ((algebraMap S St : (a : S) → St) t : St)

Tactic:
refine isIntegral_trans (A := R₂) (algebraMap S St t) ?_

Premises used: Algebra.algebraMap, isIntegral_trans, DFunLike.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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this_4 : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
obtain :
  ∀ (q : R[X][X]) (hq : q.Monic) (hq' : eval₂ φ.toRingHom t q = 0),
    IsIntegral ↥R₂ (A := St) ((algebraMap S St : (a : S) → St) t : St)
⊢ IsIntegral ↥R₂ (A := St) ((algebraMap S St : (a : S) → St) t : St)

Tactic:
obtain ⟨q, hq, hq'⟩ := ht
-- 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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this_4 : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
q : R[X][X]
hq : q.Monic
hq' : eval₂ φ.toRingHom t q = 0
⊢ IsIntegral ↥R₂ (A := St) ((algebraMap S St : (a : S) → St) t : St)

Tactic:
⟨q.map (aeval ⟨_, Algebra.self_mem_adjoin_singleton _ _⟩).toRingHom, hq.map _, ?_⟩

Premises used: RingHom.IsIntegralElem, IsIntegral, AlgHom.toRingHom, And.intro, Exists.intro, Polynomial.map, Polynomial.aeval, Polynomial.Monic.map
-- 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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this_4 : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
q : R[X][X]
hq : q.Monic
hq' : eval₂ φ.toRingHom t q = 0
refine :
  eval₂ (R := ↥R₂) (algebraMap (↥R₂) St : ↥R₂ →+* St) ((algebraMap S St : (a : S) → St) t)
      (map
          (AlgHom.toRingHom (R := R)
            (aeval
              (Subtype.mk (p := fun (x : St) ↦ x ∈ R₂) ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X)) ⋯)))
          q :
        (↥R₂)[X]) =
    0
⊢ IsIntegral ↥R₂ (A := St) ((algebraMap S St : (a : S) → St) t : St)

Tactic:
refine ⟨q.map (aeval ⟨_, Algebra.self_mem_adjoin_singleton _ _⟩).toRingHom, hq.map _, ?_⟩
-- 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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this_4 : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
q : R[X][X]
hq : q.Monic
hq' : eval₂ φ.toRingHom t q = 0
rw :
  eval₂
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R₂) St)
        (↑(aeval
                (Subtype.mk (p := fun (x : St) ↦ x ∈ R₂) ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X))
                  ⋯) :
              AlgHom.{u_1, u_1, u_2} R R[X] ↥R₂) :
          R[X] →+* ↥R₂))
      ((algebraMap S St : (a : S) → St) t) q =
    eval₂ (RingHom.comp (algebraMap S St) φ.toRingHom) ((algebraMap S St : (a : S) → St) t) q
⊢ eval₂ (R := ↥R₂) (algebraMap (↥R₂) St : ↥R₂ →+* St) ((algebraMap S St : (a : S) → St) t)
      (map
          (AlgHom.toRingHom (R := R)
            (aeval
              (Subtype.mk (p := fun (x : St) ↦ x ∈ R₂) ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X)) ⋯)))
          q :
        (↥R₂)[X]) =
    0

Tactic:
rw [AlgHom.toRingHom_eq_coe, eval₂_map, ← map_zero (algebraMap S St), ← hq',
      hom_eval₂]

Premises used: Algebra.algebraMap, Polynomial.hom_eval₂, map_zero, Polynomial.eval₂_map, 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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this_4 : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
q : R[X][X]
hq : q.Monic
hq' : eval₂ φ.toRingHom t q = 0
e_f :
  @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R₂) St)
      (↑(aeval (Subtype.mk (p := fun (x : St) ↦ x ∈ R₂) ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X)) ⋯) :
            AlgHom.{u_1, u_1, u_2} R R[X] ↥R₂) :
        R[X] →+* ↥R₂) =
    RingHom.comp (algebraMap S St) φ.toRingHom
⊢ eval₂
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R₂) St)
        (↑(aeval
                (Subtype.mk (p := fun (x : St) ↦ x ∈ R₂) ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X))
                  ⋯) :
              AlgHom.{u_1, u_1, u_2} R R[X] ↥R₂) :
          R[X] →+* ↥R₂))
      ((algebraMap S St : (a : S) → St) t) q =
    eval₂ (RingHom.comp (algebraMap S St) φ.toRingHom) ((algebraMap S St : (a : S) → St) t) q

Tactic:
congr 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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this_4 : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
q : R[X][X]
hq : q.Monic
hq' : eval₂ φ.toRingHom t q = 0
e_f :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := St)
      (((RingHom.comp
                (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R₂) St)
                  (↑(aeval
                          (Subtype.mk (p := fun (x : St) ↦ x ∈ R₂)
                            ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X)) ⋯) :
                        AlgHom.{u_1, u_1, u_2} R R[X] ↥R₂) :
                    R[X] →+* ↥R₂))
                C :
              R →+* St) :
            (a : R) → St)
          x :
        St)
      (((RingHom.comp (RingHom.comp (algebraMap S St) φ.toRingHom) C : R →+* St) : (a : R) → St) x : St)
e_f₁ :
  Eq.{u_2 + 1} (α := St)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R₂) St)
              (↑(aeval
                      (Subtype.mk (p := fun (x : St) ↦ x ∈ R₂)
                        ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X)) ⋯) :
                    AlgHom.{u_1, u_1, u_2} R R[X] ↥R₂) :
                R[X] →+* ↥R₂) :
            RingHom.{u_1, u_2} R[X] St) :
          (a : R[X]) → St)
        X :
      St)
    (((RingHom.comp (algebraMap S St) φ.toRingHom : RingHom.{u_1, u_2} R[X] St) : (a : R[X]) → St) X : St)
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R₂) St)
      (↑(aeval (Subtype.mk (p := fun (x : St) ↦ x ∈ R₂) ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X)) ⋯) :
            AlgHom.{u_1, u_1, u_2} R R[X] ↥R₂) :
        R[X] →+* ↥R₂) =
    RingHom.comp (algebraMap S St) φ.toRingHom

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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this_4 : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
q : R[X][X]
hq : q.Monic
hq' : eval₂ φ.toRingHom t q = 0
x : R
⊢ Eq.{u_2 + 1} (α := St)
    (((RingHom.comp
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R₂) St)
                (↑(aeval
                        (Subtype.mk (p := fun (x : St) ↦ x ∈ R₂)
                          ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X)) ⋯) :
                      AlgHom.{u_1, u_1, u_2} R R[X] ↥R₂) :
                  R[X] →+* ↥R₂))
              C :
            R →+* St) :
          (a : R) → St)
        x :
      St)
    (((RingHom.comp (RingHom.comp (algebraMap S St) φ.toRingHom) C : R →+* St) : (a : R) → St) x : St)

Tactic:
simp [-Polynomial.algebraMap_apply, ← algebraMap_eq, ← IsScalarTower.algebraMap_apply]

Premises used: Polynomial.algebraMap_apply, IsScalarTower.algebraMap_apply, Polynomial.algebraMap_eq
-- 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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this_4 : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
q : R[X][X]
hq : q.Monic
hq' : eval₂ φ.toRingHom t q = 0
⊢ Eq.{u_2 + 1} (α := St)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R₂) St)
              (↑(aeval
                      (Subtype.mk (p := fun (x : St) ↦ x ∈ R₂)
                        ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X)) ⋯) :
                    AlgHom.{u_1, u_1, u_2} R R[X] ↥R₂) :
                R[X] →+* ↥R₂) :
            RingHom.{u_1, u_2} R[X] St) :
          (a : R[X]) → St)
        X :
      St)
    (((RingHom.comp (algebraMap S St) φ.toRingHom : RingHom.{u_1, u_2} R[X] St) : (a : R[X]) → St) X : St)

Tactic:
simp [-Polynomial.algebraMap_apply, ← algebraMap_eq, ← IsScalarTower.algebraMap_apply]

Premises used: Polynomial.algebraMap_apply, IsScalarTower.algebraMap_apply, Polynomial.algebraMap_eq
-- 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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this_4 : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
⊢ IsIntegral ↥R₁ (A := St) ((algebraMap S St : (a : S) → St) t : St)

Tactic:
have : IsIntegral R₁ (algebraMap S St t) := by
    refine isIntegral_trans (A := R₂) (algebraMap S St t) ?_
    obtain ⟨q, hq, hq'⟩ := ht
    refine ⟨q.map (aeval ⟨_, Algebra.self_mem_adjoin_singleton _ _⟩).toRingHom, hq.map _, ?_⟩
    rw [AlgHom.toRingHom_eq_coe, eval₂_map, ← map_zero (algebraMap S St), ← hq',
      hom_eval₂]
    congr 1
    ext <;> simp [-Polynomial.algebraMap_apply, ← algebraMap_eq, ← IsScalarTower.algebraMap_apply]
-- 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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this_4 : IsScalarTower (↥R₁) (↥R₂) St
this_5 : Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
this : IsIntegral ↥R₁ (A := St) ((algebraMap S St : (a : S) → St) t : St)
⊢ IsIntegral R t

Tactic:
simpa using IsLocalization.Away.isIntegral_of_isIntegral_map t
    (isIntegral_of_isIntegral_adjoin_of_mul_eq_one _ _ ht't this)

Premises used: IsLocalization.Away.isIntegral_of_isIntegral_map, isIntegral_of_isIntegral_adjoin_of_mul_eq_one