awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (HPow.hPow (α := R[X]) X m) q).Monic
hm₂ : p.natDegree < m
h₀ : Eq.{u_2 + 1} (α := S[X]) ((algebraMap R[X] S[X] : (a : R[X]) → S[X]) X : S[X]) (X : S[X])
⊢ IsRoot
    (Polynomial.map.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])
      ((taylor (HPow.hPow (α := R[X]) X m) : (a : R[X][X]) → R[X][X]) q))
    (p - HPow.hPow (α := S[X]) X m)

Tactic:
have : (((taylor (X ^ m)) q).map (algebraMap R[X] S[X])).IsRoot (p - X ^ m) := by
    simpa [-algebraMap_def, q, h₀] using
      ((q.map (algebraMap _ _)).taylor_eval (X ^ m) (p - X ^ m) :)
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (HPow.hPow (α := R[X]) X m) q).Monic
hm₂ : p.natDegree < m
h₀ : Eq.{u_2 + 1} (α := S[X]) ((algebraMap R[X] S[X] : (a : R[X]) → S[X]) X : S[X]) (X : S[X])
this :
  IsRoot
    (Polynomial.map.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])
      ((taylor (HPow.hPow (α := R[X]) X m) : (a : R[X][X]) → R[X][X]) q))
    (p - HPow.hPow (α := S[X]) X m)
rw :
  p - HPow.hPow (α := S[X]) X m ∣
    ((aeval ((Algebra.ofId R[X] S[X] : (a : R[X]) → S[X]) (HPow.hPow (α := R[X]) X m)) :
          AlgHom.{u_1, u_1, u_2} R[X] R[X][X] S[X]) :
        (a : R[X][X]) → S[X])
      q
⊢ HPow.hPow (α := S[X]) X m - p ∣ (Algebra.ofId R[X] S[X] : (a : R[X]) → S[X]) (eval (HPow.hPow (α := R[X]) X m) q)

Tactic:
rw [← coe_aeval_eq_eval, ← aeval_algHom_apply, ← neg_dvd, neg_sub]

Premises used: neg_sub, Polynomial.coe_aeval_eq_eval, Polynomial.aeval_algHom_apply, neg_dvd
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (HPow.hPow (α := R[X]) X m) q).Monic
hm₂ : p.natDegree < m
h₀ : Eq.{u_2 + 1} (α := S[X]) ((algebraMap R[X] S[X] : (a : R[X]) → S[X]) X : S[X]) (X : S[X])
this :
  IsRoot
    (Polynomial.map.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])
      ((taylor (HPow.hPow (α := R[X]) X m) : (a : R[X][X]) → R[X][X]) q))
    (p - HPow.hPow (α := S[X]) X m)
⊢ p - HPow.hPow (α := S[X]) X m ∣
    ((aeval ((Algebra.ofId R[X] S[X] : (a : R[X]) → S[X]) (HPow.hPow (α := R[X]) X m)) :
          AlgHom.{u_1, u_1, u_2} R[X] R[X][X] S[X]) :
        (a : R[X][X]) → S[X])
      q

Tactic:
simpa [Polynomial.taylor_coeff_zero, -algebraMap_def, h₀] using this.dvd_coeff_zero

Premises used: Polynomial.algebraMap_def, Polynomial.taylor_coeff_zero, Polynomial.IsRoot.dvd_coeff_zero
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (HPow.hPow (α := R[X]) X m) q).Monic
hm₂ : p.natDegree < m
h₀ : Eq.{u_2 + 1} (α := S[X]) ((algebraMap R[X] S[X] : (a : R[X]) → S[X]) X : S[X]) (X : S[X])
this :
  IsRoot
    (Polynomial.map.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])
      ((taylor (HPow.hPow (α := R[X]) X m) : (a : R[X][X]) → R[X][X]) q))
    (p - HPow.hPow (α := S[X]) X m)
⊢ HPow.hPow (α := S[X]) X m - p ∣ Polynomial.map (algebraMap R S) (eval (HPow.hPow (α := R[X]) X m) q)

Tactic:
have : X ^ m - p ∣ (eval (X ^ m) q).map (algebraMap _ _) := by
    change X ^ m - p ∣ Algebra.ofId R[X] S[X] _
    rw [← coe_aeval_eq_eval, ← aeval_algHom_apply, ← neg_dvd, neg_sub]
    simpa [Polynomial.taylor_coeff_zero, -algebraMap_def, h₀] using this.dvd_coeff_zero
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (HPow.hPow (α := R[X]) X m) q).Monic
hm₂ : p.natDegree < m
h₀ : Eq.{u_2 + 1} (α := S[X]) ((algebraMap R[X] S[X] : (a : R[X]) → S[X]) X : S[X]) (X : S[X])
this_1 :
  IsRoot
    (Polynomial.map.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])
      ((taylor (HPow.hPow (α := R[X]) X m) : (a : R[X][X]) → R[X][X]) q))
    (p - HPow.hPow (α := S[X]) X m)
this : HPow.hPow (α := S[X]) X m - p ∣ Polynomial.map (algebraMap R S) (eval (HPow.hPow (α := R[X]) X m) q)
⊢ p.degree < (HPow.hPow (α := S[X]) X m).degree

Tactic:
simpa [← natDegree_lt_iff_degree_lt, hp0]

Premises used: Polynomial.natDegree_lt_iff_degree_lt
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (HPow.hPow (α := R[X]) X m) q).Monic
hm₂ : p.natDegree < m
h₀ : Eq.{u_2 + 1} (α := S[X]) ((algebraMap R[X] S[X] : (a : R[X]) → S[X]) X : S[X]) (X : S[X])
this_1 :
  IsRoot
    (Polynomial.map.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])
      ((taylor (HPow.hPow (α := R[X]) X m) : (a : R[X][X]) → R[X][X]) q))
    (p - HPow.hPow (α := S[X]) X m)
this : HPow.hPow (α := S[X]) X m - p ∣ Polynomial.map (algebraMap R S) (eval (HPow.hPow (α := R[X]) X m) q)
⊢ IsIntegral R (-(HPow.hPow (α := S[X]) X m - p).coeff i)

Tactic:
have := (isIntegral_coeff_of_dvd _ _ hm₁'
    ((monic_X_pow _).sub_of_left (by simpa [← natDegree_lt_iff_degree_lt, hp0])) this i).neg
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (HPow.hPow (α := R[X]) X m) q).Monic
hm₂ : p.natDegree < m
h₀ : Eq.{u_2 + 1} (α := S[X]) ((algebraMap R[X] S[X] : (a : R[X]) → S[X]) X : S[X]) (X : S[X])
this_1 :
  IsRoot
    (Polynomial.map.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])
      ((taylor (HPow.hPow (α := R[X]) X m) : (a : R[X][X]) → R[X][X]) q))
    (p - HPow.hPow (α := S[X]) X m)
this_2 : HPow.hPow (α := S[X]) X m - p ∣ Polynomial.map (algebraMap R S) (eval (HPow.hPow (α := R[X]) X m) q)
this : IsIntegral R (-(HPow.hPow (α := S[X]) X m - p).coeff i)
inr : ∀ (hi : i ≤ p.natDegree), IsIntegral R (p.coeff i)
inr₁ : ∀ (hi : p.natDegree < i), IsIntegral R (p.coeff i)
⊢ IsIntegral R (p.coeff i)

Tactic:
obtain hi | hi := le_or_gt i p.natDegree

Premises used: le_or_gt, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (HPow.hPow (α := R[X]) X m) q).Monic
hm₂ : p.natDegree < m
h₀ : Eq.{u_2 + 1} (α := S[X]) ((algebraMap R[X] S[X] : (a : R[X]) → S[X]) X : S[X]) (X : S[X])
this_1 :
  IsRoot
    (Polynomial.map.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])
      ((taylor (HPow.hPow (α := R[X]) X m) : (a : R[X][X]) → R[X][X]) q))
    (p - HPow.hPow (α := S[X]) X m)
this_2 : HPow.hPow (α := S[X]) X m - p ∣ Polynomial.map (algebraMap R S) (eval (HPow.hPow (α := R[X]) X m) q)
this : IsIntegral R (-(HPow.hPow (α := S[X]) X m - p).coeff i)
hi : i ≤ p.natDegree
⊢ i ≠ m

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (HPow.hPow (α := R[X]) X m) q).Monic
hm₂ : p.natDegree < m
h₀ : Eq.{u_2 + 1} (α := S[X]) ((algebraMap R[X] S[X] : (a : R[X]) → S[X]) X : S[X]) (X : S[X])
this_1 :
  IsRoot
    (Polynomial.map.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])
      ((taylor (HPow.hPow (α := R[X]) X m) : (a : R[X][X]) → R[X][X]) q))
    (p - HPow.hPow (α := S[X]) X m)
this_2 : HPow.hPow (α := S[X]) X m - p ∣ Polynomial.map (algebraMap R S) (eval (HPow.hPow (α := R[X]) X m) q)
this : IsIntegral R (-(HPow.hPow (α := S[X]) X m - p).coeff i)
hi : i ≤ p.natDegree
⊢ IsIntegral R (p.coeff i)

Tactic:
simpa [show i ≠ m by lia] using this
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hp : IsIntegral.{u_1, u_2} R[X] p
i : ℕ
h : Nontrivial R
h_1 : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun (i : ℕ) ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (HPow.hPow (α := R[X]) X m) q).Monic
hm₂ : p.natDegree < m
h₀ : Eq.{u_2 + 1} (α := S[X]) ((algebraMap R[X] S[X] : (a : R[X]) → S[X]) X : S[X]) (X : S[X])
this_1 :
  IsRoot
    (Polynomial.map.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])
      ((taylor (HPow.hPow (α := R[X]) X m) : (a : R[X][X]) → R[X][X]) q))
    (p - HPow.hPow (α := S[X]) X m)
this_2 : HPow.hPow (α := S[X]) X m - p ∣ Polynomial.map (algebraMap R S) (eval (HPow.hPow (α := R[X]) X m) q)
this : IsIntegral R (-(HPow.hPow (α := S[X]) X m - p).coeff i)
hi : p.natDegree < i
⊢ IsIntegral R (p.coeff i)

Tactic:
simp [coeff_eq_zero_of_natDegree_lt hi, isIntegral_zero]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt, isIntegral_zero
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
⊢ IsIntegral.{u_1, u_2} R[X] f ↔ ∀ (n : ℕ), IsIntegral R (f.coeff n)

Tactic:
⟨IsIntegral.coeff, fun H ↦ ?_⟩

Premises used: IsIntegral.coeff, Iff.intro
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
refine : ∀ (H : ∀ (n : ℕ), IsIntegral R (f.coeff n)), IsIntegral.{u_1, u_2} R[X] f
⊢ IsIntegral.{u_1, u_2} R[X] f ↔ ∀ (n : ℕ), IsIntegral R (f.coeff n)

Tactic:
refine ⟨IsIntegral.coeff, fun H ↦ ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
H : ∀ (n : ℕ), IsIntegral R (f.coeff n)
rw : IsIntegral.{u_1, u_2} R[X] (A := S[X]) (∑ n ∈ f.support, (monomial n : (a : S) → S[X]) (f.coeff n))
⊢ IsIntegral.{u_1, u_2} R[X] f

Tactic:
rw [← f.sum_monomial_eq, Polynomial.sum]

Premises used: Polynomial.sum, Polynomial.sum_monomial_eq
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
H : ∀ (n : ℕ), IsIntegral R (f.coeff n)
simp :
  IsIntegral.{u_1, u_2} R[X] (A := S[X])
    (∑ x ∈ f.support,
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (f.coeff x) : S[X])
        (HPow.hPow (α := S[X]) (map (algebraMap R S) X) x))
⊢ IsIntegral.{u_1, u_2} R[X] (A := S[X]) (∑ n ∈ f.support, (monomial n : (a : S) → S[X]) (f.coeff n))

Tactic:
simp only [← C_mul_X_pow_eq_monomial, ← map_X (algebraMap R S)]

Premises used: Algebra.algebraMap, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.map_X
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
H : ∀ (n : ℕ), IsIntegral R (f.coeff n)
⊢ IsIntegral.{u_1, u_2} R[X] (A := S[X])
    (∑ x ∈ f.support,
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (f.coeff x) : S[X])
        (HPow.hPow (α := S[X]) (map (algebraMap R S) X) x))

Tactic:
.sum _ fun i _ ↦ ((H i).map (CAlgHom (R := R))).tower_top.mul (.pow isIntegral_algebraMap _)

Premises used: IsIntegral.mul, Polynomial.CAlgHom, IsIntegral.pow, isIntegral_algebraMap, IsIntegral.map, IsIntegral.tower_top, IsIntegral.sum
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
H : ∀ (n : ℕ), IsIntegral R (f.coeff n)
⊢ IsIntegral.{u_1, u_2} R[X] (A := S[X])
    (∑ x ∈ f.support,
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (f.coeff x) : S[X])
        (HPow.hPow (α := S[X]) (map (algebraMap R S) X) x))

Tactic:
exact .sum _ fun i _ ↦ ((H i).map (CAlgHom (R := R))).tower_top.mul (.pow isIntegral_algebraMap _)
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x : A
p : A[X]
monic : p.Monic
deg : p.natDegree ≠ 0
hx : IsIntegral R (eval x p)
hp : ∀ (i : ℕ), IsIntegral R (p.coeff i)
⊢ ∀ (n : ℕ),
    Membership.mem (γ := Set A)
      (Set.range (ι := ↥(integralClosure R A))
        (⇑(algebraMap (↥(integralClosure R A)) A) : (a : ↥(integralClosure R A)) → A))
      (p.coeff n)

Tactic:
simpa
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x : A
p : A[X]
monic : p.Monic
deg : p.natDegree ≠ 0
hx : IsIntegral R (eval x p)
hp : ∀ (i : ℕ), IsIntegral R (p.coeff i)
obtain :
  ∀ (q : (↥(integralClosure R A))[X]) (hqp : Polynomial.map (algebraMap (↥(integralClosure R A)) A) q = p)
    (hdeg : q.natDegree = p.natDegree) (hq : q.Monic), IsIntegral R x
⊢ IsIntegral R x

Tactic:
obtain ⟨q, hqp, hdeg, hq⟩ :=
    lifts_and_natDegree_eq_and_monic (p := p) (f := algebraMap (integralClosure R A) _)
    (p.lifts_iff_coeff_lifts.mpr (by simpa)) monic

Premises used: Iff.mpr, Polynomial.lifts_iff_coeff_lifts, Polynomial.lifts_and_natDegree_eq_and_monic
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x : A
p : A[X]
monic : p.Monic
deg : p.natDegree ≠ 0
hx : IsIntegral R (eval x p)
hp : ∀ (i : ℕ), IsIntegral R (p.coeff i)
q : (↥(integralClosure R A))[X]
hqp : Polynomial.map (algebraMap (↥(integralClosure R A)) A) q = p
hdeg : q.natDegree = p.natDegree
hq : q.Monic
⊢ IsIntegral ↥(integralClosure R A) (A := A) ((aeval x : (a : (↥(integralClosure R A))[X]) → A) q : A)

Tactic:
simpa [← eval_map_algebraMap, hqp] using hx.tower_top

Premises used: Polynomial.eval_map_algebraMap, IsIntegral.tower_top
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x : A
p : A[X]
monic : p.Monic
deg : p.natDegree ≠ 0
hx : IsIntegral R (eval x p)
hp : ∀ (i : ℕ), IsIntegral R (p.coeff i)
q : (↥(integralClosure R A))[X]
hqp : Polynomial.map (algebraMap (↥(integralClosure R A)) A) q = p
hdeg : q.natDegree = p.natDegree
hq : q.Monic
⊢ IsIntegral R x

Tactic:
exact isIntegral_trans _ (.of_aeval_monic hq (hdeg ▸ deg)
    (by simpa [← eval_map_algebraMap, hqp] using hx.tower_top))

Premises used: isIntegral_trans, Eq.rec, IsIntegral.of_aeval_monic, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R_1 : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Algebra R_1 S
R : Type u_4
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsIntegrallyClosed R
K : Type u_4 := FractionRing R
⊢ IsIntegrallyClosed.{u_4} K[X]

Tactic:
have : IsIntegrallyClosed K[X] := UniqueFactorizationMonoid.instIsIntegrallyClosed
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R_1 : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Algebra R_1 S
R : Type u_4
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsIntegrallyClosed R
K : Type u_4 := FractionRing R
this : IsIntegrallyClosed.{u_4} K[X]
suffices : IsIntegrallyClosedIn.{u_4, u_4} R[X] K[X]
⊢ IsIntegrallyClosed.{u_4} R[X]

Tactic:
suffices IsIntegrallyClosedIn R[X] K[X] from .of_isIntegrallyClosed_of_isIntegrallyClosedIn _ K[X]
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R_1 : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Algebra R_1 S
R : Type u_4
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsIntegrallyClosed R
K : Type u_4 := FractionRing R
this : IsIntegrallyClosed.{u_4} K[X]
⊢ IsIntegrallyClosedIn.{u_4, u_4} R[X] K[X]

Tactic:
isIntegrallyClosedIn_iff.mpr ⟨map_injective _ (IsFractionRing.injective _ _), ?_⟩

Premises used: Iff.mpr, IsFractionRing.injective, Polynomial.map_injective, isIntegrallyClosedIn_iff, And.intro
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R_1 : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Algebra R_1 S
R : Type u_4
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsIntegrallyClosed R
K : Type u_4 := FractionRing R
this : IsIntegrallyClosed.{u_4} K[X]
refine : ∀ {x : K[X]}, IsIntegral R[X] x → ∃ (y : R[X]), (algebraMap R[X] K[X] : (a : R[X]) → K[X]) y = x
⊢ IsIntegrallyClosedIn.{u_4, u_4} R[X] K[X]

Tactic:
refine isIntegrallyClosedIn_iff.mpr ⟨map_injective _ (IsFractionRing.injective _ _), ?_⟩

Premises used: Iff.mpr, isIntegrallyClosedIn_iff, And.intro
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R_1 : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Algebra R_1 S
R : Type u_4
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsIntegrallyClosed R
K : Type u_4 := FractionRing R
this : IsIntegrallyClosed.{u_4} K[X]
⊢ ∀ {x : K[X]}, IsIntegral R[X] x → ∃ (y : R[X]), (algebraMap R[X] K[X] : (a : R[X]) → K[X]) y = x

Tactic:
fun {p} hp ↦ (lifts_iff_coeff_lifts _).mpr fun n ↦ ?_

Premises used: Iff.mpr, Set.Mem, setOf, Polynomial.lifts_iff_coeff_lifts, Set.range
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R_1 : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Algebra R_1 S
R : Type u_4
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsIntegrallyClosed R
K : Type u_4 := FractionRing R
this : IsIntegrallyClosed.{u_4} K[X]
refine :
  ∀ {p : K[X]} (hp : IsIntegral R[X] p) (n : ℕ),
    Membership.mem (γ := Set K) (Set.range (ι := R) (⇑(algebraMap R K) : (a : R) → K)) (p.coeff n)
⊢ ∀ {x : K[X]}, IsIntegral R[X] x → ∃ (y : R[X]), (algebraMap R[X] K[X] : (a : R[X]) → K[X]) y = x

Tactic:
refine fun {p} hp ↦ (lifts_iff_coeff_lifts _).mpr fun n ↦ ?_

Premises used: Iff.mpr, Polynomial.lifts_iff_coeff_lifts
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R_1 : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Algebra R_1 S
R : Type u_4
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsIntegrallyClosed R
K : Type u_4 := FractionRing R
this : IsIntegrallyClosed.{u_4} K[X]
p : K[X]
hp : IsIntegral R[X] p
n : ℕ
⊢ Membership.mem (γ := Set K) (Set.range (ι := R) (⇑(algebraMap R K) : (a : R) → K)) (p.coeff n)

Tactic:
IsIntegrallyClosed.isIntegral_iff.mp (hp.coeff _)

Premises used: IsIntegrallyClosed.isIntegral_iff, Set.Mem, setOf, IsIntegral.coeff, Iff.mp, Set.range
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R_1 : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Algebra R_1 S
R : Type u_4
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsIntegrallyClosed R
K : Type u_4 := FractionRing R
this : IsIntegrallyClosed.{u_4} K[X]
p : K[X]
hp : IsIntegral R[X] p
n : ℕ
⊢ Membership.mem (γ := Set K) (Set.range (ι := R) (⇑(algebraMap R K) : (a : R) → K)) (p.coeff n)

Tactic:
exact IsIntegrallyClosed.isIntegral_iff.mp (hp.coeff _)

Premises used: IsIntegrallyClosed.isIntegral_iff, IsIntegral.coeff, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
⊢ IsIntegral (MvPolynomial σ R) f ↔ ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)

Tactic:
⟨fun H n ↦ ?mp, fun H ↦ ?mpr⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
mp : ∀ (H : IsIntegral (MvPolynomial σ R) f) (n : σ →₀ ℕ), IsIntegral R (coeff n f)
refine : ∀ (H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)), IsIntegral (MvPolynomial σ R) f
⊢ IsIntegral (MvPolynomial σ R) f ↔ ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)

Tactic:
refine ⟨fun H n ↦ ?mp, fun H ↦ ?mpr⟩
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
rw :
  IsIntegral (MvPolynomial σ R) (A := MvPolynomial σ S)
    (∑ v ∈ f.support, (monomial v : (a : S) → MvPolynomial σ S) (coeff v f))
⊢ IsIntegral (MvPolynomial σ R) f

Tactic:
rw [← f.support_sum_monomial_coeff]

Premises used: MvPolynomial.support_sum_monomial_coeff
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
simp_rw :
  IsIntegral (MvPolynomial σ R) (A := MvPolynomial σ S)
    (∑ x ∈ f.support,
      HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
        ((C : (a : S) → MvPolynomial σ S) (coeff x f) : MvPolynomial σ S)
        (x.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ S) (X n) e : MvPolynomial σ S))
⊢ IsIntegral (MvPolynomial σ R) (A := MvPolynomial σ S)
    (∑ v ∈ f.support, (monomial v : (a : S) → MvPolynomial σ S) (coeff v f))

Tactic:
simp_rw [monomial_eq]

Premises used: MvPolynomial.monomial_eq
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) (A := MvPolynomial σ S)
    (∑ x ∈ f.support,
      HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
        ((C : (a : S) → MvPolynomial σ S) (coeff x f) : MvPolynomial σ S)
        (x.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ S) (X n) e : MvPolynomial σ S))

Tactic:
IsIntegral.sum _ fun n _ ↦ .mul ((H n).map (Algebra.ofId _ _)).tower_top
      (.prod _ fun i _ ↦ .pow ?_ _)

Premises used: IsIntegral.mul, MvPolynomial.X, IsIntegral.pow, IsIntegral.prod, Algebra.ofId, HPow.hPow, IsIntegral.map, MvPolynomial, IsIntegral.tower_top, DFunLike.coe, IsIntegral.sum