awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x y : B
r : R
hr : HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) y = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
h :
  ∀ (hr : HMul.hMul (β := B) y ((algebraMap R B : (a : R) → B) r : B) = 1) (p : R[X]) (p_monic : p.Monic)
    (hp : eval₂ (algebraMap R B) (x * y) p = 0),
    Eq (α := (p : R[X]) → B) (eval₂ (algebraMap R B) x)
      (⇑(aeval (HMul.hMul (β := B) (x * y) ((algebraMap R B : (a : R) → B) r : B))) : (a : R[X]) → B)
⊢ Eq (α := (p : R[X]) → B) (eval₂ (algebraMap R B) x)
    (⇑(aeval (HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) (x * y))) : (a : R[X]) → B)

Tactic:
rw [Algebra.commutes] at hr ⊢

Premises used: Algebra.commutes
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x y : B
r : R
hr : HMul.hMul (β := B) y ((algebraMap R B : (a : R) → B) r : B) = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
h : Eq (α := (p : R[X]) → B) (eval₂ (algebraMap R B) x) (⇑(aeval x) : (a : R[X]) → B)
⊢ Eq (α := (p : R[X]) → B) (eval₂ (algebraMap R B) x)
    (⇑(aeval (HMul.hMul (β := B) (x * y) ((algebraMap R B : (a : R) → B) r : B))) : (a : R[X]) → B)

Tactic:
rw [mul_assoc, hr, mul_one]

Premises used: mul_assoc, mul_one
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x y : B
r : R
hr : HMul.hMul (β := B) y ((algebraMap R B : (a : R) → B) r : B) = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ Eq (α := (p : R[X]) → B) (eval₂ (algebraMap R B) x) (⇑(aeval x) : (a : R[X]) → B)

Tactic:
rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x y : S
r : R
hr : HMul.hMul (α := S) ((f : (a : R) → S) r : S) y = 1
hx : f.IsIntegralElem (x * y)
⊢ f.IsIntegralElem x

Tactic:
letI : Algebra R S := f.toAlgebra
  IsIntegral.of_mul_unit hr hx

Premises used: IsIntegral.of_mul_unit, IsIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
G : Set A
hG : ∀ x ∈ G, IsIntegral R x
⊢ ∀ (x : A), Membership.mem (γ := Subring A) (Subring.closure G) x → IsIntegral R x

Tactic:
fun _ hx ↦
  Subring.closure_induction hG isIntegral_zero isIntegral_one (fun _ _ _ _ ↦ IsIntegral.add)
    (fun _ _ ↦ IsIntegral.neg) (fun _ _ _ _ ↦ IsIntegral.mul) hx

Premises used: Subring.closure_induction
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_5
inst_1 : CommRing S
f : R →+* S
G : Set S
hG : ∀ x ∈ G, f.IsIntegralElem x
⊢ ∀ (x : S), Membership.mem (γ := Subring S) (Subring.closure G) x → f.IsIntegralElem x

Tactic:
fun x hx =>
  @IsIntegral.of_mem_closure' R S _ _ f.toAlgebra G hG x hx

Premises used: IsIntegral.of_mem_closure', IsIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
h : IsIntegral R x
n : ℕ
⊢ Membership.mem (γ := Subalgebra R B) R[x] x

Tactic:
Algebra.subset_adjoin rfl

Premises used: Algebra.subset_adjoin, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
h : IsIntegral R x
n : ℕ
⊢ Membership.mem (γ := Subalgebra R B) R[x] x

Tactic:
exact Algebra.subset_adjoin rfl

Premises used: Algebra.subset_adjoin, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
h : IsIntegral R x
n : ℕ
⊢ IsIntegral R (n • x)

Tactic:
h.smul n

Premises used: IsIntegral.smul
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
h : IsIntegral R x
n : ℤ
⊢ IsIntegral R (n • x)

Tactic:
h.smul n

Premises used: IsIntegral.smul
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Multiset A
h : ∀ x ∈ s, IsIntegral R x
⊢ IsIntegral R s.prod

Tactic:
(integralClosure R A).multiset_prod_mem h

Premises used: Set.Mem, setOf, Subalgebra.multiset_prod_mem, RingHom.IsIntegralElem, IsIntegral, integralClosure
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Multiset A
h : ∀ x ∈ s, IsIntegral R x
⊢ IsIntegral R s.sum

Tactic:
(integralClosure R A).multiset_sum_mem h

Premises used: Set.Mem, setOf, Subalgebra.multiset_sum_mem, RingHom.IsIntegralElem, IsIntegral, integralClosure
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
α : Type u_5
s : Finset α
f : α → A
h : ∀ x ∈ s, IsIntegral R (f x)
⊢ IsIntegral.{u_1, u_2} R (A := A) (∏ x ∈ s, f x)

Tactic:
(integralClosure R A).prod_mem h

Premises used: Set.Mem, setOf, RingHom.IsIntegralElem, Subalgebra.prod_mem, IsIntegral, integralClosure
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
α : Type u_5
s : Finset α
f : α → A
h : ∀ x ∈ s, IsIntegral R (f x)
⊢ IsIntegral.{u_1, u_2} R (A := A) (∑ x ∈ s, f x)

Tactic:
(integralClosure R A).sum_mem h

Premises used: Set.Mem, setOf, Subalgebra.sum_mem, RingHom.IsIntegralElem, IsIntegral, integralClosure
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : Type u_5
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix n n A
h : ∀ (i j : n), IsIntegral R (M i j)
rw :
  IsIntegral.{u_1, u_2} R (A := A)
    (∑ σ : Equiv.Perm n,
      HSMul.hSMul (α := ℤˣ) (β := A) (((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
        (∏ i : n, M ((σ : (a : n) → n) i) i))
⊢ IsIntegral R M.det

Tactic:
rw [Matrix.det_apply]

Premises used: Matrix.det_apply
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : Type u_5
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix n n A
h : ∀ (i j : n), IsIntegral R (M i j)
⊢ IsIntegral.{u_1, u_2} R (A := A)
    (∑ σ : Equiv.Perm n,
      HSMul.hSMul (α := ℤˣ) (β := A) (((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
        (∏ i : n, M ((σ : (a : n) → n) i) i))

Tactic:
IsIntegral.sum _ fun σ _hσ ↦ (IsIntegral.prod _ fun i _hi => h _ _).zsmul _

Premises used: Units.val, Equiv.Perm.sign, IsIntegral.prod, DFunLike.coe, IsIntegral.sum, IsIntegral.zsmul
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : Type u_5
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix n n A
h : ∀ (i j : n), IsIntegral R (M i j)
⊢ IsIntegral.{u_1, u_2} R (A := A)
    (∑ σ : Equiv.Perm n,
      HSMul.hSMul (α := ℤˣ) (β := A) (((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
        (∏ i : n, M ((σ : (a : n) → n) i) i))

Tactic:
exact IsIntegral.sum _ fun σ _hσ ↦ (IsIntegral.prod _ fun i _hi => h _ _).zsmul _

Premises used: IsIntegral.prod, IsIntegral.sum, IsIntegral.zsmul
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x : A
n : ℕ
hn : 0 < n
⊢ IsIntegral R (x ^ n) ↔ IsIntegral R x

Tactic:
⟨IsIntegral.of_pow hn, fun hx ↦ hx.pow n⟩

Premises used: IsIntegral.of_pow, IsIntegral.pow, Iff.intro
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
S : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing S
inst_3 : Algebra R A
inst_4 : Algebra R S
int : Algebra.IsIntegral R S
SA : Type u_5
inst_5 : CommRing SA
inst_6 : Algebra R SA
inst_7 : Algebra S SA
inst_8 : Algebra A SA
inst_9 : IsScalarTower R S SA
inst_10 : IsScalarTower R A SA
inst_11 : IsPushout R A S SA
⊢ Algebra.IsIntegral A SA

Tactic:
(equiv R A S SA).isIntegral_iff.mp inferInstance

Premises used: Algebra.IsPushout.equiv, inferInstance, AlgEquiv.isIntegral_iff, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
S : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing S
inst_3 : Algebra R A
inst_4 : Algebra R S
int : Algebra.IsIntegral R S
SA : Type u_5
inst_5 : CommRing SA
inst_6 : Algebra R SA
inst_7 : Algebra S SA
inst_8 : Algebra A SA
inst_9 : IsScalarTower R S SA
inst_10 : IsScalarTower R A SA
h : IsPushout R S A SA
⊢ Algebra.IsIntegral A SA

Tactic:
h.symm.isIntegral'

Premises used: Algebra.IsPushout.isIntegral'
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : CommRing S
inst_4 : Algebra R A
inst_5 : Algebra R B
f_1 f : R →+* S
inst_6 : Algebra R S
int : Algebra.IsIntegral R S
SA : Type u_5
inst_7 : CommRing SA
inst_8 : Algebra R SA
inst_9 : Algebra S SA
inst_10 : Algebra A SA
inst_11 : IsScalarTower R S SA
inst_12 : IsScalarTower R A SA
⊢ Algebra.IsIntegral.{u_1, u_4} R[X] S[X]

Tactic:
Algebra.IsPushout.isIntegral R _ S _

Premises used: Algebra.IsPushout.isIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : CommRing S
inst_4 : Algebra R A
inst_5 : Algebra R B
f_1 f : R →+* S
inst_6 : Algebra R S
int : Algebra.IsIntegral R S
SA : Type u_5
inst_7 : CommRing SA
inst_8 : Algebra R SA
inst_9 : Algebra S SA
inst_10 : Algebra A SA
inst_11 : IsScalarTower R S SA
inst_12 : IsScalarTower R A SA
σ : Type u_6
⊢ Algebra.IsIntegral (MvPolynomial σ R) (MvPolynomial σ S)

Tactic:
Algebra.IsPushout.isIntegral R _ S _

Premises used: Algebra.IsPushout.isIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
pos : ∀ (h' : 1 ≤ p.natDegree), f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
neg : ∀ (h' : ¬1 ≤ p.natDegree), f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)

Tactic:
by_cases h' : 1 ≤ p.natDegree

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
h₁ :
  p.integralNormalization.Monic ∧
    eval₂ f (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x) p.integralNormalization = 0
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)

Tactic:
use integralNormalization p

Premises used: Polynomial.integralNormalization
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
h'' : p = 0
⊢ LE.le (α := ℕ) 1 0

Tactic:
rw [h'', natDegree_zero] at h'

Premises used: Polynomial.natDegree_zero
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
h'' : p = 0
h'₁ : LE.le (α := ℕ) 1 0
⊢ p = 0

Tactic:
rw [h'', natDegree_zero] at h'

Premises used: Polynomial.natDegree_zero
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : LE.le (α := ℕ) 1 0
h'' : p = 0
⊢ False

Tactic:
Nat.not_succ_le_zero 0 h'

Premises used: Nat.not_succ_le_zero, OfNat.ofNat
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : LE.le (α := ℕ) 1 0
h'' : p = 0
⊢ False

Tactic:
exact Nat.not_succ_le_zero 0 h'

Premises used: Nat.not_succ_le_zero, OfNat.ofNat
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
⊢ p ≠ 0

Tactic:
have : p ≠ 0 := fun h'' => by
      rw [h'', natDegree_zero] at h'
      exact Nat.not_succ_le_zero 0 h'
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
this : p ≠ 0
right : eval₂ f (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x) p.integralNormalization = 0
⊢ p.integralNormalization.Monic ∧
    eval₂ f (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x) p.integralNormalization = 0

Tactic:
use monic_integralNormalization this

Premises used: Polynomial.monic_integralNormalization
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
this : p ≠ 0
right : HPow.hPow (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (p.natDegree - 1) * eval₂ f x p = 0
right₁ : HPow.hPow (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (p.natDegree - 1) * 0 = 0
right₂ right₃ : Eq.{u_4 + 1} (α := S) 0 0
⊢ eval₂ f (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x) p.integralNormalization = 0

Tactic:
rw [integralNormalization_eval₂_leadingCoeff_mul h' f x, h, mul_zero]

Premises used: MulZeroClass.mul_zero, Polynomial.integralNormalization_eval₂_leadingCoeff_mul
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
pos : ∀ (hp : Polynomial.map f p = 0), f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
neg : ∀ (hp : ¬Polynomial.map f p = 0), f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)

Tactic:
by_cases hp : p.map f = 0

Premises used: Polynomial.map
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : Polynomial.map f p = 0
⊢ (Polynomial.map f p).coeff p.natDegree = coeff 0 p.natDegree

Tactic:
apply_fun fun q => coeff q p.natDegree at hp

Premises used: Polynomial.coeff, Polynomial.natDegree
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : (Polynomial.map f p).coeff p.natDegree = coeff 0 p.natDegree
⊢ Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)

Tactic:
rw [coeff_map, coeff_zero, coeff_natDegree] at hp

Premises used: Polynomial.coeff_map, Polynomial.coeff_natDegree, Polynomial.coeff_zero
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
pos : f.IsIntegralElem 0
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)

Tactic:
rw [hp, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ f.IsIntegralElem 0

Tactic:
f.isIntegralElem_zero

Premises used: RingHom.isIntegralElem_zero
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ f.IsIntegralElem 0

Tactic:
exact f.isIntegralElem_zero

Premises used: RingHom.isIntegralElem_zero
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : ¬Polynomial.map f p = 0
⊢ p.natDegree = 0

Tactic:
rw [Nat.one_le_iff_ne_zero, Classical.not_not] at h'

Premises used: Classical.not_not, Nat.one_le_iff_ne_zero
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : ¬Polynomial.map f p = 0
h'₁ : p.natDegree = 0
⊢ ¬Polynomial.map f p = 0

Tactic:
rw [Nat.one_le_iff_ne_zero, Classical.not_not] at h'

Premises used: Classical.not_not, Nat.one_le_iff_ne_zero
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
⊢ Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (p.coeff 0) : S) (0 : S)

Tactic:
rw [eq_C_of_natDegree_eq_zero h', eval₂_C] at h

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, Polynomial.eval₂_C
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
h₁ : Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (p.coeff 0) : S) (0 : S)
⊢ p.natDegree = 0

Tactic:
rw [eq_C_of_natDegree_eq_zero h', eval₂_C] at h

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, Polynomial.eval₂_C
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
h₁ : Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (p.coeff 0) : S) (0 : S)
h'₁ : p.natDegree = 0
⊢ ¬Polynomial.map f p = 0

Tactic:
rw [eq_C_of_natDegree_eq_zero h', eval₂_C] at h

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, Polynomial.eval₂_C
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (p.coeff 0) : S) (0 : S)
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
this : Polynomial.map f p = 0
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)

Tactic:
(hp this).elim

Premises used: False.elim
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (p.coeff 0) : S) (0 : S)
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
this : Polynomial.map f p = 0
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)

Tactic:
exact (hp this).elim

Premises used: False.elim
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (p.coeff 0) : S) (0 : S)
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
neg : Polynomial.map f p = 0
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)

Tactic:
suffices p.map f = 0 by exact (hp this).elim
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
x : S
h : Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (p.coeff 0) : S) (0 : S)
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
neg : Polynomial.map f ((C : (a : R) → R[X]) (p.coeff 0)) = 0
neg₁ : Eq.{u_4 + 1} (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) (p.coeff 0)) : S[X]) (0 : S[X])
neg₂ : Eq.{u_4 + 1} (α := S[X]) ((C : (a : S) → S[X]) 0) 0
neg₃ neg₄ : Eq.{u_4 + 1} (α := S) 0 0
⊢ Polynomial.map f p = 0

Tactic:
rw [eq_C_of_natDegree_eq_zero h', map_C, h, C_eq_zero]

Premises used: Polynomial.C_eq_zero, Polynomial.eq_C_of_natDegree_eq_zero, Polynomial.map_C
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
p : R[X]
x : S
inst_2 : Algebra R S
h : Eq.{u_4 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
⊢ eval₂ (algebraMap R S) x p = 0

Tactic:
rw [aeval_def] at h

Premises used: Polynomial.aeval_def
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
p : R[X]
x : S
inst_2 : Algebra R S
h : eval₂ (algebraMap R S) x p = 0
rw : IsIntegral R (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) x)
⊢ IsIntegral R (p.leadingCoeff • x)

Tactic:
rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
p : R[X]
x : S
inst_2 : Algebra R S
h : eval₂ (algebraMap R S) x p = 0
⊢ IsIntegral R (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) x)

Tactic:
(algebraMap R S).isIntegralElem_leadingCoeff_mul p x h

Premises used: Algebra.algebraMap, RingHom.isIntegralElem_leadingCoeff_mul, IsIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
p : R[X]
x : S
inst_2 : Algebra R S
h : eval₂ (algebraMap R S) x p = 0
⊢ IsIntegral R (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) x)

Tactic:
exact (algebraMap R S).isIntegralElem_leadingCoeff_mul p x h

Premises used: Algebra.algebraMap, RingHom.isIntegralElem_leadingCoeff_mul
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
S : Type u_4
inst : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
rw :
  Eq (α := S[X] ⧸ I)
    (∑ i ∈ Finset.range (g.natDegree + 1),
        HMul.hMul (α := S[X] ⧸ I)
          ((RingHom.comp (Ideal.Quotient.mk I) (algebraMap S S[X]) : (a : S) → S[X] ⧸ I) (g.coeff i) : S[X] ⧸ I)
          (HPow.hPow (α := S[X] ⧸ I) ((Ideal.Quotient.mk I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I) i) :
      S[X] ⧸ I)
    ((Ideal.Quotient.mk I : (a : S[X]) → S[X] ⧸ I) g : S[X] ⧸ I)
⊢ eval₂ (RingHom.comp (Ideal.Quotient.mk I) (algebraMap S S[X])) ((Ideal.Quotient.mk I : (a : S[X]) → S[X] ⧸ I) X) g = 0

Tactic:
rw [← (Ideal.Quotient.eq_zero_iff_mem.mpr h), eval₂_eq_sum_range]

Premises used: Iff.mpr, Ideal.Quotient.eq_zero_iff_mem, Polynomial.eval₂_eq_sum_range