awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra Rₘ S
inst_7 : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
p' : R[X]
hp'₁ :
  Polynomial.map (algebraMap R Rₘ) p' =
    p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))
hp'₂ : p'.Monic
inr :
  eval₂ (algebraMap Rₘ S)
      (HMul.hMul (α := S)
        ((algebraMap Rₘ S : (a : Rₘ) → S)
            ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ) :
          S)
        x)
      (p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))) =
    0
⊢ eval₂ (algebraMap R S) (commonDenom M p.support p.coeff • x) p' = 0

Tactic:
rw [IsScalarTower.algebraMap_eq R Rₘ S, ← Polynomial.eval₂_map, hp'₁, Submonoid.smul_def,
      Algebra.smul_def, IsScalarTower.algebraMap_apply R Rₘ S]

Premises used: Polynomial.eval₂_map, Submonoid.smul_def, IsScalarTower.algebraMap_eq, Algebra.smul_def, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra Rₘ S
inst_7 : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
p' : R[X]
hp'₁ :
  Polynomial.map (algebraMap R Rₘ) p' =
    p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))
hp'₂ : p'.Monic
⊢ eval₂ (algebraMap Rₘ S)
      (HMul.hMul (α := S)
        ((algebraMap Rₘ S : (a : Rₘ) → S)
            ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ) :
          S)
        x)
      (p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))) =
    0

Tactic:
Polynomial.scaleRoots_eval₂_eq_zero _ hp₂

Premises used: Polynomial.scaleRoots_eval₂_eq_zero
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra Rₘ S
inst_7 : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
p' : R[X]
hp'₁ :
  Polynomial.map (algebraMap R Rₘ) p' =
    p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))
hp'₂ : p'.Monic
⊢ eval₂ (algebraMap Rₘ S)
      (HMul.hMul (α := S)
        ((algebraMap Rₘ S : (a : Rₘ) → S)
            ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ) :
          S)
        x)
      (p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))) =
    0

Tactic:
exact Polynomial.scaleRoots_eval₂_eq_zero _ hp₂

Premises used: Polynomial.scaleRoots_eval₂_eq_zero
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra Rₘ S
inst_7 : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
inr : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) 1
⊢ Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff

Tactic:
rw [hp₁.leadingCoeff]

Premises used: Polynomial.Monic.leadingCoeff
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra Rₘ S
inst_7 : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
⊢ Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) 1

Tactic:
one_mem _

Premises used: OneMemClass.one_mem
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra Rₘ S
inst_7 : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
⊢ Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) 1

Tactic:
exact one_mem _

Premises used: OneMemClass.one_mem
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra Rₘ S
inst_7 : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
inr inr₁ inr₂ inr₃ : p.Monic
⊢ (p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))).Monic

Tactic:
rwa [Polynomial.monic_scaleRoots_iff]

Premises used: Polynomial.monic_scaleRoots_iff
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
M : Submonoid R
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
x : S
hx : IsIntegral.{u_5, u_7} R (A := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
obtain :
  ∀ (p : R[X]) (hpm : p.Monic) (hp : eval₂ (algebraMap R Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x) p = 0),
    ∃ m ∈ M, IsIntegral R (m • x)
⊢ ∃ m ∈ M, IsIntegral R (m • x)

Tactic:
obtain ⟨p, hpm, hp⟩ := hx
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
M : Submonoid R
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
x : S
p : R[X]
hpm : p.Monic
hp : eval₂ (algebraMap R Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x) p = 0
⊢ ∃ a ∈ M, HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S) (eval₂ (algebraMap R S) x p) = 0

Tactic:
simp only [IsScalarTower.algebraMap_eq R S Sₘ, ← hom_eval₂,
    IsLocalization.map_eq_zero_iff (Algebra.algebraMapSubmonoid S M), Algebra.algebraMapSubmonoid,
    Subtype.exists, Submonoid.mem_map, exists_prop, exists_exists_and_eq_and] at hp

Premises used: Submonoid.mem_map, Polynomial.hom_eval₂, IsLocalization.map_eq_zero_iff, Subtype.exists, exists_prop, exists_exists_and_eq_and, IsScalarTower.algebraMap_eq, Algebra.algebraMapSubmonoid
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
M : Submonoid R
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
x : S
p : R[X]
hpm : p.Monic
hp : ∃ a ∈ M, HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S) (eval₂ (algebraMap R S) x p) = 0
obtain :
  ∀ (m : R) (hm : m ∈ M)
    (e : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) m : S) (eval₂ (algebraMap R S) x p) = 0),
    ∃ m ∈ M, IsIntegral R (m • x)
⊢ ∃ m ∈ M, IsIntegral R (m • x)

Tactic:
obtain ⟨m, hm, e⟩ := hp
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
M : Submonoid R
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
x : S
p : R[X]
hpm : p.Monic
m : R
hm : m ∈ M
e : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) m : S) (eval₂ (algebraMap R S) x p) = 0
⊢ eval₂ (algebraMap R S) x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) m : R[X]) p) = 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
M : Submonoid R
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
x : S
p : R[X]
hpm : p.Monic
m : R
hm : m ∈ M
e : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) m : S) (eval₂ (algebraMap R S) x p) = 0
⊢ IsIntegral R (m • x)

Tactic:
simpa [Algebra.smul_def, leadingCoeff_mul_monic hpm] using
    RingHom.isIntegralElem_leadingCoeff_mul (algebraMap R S) (C m * p) x (by simpa)

Premises used: Polynomial.C, HMul.hMul, Algebra.algebraMap, RingHom.isIntegralElem_leadingCoeff_mul, Polynomial.leadingCoeff_mul_monic, Algebra.smul_def, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
M : Submonoid R
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
x : S
p : R[X]
hpm : p.Monic
m : R
hm : m ∈ M
e : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) m : S) (eval₂ (algebraMap R S) x p) = 0
⊢ ∃ m ∈ M, IsIntegral R (m • x)

Tactic:
exact ⟨m, hm, by simpa [Algebra.smul_def, leadingCoeff_mul_monic hpm] using
    RingHom.isIntegralElem_leadingCoeff_mul (algebraMap R S) (C m * p) x (by simpa)⟩
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
hx : IsIntegral.{u_5, u_7} R (A := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
⊢ Nontrivial S

Tactic:
nontriviality S
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
hx : IsIntegral.{u_5, u_7} R (A := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
h : Nontrivial S
obtain :
  ∀ (p : R[X]) (hpm : p.Monic) (hp : eval₂ (algebraMap R Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x) p = 0),
    ∃ (n : ℕ), IsIntegral R (r ^ n * x)
⊢ ∃ (n : ℕ), IsIntegral R (r ^ n * x)

Tactic:
obtain ⟨p, hpm, hp⟩ := hx
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
h : Nontrivial S
p : R[X]
hpm : p.Monic
hp : eval₂ (algebraMap R Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x) p = 0
⊢ ∃ (a : ℕ), r ^ a * eval₂ (algebraMap R S) x p = 0

Tactic:
simp only [IsScalarTower.algebraMap_eq R S Sₘ, ← hom_eval₂,
    IsLocalization.map_eq_zero_iff (.powers r), Subtype.exists, Submonoid.mem_powers_iff,
    exists_prop, exists_exists_eq_and] at hp

Premises used: Polynomial.hom_eval₂, IsLocalization.map_eq_zero_iff, Subtype.exists, exists_prop, exists_exists_eq_and, Submonoid.powers, IsScalarTower.algebraMap_eq, Submonoid.mem_powers_iff
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
h : Nontrivial S
p : R[X]
hpm : p.Monic
hp : ∃ (a : ℕ), r ^ a * eval₂ (algebraMap R S) x p = 0
obtain : ∀ (m : ℕ) (hm : r ^ m * eval₂ (algebraMap R S) x p = 0), ∃ (n : ℕ), IsIntegral R (r ^ n * x)
⊢ ∃ (n : ℕ), IsIntegral R (r ^ n * x)

Tactic:
obtain ⟨m, hm⟩ := hp
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
h : Nontrivial S
p : R[X]
hpm : p.Monic
m : ℕ
hm : r ^ m * eval₂ (algebraMap R S) x p = 0
⊢ Eq (α := S)
    ((aeval x : (a : (↥(integralClosure R S))[X]) → S)
        (HPow.hPow (α := (↥(integralClosure R S))[X])
            ((C : (a : ↥(integralClosure R S)) → (↥(integralClosure R S))[X])
                (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) r hr) :
              (↥(integralClosure R S))[X])
            m *
          Polynomial.map (algebraMap R ↥(integralClosure R S)) p) :
      S)
    (0 : S)

Tactic:
simpa [← aeval_def] using hm

Premises used: Polynomial.aeval_def
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
h : Nontrivial S
p : R[X]
hpm : p.Monic
m : ℕ
hm : r ^ m * eval₂ (algebraMap R S) x p = 0
⊢ IsIntegral R
    ((HPow.hPow (α := (↥(integralClosure R S))[X])
            ((C : (a : ↥(integralClosure R S)) → (↥(integralClosure R S))[X])
                (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) r hr) :
              (↥(integralClosure R S))[X])
            m *
          Polynomial.map (algebraMap R ↥(integralClosure R S)) p).leadingCoeff •
      x)

Tactic:
have := isIntegral_trans (R := R) _ (isIntegral_leadingCoeff_smul (R := integralClosure R S)
    (C ⟨r, hr⟩ ^ m * p.map (algebraMap _ _)) x (by simpa [← aeval_def] using hm))
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
h : Nontrivial S
p : R[X]
hpm : p.Monic
m : ℕ
hm : r ^ m * eval₂ (algebraMap R S) x p = 0
this :
  IsIntegral R
    ((HPow.hPow (α := (↥(integralClosure R S))[X])
            ((C : (a : ↥(integralClosure R S)) → (↥(integralClosure R S))[X])
                (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) r hr) :
              (↥(integralClosure R S))[X])
            m *
          Polynomial.map (algebraMap R ↥(integralClosure R S)) p).leadingCoeff •
      x)
⊢ IsIntegral R
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) r hr ^ m • x)

Tactic:
rw [← map_pow, (hpm.map _).leadingCoeff_C_mul] at this

Premises used: Polynomial.Monic.leadingCoeff_C_mul, map_pow, Polynomial.Monic.map
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
h : Nontrivial S
p : R[X]
hpm : p.Monic
m : ℕ
hm : r ^ m * eval₂ (algebraMap R S) x p = 0
this :
  IsIntegral R
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) r hr ^ m • x)
⊢ ∃ (n : ℕ), IsIntegral R (r ^ n * x)

Tactic:
⟨m, this⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
h : Nontrivial S
p : R[X]
hpm : p.Monic
m : ℕ
hm : r ^ m * eval₂ (algebraMap R S) x p = 0
this :
  IsIntegral R
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) r hr ^ m • x)
⊢ ∃ (n : ℕ), IsIntegral R (r ^ n * x)

Tactic:
exact ⟨m, this⟩
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
a : ↥(Submonoid.powers r)
hx : IsIntegral R (mk' Sₘ x a)
⊢ ∃ (n : ℕ), IsIntegral R (r ^ n * x)

Tactic:
IsLocalization.Away.exists_isIntegral_mul_of_isIntegral_algebraMap (Sₘ := Sₘ) hr ?_

Premises used: IsLocalization.Away.exists_isIntegral_mul_of_isIntegral_algebraMap
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
a : ↥(Submonoid.powers r)
hx : IsIntegral R (mk' Sₘ x a)
refine : IsIntegral.{u_5, u_7} R (A := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
⊢ ∃ (n : ℕ), IsIntegral R (r ^ n * x)

Tactic:
refine IsLocalization.Away.exists_isIntegral_mul_of_isIntegral_algebraMap (Sₘ := Sₘ) hr ?_

Premises used: IsLocalization.Away.exists_isIntegral_mul_of_isIntegral_algebraMap
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
a : ↥(Submonoid.powers r)
hx : IsIntegral R (mk' Sₘ x a)
obtain :
  ∀ (n : ℕ)
    (hx :
      IsIntegral R
        (mk' Sₘ x
          (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers r) x)
            ((fun (x : ℕ) ↦ r ^ x) n) ⋯))),
    IsIntegral.{u_5, u_7} R (A := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
⊢ IsIntegral.{u_5, u_7} R (A := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)

Tactic:
obtain ⟨_, ⟨n, rfl⟩⟩ := a

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
n : ℕ
hx :
  IsIntegral R
    (mk' Sₘ x
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers r) x)
        ((fun (x : ℕ) ↦ r ^ x) n) ⋯))
⊢ IsIntegral R
    (HMul.hMul (α := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) (r ^ n) : Sₘ)
      (mk' Sₘ x
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers r) x)
          ((fun (x : ℕ) ↦ r ^ x) n) ⋯)))

Tactic:
(hr.pow n).algebraMap.mul hx

Premises used: IsIntegral.mul, IsIntegral.pow, IsIntegral.algebraMap
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
n : ℕ
hx :
  IsIntegral R
    (mk' Sₘ x
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers r) x)
        ((fun (x : ℕ) ↦ r ^ x) n) ⋯))
h :
  (algebraMap S Sₘ : (a : S) → Sₘ) x =
    HMul.hMul (α := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) (r ^ n) : Sₘ)
      (mk' Sₘ x
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers r) x)
          ((fun (x : ℕ) ↦ r ^ x) n) ⋯))
⊢ IsIntegral.{u_5, u_7} R (A := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)

Tactic:
convert! (hr.pow n).algebraMap.mul hx

Premises used: IsIntegral.mul, IsIntegral.pow, IsIntegral.algebraMap
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
n : ℕ
hx :
  IsIntegral R
    (mk' Sₘ x
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers r) x)
        ((fun (x : ℕ) ↦ r ^ x) n) ⋯))
⊢ (algebraMap S Sₘ : (a : S) → Sₘ) x =
    HMul.hMul (α := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) (r ^ n) : Sₘ)
      (mk' Sₘ x
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers r) x)
          ((fun (x : ℕ) ↦ r ^ x) n) ⋯))

Tactic:
(mk'_spec'_mk ..).symm

Premises used: Set.Mem, IsLocalization.mk'_spec'_mk, Eq.symm
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
n : ℕ
hx :
  IsIntegral R
    (mk' Sₘ x
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers r) x)
        ((fun (x : ℕ) ↦ r ^ x) n) ⋯))
⊢ (algebraMap S Sₘ : (a : S) → Sₘ) x =
    HMul.hMul (α := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) (r ^ n) : Sₘ)
      (mk' Sₘ x
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers r) x)
          ((fun (x : ℕ) ↦ r ^ x) n) ⋯))

Tactic:
exact (mk'_spec'_mk ..).symm

Premises used: IsLocalization.mk'_spec'_mk, Eq.symm
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
⊢ Nontrivial S

Tactic:
nontriviality S
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
obtain : ∀ (p : (↥R[s])[X]) (hpm : p.Monic) (hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0), φ.IsIntegralElem t
⊢ φ.IsIntegralElem t

Tactic:
obtain ⟨p, hpm, hpt⟩ := ht
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
p : (↥R[s])[X]
hpm : p.Monic
hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0
⊢ ∀ (n : ℕ),
    Membership.mem (γ := Set S) (Set.range.{u_2, u_1 + 1} (ι := R[X]) (⇑φ.toRingHom : (a : R[X]) → S))
      (coeff (Polynomial.map (algebraMap (↥R[s]) S) p) n)

Tactic:
simp [← AlgHom.mem_range, φ, ← Algebra.adjoin_singleton_eq_range_aeval]

Premises used: Algebra.adjoin_singleton_eq_range_aeval, AlgHom.mem_range
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
p : (↥R[s])[X]
hpm : p.Monic
hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0
⊢ Polynomial.map (algebraMap (↥R[s]) S) p ∈ lifts φ.toRingHom

Tactic:
have : p.map (algebraMap _ S) ∈ lifts φ.toRingHom := (lifts_iff_coeff_lifts _).mpr
      (by simp [← AlgHom.mem_range, φ, ← Algebra.adjoin_singleton_eq_range_aeval])