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[X]
ht : φ.IsIntegralElem t
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')
r : R[X]
hr : (φ : (a : R[X]) → S) r = HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t
h :
  ((AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))) :
          RingHom.{u_1, u_2} R'[X] S') :
        (a : R'[X]) → S')
      (HMul.hMul (α := R'[X]) (β := R'[X]) ((C : (a_1 : R') → R'[X]) (↑ha.unit⁻¹ : R') : R'[X])
        ((mapRingHom (algebraMap R R') : (a_1 : R[X]) → R'[X]) r : R'[X])) =
    HMul.hMul (α := S') (β := S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S')
          (HMul.hMul (α := R'[X]) ((C : (a_1 : R') → R'[X]) (↑ha.unit⁻¹ : R') : R'[X]) (map (algebraMap R R') p)) :
        S')
      ((algebraMap S S' : (a : S) → S') t : S')
⊢ Membership.mem (γ := Subalgebra R' S')
    (AlgHom.range (A := R'[X]) (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))) : Subalgebra R' S')
    (HMul.hMul (α := S') (β := S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S')
          (HMul.hMul (α := R'[X]) ((C : (a_1 : R') → R'[X]) (↑ha.unit⁻¹ : R') : R'[X]) (map (algebraMap R R') p)) :
        S')
      ((algebraMap S S' : (a : S) → S') t : S'))

Tactic:
use C ha.unit⁻¹.1 * mapRingHom (algebraMap R R') r

Premises used: Units.val, Polynomial.C, Algebra.algebraMap, Inv.inv, Polynomial.mapRingHom, IsUnit.unit, 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[X]
ht : φ.IsIntegralElem t
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')
r : R[X]
hr : (φ : (a : R[X]) → S) r = HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t
⊢ ((AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))) :
          RingHom.{u_1, u_2} R'[X] S') :
        (a : R'[X]) → S')
      (HMul.hMul (α := R'[X]) (β := R'[X]) ((C : (a_1 : R') → R'[X]) (↑ha.unit⁻¹ : R') : R'[X])
        ((mapRingHom (algebraMap R R') : (a_1 : R[X]) → R'[X]) r : R'[X])) =
    HMul.hMul (α := S') (β := S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S')
          (HMul.hMul (α := R'[X]) ((C : (a_1 : R') → R'[X]) (↑ha.unit⁻¹ : R') : R'[X]) (map (algebraMap R R') p)) :
        S')
      ((algebraMap S S' : (a : S) → S') t : S')

Tactic:
simp [aeval_algebraMap_apply, aeval_algHom_apply, hr, mul_assoc]

Premises used: mul_assoc, 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[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')
obtain :
  ∀ (q : R'[X])
    (hq :
      IsIntegral R'
        (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
          (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S')
              q :
            S'))),
    ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))
⊢ ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))

Tactic:
obtain ⟨q, hq⟩ := exists_isIntegral_sub_of_isIntegralElem_of_mul_mem_range (R := R')
    (aeval (algebraMap S S' (φ X))) (algebraMap S S' t) (C ha.unit⁻¹.1 * p.map (algebraMap _ _)) (by
      obtain ⟨q, hqm, hq⟩ := ht
      refine ⟨q.map (mapRingHom (algebraMap _ _)), hqm.map _, ?_⟩
      rw [eval₂_map, H, ← hom_eval₂, ← AlgHom.toRingHom_eq_coe, hq, map_zero]) (by
      nontriviality R'
      simp [Monic, leadingCoeff_C_mul_of_isUnit,
        leadingCoeff_map_of_leadingCoeff_ne_zero _ ha.ne_zero, a]) (by
      obtain ⟨r, hr : φ r = _⟩ := hp
      use C ha.unit⁻¹.1 * mapRingHom (algebraMap R R') r
      simp [aeval_algebraMap_apply, aeval_algHom_apply, hr, mul_assoc])

Premises used: exists_isIntegral_sub_of_isIntegralElem_of_mul_mem_range, Units.val, Polynomial.C, HMul.hMul, Algebra.algebraMap, Inv.inv, IsUnit.unit, Polynomial.map, Polynomial.aeval, Polynomial.X, 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[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')
q : R'[X]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
obtain :
  ∀ (n : ℕ)
    (e :
      map (algebraMap R R') (IsLocalization.integerNormalization (Submonoid.powers a) q) =
        HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q),
    ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))
⊢ ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))

Tactic:
obtain ⟨_, ⟨n, rfl⟩, e⟩ := IsLocalization.integerNormalization_spec (.powers a) q

Premises used: Submonoid.powers, IsLocalization.integerNormalization_spec, rfl
-- 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[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')
q : R'[X]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
n : ℕ
e :
  map (algebraMap R R') (IsLocalization.integerNormalization (Submonoid.powers a) q) =
    HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q
generalize :
  ∀ (q' : R[X]) (e : map (algebraMap R R') q' = HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q),
    ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))
⊢ ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))

Tactic:
generalize IsLocalization.integerNormalization (.powers a) q = q' at e

Premises used: Submonoid.powers, IsLocalization.integerNormalization
-- 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[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')
q : R'[X]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q
⊢ (algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) q') =
    HMul.hMul (β := S') (HPow.hPow (α := S') (((algebraMap R S' : R →+* S') : (a : R) → S') a : S') n)
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S')

Tactic:
simpa [Algebra.smul_def, aeval_algebraMap_apply, aeval_algHom_apply, ← algebraMap_apply] using
        congr(aeval (algebraMap S S' (φ X)) $e)

Premises used: Algebra.smul_def, Polynomial.aeval_algHom_apply, IsScalarTower.algebraMap_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[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')
q : R'[X]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q
⊢ (algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) q') =
    HMul.hMul (β := S') (HPow.hPow (α := S') (((algebraMap R S' : R →+* S') : (a : R) → S') a : S') n)
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S')

Tactic:
have : algebraMap S S' (φ q') = (algebraMap R S' a) ^ n * aeval (algebraMap S S' (φ X)) q := by
      simpa [Algebra.smul_def, aeval_algebraMap_apply, aeval_algHom_apply, ← algebraMap_apply] using
        congr(aeval (algebraMap S S' (φ X)) $e)
-- 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[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_2 : 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]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q
this :
  (algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) q') =
    HMul.hMul (β := S') (HPow.hPow (α := S') (((algebraMap R S' : R →+* S') : (a : R) → S') a : S') n)
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S')
⊢ IsIntegral R' (A := S')
    ((algebraMap S S' : (a : S) → S') (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q' : S)) : S')

Tactic:
simpa [Algebra.smul_def, ← mul_sub, ← algebraMap_apply, this] using
      (isIntegral_algebraMap (A := S') (x := algebraMap R R' a ^ n)).mul hq

Premises used: mul_sub, IsIntegral.mul, isIntegral_algebraMap, Algebra.smul_def, 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[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')
q : R'[X]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q
⊢ IsIntegral R' (A := S')
    ((algebraMap S S' : (a : S) → S') (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q' : S)) : S')

Tactic:
have : IsIntegral R' ((algebraMap S S') (a ^ n • t - φ q')) := by
    have : algebraMap S S' (φ q') = (algebraMap R S' a) ^ n * aeval (algebraMap S S' (φ X)) q := by
      simpa [Algebra.smul_def, aeval_algebraMap_apply, aeval_algHom_apply, ← algebraMap_apply] using
        congr(aeval (algebraMap S S' (φ X)) $e)
    simpa [Algebra.smul_def, ← mul_sub, ← algebraMap_apply, this] using
      (isIntegral_algebraMap (A := S') (x := algebraMap R R' a ^ n)).mul hq
-- 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[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_2 : 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]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q
this :
  IsIntegral R' (A := S')
    ((algebraMap S S' : (a : S) → S') (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q' : S)) : S')
obtain :
  ∀ (m : ℕ)
    (hm :
      IsIntegral R
        (HSMul.hSMul (β := S')
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
            ((fun (x : ℕ) ↦ a ^ x) m) ⋯)
          ((algebraMap S S' : (a : S) → S') (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q' : S)) : S'))),
    ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))
⊢ ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))

Tactic:
obtain ⟨⟨_, m, rfl⟩, hm⟩ := this.exists_multiple_integral_of_isLocalization (.powers a) _

Premises used: IsIntegral.exists_multiple_integral_of_isLocalization, Submonoid.powers, rfl
-- 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[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_2 : 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]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q
this :
  IsIntegral R' (A := S')
    ((algebraMap S S' : (a : S) → S') (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q' : S)) : S')
m : ℕ
hm :
  IsIntegral R
    (HSMul.hSMul (β := S')
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
        ((fun (x : ℕ) ↦ a ^ x) m) ⋯)
      ((algebraMap S S' : (a : S) → S') (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q' : S)) : S'))
⊢ IsIntegral R (A := S')
    ((algebraMap S S' : (a : S) → S')
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
          (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
            ((φ : (a : R[X]) → S) q' : S))) :
      S')

Tactic:
simp only [Algebra.smul_def, Submonoid.smul_def, algebraMap_apply R S S', ← map_mul] at hm

Premises used: Submonoid.smul_def, map_mul, Algebra.smul_def, 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[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_2 : 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]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q
this :
  IsIntegral R' (A := S')
    ((algebraMap S S' : (a : S) → S') (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q' : S)) : S')
m : ℕ
hm :
  IsIntegral R (A := S')
    ((algebraMap S S' : (a : S) → S')
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
          (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
            ((φ : (a : R[X]) → S) q' : S))) :
      S')
obtain :
  ∀ (k : ℕ)
    (hk :
      IsIntegral R
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ a ^ x) k)
          (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
            (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
              ((φ : (a : R[X]) → S) q' : S))))),
    ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))
⊢ ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))

Tactic:
obtain ⟨_, ⟨k, rfl⟩, hk⟩ := IsLocalization.exists_isIntegral_smul_of_isIntegral_map (.powers a) hm

Premises used: IsLocalization.exists_isIntegral_smul_of_isIntegral_map, Submonoid.powers, rfl