awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Integral
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
⊢ ¬1 ≤ natDegree.{u_1} (R := R) 1

Tactic:
obtain rfl : p = 1 := eq_one_of_monic_natDegree_zero hp (by lia)

Premises used: Polynomial.eq_one_of_monic_natDegree_zero, rfl
-- Module: Mathlib.RingTheory.RingHom.Integral
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 m : ℕ
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
hp' : ¬1 ≤ natDegree.{u_1} (R := R) 1
⊢ HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) t : S) m = 0

Tactic:
simpa using e
-- Module: Mathlib.RingTheory.RingHom.Integral
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 m : ℕ
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
hp' : ¬1 ≤ natDegree.{u_1} (R := R) 1
⊢ 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) ^ m • r)

Tactic:
simp [Algebra.smul_def, show algebraMap R S t ^ m = 0 by simpa using e]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.RingHom.Integral
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 m : ℕ
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
hp' : ¬1 ≤ natDegree.{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)

Tactic:
exact ⟨m, by simp [Algebra.smul_def, show algebraMap R S t ^ m = 0 by simpa using e]⟩
-- Module: Mathlib.RingTheory.RingHom.Integral
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)

Tactic:
⟨m + n, p.scaleRoots (t ^ m), (monic_scaleRoots_iff _).mpr hp, ?_⟩

Premises used: Iff.mpr, HPow.hPow, HAdd.hAdd, And.intro, Exists.intro, Polynomial.scaleRoots, Polynomial.monic_scaleRoots_iff
-- Module: Mathlib.RingTheory.RingHom.Integral
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
pos :
  eval₂ (algebraMap R S) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ (m + n) • r) (p.scaleRoots (t ^ m)) = 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)

Tactic:
refine ⟨m + n, p.scaleRoots (t ^ m), (monic_scaleRoots_iff _).mpr hp, ?_⟩
-- Module: Mathlib.RingTheory.RingHom.Integral
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) (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)
-- Module: Mathlib.RingTheory.RingHom.Integral
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
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
⊢ eval₂ (algebraMap R S) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ (m + n) • r) (p.scaleRoots (t ^ m)) = 0

Tactic:
simp only [pow_add, ← Algebra.smul_def, mul_smul, ← map_pow] at e this ⊢

Premises used: pow_add, map_pow, Algebra.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.RingHom.Integral
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
pos₄ : HSMul.hSMul (β := S) ((t ^ m) ^ (p.natDegree - 1)) 0 = 0
pos₅ pos₆ : Eq.{u_1 + 1} (α := S) 0 0
⊢ eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) = 0

Tactic:
rw [this, ← tsub_add_cancel_of_le hp', pow_succ, mul_smul, e, smul_zero]

Premises used: pow_succ, smul_zero, tsub_add_cancel_of_le, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f ↔
    Eq.{u + 1} (α := Ideal S)
      (Ideal.span {g : S | P (S := Localization.Away g) (comp (algebraMap S (Localization.Away g)) f)}) ⊤

Tactic:
⟨fun ⟨s, hs, h⟩ ↦ ?_, fun h ↦ ⟨_, h, fun g hg ↦ hg⟩⟩

Premises used: Algebra.algebraMap, setOf, Localization.Away, RingHom.comp, Iff.intro, Exists.intro, Ideal.span, _private.0.RingHom.locally_iff_span_eq_top.match_1, Top.top, Eq
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
refine :
  Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
    ∀ (s : Set S) (hs : Eq (α := Ideal S) (Ideal.span s) ⊤)
      (h :
        ∀ t ∈ s,
          (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
            (comp (algebraMap S (Localization.Away t)) f)),
      Eq.{u + 1} (α := Ideal S)
        (Ideal.span {g : S | P (S := Localization.Away g) (comp (algebraMap S (Localization.Away g)) f)}) ⊤
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f ↔
    Eq.{u + 1} (α := Ideal S)
      (Ideal.span {g : S | P (S := Localization.Away g) (comp (algebraMap S (Localization.Away g)) f)}) ⊤

Tactic:
refine ⟨fun ⟨s, hs, h⟩ ↦ ?_, fun h ↦ ⟨_, h, fun g hg ↦ hg⟩⟩
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
h_1 : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
h :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
rw : s ⊆ (↑(Ideal.span {g : S | P (S := Localization.Away g) (comp (algebraMap S (Localization.Away g)) f)}) : Set S)
⊢ Eq.{u + 1} (α := Ideal S)
    (Ideal.span {g : S | P (S := Localization.Away g) (comp (algebraMap S (Localization.Away g)) f)}) ⊤

Tactic:
rw [eq_top_iff, ← hs, Ideal.span_le]

Premises used: Ideal.span_le, eq_top_iff
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
h_1 : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
h :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
g : S
hg : g ∈ s
⊢ g ∈ (↑(Ideal.span {g : S | P (S := Localization.Away g) (comp (algebraMap S (Localization.Away g)) f)}) : Set S)

Tactic:
Ideal.subset_span (h _ hg)

Premises used: Ideal.subset_span
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
h_1 : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
h :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
g : S
hg : g ∈ s
⊢ g ∈ (↑(Ideal.span {g : S | P (S := Localization.Away g) (comp (algebraMap S (Localization.Away g)) f)}) : Set S)

Tactic:
exact Ideal.subset_span (h _ hg)
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
mp :
  Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
    ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
      ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
mpr :
  (∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
      ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)) →
    Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f ↔
    ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
      ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)

Tactic:
constructor
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
mp :
  ∀ (s' : Finset S) (h₁ : (↑s' : Set S) ⊆ s) (h₂ : Eq (α := Ideal S) (Ideal.span (↑s' : Set S)) ⊤),
    ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
      ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
⊢ ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)

Tactic:
obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hsone

Premises used: Ideal.span_eq_top_iff_finite, Iff.mp