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[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')
⊢ (HMul.hMul (α := R'[X]) ((C : (a_1 : R') → R'[X]) (↑ha.unit⁻¹ : R') : R'[X]) (map (algebraMap R R') p)).Monic
have a₁ : Nontrivial R'
Tactic: nontriviality 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[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')
⊢ 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'))
have obtain : ∀ (r : R[X]) (hr : (φ : (a : R[X]) → S) r = HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t),
  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: 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
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
⊢ 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'))
have 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')
Tactic: use C ha.unit⁻¹.1 * mapRingHom (algebraMap R R') 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[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]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))
have 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))
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])
-- 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')
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))
have 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))
Tactic: obtain ⟨_, ⟨n, rfl⟩, e⟩ := IsLocalization.integerNormalization_spec (.powers a) q
-- 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')
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
⊢ ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))
have 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))
Tactic: generalize IsLocalization.integerNormalization (.powers a) q = q' at e
Cleared hypotheses: e
-- 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')
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')
have 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')
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)
-- 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')
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
⊢ ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))
have this₁ : 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
-- 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_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')
⊢ ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))
have 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) sorry)
        ((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))
Tactic: obtain ⟨⟨_, m, rfl⟩, hm⟩ := this.exists_multiple_integral_of_isLocalization (.powers a) _
-- 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_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'))
⊢ ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))
have 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')
Tactic: simp only [Algebra.smul_def, Submonoid.smul_def, algebraMap_apply R S S', ← map_mul] at hm
Cleared hypotheses: hm
-- 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_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')
⊢ ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))
have 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))
Tactic: obtain ⟨_, ⟨k, rfl⟩, hk⟩ := IsLocalization.exists_isIntegral_smul_of_isIntegral_map (.powers a) hm
-- 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_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')
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))
have refine : IsIntegral R
  (HSub.hSub (β := S) (a ^ (k + m + n) • t)
    ((φ : (a : R[X]) → S) (HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (k + m) * q') : S))
Tactic: refine ⟨C a ^ (k + m) * q', k + m + n, ?_⟩