awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsIntegral
M : Submonoid R
⊢ RingHom.IsIntegral.{u_5, u_6} (R := Localization (M := R) M) (A :=
    Localization (Submonoid.map (F := R →* S) (↑f : R →* S) M))
    (IsLocalization.map (Localization (Submonoid.map (F := R →* S) (↑f : R →* S) M)) f ⋯)

Tactic:
let _ := f.toAlgebra
  have : Algebra.IsIntegral R S := ⟨hf⟩
  have : IsLocalization (Algebra.algebraMapSubmonoid S M)
    (Localization (Submonoid.map (f : R →* S) M)) := Localization.isLocalization
  isIntegral_localization

Premises used: isIntegral_localization, MonoidHomClass.toMonoidHom, Submonoid.map, Localization.isLocalization, Algebra.algebraMapSubmonoid, Algebra.IsIntegral.mk, RingHom.toAlgebra
-- Module: Mathlib.RingTheory.Localization.Integral
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
rw :
  ∀ (n : ℕ),
    Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
      ((p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))).coeff n)
⊢ Membership.mem (γ := Subsemiring Rₘ[X]) (lifts (algebraMap R Rₘ))
    (p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R)))

Tactic:
rw [Polynomial.lifts_iff_coeff_lifts]

Premises used: Polynomial.lifts_iff_coeff_lifts
-- Module: Mathlib.RingTheory.Localization.Integral
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 : ℕ
rw :
  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))
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    ((p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))).coeff n)

Tactic:
rw [Polynomial.coeff_scaleRoots]

Premises used: Polynomial.coeff_scaleRoots
-- Module: Mathlib.RingTheory.Localization.Integral
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 : ℕ
pos :
  ∀ (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))
neg :
  ∀ (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))
⊢ 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))

Tactic:
by_cases h₁ : n ∈ p.support

Premises used: Polynomial.support
-- Module: Mathlib.RingTheory.Localization.Integral
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
pos :
  ∀ (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))
neg :
  ∀ (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))
⊢ 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))

Tactic:
by_cases h₂ : n = p.natDegree

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Localization.Integral
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
pos :
  ∀ (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))
neg :
  ∀ (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))
⊢ 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))

Tactic:
on_goal 1 => by_cases h₂ : n = p.natDegree

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Localization.Integral
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)
pos₄ pos₅ pos₆ pos₇ :
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ)) p.leadingCoeff
⊢ 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))

Tactic:
rwa [h₂, Polynomial.coeff_natDegree, tsub_self, pow_zero, _root_.mul_one]

Premises used: Polynomial.coeff_natDegree, tsub_self, pow_zero, mul_one
-- Module: Mathlib.RingTheory.Localization.Integral
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
⊢ n + 1 ≤ p.natDegree

Tactic:
have : n + 1 ≤ p.natDegree := lt_of_le_of_ne (Polynomial.le_natDegree_of_mem_supp _ h₁) h₂
-- Module: Mathlib.RingTheory.Localization.Integral
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 (γ := 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)))
⊢ 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))

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]

Premises used: le_tsub_of_add_le_left, mul_assoc, pow_add, tsub_add_cancel_of_le, map_pow, pow_one, mul_comm
-- Module: Mathlib.RingTheory.Localization.Integral
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 (γ := 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)))
⊢ 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:
change _ ∈ (algebraMap R Rₘ).range

Premises used: Algebra.algebraMap, RingHom.range
-- Module: Mathlib.RingTheory.Localization.Integral
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ₘ)
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))
⊢ 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:
apply mul_mem

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.Localization.Integral
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.{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:
RingHom.mem_range_self _ _

Premises used: Set.Mem, RingHom.mem_range_self
-- Module: Mathlib.RingTheory.Localization.Integral
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.{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:
exact RingHom.mem_range_self _ _

Premises used: RingHom.mem_range_self
-- Module: Mathlib.RingTheory.Localization.Integral
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 (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ))
    ((↑(commonDenom M p.support p.coeff) : R) • p.coeff n)
⊢ 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:
rw [← Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Localization.Integral
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ₘ))
    ((↑(commonDenom M p.support p.coeff) : R) • p.coeff n)

Tactic:
⟨_, IsLocalization.map_integerMultiple M p.support p.coeff ⟨n, h₁⟩⟩

Premises used: Set.Mem, setOf, IsLocalization.map_integerMultiple, Polynomial.coeff, Subtype.mk, Exists.intro, Set.range, Polynomial.support
-- Module: Mathlib.RingTheory.Localization.Integral
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ₘ))
    ((↑(commonDenom M p.support p.coeff) : R) • p.coeff n)

Tactic:
exact ⟨_, IsLocalization.map_integerMultiple M p.support p.coeff ⟨n, h₁⟩⟩
-- Module: Mathlib.RingTheory.Localization.Integral
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
⊢ p.coeff n = 0

Tactic:
rw [Polynomial.notMem_support_iff] at h₁

Premises used: Polynomial.notMem_support_iff
-- Module: Mathlib.RingTheory.Localization.Integral
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
neg : Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : 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))

Tactic:
rw [h₁, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.RingTheory.Localization.Integral
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ₘ)) 0

Tactic:
zero_mem (algebraMap R Rₘ).range

Premises used: Algebra.algebraMap, Set.Mem, setOf, RingHom.range, ZeroMemClass.zero_mem, Set.range
-- Module: Mathlib.RingTheory.Localization.Integral
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ₘ)) 0

Tactic:
exact zero_mem (algebraMap R Rₘ).range

Premises used: Algebra.algebraMap, RingHom.range, ZeroMemClass.zero_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
hx : IsIntegral Rₘ x
inl : Subsingleton Rₘ → ∃ (m : ↥M), IsIntegral R (m • x)
inr : ∀ (nontriv : Nontrivial Rₘ), ∃ (m : ↥M), IsIntegral R (m • x)
⊢ ∃ (m : ↥M), IsIntegral R (m • x)

Tactic:
rcases subsingleton_or_nontrivial Rₘ with _ | nontriv

Premises used: subsingleton_or_nontrivial
-- 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
hx : IsIntegral Rₘ x
h : Subsingleton Rₘ
⊢ Subsingleton S

Tactic:
haveI := (algebraMap Rₘ S).codomain_trivial
-- 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
hx : IsIntegral Rₘ x
h : Subsingleton Rₘ
this : Subsingleton S
⊢ ∃ (m : ↥M), IsIntegral R (m • x)

Tactic:
⟨1, Polynomial.X, Polynomial.monic_X, Subsingleton.elim _ _⟩

Premises used: And.intro, Exists.intro, Subsingleton.elim, OfNat.ofNat, Polynomial.X, Polynomial.monic_X
-- 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
hx : IsIntegral Rₘ x
h : Subsingleton Rₘ
this : Subsingleton S
⊢ ∃ (m : ↥M), IsIntegral R (m • x)

Tactic:
exact ⟨1, Polynomial.X, Polynomial.monic_X, Subsingleton.elim _ _⟩
-- 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
hx : IsIntegral Rₘ x
nontriv : Nontrivial Rₘ
inr : ∀ (p : Rₘ[X]) (hp₁ : p.Monic) (hp₂ : eval₂ (algebraMap Rₘ S) x p = 0), ∃ (m : ↥M), IsIntegral R (m • x)
⊢ ∃ (m : ↥M), IsIntegral R (m • x)

Tactic:
obtain ⟨p, hp₁, hp₂⟩ := hx
-- 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 :
  ∀
    (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
inr₂ : (p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))).Monic
⊢ ∃ (m : ↥M), IsIntegral R (m • x)

Tactic:
have :=
    lifts_and_natDegree_eq_and_monic (IsLocalization.scaleRoots_commonDenom_mem_lifts M p ?_) ?_
-- 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
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
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)
⊢ ∃ (m : ↥M), IsIntegral R (m • x)

Tactic:
obtain ⟨p', hp'₁, -, hp'₂⟩ := this
-- 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
⊢ ∃ (m : ↥M), IsIntegral R (m • x)

Tactic:
⟨IsLocalization.commonDenom M p.support p.coeff, p', hp'₂, ?_⟩

Premises used: IsLocalization.commonDenom, Polynomial.coeff, And.intro, Exists.intro, Polynomial.support
-- 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) (commonDenom M p.support p.coeff • x) p' = 0
⊢ ∃ (m : ↥M), IsIntegral R (m • x)

Tactic:
refine ⟨IsLocalization.commonDenom M p.support p.coeff, p', hp'₂, ?_⟩