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
φ : 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 t
have this₁ : 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]
-- 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[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
⊢ ∃ (q : R[X]), IsIntegral R (HSub.hSub (β := S) t ((φ : (a : R[X]) → S) q : S))
have obtain : ∀ (r : R[X]) (hr : (φ : (a : R[X]) → S) r = HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t),
  ∃ (q : R[X]), IsIntegral R (HSub.hSub (β := S) t ((φ : (a : R[X]) → S) q : S))
Tactic: obtain ⟨r, hr : φ r = _⟩ := hp
Cleared hypotheses: hp
-- 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[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
r : R[X]
hr : (φ : (a : R[X]) → S) r = HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t
⊢ ∃ (q : R[X]), IsIntegral R (HSub.hSub (β := S) t ((φ : (a : R[X]) → S) q : S))
have inl : ∀ (hpm : Monic.{u_1} (R := R) 1) (hr : (φ : (a : R[X]) → S) r = HMul.hMul (α := S) ((φ : (a : R[X]) → S) 1 : S) t),
  ∃ (q : R[X]), IsIntegral R (HSub.hSub (β := S) t ((φ : (a : R[X]) → S) q : S))
Tactic: obtain rfl | hp1 := eq_or_ne p 1
Cleared hypotheses: p, hpm, hr
-- 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[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
r : R[X]
hr : (φ : (a : R[X]) → S) r = HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t
inl :
  ∀ (hpm : Monic.{u_1} (R := R) 1) (hr : (φ : (a : R[X]) → S) r = HMul.hMul (α := S) ((φ : (a : R[X]) → S) 1 : S) t),
    ∃ (q : R[X]), IsIntegral R (HSub.hSub (β := S) t ((φ : (a : R[X]) → S) q : S))
⊢ ∃ (q : R[X]), IsIntegral R (HSub.hSub (β := S) t ((φ : (a : R[X]) → S) q : S))
have inr : ∀ (hp1 : p ≠ 1), ∃ (q : R[X]), IsIntegral R (HSub.hSub (β := S) t ((φ : (a : R[X]) → S) q : S))
Tactic: obtain rfl | hp1 := eq_or_ne p 1
-- 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[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
⊢ ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))
have this₁ : IsScalarTower R R' S'
Tactic: have : IsScalarTower R R' S' := .of_algebraMap_eq (by
    simp +zetaDelta [RingHom.algebraMap_toAlgebra, IsLocalization.Away.map, ← algebraMap_apply R S])
-- 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[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
⊢ ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))
have ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
Tactic: have ha : IsUnit (algebraMap R R' a) := IsLocalization.Away.algebraMap_isUnit a
-- 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[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
⊢ Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
have h₁ : ∀ (x : R),
  Eq.{u_2 + 1} (α := S')
    (((RingHom.comp
              (RingHom.comp
                (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
                (mapRingHom (algebraMap R R')))
              C :
            R →+* S') :
          (a : R) → S')
        x :
      S')
    (((RingHom.comp (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S)) C :
            R →+* S') :
          (a : R) → S')
        x :
      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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
h₁ :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S')
      (((RingHom.comp
                (RingHom.comp
                  (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
                  (mapRingHom (algebraMap R R')))
                C :
              R →+* S') :
            (a : R) → S')
          x :
        S')
      (((RingHom.comp (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S)) C :
              R →+* S') :
            (a : R) → S')
          x :
        S')
⊢ Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
have h₂ : Eq.{u_2 + 1} (α := S')
  (((RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
            (mapRingHom (algebraMap R R')) :
          RingHom.{u_1, u_2} R[X] S') :
        (a : R[X]) → S')
      X :
    S')
  (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
          RingHom.{u_1, u_2} R[X] S') :
        (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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
⊢ ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))
have H : Eq (α := RingHom.{u_1, u_2} R[X] S')
  (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
      (mapRingHom (algebraMap R R')) :
    RingHom.{u_1, u_2} R[X] S')
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) : RingHom.{u_1, u_2} R[X] S')
Tactic: have H : (aeval ((algebraMap S S') (φ X))).toRingHom.comp (mapRingHom (algebraMap R R')) =
    (algebraMap S S').comp φ := by ext <;>
      simp [-Polynomial.algebraMap_apply, ← Polynomial.algebraMap_eq, ← algebraMap_apply]
-- 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[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
⊢ RingHom.IsIntegralElem.{u_1, u_2} (R := R'[X]) (A := S')
    (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))) :
      RingHom.{u_1, u_2} R'[X] S')
    ((algebraMap S S' : (a : S) → S') t : S')
have obtain : ∀ (q : R[X][X]) (hqm : q.Monic) (hq : eval₂ φ.toRingHom t q = 0),
  RingHom.IsIntegralElem.{u_1, u_2} (R := R'[X]) (A := S')
    (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))) :
      RingHom.{u_1, u_2} R'[X] S')
    ((algebraMap S S' : (a : S) → S') t : S')
Tactic: obtain ⟨q, hqm, 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[X]
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R[X][X]
hqm : q.Monic
hq : eval₂ φ.toRingHom t q = 0
⊢ RingHom.IsIntegralElem.{u_1, u_2} (R := R'[X]) (A := S')
    (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))) :
      RingHom.{u_1, u_2} R'[X] S')
    ((algebraMap S S' : (a : S) → S') t : S')
have refine : Eq (α := S')
  (eval₂ (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
      ((algebraMap S S' : (a : S) → S') t) (map (mapRingHom (algebraMap R R')) q) :
    S')
  (0 : S')
Tactic: refine ⟨q.map (mapRingHom (algebraMap _ _)), hqm.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[X]
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R[X][X]
hqm : q.Monic
hq : eval₂ φ.toRingHom t q = 0
⊢ Eq (α := S')
    (eval₂ (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        ((algebraMap S S' : (a : S) → S') t) (map (mapRingHom (algebraMap R R')) q) :
      S')
    (0 : S')
have rw : Eq (α := S')
  (eval₂
      (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')))
      ((algebraMap S S' : (a : S) → S') t) q :
    S')
  (0 : S')
Tactic: rw [eval₂_map, H, ← hom_eval₂, ← AlgHom.toRingHom_eq_coe, hq, map_zero]
-- 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[X]
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R[X][X]
hqm : q.Monic
hq : eval₂ φ.toRingHom t q = 0
rw :
  Eq (α := S')
    (eval₂
        (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
          (mapRingHom (algebraMap R R')))
        ((algebraMap S S' : (a : S) → S') t) q :
      S')
    (0 : S')
⊢ Eq (α := S')
    (eval₂ (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        ((algebraMap S S' : (a : S) → S') t) (map (mapRingHom (algebraMap R R')) q) :
      S')
    (0 : S')
have rw₁ : eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S))
    ((algebraMap S S' : (a : S) → S') t) q =
  0
Tactic: rw [eval₂_map, H, ← hom_eval₂, ← AlgHom.toRingHom_eq_coe, hq, map_zero]
-- 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[X]
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R[X][X]
hqm : q.Monic
hq : eval₂ φ.toRingHom t q = 0
rw :
  Eq (α := S')
    (eval₂
        (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
          (mapRingHom (algebraMap R R')))
        ((algebraMap S S' : (a : S) → S') t) q :
      S')
    (0 : S')
rw₁ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S))
      ((algebraMap S S' : (a : S) → S') t) q =
    0
⊢ Eq (α := S')
    (eval₂ (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        ((algebraMap S S' : (a : S) → S') t) (map (mapRingHom (algebraMap R R')) q) :
      S')
    (0 : S')
have rw₂ : Eq (α := S') ((algebraMap S S' : (a : S) → S') (eval₂ (↑φ : R[X] →+* S) t q) : S') (0 : S')
Tactic: rw [eval₂_map, H, ← hom_eval₂, ← AlgHom.toRingHom_eq_coe, hq, map_zero]
-- 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[X]
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R[X][X]
hqm : q.Monic
hq : eval₂ φ.toRingHom t q = 0
rw :
  Eq (α := S')
    (eval₂
        (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
          (mapRingHom (algebraMap R R')))
        ((algebraMap S S' : (a : S) → S') t) q :
      S')
    (0 : S')
rw₁ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S))
      ((algebraMap S S' : (a : S) → S') t) q =
    0
rw₂ : Eq (α := S') ((algebraMap S S' : (a : S) → S') (eval₂ (↑φ : R[X] →+* S) t q) : S') (0 : S')
⊢ Eq (α := S')
    (eval₂ (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        ((algebraMap S S' : (a : S) → S') t) (map (mapRingHom (algebraMap R R')) q) :
      S')
    (0 : S')
have rw₃ : Eq (α := S') ((algebraMap S S' : (a : S) → S') (eval₂ φ.toRingHom t q) : S') (0 : S')
Tactic: rw [eval₂_map, H, ← hom_eval₂, ← AlgHom.toRingHom_eq_coe, hq, map_zero]
-- 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[X]
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R[X][X]
hqm : q.Monic
hq : eval₂ φ.toRingHom t q = 0
rw :
  Eq (α := S')
    (eval₂
        (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
          (mapRingHom (algebraMap R R')))
        ((algebraMap S S' : (a : S) → S') t) q :
      S')
    (0 : S')
rw₁ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S))
      ((algebraMap S S' : (a : S) → S') t) q =
    0
rw₂ : Eq (α := S') ((algebraMap S S' : (a : S) → S') (eval₂ (↑φ : R[X] →+* S) t q) : S') (0 : S')
rw₃ : Eq (α := S') ((algebraMap S S' : (a : S) → S') (eval₂ φ.toRingHom t q) : S') (0 : S')
⊢ Eq (α := S')
    (eval₂ (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        ((algebraMap S S' : (a : S) → S') t) (map (mapRingHom (algebraMap R R')) q) :
      S')
    (0 : S')
have rw₄ : Eq (α := S') ((algebraMap S S' : (a : S) → S') 0) 0
Tactic: rw [eval₂_map, H, ← hom_eval₂, ← AlgHom.toRingHom_eq_coe, hq, map_zero]
-- 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[X]
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R[X][X]
hqm : q.Monic
hq : eval₂ φ.toRingHom t q = 0
rw :
  Eq (α := S')
    (eval₂
        (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
          (mapRingHom (algebraMap R R')))
        ((algebraMap S S' : (a : S) → S') t) q :
      S')
    (0 : S')
rw₁ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S))
      ((algebraMap S S' : (a : S) → S') t) q =
    0
rw₂ : Eq (α := S') ((algebraMap S S' : (a : S) → S') (eval₂ (↑φ : R[X] →+* S) t q) : S') (0 : S')
rw₃ : Eq (α := S') ((algebraMap S S' : (a : S) → S') (eval₂ φ.toRingHom t q) : S') (0 : S')
rw₄ : Eq (α := S') ((algebraMap S S' : (a : S) → S') 0) 0
⊢ Eq (α := S')
    (eval₂ (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        ((algebraMap S S' : (a : S) → S') t) (map (mapRingHom (algebraMap R R')) q) :
      S')
    (0 : S')
have rw₅ : Eq.{u_2 + 1} (α := S') 0 0
Tactic: rw [eval₂_map, H, ← hom_eval₂, ← AlgHom.toRingHom_eq_coe, hq, map_zero]