awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
p : Ideal T
inst_7 : p.IsPrime
s : S
hsp : s ∉ Ideal.under S p
hs : IsIntegral R s
Hs : ∀ (x : S), ∃ (m : ℕ), IsIntegral R (s ^ m * x)
t : S
htp : t ∉ Ideal.under S p
Ht :
  Eq.{u_3 + 1} (α := Subalgebra S T)
    (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) t)) ⋯ : Subalgebra S T)
    (⊤ : Subalgebra S T)
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha : (algebraMap S T : (a : S) → T) a = HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) n * x
k : ℕ
hk : IsIntegral R (s ^ k * a)
⊢ HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) (k + n) * x =
    (algebraMap S T : (a : S) → T) (s ^ ((m + 1) * n) * (s ^ m * t) ^ k * (s ^ k * a))
have h : HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) m ^ k *
          HPow.hPow (α := T) (β := ℕ) ((algebraMap S T : (a : S) → T) s : T) 1 ^ k *
        HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) k *
      (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) m ^ n *
          HPow.hPow (α := T) (β := ℕ) ((algebraMap S T : (a : S) → T) s : T) 1 ^ n *
        HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) n) *
    x =
  HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) ((m + 1) * n) *
      (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) m ^ k *
        HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) k) *
    (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) k *
      (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) n * x))
Tactic: simp only [map_pow, map_mul, ha, pow_add, mul_pow]
-- 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
φ : 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
⊢ HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
have rw : HMul.hMul (α := St) ((algebraMap S St : (a : S) → St) t : St) t' = 1
Tactic: rw [mul_comm, IsLocalization.Away.mul_invSelf]
-- 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
φ : 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
rw : HMul.hMul (α := St) ((algebraMap S St : (a : S) → St) t : St) t' = 1
⊢ HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
have rw₁ : Eq.{u_2 + 1} (α := St) 1 1
Tactic: rw [mul_comm, IsLocalization.Away.mul_invSelf]
-- 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
φ : 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
⊢ IsIntegral R t
have ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
Tactic: have ht't : t' * algebraMap S St t = 1 := by rw [mul_comm, IsLocalization.Away.mul_invSelf]
-- 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
φ : 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 : Algebra (↥R₁) St := R₁.toAlgebra
⊢ IsIntegral R t
have this₁ : IsScalarTower (↥R₁) (↥R₂) St
Tactic: haveI : IsScalarTower R₁ R₂ St := Subalgebra.isScalarTower_mid _
-- 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
φ : 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₂
have inl : Subsingleton.{u_2 + 1} ↥R₁ → Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
Tactic: cases subsingleton_or_nontrivial R₁
-- 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
φ : 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
inl : Subsingleton.{u_2 + 1} ↥R₁ → Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
⊢ Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
have inr : Nontrivial.{u_2} ↥R₁ → Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
Tactic: cases subsingleton_or_nontrivial R₁
-- 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
φ : 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 : Subsingleton.{u_2 + 1} ↥R₁
⊢ Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
have this₁ : Subsingleton.{u_2 + 1} ↥R₂
Tactic: have := (algebraMap R₁ R₂).codomain_trivial
-- 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
φ : 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₁
⊢ Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
have inr : IsIntegral ↥R₁ (A := St) ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)
Tactic: rw [← le_integralClosure_iff_isIntegral, Algebra.adjoin_le_iff, Set.singleton_subset_iff,
      SetLike.mem_coe, mem_integralClosure_iff]
-- 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
φ : 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₁
⊢ IsIntegral ↥R₁ (A := St) ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)
have inr : (HMul.hMul (α := (↥R₁)[X]) (β := (↥R₁)[X])
      ((C : (a : ↥R₁) → (↥R₁)[X]) (Subtype.mk (p := fun (x : St) ↦ x ∈ R₁) t' sorry) : (↥R₁)[X])
      (map (algebraMap R ↥R₁) r)).natDegree <
  natDegree.{u_2} (R := ↥R₁) (map (algebraMap R ↥R₁) p)
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 ?_), ?_⟩
-- 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
φ : 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)
⊢ IsIntegral ↥R₁ (A := St) ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)
have 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' sorry) : (↥R₁)[X])
        (map (algebraMap R ↥R₁) r)) =
  0
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 ?_), ?_⟩
-- 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
φ : 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
⊢ IsIntegral R t
have this₁ : 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]
-- 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
φ : 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)
have refine : IsIntegral ↥R₂ (A := St) ((algebraMap S St : (a : S) → St) t : St)
Tactic: refine isIntegral_trans (A := R₂) (algebraMap S St t) ?_
-- 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
φ : 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)
have 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)
Tactic: obtain ⟨q, hq, hq'⟩ := ht
Cleared hypotheses: ht
-- 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
φ : 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)
have 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)) sorry)))
        q :
      (↥R₂)[X]) =
  0
Tactic: refine ⟨q.map (aeval ⟨_, Algebra.self_mem_adjoin_singleton _ _⟩).toRingHom, hq.map _, ?_⟩
-- 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
φ : 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
⊢ 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
have 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)) sorry) :
            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: rw [AlgHom.toRingHom_eq_coe, eval₂_map, ← map_zero (algebraMap S St), ← hq',
      hom_eval₂]
-- 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
φ : 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
⊢ 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
have 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)) sorry) :
          AlgHom.{u_1, u_1, u_2} R R[X] ↥R₂) :
      R[X] →+* ↥R₂) =
  RingHom.comp (algebraMap S St) φ.toRingHom
Tactic: congr 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
φ : 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
⊢ @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
have 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)) sorry) :
                      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: 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
φ : 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)
⊢ @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
have 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))
                      sorry) :
                  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: ext