awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
a : R
b : S
b' : R
hb : (algebraMap R S : (a : R) → S) b' = b
h : (algebraMap R S : (a : R) → S) (a * b') = HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) b' : S)
h₁ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b' : S) =
    HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) b' : S)
h₂ h₃ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b' : S) =
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b' : S)
⊢ (algebraMap R S : (a : R) → S) (a * b') = a • b

Tactic:
rw [← hb, (algebraMap R S).map_mul, Algebra.smul_def]

Premises used: Algebra.algebraMap, Algebra.smul_def, RingHom.map_mul
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
a : S
⊢ ∃ (b : ↥M), IsInteger R (HMul.hMul (β := S) a ((algebraMap R S : (a : R) → S) (↑b : R) : S))

Tactic:
let ⟨⟨Num, denom⟩, h⟩ := IsLocalization.surj _ a
  ⟨denom, Set.mem_range.mpr ⟨Num, h.symm⟩⟩

Premises used: IsLocalization.IsInteger, Iff.mpr, Set.mem_range, IsLocalization.surj, HMul.hMul, Algebra.algebraMap, Exists, Exists.intro, Eq.symm, Subtype.val, DFunLike.coe, _private.0.IsLocalization.exists_integer_multiple'.match_1
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
a : S
simp_rw : ∃ (b : ↥M), IsInteger R (HMul.hMul (β := S) a ((algebraMap R S : (a : R) → S) (↑b : R) : S))
⊢ ∃ (b : ↥M), IsInteger R ((↑b : R) • a)

Tactic:
simp_rw [Algebra.smul_def, mul_comm _ a]

Premises used: mul_comm, Algebra.smul_def
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
a : S
⊢ ∃ (b : ↥M), IsInteger R (HMul.hMul (β := S) a ((algebraMap R S : (a : R) → S) (↑b : R) : S))

Tactic:
apply exists_integer_multiple'

Premises used: IsLocalization.exists_integer_multiple'
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
haveI : ∀ (this : (a : Prop) → Decidable a), ∃ (b : ↥M), ∀ i ∈ s, IsInteger R ((↑b : R) • f i)
⊢ ∃ (b : ↥M), ∀ i ∈ s, IsInteger R ((↑b : R) • f i)

Tactic:
haveI := Classical.propDecidable
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
⊢ ∃ (b : ↥M), ∀ i ∈ s, IsInteger R ((↑b : R) • f i)

Tactic:
⟨∏ i ∈ s, (sec M (f i)).2, fun i hi => ⟨?_, ?_⟩⟩

Premises used: IsLocalization.sec, Finset.prod, Exists.intro, Prod.snd
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
refine_1 : (i : ι) → (hi : i ∈ s) → R
refine_2 :
  ∀ (i : ι) (hi : i ∈ s),
    (algebraMap R S : (a : R) → S) ((↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (sec M (f i)).1) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑(∏ i ∈ s, (sec M (f i)).2) : R) (f i)
⊢ ∃ (b : ↥M), ∀ i ∈ s, IsInteger R ((↑b : R) • f i)

Tactic:
refine ⟨∏ i ∈ s, (sec M (f i)).2, fun i hi => ⟨?_, ?_⟩⟩
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ R

Tactic:
exact (∏ j ∈ s.erase i, (sec M (f j)).2) * (sec M (f i)).1

Premises used: IsLocalization.sec, Prod.fst, Finset.prod, Finset.erase, Prod.snd
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
refine_2 :
  ((↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (↑(sec M (f i)).2 : R)) • f i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑(∏ i ∈ s, (sec M (f i)).2) : R) (f i)
⊢ (algebraMap R S : (a : R) → S) ((↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (sec M (f i)).1) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑(∏ i ∈ s, (sec M (f i)).2) : R) (f i)

Tactic:
rw [map_mul, sec_spec', ← mul_assoc, ← (algebraMap R S).map_mul, ← Algebra.smul_def]

Premises used: Algebra.algebraMap, mul_assoc, IsLocalization.sec_spec', map_mul, Algebra.smul_def, RingHom.map_mul
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
refine_2 : (↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (↑(sec M (f i)).2 : R) = (↑(∏ i ∈ s, (sec M (f i)).2) : R)
⊢ ((↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (↑(sec M (f i)).2 : R)) • f i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑(∏ i ∈ s, (sec M (f i)).2) : R) (f i)

Tactic:
congr 2
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ (↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (↑(sec M (f i)).2 : R) = (↑(∏ i ∈ s, (sec M (f i)).2) : R)

Tactic:
_root_.trans ?_ (map_prod (Submonoid.subtype M) _ _).symm

Premises used: trans, map_prod, Submonoid.subtype, Eq.symm
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
refine_2 :
  (↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (↑(sec M (f i)).2 : R) =
    ∏ x ∈ s, (M.subtype : (a : ↥M) → R) (sec M (f x)).2
⊢ (↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (↑(sec M (f i)).2 : R) = (↑(∏ i ∈ s, (sec M (f i)).2) : R)

Tactic:
refine _root_.trans ?_ (map_prod (Submonoid.subtype M) _ _).symm

Premises used: trans, map_prod, Submonoid.subtype, Eq.symm
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
refine_2 : Eq.{u_1 + 1} (α := R) (∏ x ∈ s, (↑(sec M (f x)).2 : R)) (∏ x ∈ s, (M.subtype : (a : ↥M) → R) (sec M (f x)).2)
⊢ (↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (↑(sec M (f i)).2 : R) =
    ∏ x ∈ s, (M.subtype : (a : ↥M) → R) (sec M (f x)).2

Tactic:
rw [mul_comm, Submonoid.coe_finsetProd,
    -- Porting note: explicitly supplied `f`
    ← Finset.prod_insert (f := fun i => ((sec M (f i)).snd : R)) (s.notMem_erase i),
    Finset.insert_erase hi]

Premises used: Finset.prod_insert, Submonoid.coe_finsetProd, mul_comm, Finset.notMem_erase, Finset.insert_erase
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ Eq.{u_1 + 1} (α := R) (∏ x ∈ s, (↑(sec M (f x)).2 : R)) (∏ x ∈ s, (M.subtype : (a : ↥M) → R) (sec M (f x)).2)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
inst_4 : Finite ι
f : ι → S
intro : ∀ (val : Fintype ι), ∃ (b : ↥M), ∀ (i : ι), IsInteger R ((↑b : R) • f i)
⊢ ∃ (b : ↥M), ∀ (i : ι), IsInteger R ((↑b : R) • f i)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
inst_4 : Finite ι
f : ι → S
val : Fintype ι
intro :
  ∀ (b : ↥M) (hb : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → IsInteger R ((↑b : R) • f i)),
    ∃ (b : ↥M), ∀ (i : ι), IsInteger R ((↑b : R) • f i)
⊢ ∃ (b : ↥M), ∀ (i : ι), IsInteger R ((↑b : R) • f i)

Tactic:
obtain ⟨b, hb⟩ := exist_integer_multiples M Finset.univ f

Premises used: Finset.univ, IsLocalization.exist_integer_multiples
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
inst_4 : Finite ι
f : ι → S
val : Fintype ι
b : ↥M
hb : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → IsInteger R ((↑b : R) • f i)
⊢ ∃ (b : ↥M), ∀ (i : ι), IsInteger R ((↑b : R) • f i)

Tactic:
⟨b, fun i => hb i (Finset.mem_univ _)⟩

Premises used: Finset.mem_univ, Exists.intro
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
inst_4 : Finite ι
f : ι → S
val : Fintype ι
b : ↥M
hb : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → IsInteger R ((↑b : R) • f i)
⊢ ∃ (b : ↥M), ∀ (i : ι), IsInteger R ((↑b : R) • f i)

Tactic:
exact ⟨b, fun i => hb i (Finset.mem_univ _)⟩
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
s : Finset S
⊢ ∃ (b : ↥M), ∀ a ∈ s, IsInteger R ((↑b : R) • a)

Tactic:
exist_integer_multiples M s id

Premises used: id, IsLocalization.exist_integer_multiples
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
i : ↥s
⊢ (algebraMap R S : (a : R) → S) (integerMultiple M s f i) = commonDenom M s f • f (↑i : ι)

Tactic:
((exist_integer_multiples M s f).choose_spec _ i.prop).choose_spec

Premises used: Exists.choose_spec, IsLocalization.integerMultiple, Subtype.prop, IsLocalization.exist_integer_multiples
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : DecidableEq R
s : Finset S
rw :
  Set.image.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S)
      ((fun (t : ↥s) ↦ integerMultiple M s id t) '' (↑s.attach : Set ↥s)) =
    commonDenomOfFinset M s • (↑s : Set S)
⊢ (⇑(algebraMap R S) : (a : R) → S) '' (↑(Finset.image (fun (t : ↥s) ↦ integerMultiple M s id t) s.attach) : Set R) =
    commonDenomOfFinset M s • (↑s : Set S)

Tactic:
rw [Finset.coe_image]

Premises used: Finset.coe_image
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : DecidableEq R
s : Finset S
h :
  ∀ (x : S),
    Membership.mem (γ := Set S)
        (Set.image.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S)
          ((fun (t : ↥s) ↦ integerMultiple M s id t) '' (↑s.attach : Set ↥s)))
        x ↔
      x ∈ commonDenomOfFinset M s • (↑s : Set S)
⊢ Set.image.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S)
      ((fun (t : ↥s) ↦ integerMultiple M s id t) '' (↑s.attach : Set ↥s)) =
    commonDenomOfFinset M s • (↑s : Set S)

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : DecidableEq R
s : Finset S
x : S
h :
  Membership.mem (γ := Set S)
      (Set.image.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S)
        ((fun (t : ↥s) ↦ integerMultiple M s id t) '' (↑s.attach : Set ↥s)))
      x →
    x ∈ commonDenomOfFinset M s • (↑s : Set S)
h₁ :
  x ∈ commonDenomOfFinset M s • (↑s : Set S) →
    Membership.mem (γ := Set S)
      (Set.image.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S)
        ((fun (t : ↥s) ↦ integerMultiple M s id t) '' (↑s.attach : Set ↥s)))
      x
⊢ Membership.mem (γ := Set S)
      (Set.image.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S)
        ((fun (t : ↥s) ↦ integerMultiple M s id t) '' (↑s.attach : Set ↥s)))
      x ↔
    x ∈ commonDenomOfFinset M s • (↑s : Set S)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : DecidableEq R
s : Finset S
x : ↥s
h : commonDenom M s id • id (↑x : S) ∈ commonDenomOfFinset M s • (↑s : Set S)
⊢ Membership.mem (α := S) (commonDenomOfFinset M s • (↑s : Set S))
    ((algebraMap R S : (a : R) → S) ((fun (t : ↥s) ↦ integerMultiple M s id t) x) : S)

Tactic:
rw [map_integerMultiple]

Premises used: IsLocalization.map_integerMultiple
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : DecidableEq R
s : Finset S
x : ↥s
⊢ commonDenom M s id • id (↑x : S) ∈ commonDenomOfFinset M s • (↑s : Set S)

Tactic:
Set.mem_image_of_mem _ x.prop

Premises used: Set.Mem, Set.mem_image_of_mem, Subtype.prop
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : DecidableEq R
s : Finset S
x : ↥s
⊢ commonDenom M s id • id (↑x : S) ∈ commonDenomOfFinset M s • (↑s : Set S)

Tactic:
exact Set.mem_image_of_mem _ x.prop

Premises used: Set.mem_image_of_mem, Subtype.prop
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : DecidableEq R
s : Finset S
x : S
hx : x ∈ (↑s : Set S)
⊢ Membership.mem (γ := Set S)
    (Set.image.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S)
      ((fun (t : ↥s) ↦ integerMultiple M s id t) '' (↑s.attach : Set ↥s)))
    ((fun (x : S) ↦ (↑(commonDenomOfFinset M s) : R) • x) x)

Tactic:
⟨_, ⟨⟨x, hx⟩, s.mem_attach _, rfl⟩, map_integerMultiple M s id _⟩

Premises used: Set.Mem, setOf, Finset.mem_attach, id, IsLocalization.map_integerMultiple, Subtype.mk, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : DecidableEq R
s : Finset S
x : S
hx : x ∈ (↑s : Set S)
⊢ Membership.mem (γ := Set S)
    (Set.image.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S)
      ((fun (t : ↥s) ↦ integerMultiple M s id t) '' (↑s.attach : Set ↥s)))
    ((fun (x : S) ↦ (↑(commonDenomOfFinset M s) : R) • x) x)

Tactic:
exact ⟨_, ⟨⟨x, hx⟩, s.mem_attach _, rfl⟩, map_integerMultiple M s id _⟩
-- 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
inst_3 : IsLocalization M S
p : S[X]
obtain :
  ∀ (b : R) (hb : b ∈ (↑M : Set R))
    (h :
      IsInteger.{u_1, u_2} R[X]
        (HSMul.hSMul (α := R[X])
          ((↑(Subtype.mk (p := fun (x : R[X]) ↦
                  Membership.mem (γ := Submonoid R[X]) (Submonoid.map (F := R →+* R[X]) C M) x) ((C : (a : R) → R[X]) b)
                  ⋯) :
              R[X]) :
            R[X])
          p)),
    ∃ b ∈ M, ∃ (q : R[X]), Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support
⊢ ∃ b ∈ M, ∃ (q : R[X]), Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support

Tactic:
obtain ⟨⟨_, b, hb, rfl⟩, h⟩ := exists_integer_multiple (Submonoid.map C M) p

Premises used: Polynomial.C, Submonoid.map, IsLocalization.exists_integer_multiple, rfl
-- 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
inst_3 : IsLocalization M S
p : S[X]
b : R
hb : b ∈ (↑M : Set R)
h :
  IsInteger.{u_1, u_2} R[X]
    (HSMul.hSMul (α := R[X])
      ((↑(Subtype.mk (p := fun (x : R[X]) ↦
              Membership.mem (γ := Submonoid R[X]) (Submonoid.map (F := R →+* R[X]) C M) x) ((C : (a : R) → R[X]) b)
              ⋯) :
          R[X]) :
        R[X])
      p)
⊢ IsInteger.{u_1, u_2} R[X] (b • p)

Tactic:
rw [Subtype.coe_mk, C_eq_algebraMap, algebraMap_smul] at h

Premises used: Subtype.coe_mk, algebraMap_smul, Polynomial.C_eq_algebraMap
-- 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
inst_3 : IsLocalization M S
p : S[X]
b : R
hb : b ∈ (↑M : Set R)
h : IsInteger.{u_1, u_2} R[X] (b • p)
obtain :
  ∀ (q' : R[X]) (h₁ : Polynomial.map (algebraMap R S) q' = b • p) (h₂ : q'.support = (b • p).support),
    ∃ b ∈ M, ∃ (q : R[X]), Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support
⊢ ∃ b ∈ M, ∃ (q : R[X]), Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support

Tactic:
obtain ⟨q', h₁, h₂⟩ := exists_support_eq_of_mem_lifts h

Premises used: Polynomial.exists_support_eq_of_mem_lifts
-- 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
inst_3 : IsLocalization M S
p : S[X]
b : R
hb : b ∈ (↑M : Set R)
h : IsInteger.{u_1, u_2} R[X] (b • p)
q' : R[X]
h₁ : Polynomial.map (algebraMap R S) q' = b • p
h₂ : q'.support = (b • p).support
⊢ ∃ b ∈ M, ∃ (q : R[X]), Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support

Tactic:
⟨b, hb, q', h₁, h₂ ▸ support_smul b p⟩

Premises used: Eq.rec, Polynomial.support_smul, And.intro, Exists.intro, Eq.symm
-- 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
inst_3 : IsLocalization M S
p : S[X]
b : R
hb : b ∈ (↑M : Set R)
h : IsInteger.{u_1, u_2} R[X] (b • p)
q' : R[X]
h₁ : Polynomial.map (algebraMap R S) q' = b • p
h₂ : q'.support = (b • p).support
⊢ ∃ b ∈ M, ∃ (q : R[X]), Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support

Tactic:
exact ⟨b, hb, q', h₁, h₂ ▸ support_smul b 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
inst_3 : IsLocalization M S
p : S[X]
⊢ ∃ b ∈ M, Polynomial.map (algebraMap R S) (integerNormalization M p) = b • p

Tactic:
let e := exists_integer_polynomial_multiple_and_support_subset M p
  ⟨e.choose, e.choose_spec.1, e.choose_spec.2.choose_spec.1⟩

Premises used: Exists.choose_spec, _private.0.IsLocalization.exists_integer_polynomial_multiple_and_support_subset, And.right, And.left, And.intro, Exists.intro, Exists.choose
-- 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
inst_3 : IsLocalization M S
p : S[X]
⊢ (integerNormalization M p).support ⊆ p.support

Tactic:
(exists_integer_polynomial_multiple_and_support_subset M p).choose_spec.2.choose_spec.2

Premises used: Exists.choose_spec, Set.Mem, setOf, _private.0.IsLocalization.exists_integer_polynomial_multiple_and_support_subset, And.right, IsLocalization.integerNormalization
-- 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
inst_3 : IsLocalization M S
p : S[X]
i : ℕ
h : p.coeff i = 0
⊢ coeffIntegerNormalization M p i = 0

Tactic:
notMem_support_iff.mp <| Finset.not_mem_subset (integerNormalization_support M p) <|
    notMem_support_iff.mpr h

Premises used: Iff.mpr, IsLocalization.integerNormalization_support, IsLocalization.coeffIntegerNormalization, Polynomial.notMem_support_iff, Finset.not_mem_subset, Iff.mp
-- 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
inst_3 : IsLocalization M S
p : S[X]
i : ℕ
h : coeffIntegerNormalization M p i ≠ 0
contrapose : ∀ (h : i ∉ p.support), coeffIntegerNormalization M p i = 0
⊢ i ∈ p.support

Tactic:
contrapose h
-- 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
inst_3 : IsLocalization M S
p : S[X]
i : ℕ
h : i ∉ p.support
⊢ p.coeff i = 0

Tactic:
simp only [mem_support_iff, ne_eq, not_not] at h

Premises used: Classical.not_not, Polynomial.mem_support_iff, ne_eq
-- 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
inst_3 : IsLocalization M S
p : S[X]
i : ℕ
h : p.coeff i = 0
⊢ coeffIntegerNormalization M p i = 0

Tactic:
coeffIntegerNormalization_of_coeff_zero M p i h

Premises used: IsLocalization.coeffIntegerNormalization_of_coeff_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
inst_3 : IsLocalization M S
p : S[X]
i : ℕ
h : p.coeff i = 0
⊢ coeffIntegerNormalization M p i = 0

Tactic:
exact coeffIntegerNormalization_of_coeff_zero M p i h

Premises used: IsLocalization.coeffIntegerNormalization_of_coeff_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
inst_3 : IsLocalization M S
p : S[X]
i : ℕ
⊢ (integerNormalization M p).coeff i = coeffIntegerNormalization M p i

Tactic:
rfl

Premises used: IsLocalization.coeffIntegerNormalization, rfl
-- 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
inst_3 : IsLocalization M S
inst_4 : IsDomain R
hM : M ≤ nonZeroDivisors R
p : S[X]
obtain :
  ∀ (w : R) (hb₁ : w ∈ M) (hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = w • p),
    integerNormalization M p = 0 ↔ p = 0
⊢ integerNormalization M p = 0 ↔ p = 0

Tactic:
obtain ⟨_, hb₁, hb₂⟩ := integerNormalization_spec M p

Premises used: IsLocalization.integerNormalization_spec
-- 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
inst_3 : IsLocalization M S
inst_4 : IsDomain R
hM : M ≤ nonZeroDivisors R
p : S[X]
w : R
hb₁ : w ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = w • p
this_1 : IsDomain S := ⋯
this : FaithfulSMul R S := ⋯
rw : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S[X]) (⇑(mapRingHom (algebraMap R S)) : (a : R[X]) → S[X])

Tactic:
rw [coe_mapRingHom, map_injective_iff]

Premises used: Polynomial.map_injective_iff, Polynomial.coe_mapRingHom