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
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 := ⋯
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
IsLocalization.injective S hM

Premises used: IsLocalization.injective
-- 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 := ⋯
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
exact IsLocalization.injective S hM

Premises used: IsLocalization.injective
-- 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_2 : FaithfulSMul R S := ⋯
this : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S[X])
  (⇑(mapRingHom (algebraMap R S)) : (a : R[X]) → S[X]) :=
  ⋯
rw : w • p = 0 ↔ p = 0
⊢ integerNormalization M p = 0 ↔ p = 0

Tactic:
rw [← _root_.map_eq_zero_iff (mapRingHom (algebraMap R S)) this, coe_mapRingHom, hb₂]

Premises used: Algebra.algebraMap, Polynomial.coe_mapRingHom, map_eq_zero_iff, Polynomial.mapRingHom
-- 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_2 : FaithfulSMul R S := ⋯
this : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S[X])
  (⇑(mapRingHom (algebraMap R S)) : (a : R[X]) → S[X]) :=
  ⋯
⊢ w • p = 0 ↔ p = 0

Tactic:
smul_eq_zero_iff_right <| nonZeroDivisors.ne_zero (hM hb₁)

Premises used: nonZeroDivisors.ne_zero, smul_eq_zero_iff_right
-- 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_2 : FaithfulSMul R S := ⋯
this : Function.Injective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S[X])
  (⇑(mapRingHom (algebraMap R S)) : (a : R[X]) → S[X]) :=
  ⋯
⊢ w • p = 0 ↔ p = 0

Tactic:
exact smul_eq_zero_iff_right <| nonZeroDivisors.ne_zero (hM hb₁)

Premises used: nonZeroDivisors.ne_zero, smul_eq_zero_iff_right
-- 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) (hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = b • p),
    ∃ (b : ↥M), Polynomial.map (algebraMap R S) (integerNormalization M p) = (↑b : R) • p
⊢ ∃ (b : ↥M), Polynomial.map (algebraMap R S) (integerNormalization M p) = (↑b : R) • p

Tactic:
obtain ⟨b, 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
p : S[X]
b : R
hb₁ : b ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = b • p
⊢ ∃ (b : ↥M), Polynomial.map (algebraMap R S) (integerNormalization M p) = (↑b : R) • p

Tactic:
⟨⟨b, hb₁⟩, hb₂⟩

Premises used: Subtype.mk, Exists.intro
-- 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
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = b • p
⊢ ∃ (b : ↥M), Polynomial.map (algebraMap R S) (integerNormalization M p) = (↑b : R) • p

Tactic:
exact ⟨⟨b, hb₁⟩, hb₂⟩
-- 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
R' : Type u_3
inst_4 : CommRing R'
g : S →+* R'
p : S[X]
x : R'
hx : eval₂ g x p = 0
b : R
hb₁ : b ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = b • p
rw : eval₂ g x (b • p) = 0
rw₁ : eval₂ g x (HSMul.hSMul (α := S) ((algebraMap R S : (a : R) → S) b : S) p) = 0
rw₂ : HMul.hMul (α := R') ((g : (a : S) → R') ((algebraMap R S : (a : R) → S) b : S) : R') (eval₂ g x p) = 0
rw₃ : HMul.hMul (α := R') (β := R') ((g : (a : S) → R') ((algebraMap R S : (a : R) → S) b : S) : R') (0 : R') = 0
rw₄ rw₅ : Eq.{u_3 + 1} (α := R') 0 0
⊢ eval₂ g x (Polynomial.map (algebraMap R S) (integerNormalization M p)) = 0

Tactic:
rw [hb₂, ← IsScalarTower.algebraMap_smul S b p, eval₂_smul, hx, mul_zero]

Premises used: MulZeroClass.mul_zero, IsScalarTower.algebraMap_smul, Polynomial.eval₂_smul
-- 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
R' : Type u_3
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : Algebra S R'
inst_7 : IsScalarTower R S R'
p : S[X]
x : R'
hx : Eq.{u_3 + 1} (α := R') ((aeval x : (a : S[X]) → R') p : R') (0 : R')
rwa : eval₂ (algebraMap R R') x (integerNormalization M p) = 0
rwa₁ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S R') (algebraMap R S)) x
      (integerNormalization M p) =
    0
rwa₂ : Eq.{u_3 + 1} (α := R') 0 0
hx₁ : eval₂ (algebraMap S R') x p = 0
rwa₃ : Eq.{u_3 + 1} (α := R') 0 0
hx₂ hx₃ hx₄ : eval₂ (algebraMap S R') x p = 0
⊢ Eq.{u_3 + 1} (α := R') ((aeval x : (a : R[X]) → R') (integerNormalization M p) : R') (0 : R')

Tactic:
rwa [aeval_def, IsScalarTower.algebraMap_eq R S R', integerNormalization_eval₂_eq_zero]

Premises used: Polynomial.aeval_def, IsScalarTower.algebraMap_eq, IsLocalization.integerNormalization_eval₂_eq_zero
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
K : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
p : K[X]
⊢ Eq.{u_3 + 1} (α := A[X]) (integerNormalization (nonZeroDivisors A) p) 0 ↔ p = 0

Tactic:
IsLocalization.integerNormalization_eq_zero_iff le_rfl p

Premises used: le_rfl, IsLocalization.integerNormalization_eq_zero_iff
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
K : Type u_4
C : Type u_5
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : CommRing C
inst_6 : Algebra A C
inst_7 : Algebra K C
inst_8 : IsScalarTower A K C
x : C
mp : IsAlgebraic A x → IsAlgebraic K x
mpr : IsAlgebraic K x → IsAlgebraic A x
⊢ IsAlgebraic A x ↔ IsAlgebraic K x

Tactic:
constructor
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
K : Type u_4
C : Type u_5
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : CommRing C
inst_6 : Algebra A C
inst_7 : Algebra K C
inst_8 : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : Eq.{u_5 + 1} (α := C) ((aeval x : (a : A[X]) → C) p : C) (0 : C)
⊢ IsAlgebraic K x

Tactic:
⟨p.map (algebraMap A K), fun h => hp (Polynomial.ext fun i => ?_), ?_⟩

Premises used: Algebra.algebraMap, IsAlgebraic, Polynomial.ext, And.intro, Exists.intro, Polynomial.map
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
K : Type u_4
C : Type u_5
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : CommRing C
inst_6 : Algebra A C
inst_7 : Algebra K C
inst_8 : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : Eq.{u_5 + 1} (α := C) ((aeval x : (a : A[X]) → C) p : C) (0 : C)
mp : ∀ (h : Eq (α := K[X]) (Polynomial.map (algebraMap A K) p) 0) (i : ℕ), p.coeff i = coeff 0 i
mp₁ : Eq.{u_5 + 1} (α := C) ((aeval x : (a : K[X]) → C) (Polynomial.map (algebraMap A K) p) : C) (0 : C)
⊢ IsAlgebraic K x

Tactic:
refine ⟨p.map (algebraMap A K), fun h => hp (Polynomial.ext fun i => ?_), ?_⟩
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
K : Type u_4
C : Type u_5
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : CommRing C
inst_6 : Algebra A C
inst_7 : Algebra K C
inst_8 : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : Eq.{u_5 + 1} (α := C) ((aeval x : (a : A[X]) → C) p : C) (0 : C)
h : Eq (α := K[X]) (Polynomial.map (algebraMap A K) p) 0
i : ℕ
⊢ coeff (Polynomial.map (algebraMap A K) p) i = 0

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
K : Type u_4
C : Type u_5
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : CommRing C
inst_6 : Algebra A C
inst_7 : Algebra K C
inst_8 : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : Eq.{u_5 + 1} (α := C) ((aeval x : (a : A[X]) → C) p : C) (0 : C)
h : Eq (α := K[X]) (Polynomial.map (algebraMap A K) p) 0
i : ℕ
⊢ Eq.{u_4 + 1} (α := K) ((algebraMap A K : (a : A) → K) (p.coeff i) : K) (0 : K)

Tactic:
have : algebraMap A K (p.coeff i) = 0 :=
        _root_.trans (Polynomial.coeff_map _ _).symm (by simp [h])
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
K : Type u_4
C : Type u_5
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : CommRing C
inst_6 : Algebra A C
inst_7 : Algebra K C
inst_8 : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : Eq.{u_5 + 1} (α := C) ((aeval x : (a : A[X]) → C) p : C) (0 : C)
h : Eq (α := K[X]) (Polynomial.map (algebraMap A K) p) 0
i : ℕ
this : Eq.{u_4 + 1} (α := K) ((algebraMap A K : (a : A) → K) (p.coeff i) : K) (0 : K)
⊢ p.coeff i = coeff 0 i

Tactic:
to_map_eq_zero_iff.mp this

Premises used: IsFractionRing.to_map_eq_zero_iff, Polynomial.coeff, Iff.mp
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
K : Type u_4
C : Type u_5
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : CommRing C
inst_6 : Algebra A C
inst_7 : Algebra K C
inst_8 : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : Eq.{u_5 + 1} (α := C) ((aeval x : (a : A[X]) → C) p : C) (0 : C)
h : Eq (α := K[X]) (Polynomial.map (algebraMap A K) p) 0
i : ℕ
this : Eq.{u_4 + 1} (α := K) ((algebraMap A K : (a : A) → K) (p.coeff i) : K) (0 : K)
⊢ p.coeff i = coeff 0 i

Tactic:
exact to_map_eq_zero_iff.mp this

Premises used: IsFractionRing.to_map_eq_zero_iff, Iff.mp
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
K : Type u_4
C : Type u_5
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : CommRing C
inst_6 : Algebra A C
inst_7 : Algebra K C
inst_8 : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : Eq.{u_5 + 1} (α := C) ((aeval x : (a : A[X]) → C) p : C) (0 : C)
⊢ Eq.{u_5 + 1} (α := C) ((aeval x : (a : K[X]) → C) (Polynomial.map (algebraMap A K) p) : C) (0 : C)

Tactic:
(Polynomial.aeval_map_algebraMap K _ _).trans px

Premises used: Polynomial.aeval_map_algebraMap, Eq.trans
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
K : Type u_4
C : Type u_5
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : CommRing C
inst_6 : Algebra A C
inst_7 : Algebra K C
inst_8 : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : Eq.{u_5 + 1} (α := C) ((aeval x : (a : A[X]) → C) p : C) (0 : C)
⊢ Eq.{u_5 + 1} (α := C) ((aeval x : (a : K[X]) → C) (Polynomial.map (algebraMap A K) p) : C) (0 : C)

Tactic:
exact (Polynomial.aeval_map_algebraMap K _ _).trans px

Premises used: Polynomial.aeval_map_algebraMap, Eq.trans
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
K : Type u_4
C : Type u_5
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : CommRing C
inst_6 : Algebra A C
inst_7 : Algebra K C
inst_8 : IsScalarTower A K C
x : C
p : K[X]
hp : p ≠ 0
px : Eq.{u_5 + 1} (α := C) ((aeval x : (a : K[X]) → C) p : C) (0 : C)
⊢ IsAlgebraic A x

Tactic:
⟨integerNormalization _ p, mt integerNormalization_eq_zero_iff.mp hp,
        integerNormalization_aeval_eq_zero _ p px⟩

Premises used: IsAlgebraic, IsFractionRing.integerNormalization_eq_zero_iff, mt, IsLocalization.integerNormalization_aeval_eq_zero, And.intro, Exists.intro, Iff.mp, IsLocalization.integerNormalization
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
K : Type u_4
C : Type u_5
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : CommRing C
inst_6 : Algebra A C
inst_7 : Algebra K C
inst_8 : IsScalarTower A K C
x : C
p : K[X]
hp : p ≠ 0
px : Eq.{u_5 + 1} (α := C) ((aeval x : (a : K[X]) → C) p : C) (0 : C)
⊢ IsAlgebraic A x

Tactic:
exact
      ⟨integerNormalization _ p, mt integerNormalization_eq_zero_iff.mp hp,
        integerNormalization_aeval_eq_zero _ p px⟩
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
K : Type u_4
C : Type u_5
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : CommRing C
inst_6 : Algebra A C
inst_7 : Algebra K C
inst_8 : IsScalarTower A K C
⊢ Algebra.IsAlgebraic A C ↔ Algebra.IsAlgebraic K C

Tactic:
⟨fun h => ⟨fun x => (isAlgebraic_iff A K C).mp (h.isAlgebraic x)⟩,
   fun h => ⟨fun x => (isAlgebraic_iff A K C).mpr (h.isAlgebraic x)⟩⟩

Premises used: Iff.mpr, Algebra.IsAlgebraic.isAlgebraic, Algebra.IsAlgebraic.mk, Iff.intro, Iff.mp, IsFractionRing.isAlgebraic_iff
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
pos :
  ∀ (triv : Eq.{u_7 + 1} (α := Rₘ) 1 0),
    IsIntegralElem.{u_7, u_8} (R := Rₘ) (A := Sₘ) (IsLocalization.map Sₘ f ⋯ : Rₘ →+* Sₘ)
      ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
neg :
  ∀ (triv : ¬Eq.{u_7 + 1} (α := Rₘ) 1 0),
    IsIntegralElem.{u_7, u_8} (R := Rₘ) (A := Sₘ) (IsLocalization.map Sₘ f ⋯ : Rₘ →+* Sₘ)
      ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
⊢ IsIntegralElem.{u_7, u_8} (R := Rₘ) (A := Sₘ) (IsLocalization.map Sₘ f ⋯ : Rₘ →+* Sₘ)
    ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)

Tactic:
by_cases triv : (1 : Rₘ) = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
triv : Eq.{u_7 + 1} (α := Rₘ) 1 0
⊢ IsIntegralElem.{u_7, u_8} (R := Rₘ) (A := Sₘ) (IsLocalization.map Sₘ f ⋯ : Rₘ →+* Sₘ)
    ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)

Tactic:
⟨0, ⟨_root_.trans leadingCoeff_zero triv.symm, eval₂_zero _ _⟩⟩

Premises used: trans, Polynomial.eval₂_zero, Polynomial.leadingCoeff_zero, RingHom.IsIntegralElem, And.intro, Exists.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
triv : Eq.{u_7 + 1} (α := Rₘ) 1 0
⊢ IsIntegralElem.{u_7, u_8} (R := Rₘ) (A := Sₘ) (IsLocalization.map Sₘ f ⋯ : Rₘ →+* Sₘ)
    ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)

Tactic:
exact ⟨0, ⟨_root_.trans leadingCoeff_zero triv.symm, eval₂_zero _ _⟩⟩
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬Eq.{u_7 + 1} (α := Rₘ) 1 0
⊢ Nontrivial Rₘ

Tactic:
haveI : Nontrivial Rₘ := nontrivial_of_ne 1 0 triv
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬Eq.{u_7 + 1} (α := Rₘ) 1 0
this : Nontrivial Rₘ
neg :
  ∀ (b : Rₘ)
    (hb :
      HMul.hMul (α := Rₘ)
          ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) p.leadingCoeff hM) : R) : Rₘ) b =
        1),
    IsIntegralElem.{u_7, u_8} (R := Rₘ) (A := Sₘ) (IsLocalization.map Sₘ f ⋯ : Rₘ →+* Sₘ)
      ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
⊢ IsIntegralElem.{u_7, u_8} (R := Rₘ) (A := Sₘ) (IsLocalization.map Sₘ f ⋯ : Rₘ →+* Sₘ)
    ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)

Tactic:
obtain ⟨b, hb⟩ := isUnit_iff_exists_inv.mp (map_units Rₘ ⟨p.leadingCoeff, hM⟩)

Premises used: isUnit_iff_exists_inv, Polynomial.leadingCoeff, Subtype.mk, Iff.mp, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬Eq.{u_7 + 1} (α := Rₘ) 1 0
this : Nontrivial Rₘ
b : Rₘ
hb :
  HMul.hMul (α := Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) p.leadingCoeff hM) : R) : Rₘ) b =
    1
⊢ IsIntegralElem.{u_7, u_8} (R := Rₘ) (A := Sₘ) (IsLocalization.map Sₘ f ⋯ : Rₘ →+* Sₘ)
    ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)

Tactic:
⟨p.map (algebraMap R Rₘ) * C b, ⟨?_, ?_⟩⟩

Premises used: Polynomial.C, HMul.hMul, Algebra.algebraMap, RingHom.IsIntegralElem, And.intro, Exists.intro, Polynomial.map, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬Eq.{u_7 + 1} (α := Rₘ) 1 0
this : Nontrivial Rₘ
b : Rₘ
hb :
  HMul.hMul (α := Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) p.leadingCoeff hM) : R) : Rₘ) b =
    1
neg :
  (HMul.hMul (α := Rₘ[X]) (β := Rₘ[X]) (Polynomial.map (algebraMap R Rₘ) p) ((C : (a : Rₘ) → Rₘ[X]) b : Rₘ[X])).Monic
neg₁ :
  eval₂ (IsLocalization.map Sₘ f ⋯ : Rₘ →+* Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x)
      (HMul.hMul (α := Rₘ[X]) (β := Rₘ[X]) (Polynomial.map (algebraMap R Rₘ) p) ((C : (a : Rₘ) → Rₘ[X]) b : Rₘ[X])) =
    0
⊢ IsIntegralElem.{u_7, u_8} (R := Rₘ) (A := Sₘ) (IsLocalization.map Sₘ f ⋯ : Rₘ →+* Sₘ)
    ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)

Tactic:
refine ⟨p.map (algebraMap R Rₘ) * C b, ⟨?_, ?_⟩⟩
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬Eq.{u_7 + 1} (α := Rₘ) 1 0
this : Nontrivial Rₘ
b : Rₘ
hb :
  HMul.hMul (α := Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) p.leadingCoeff hM) : R) : Rₘ) b =
    1
⊢ (HMul.hMul (α := Rₘ[X]) (β := Rₘ[X]) (Polynomial.map (algebraMap R Rₘ) p) ((C : (a : Rₘ) → Rₘ[X]) b : Rₘ[X])).Monic

Tactic:
monic_mul_C_of_leadingCoeff_mul_eq_one ?_

Premises used: Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬Eq.{u_7 + 1} (α := Rₘ) 1 0
this : Nontrivial Rₘ
b : Rₘ
hb :
  HMul.hMul (α := Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) p.leadingCoeff hM) : R) : Rₘ) b =
    1
neg : leadingCoeff (Polynomial.map (algebraMap R Rₘ) p) * b = 1
⊢ (HMul.hMul (α := Rₘ[X]) (β := Rₘ[X]) (Polynomial.map (algebraMap R Rₘ) p) ((C : (a : Rₘ) → Rₘ[X]) b : Rₘ[X])).Monic

Tactic:
refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_

Premises used: Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬Eq.{u_7 + 1} (α := Rₘ) 1 0
this : Nontrivial Rₘ
b : Rₘ
hb :
  HMul.hMul (α := Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) p.leadingCoeff hM) : R) : Rₘ) b =
    1
neg : Ne.{u_7 + 1} (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) p.leadingCoeff : Rₘ) (0 : Rₘ)
⊢ leadingCoeff (Polynomial.map (algebraMap R Rₘ) p) * b = 1

Tactic:
rwa [leadingCoeff_map_of_leadingCoeff_ne_zero (algebraMap R Rₘ)]

Premises used: Algebra.algebraMap, Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬Eq.{u_7 + 1} (α := Rₘ) 1 0
this : Nontrivial Rₘ
b : Rₘ
hb :
  HMul.hMul (α := Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) p.leadingCoeff hM) : R) : Rₘ) b =
    1
⊢ Ne.{u_7 + 1} (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) p.leadingCoeff : Rₘ) (0 : Rₘ)

Tactic:
fun hfp => zero_ne_one
      (_root_.trans (zero_mul b).symm (hfp ▸ hb) : (0 : Rₘ) = 1)

Premises used: trans, MulZeroClass.zero_mul, Eq.rec, zero_ne_one, Eq.symm, Not