awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : n ∈ p.support
h₂ : n = p.natDegree
pos :
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff p.natDegree *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - p.natDegree))
pos₁ :
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.leadingCoeff *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - p.natDegree))
pos₂ :
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.leadingCoeff *
      HPow.hPow (α := Rₘ) (β := ℕ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ) 0)
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
have pos₃ : Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
  (p.leadingCoeff * 1)
Tactic: rwa [h₂, Polynomial.coeff_natDegree, tsub_self, pow_zero, _root_.mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : n ∈ p.support
h₂ : n = p.natDegree
pos :
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff p.natDegree *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - p.natDegree))
pos₁ :
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.leadingCoeff *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - p.natDegree))
pos₂ :
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.leadingCoeff *
      HPow.hPow (α := Rₘ) (β := ℕ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ) 0)
pos₃ :
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.leadingCoeff * 1)
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
have pos₄ : Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ)) p.leadingCoeff
Tactic: rwa [h₂, Polynomial.coeff_natDegree, tsub_self, pow_zero, _root_.mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
have this : n + 1 ≤ p.natDegree
Tactic: have : n + 1 ≤ p.natDegree := lt_of_le_of_ne (Polynomial.le_natDegree_of_mem_supp _ h₁) h₂
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
have neg : Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
  (HMul.hMul (α := Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((↑(commonDenom M p.support p.coeff) : R) ^ (p.natDegree - n - 1)) : Rₘ)
    (HMul.hMul (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ) (p.coeff n)))
Tactic: rw [← tsub_add_cancel_of_le (le_tsub_of_add_le_left this), pow_add, pow_one, mul_comm,
      _root_.mul_assoc, ← map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (HMul.hMul (α := Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) ((↑(commonDenom M p.support p.coeff) : R) ^ (p.natDegree - n - 1)) : Rₘ)
      (HMul.hMul (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.coeff n)))
have neg : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ))
  (HMul.hMul (α := Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((↑(commonDenom M p.support p.coeff) : R) ^ (p.natDegree - n - 1)) : Rₘ)
    (HMul.hMul (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ) (p.coeff n)))
Tactic: change _ ∈ (algebraMap R Rₘ).range
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ))
    (HMul.hMul (α := Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) ((↑(commonDenom M p.support p.coeff) : R) ^ (p.natDegree - n - 1)) : Rₘ)
      (HMul.hMul (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.coeff n)))
have neg : Membership.mem.{u_3, u_3} (α := Rₘ) (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ))
  ((algebraMap R Rₘ : (a : R) → Rₘ) ((↑(commonDenom M p.support p.coeff) : R) ^ (p.natDegree - n - 1)) : Rₘ)
Tactic: apply mul_mem
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
neg :
  Membership.mem.{u_3, u_3} (α := Rₘ) (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ))
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((↑(commonDenom M p.support p.coeff) : R) ^ (p.natDegree - n - 1)) : Rₘ)
⊢ Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ))
    (HMul.hMul (α := Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) ((↑(commonDenom M p.support p.coeff) : R) ^ (p.natDegree - n - 1)) : Rₘ)
      (HMul.hMul (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.coeff n)))
have neg₁ : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ))
  (HMul.hMul (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ) (p.coeff n))
Tactic: apply mul_mem
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ))
    (HMul.hMul (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ) (p.coeff n))
have neg : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ))
  ((↑(commonDenom M p.support p.coeff) : R) • p.coeff n)
Tactic: rw [← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : n ∉ p.support
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
have h₂ : p.coeff n = 0
Tactic: rw [Polynomial.notMem_support_iff] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : p.coeff n = 0
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
have neg : Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ)) 0
Tactic: rw [h₁, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
hx : IsIntegral Rₘ x
⊢ ∃ (m : ↥M), IsIntegral R (m • x)
have inl : Subsingleton Rₘ → ∃ (m : ↥M), IsIntegral R (m • x)
Tactic: rcases subsingleton_or_nontrivial Rₘ with _ | nontriv
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
hx : IsIntegral Rₘ x
inl : Subsingleton Rₘ → ∃ (m : ↥M), IsIntegral R (m • x)
⊢ ∃ (m : ↥M), IsIntegral R (m • x)
have inr : ∀ (nontriv : Nontrivial Rₘ), ∃ (m : ↥M), IsIntegral R (m • x)
Tactic: rcases subsingleton_or_nontrivial Rₘ with _ | nontriv
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
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
hx : IsIntegral Rₘ x
h : Subsingleton Rₘ
⊢ ∃ (m : ↥M), IsIntegral R (m • x)
have this : Subsingleton S
Tactic: haveI := (algebraMap Rₘ S).codomain_trivial
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
hx : IsIntegral Rₘ x
nontriv : Nontrivial Rₘ
⊢ ∃ (m : ↥M), IsIntegral R (m • x)
have inr : ∀ (p : Rₘ[X]) (hp₁ : p.Monic) (hp₂ : eval₂ (algebraMap Rₘ S) x p = 0), ∃ (m : ↥M), IsIntegral R (m • x)
Tactic: obtain ⟨p, hp₁, hp₂⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ ∃ (m : ↥M), IsIntegral R (m • x)
have inr : ∀
  (this :
    ∃ (q : R[X]),
      Polynomial.map (algebraMap R Rₘ) q =
          p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R)) ∧
        q.natDegree =
            (p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))).natDegree ∧
          q.Monic),
  ∃ (m : ↥M), IsIntegral R (m • x)
Tactic: have :=
    lifts_and_natDegree_eq_and_monic (IsLocalization.scaleRoots_commonDenom_mem_lifts M p ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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 :
  ∀
    (this :
      ∃ (q : R[X]),
        Polynomial.map (algebraMap R Rₘ) q =
            p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R)) ∧
          q.natDegree =
              (p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))).natDegree ∧
            q.Monic),
    ∃ (m : ↥M), IsIntegral R (m • x)
⊢ ∃ (m : ↥M), IsIntegral R (m • x)
have inr₁ : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
Tactic: have :=
    lifts_and_natDegree_eq_and_monic (IsLocalization.scaleRoots_commonDenom_mem_lifts M p ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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 :
  ∀
    (this :
      ∃ (q : R[X]),
        Polynomial.map (algebraMap R Rₘ) q =
            p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R)) ∧
          q.natDegree =
              (p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))).natDegree ∧
            q.Monic),
    ∃ (m : ↥M), IsIntegral R (m • x)
inr₁ : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
⊢ ∃ (m : ↥M), IsIntegral R (m • x)
have inr₂ : (p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))).Monic
Tactic: have :=
    lifts_and_natDegree_eq_and_monic (IsLocalization.scaleRoots_commonDenom_mem_lifts M p ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
this :
  ∃ (q : R[X]),
    Polynomial.map (algebraMap R Rₘ) q =
        p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R)) ∧
      q.natDegree =
          (p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))).natDegree ∧
        q.Monic
⊢ ∃ (m : ↥M), IsIntegral R (m • x)
have inr : ∀ (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), ∃ (m : ↥M), IsIntegral R (m • x)
Tactic: obtain ⟨p', hp'₁, -, hp'₂⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ ∃ (m : ↥M), IsIntegral R (m • x)
have inr : eval₂ (algebraMap R S) (commonDenom M p.support p.coeff • x) p' = 0
Tactic: refine ⟨IsLocalization.commonDenom M p.support p.coeff, p', hp'₂, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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) (commonDenom M p.support p.coeff • x) p' = 0
have 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
Tactic: rw [IsScalarTower.algebraMap_eq R Rₘ S, ← Polynomial.eval₂_map, hp'₁, Submonoid.smul_def,
      Algebra.smul_def, IsScalarTower.algebraMap_apply R Rₘ S]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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ₘ)) p.leadingCoeff
have inr : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) 1
Tactic: rw [hp₁.leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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ₘ)
⊢ ∃ m ∈ M, IsIntegral R (m • x)
have 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)
Tactic: obtain ⟨p, hpm, hp⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
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
⊢ ∃ m ∈ M, IsIntegral R (m • x)
have hp₁ : ∃ 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
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ ∃ m ∈ M, IsIntegral R (m • x)
have 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)
Tactic: obtain ⟨m, hm, e⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
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ₘ)
⊢ ∃ (n : ℕ), IsIntegral R (r ^ n * x)
have a : Nontrivial S
Tactic: nontriviality S
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ ∃ (n : ℕ), IsIntegral R (r ^ n * x)
have 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)
Tactic: obtain ⟨p, hpm, hp⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
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
⊢ ∃ (n : ℕ), IsIntegral R (r ^ n * x)
have hp₁ : ∃ (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
Cleared hypotheses: hp