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
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
⊢ i ∈ p.support
have contrapose : ∀ (h : i ∉ p.support), coeffIntegerNormalization M p i = 0
Tactic: contrapose h
Cleared hypotheses: h
-- 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
inst_3 : IsLocalization M S
p : S[X]
i : ℕ
h : i ∉ p.support
⊢ coeffIntegerNormalization M p i = 0
have h₁ : p.coeff i = 0
Tactic: simp only [mem_support_iff, ne_eq, not_not] 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
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]
⊢ integerNormalization M p = 0 ↔ p = 0
have obtain : ∀ (w : R) (hb₁ : w ∈ M) (hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = w • p),
  integerNormalization M p = 0 ↔ p = 0
Tactic: obtain ⟨_, hb₁, hb₂⟩ := integerNormalization_spec 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
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[X]) (β := S[X]) (⇑(mapRingHom (algebraMap R S)) : (a : R[X]) → S[X])
have rw : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
Tactic: rw [coe_mapRingHom, map_injective_iff]
-- 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
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]) :=
  ⋯
⊢ integerNormalization M p = 0 ↔ p = 0
have rw : w • p = 0 ↔ p = 0
Tactic: rw [← _root_.map_eq_zero_iff (mapRingHom (algebraMap R S)) this, coe_mapRingHom, hb₂]
-- 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
inst_3 : IsLocalization M S
p : S[X]
⊢ ∃ (b : ↥M), Polynomial.map (algebraMap R S) (integerNormalization M p) = (↑b : R) • p
have 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
Tactic: obtain ⟨b, hb₁, hb₂⟩ := integerNormalization_spec 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
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
⊢ eval₂ g x (Polynomial.map (algebraMap R S) (integerNormalization M p)) = 0
have rw : eval₂ g x (b • p) = 0
Tactic: rw [hb₂, ← IsScalarTower.algebraMap_smul S b p, eval₂_smul, hx, mul_zero]
-- 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
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
⊢ eval₂ g x (Polynomial.map (algebraMap R S) (integerNormalization M p)) = 0
have rw₁ : eval₂ g x (HSMul.hSMul (α := S) ((algebraMap R S : (a : R) → S) b : S) p) = 0
Tactic: rw [hb₂, ← IsScalarTower.algebraMap_smul S b p, eval₂_smul, hx, mul_zero]
-- 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
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
⊢ eval₂ g x (Polynomial.map (algebraMap R S) (integerNormalization M p)) = 0
have rw₂ : HMul.hMul (α := R') ((g : (a : S) → R') ((algebraMap R S : (a : R) → S) b : S) : R') (eval₂ g x p) = 0
Tactic: rw [hb₂, ← IsScalarTower.algebraMap_smul S b p, eval₂_smul, hx, mul_zero]
-- 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
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
⊢ eval₂ g x (Polynomial.map (algebraMap R S) (integerNormalization M p)) = 0
have rw₃ : HMul.hMul (α := R') (β := R') ((g : (a : S) → R') ((algebraMap R S : (a : R) → S) b : S) : R') (0 : R') = 0
Tactic: rw [hb₂, ← IsScalarTower.algebraMap_smul S b p, eval₂_smul, hx, mul_zero]
-- 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
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
⊢ eval₂ g x (Polynomial.map (algebraMap R S) (integerNormalization M p)) = 0
have rw₄ : Eq.{u_3 + 1} (α := R') 0 0
Tactic: rw [hb₂, ← IsScalarTower.algebraMap_smul S b p, eval₂_smul, hx, mul_zero]
-- 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
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')
⊢ Eq.{u_3 + 1} (α := R') ((aeval x : (a : R[X]) → R') (integerNormalization M p) : R') (0 : R')
have rwa : eval₂ (algebraMap R R') x (integerNormalization M p) = 0
Tactic: rwa [aeval_def, IsScalarTower.algebraMap_eq R S R', integerNormalization_eval₂_eq_zero]
-- 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
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
⊢ Eq.{u_3 + 1} (α := R') ((aeval x : (a : R[X]) → R') (integerNormalization M p) : R') (0 : R')
have rwa₁ : eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S R') (algebraMap R S)) x
    (integerNormalization M p) =
  0
Tactic: rwa [aeval_def, IsScalarTower.algebraMap_eq R S R', integerNormalization_eval₂_eq_zero]
-- 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
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
⊢ Eq.{u_3 + 1} (α := R') ((aeval x : (a : R[X]) → R') (integerNormalization M p) : R') (0 : R')
have rwa₂ : Eq.{u_3 + 1} (α := R') 0 0
Tactic: rwa [aeval_def, IsScalarTower.algebraMap_eq R S R', integerNormalization_eval₂_eq_zero]
-- 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
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
⊢ Eq.{u_3 + 1} (α := R') ((aeval x : (a : R[X]) → R') (integerNormalization M p) : R') (0 : R')
have hx₁ : eval₂ (algebraMap S R') x p = 0
Tactic: rwa [aeval_def, IsScalarTower.algebraMap_eq R S R', integerNormalization_eval₂_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ IsAlgebraic A x ↔ IsAlgebraic K x
have mp : IsAlgebraic A x → IsAlgebraic K x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ IsAlgebraic A x ↔ IsAlgebraic K x
have mpr : IsAlgebraic K x → IsAlgebraic A x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
have mp : ∀ (h : Eq (α := K[X]) (Polynomial.map (algebraMap A K) p) 0) (i : ℕ), p.coeff i = coeff 0 i
Tactic: refine ⟨p.map (algebraMap A K), fun h => hp (Polynomial.ext fun i => ?_), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ IsAlgebraic K x
have mp₁ : Eq.{u_5 + 1} (α := C) ((aeval x : (a : K[X]) → C) (Polynomial.map (algebraMap A K) p) : C) (0 : C)
Tactic: refine ⟨p.map (algebraMap A K), fun h => hp (Polynomial.ext fun i => ?_), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
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 : ℕ
⊢ p.coeff i = coeff 0 i
have this : 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])
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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ₘ
⊢ IsIntegralElem.{u_7, u_8} (R := Rₘ) (A := Sₘ) (IsLocalization.map Sₘ f ⋯ : Rₘ →+* Sₘ)
    ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
have pos : ∀ (triv : Eq.{u_7 + 1} (α := Rₘ) 1 0),
  IsIntegralElem.{u_7, u_8} (R := Rₘ) (A := Sₘ) (IsLocalization.map Sₘ f sorry : Rₘ →+* Sₘ)
    ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
Tactic: by_cases triv : (1 : Rₘ) = 0
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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ₘ)
⊢ IsIntegralElem.{u_7, u_8} (R := Rₘ) (A := Sₘ) (IsLocalization.map Sₘ f ⋯ : Rₘ →+* Sₘ)
    ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
have neg : ∀ (triv : ¬Eq.{u_7 + 1} (α := Rₘ) 1 0),
  IsIntegralElem.{u_7, u_8} (R := Rₘ) (A := Sₘ) (IsLocalization.map Sₘ f sorry : Rₘ →+* Sₘ)
    ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
Tactic: by_cases triv : (1 : Rₘ) = 0
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
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ₘ)
have this : Nontrivial Rₘ
Tactic: haveI : Nontrivial Rₘ := nontrivial_of_ne 1 0 triv
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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ₘ
⊢ IsIntegralElem.{u_7, u_8} (R := Rₘ) (A := Sₘ) (IsLocalization.map Sₘ f ⋯ : Rₘ →+* Sₘ)
    ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
have 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 sorry : 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⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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ₘ)
have neg : (HMul.hMul (α := Rₘ[X]) (β := Rₘ[X]) (Polynomial.map (algebraMap R Rₘ) p) ((C : (a : Rₘ) → Rₘ[X]) b : Rₘ[X])).Monic
Tactic: refine ⟨p.map (algebraMap R Rₘ) * C b, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ IsIntegralElem.{u_7, u_8} (R := Rₘ) (A := Sₘ) (IsLocalization.map Sₘ f ⋯ : Rₘ →+* Sₘ)
    ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
have neg₁ : eval₂ (IsLocalization.map Sₘ f sorry : 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
Tactic: refine ⟨p.map (algebraMap R Rₘ) * C b, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
have neg : leadingCoeff (Polynomial.map (algebraMap R Rₘ) p) * b = 1
Tactic: refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ leadingCoeff (Polynomial.map (algebraMap R Rₘ) p) * b = 1
have neg : Ne.{u_7 + 1} (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) p.leadingCoeff : Rₘ) (0 : Rₘ)
Tactic: rwa [leadingCoeff_map_of_leadingCoeff_ne_zero (algebraMap R Rₘ)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ 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
have neg : eval₂ (IsLocalization.map Sₘ f sorry) ((algebraMap S Sₘ : (a : S) → Sₘ) x) (Polynomial.map (algebraMap R Rₘ) p) = 0
Tactic: refine eval₂_mul_eq_zero_of_left _ _ _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ eval₂ (IsLocalization.map Sₘ f ⋯) ((algebraMap S Sₘ : (a : S) → Sₘ) x) (Polynomial.map (algebraMap R Rₘ) p) = 0
have neg : Eq.{u_8 + 1} (α := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) (eval₂ f x p) : Sₘ) (0 : Sₘ)
Tactic: rw [eval₂_map, IsLocalization.map_comp, ← hom_eval₂ _ f (algebraMap S Sₘ) x]
-- 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
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : CommRing Sₘ
inst_5 : Algebra R Rₘ
inst_6 : IsLocalization M Rₘ
inst_7 : Algebra S Sₘ
inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra.IsIntegral R S
x : Sₘ
⊢ RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) ⋯) x
have obtain : ∀ (s u : S) (hu : Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) u)
  (hx :
    HMul.hMul (β := Sₘ) x
        ((algebraMap S Sₘ : (a : S) → Sₘ)
            (↑(s,
                    Subtype.mk (p := fun (x : S) ↦
                      Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x) u hu).2 :
              S) :
          Sₘ) =
      (algebraMap S Sₘ : (a : S) → Sₘ)
        (s,
            Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x) u
              hu).1),
  RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) sorry) x
Tactic: obtain ⟨⟨s, ⟨u, hu⟩⟩, hx⟩ := surj (Algebra.algebraMapSubmonoid S M) x