awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
e :
  (↑(Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) t) : Submonoid S) x)
            (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) t : S) m) ⋯) :
        S) *
      eval₂ (algebraMap R S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x)
                    ((fun (x : ℕ) ↦ t ^ x) n) ⋯) :
                R) :
            S)
          r)
        p =
    0
pos :
  ∀ (hp' : 1 ≤ p.natDegree),
    ∃ (n : ℕ),
      Membership.mem (γ := Submodule R S)
        ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
        ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ n • r)
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ n • r)
have neg : ∀ (hp' : ¬1 ≤ p.natDegree),
  ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ n • r)
Tactic: by_cases hp' : 1 ≤ p.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (hypothesis)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
e :
  (↑(Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) t) : Submonoid S) x)
            (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) t : S) m) ⋯) :
        S) *
      eval₂ (algebraMap R S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x)
                    ((fun (x : ℕ) ↦ t ^ x) n) ⋯) :
                R) :
            S)
          r)
        p =
    0
hp' : ¬1 ≤ p.natDegree
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ n • r)
have hp₁ : Monic.{u_1} (R := R) 1
Tactic: obtain rfl : p = 1 := eq_one_of_monic_natDegree_zero hp (by lia)
Cleared hypotheses: p, hp, e, hp'
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (hypothesis)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
e :
  (↑(Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) t) : Submonoid S) x)
            (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) t : S) m) ⋯) :
        S) *
      eval₂ (algebraMap R S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x)
                    ((fun (x : ℕ) ↦ t ^ x) n) ⋯) :
                R) :
            S)
          r)
        p =
    0
hp' : ¬1 ≤ p.natDegree
hp₁ : Monic.{u_1} (R := R) 1
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ n • r)
have e₁ : (↑(Subtype.mk (p := fun (x : S) ↦
          Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) t) : Submonoid S) x)
          (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) t : S) m) sorry) :
      S) *
    eval₂ (algebraMap R S)
      (HMul.hMul (α := S)
        ((algebraMap R S : (a : R) → S)
            (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x)
                  ((fun (x : ℕ) ↦ t ^ x) n) sorry) :
              R) :
          S)
        r)
      1 =
  0
Tactic: obtain rfl : p = 1 := eq_one_of_monic_natDegree_zero hp (by lia)
Cleared hypotheses: p, hp, e, hp'
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (hypothesis)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
e :
  (↑(Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) t) : Submonoid S) x)
            (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) t : S) m) ⋯) :
        S) *
      eval₂ (algebraMap R S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x)
                    ((fun (x : ℕ) ↦ t ^ x) n) ⋯) :
                R) :
            S)
          r)
        p =
    0
hp' : ¬1 ≤ p.natDegree
hp₁ : Monic.{u_1} (R := R) 1
e₁ :
  (↑(Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) t) : Submonoid S) x)
            (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) t : S) m) ⋯) :
        S) *
      eval₂ (algebraMap R S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x)
                    ((fun (x : ℕ) ↦ t ^ x) n) ⋯) :
                R) :
            S)
          r)
        1 =
    0
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ n • r)
have hp'₁ : ¬1 ≤ natDegree.{u_1} (R := R) 1
Tactic: obtain rfl : p = 1 := eq_one_of_monic_natDegree_zero hp (by lia)
Cleared hypotheses: p, hp, e, hp'
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
e :
  (↑(Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) t) : Submonoid S) x)
            (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) t : S) m) ⋯) :
        S) *
      eval₂ (algebraMap R S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x)
                    ((fun (x : ℕ) ↦ t ^ x) n) ⋯) :
                R) :
            S)
          r)
        p =
    0
hp' : 1 ≤ p.natDegree
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ n • r)
have pos : eval₂ (algebraMap R S) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ (m + n) • r) (p.scaleRoots (t ^ m)) = 0
Tactic: refine ⟨m + n, p.scaleRoots (t ^ m), (monic_scaleRoots_iff _).mpr hp, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (hypothesis)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
e :
  (↑(Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) t) : Submonoid S) x)
            (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) t : S) m) ⋯) :
        S) *
      eval₂ (algebraMap R S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x)
                    ((fun (x : ℕ) ↦ t ^ x) n) ⋯) :
                R) :
            S)
          r)
        p =
    0
hp' : 1 ≤ p.natDegree
⊢ eval₂ (algebraMap R S) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ (m + n) • r) (p.scaleRoots (t ^ m)) = 0
have this₁ : eval₂ (algebraMap R S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (t ^ m) : S) (t ^ n • r))
    (p.scaleRoots (t ^ m)) =
  HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) (t ^ m) : S) p.natDegree * eval₂ (algebraMap R S) (t ^ n • r) p
Tactic: have := p.scaleRoots_eval₂_mul (algebraMap R S) (t ^ n • r) (t ^ m)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this_4 :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
e :
  (↑(Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) t) : Submonoid S) x)
            (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) t : S) m) ⋯) :
        S) *
      eval₂ (algebraMap R S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x)
                    ((fun (x : ℕ) ↦ t ^ x) n) ⋯) :
                R) :
            S)
          r)
        p =
    0
hp' : 1 ≤ p.natDegree
this :
  eval₂ (algebraMap R S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (t ^ m) : S) (t ^ n • r))
      (p.scaleRoots (t ^ m)) =
    HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) (t ^ m) : S) p.natDegree * eval₂ (algebraMap R S) (t ^ n • r) p
⊢ eval₂ (algebraMap R S) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ (m + n) • r) (p.scaleRoots (t ^ m)) = 0
have pos : ∀ (e : t ^ m • eval₂ (algebraMap R S) (t ^ n • r) p = 0)
  (this :
    eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) =
      (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p),
  eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) = 0
Tactic: simp only [pow_add, ← Algebra.smul_def, mul_smul, ← map_pow] at e this ⊢
Cleared hypotheses: e, this
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this_4 :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
hp' : 1 ≤ p.natDegree
e : t ^ m • eval₂ (algebraMap R S) (t ^ n • r) p = 0
this :
  eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) =
    (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p
⊢ eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) = 0
have pos : (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p = 0
Tactic: rw [this, ← tsub_add_cancel_of_le hp', pow_succ, mul_smul, e, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this_4 :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
hp' : 1 ≤ p.natDegree
e : t ^ m • eval₂ (algebraMap R S) (t ^ n • r) p = 0
this :
  eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) =
    (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p
pos : (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p = 0
⊢ eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) = 0
have pos₁ : (t ^ m) ^ (p.natDegree - 1 + 1) • eval₂ (algebraMap R S) (t ^ n • r) p = 0
Tactic: rw [this, ← tsub_add_cancel_of_le hp', pow_succ, mul_smul, e, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this_4 :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
hp' : 1 ≤ p.natDegree
e : t ^ m • eval₂ (algebraMap R S) (t ^ n • r) p = 0
this :
  eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) =
    (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p
pos : (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p = 0
pos₁ : (t ^ m) ^ (p.natDegree - 1 + 1) • eval₂ (algebraMap R S) (t ^ n • r) p = 0
⊢ eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) = 0
have pos₂ : ((t ^ m) ^ (p.natDegree - 1) * t ^ m) • eval₂ (algebraMap R S) (t ^ n • r) p = 0
Tactic: rw [this, ← tsub_add_cancel_of_le hp', pow_succ, mul_smul, e, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this_4 :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
hp' : 1 ≤ p.natDegree
e : t ^ m • eval₂ (algebraMap R S) (t ^ n • r) p = 0
this :
  eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) =
    (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p
pos : (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p = 0
pos₁ : (t ^ m) ^ (p.natDegree - 1 + 1) • eval₂ (algebraMap R S) (t ^ n • r) p = 0
pos₂ : ((t ^ m) ^ (p.natDegree - 1) * t ^ m) • eval₂ (algebraMap R S) (t ^ n • r) p = 0
⊢ eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) = 0
have pos₃ : (t ^ m) ^ (p.natDegree - 1) • t ^ m • eval₂ (algebraMap R S) (t ^ n • r) p = 0
Tactic: rw [this, ← tsub_add_cancel_of_le hp', pow_succ, mul_smul, e, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this_4 :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
hp' : 1 ≤ p.natDegree
e : t ^ m • eval₂ (algebraMap R S) (t ^ n • r) p = 0
this :
  eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) =
    (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p
pos : (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p = 0
pos₁ : (t ^ m) ^ (p.natDegree - 1 + 1) • eval₂ (algebraMap R S) (t ^ n • r) p = 0
pos₂ : ((t ^ m) ^ (p.natDegree - 1) * t ^ m) • eval₂ (algebraMap R S) (t ^ n • r) p = 0
pos₃ : (t ^ m) ^ (p.natDegree - 1) • t ^ m • eval₂ (algebraMap R S) (t ^ n • r) p = 0
⊢ eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) = 0
have pos₄ : HSMul.hSMul (β := S) ((t ^ m) ^ (p.natDegree - 1)) 0 = 0
Tactic: rw [this, ← tsub_add_cancel_of_le hp', pow_succ, mul_smul, e, smul_zero]