awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
p : (↥R[s])[X]
hpm : p.Monic
hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0
this : Polynomial.map (algebraMap (↥R[s]) S) p ∈ lifts φ.toRingHom
obtain :
  ∀ (q : R[X][X]) (hqp : Polynomial.map φ.toRingHom q = Polynomial.map (algebraMap (↥R[s]) S) p)
    (hqd : q.degree = degree (Polynomial.map (algebraMap (↥R[s]) S) p)) (hqm : q.Monic), φ.IsIntegralElem t
⊢ φ.IsIntegralElem t

Tactic:
obtain ⟨q, hqp, hqd, hqm⟩ := lifts_and_degree_eq_and_monic this (hpm.map _)

Premises used: Polynomial.lifts_and_degree_eq_and_monic, Polynomial.Monic.map
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
p : (↥R[s])[X]
hpm : p.Monic
hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0
this : Polynomial.map (algebraMap (↥R[s]) S) p ∈ lifts φ.toRingHom
q : R[X][X]
hqp : Polynomial.map φ.toRingHom q = Polynomial.map (algebraMap (↥R[s]) S) p
hqd : q.degree = degree (Polynomial.map (algebraMap (↥R[s]) S) p)
hqm : q.Monic
rw : eval t (Polynomial.map φ.toRingHom q) = 0
rw₁ : eval t (Polynomial.map (algebraMap (↥R[s]) S) p) = 0
rw₂ : eval₂ (algebraMap (↥R[s]) S) t p = 0
rw₃ rw₄ : Eq.{u_2 + 1} (α := S) 0 0
⊢ eval₂ φ.toRingHom t q = 0

Tactic:
rw [← eval_map, hqp, eval_map, hpt]

Premises used: Polynomial.eval_map
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
p : (↥R[s])[X]
hpm : p.Monic
hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0
this : Polynomial.map (algebraMap (↥R[s]) S) p ∈ lifts φ.toRingHom
q : R[X][X]
hqp : Polynomial.map φ.toRingHom q = Polynomial.map (algebraMap (↥R[s]) S) p
hqd : q.degree = degree (Polynomial.map (algebraMap (↥R[s]) S) p)
hqm : q.Monic
⊢ φ.IsIntegralElem t

Tactic:
exact ⟨q, hqm, by rw [← eval_map, hqp, eval_map, hpt]⟩
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
obtain : ∀ (q : R[X][X]) (hqm : q.Monic) (hqt : eval₂ φ.toRingHom t q = 0), IsIntegral R t
⊢ IsIntegral R t

Tactic:
obtain ⟨q, hqm, hqt⟩ : φ.IsIntegralElem t := by
    obtain ⟨p, hpm, hpt⟩ := ht
    have : p.map (algebraMap _ S) ∈ lifts φ.toRingHom := (lifts_iff_coeff_lifts _).mpr
      (by simp [← AlgHom.mem_range, φ, ← Algebra.adjoin_singleton_eq_range_aeval])
    obtain ⟨q, hqp, hqd, hqm⟩ := lifts_and_degree_eq_and_monic this (hpm.map _)
    exact ⟨q, hqm, by rw [← eval_map, hqp, eval_map, hpt]⟩

Premises used: RingHom.IsIntegralElem, AlgHom.toRingHom
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
i : ℕ
pos : ∀ (hi : i ∈ q.support), (q.coeff i).natDegree ≤ N
neg : ∀ (hi : i ∉ q.support), (q.coeff i).natDegree ≤ N
⊢ (q.coeff i).natDegree ≤ N

Tactic:
by_cases hi : i ∈ q.support

Premises used: Polynomial.support
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
i : ℕ
hi : i ∈ q.support
⊢ (q.coeff i).natDegree ≤ N

Tactic:
Finset.le_sup (f := (q.coeff · |>.natDegree)) hi

Premises used: Finset.le_sup
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
i : ℕ
hi : i ∈ q.support
⊢ (q.coeff i).natDegree ≤ N

Tactic:
exact Finset.le_sup (f := (q.coeff · |>.natDegree)) hi

Premises used: Finset.le_sup
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
i : ℕ
hi : i ∉ q.support
⊢ (q.coeff i).natDegree ≤ N

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
⊢ ∀ (i : ℕ), (q.coeff i).natDegree ≤ N

Tactic:
have hN (i : _) : (q.coeff i).natDegree ≤ N := by
    by_cases hi : i ∈ q.support
    · exact Finset.le_sup (f := (q.coeff · |>.natDegree)) hi
    · simp_all
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
i : ℕ
this : Invertible t := { invOf := s, invOf_mul_self := hst, mul_invOf_self := ⋯ }
⊢ max N (q.coeff i).natDegree ≤ N

Tactic:
simp [hN]
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
i : ℕ
this : Invertible t := { invOf := s, invOf_mul_self := hst, mul_invOf_self := ⋯ }
rw :
  eval₂ (algebraMap R S) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne t _)
        (reflect N (reflect N (q.coeff i))) *
      t ^ N =
    HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
⊢ (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
    HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)

Tactic:
rw [aeval_def, ← eval₂_reflect_mul_pow _ _ N _ ((natDegree_reflect_le ..).trans (by simp [hN]))]

Premises used: Polynomial.eval₂_reflect_mul_pow, Polynomial.natDegree_reflect_le, Polynomial.aeval_def, LE.le.trans
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
i : ℕ
this : Invertible t := { invOf := s, invOf_mul_self := hst, mul_invOf_self := ⋯ }
⊢ eval₂ (algebraMap R S) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne t _)
        (reflect N (reflect N (q.coeff i))) *
      t ^ N =
    HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)

Tactic:
simp +instances [mul_comm, this, aeval_def]

Premises used: Polynomial.aeval_def, mul_comm
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
⊢ ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)

Tactic:
have (i : _) : aeval t (reflect N (q.coeff i)) = t ^ N * (aeval s (q.coeff i)) := by
    letI : Invertible t := ⟨s, hst, (mul_comm _ _).trans hst⟩
    rw [aeval_def, ← eval₂_reflect_mul_pow _ _ N _ ((natDegree_reflect_le ..).trans (by simp [hN]))]
    simp +instances [mul_comm, this, aeval_def]
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
⊢ IsIntegral R t

Tactic:
⟨q', ?_, ?_⟩

Premises used: RingHom.IsIntegralElem, IsIntegral, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
refine_1 : q'.Monic
refine_2 : eval₂ (algebraMap R S) t q' = 0
⊢ IsIntegral R t

Tactic:
refine ⟨q', ?_, ?_⟩
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
⊢ q'.Monic

Tactic:
monic_of_natDegree_le_of_coeff_eq_one (q.natDegree + N) ?_ ?_

Premises used: Polynomial.monic_of_natDegree_le_of_coeff_eq_one, HAdd.hAdd, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
refine_1 : q'.natDegree ≤ q.natDegree + N
refine_1₁ : q'.coeff (q.natDegree + N) = 1
⊢ q'.Monic

Tactic:
refine monic_of_natDegree_le_of_coeff_eq_one (q.natDegree + N) ?_ ?_

Premises used: Polynomial.monic_of_natDegree_le_of_coeff_eq_one, HAdd.hAdd, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
⊢ q'.natDegree ≤ q.natDegree + N

Tactic:
natDegree_sum_le_of_forall_le _ _ fun i hi ↦ ?_

Premises used: Polynomial.sum, Polynomial.natDegree_sum_le_of_forall_le
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
refine_1 :
  ∀ (i : ℕ) (hi : i ∈ q.support),
    natDegree.{u_1} (R := R) ((fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r) i (q.coeff i)) ≤
      q.natDegree + N
⊢ q'.natDegree ≤ q.natDegree + N

Tactic:
refine natDegree_sum_le_of_forall_le _ _ fun i hi ↦ ?_

Premises used: Polynomial.natDegree_sum_le_of_forall_le
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
i : ℕ
hi : i ∈ q.support
refine_1 : i * 1 + max N (q.coeff i).natDegree ≤ q.natDegree + N
⊢ natDegree.{u_1} (R := R) ((fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r) i (q.coeff i)) ≤
    q.natDegree + N

Tactic:
grw [natDegree_mul_le, natDegree_pow_le, natDegree_X_le, natDegree_reflect_le]

Premises used: Polynomial.natDegree_reflect_le, Polynomial.natDegree_pow_le, Polynomial.natDegree_X_le, Polynomial.natDegree_mul_le
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
i : ℕ
hi : i ∈ q.support
⊢ i * 1 + max N (q.coeff i).natDegree ≤ q.natDegree + N

Tactic:
simp [max_eq_left (hN _), le_natDegree_of_mem_supp _ hi]

Premises used: Polynomial.le_natDegree_of_mem_supp, max_eq_left
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
refine_1 :
  Eq.{u_1 + 1} (α := R)
    (∑ x ∈ q.support,
      if x ≤ q.natDegree + N then (q.coeff x).coeff ((revAt N : (a : ℕ) → ℕ) (q.natDegree + N - x)) else 0)
    1
⊢ q'.coeff (q.natDegree + N) = 1

Tactic:
simp only [sum, finsetSum_coeff, coeff_X_pow_mul', coeff_reflect, q']

Premises used: Polynomial.coeff_X_pow_mul', Polynomial.sum, Polynomial.finsetSum_coeff, Polynomial.coeff_reflect
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
refine_1 :
  (if q.natDegree ≤ q.natDegree + N then
      (q.coeff q.natDegree).coeff ((revAt N : (a : ℕ) → ℕ) (q.natDegree + N - q.natDegree))
    else 0) =
    1
refine_1₁ :
  ∀ b ∈ q.support,
    b ≠ q.natDegree →
      (if b ≤ q.natDegree + N then (q.coeff b).coeff ((revAt N : (a : ℕ) → ℕ) (q.natDegree + N - b)) else 0) = 0
refine_1₂ :
  q.natDegree ∉ q.support →
    (if q.natDegree ≤ q.natDegree + N then
        (q.coeff q.natDegree).coeff ((revAt N : (a : ℕ) → ℕ) (q.natDegree + N - q.natDegree))
      else 0) =
      0
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ q.support,
      if x ≤ q.natDegree + N then (q.coeff x).coeff ((revAt N : (a : ℕ) → ℕ) (q.natDegree + N - x)) else 0)
    1

Tactic:
rw [Finset.sum_eq_single q.natDegree]

Premises used: Finset.sum_eq_single, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
⊢ (if q.natDegree ≤ q.natDegree + N then
      (q.coeff q.natDegree).coeff ((revAt N : (a : ℕ) → ℕ) (q.natDegree + N - q.natDegree))
    else 0) =
    1

Tactic:
simp [hqm.leadingCoeff]

Premises used: Polynomial.Monic.leadingCoeff
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
i : ℕ
hi₁ : i ∈ q.support
hi₂ : i ≠ q.natDegree
⊢ N + i < q.natDegree + N

Tactic:
have : N + i < q.natDegree + N :=
          add_comm N i ▸ add_lt_add_left ((le_natDegree_of_mem_supp _ hi₁).lt_of_ne hi₂) _
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this_1 :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
i : ℕ
hi₁ : i ∈ q.support
hi₂ : i ≠ q.natDegree
this : N + i < q.natDegree + N
⊢ (q.coeff i).natDegree < q.natDegree + N - i

Tactic:
grind
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this_1 :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
i : ℕ
hi₁ : i ∈ q.support
hi₂ : i ≠ q.natDegree
this : N + i < q.natDegree + N
⊢ (if i ≤ q.natDegree + N then (q.coeff i).coeff ((revAt N : (a : ℕ) → ℕ) (q.natDegree + N - i)) else 0) = 0

Tactic:
simpa [(le_natDegree_of_mem_supp _ hi₁).trans, revAt, this.not_ge] using
          coeff_eq_zero_of_natDegree_lt (by grind)

Premises used: Polynomial.le_natDegree_of_mem_supp, Polynomial.revAt, Polynomial.coeff_eq_zero_of_natDegree_lt, LE.le.trans, LT.lt.not_ge
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
⊢ q.natDegree ∉ q.support →
    (if q.natDegree ≤ q.natDegree + N then
        (q.coeff q.natDegree).coeff ((revAt N : (a : ℕ) → ℕ) (q.natDegree + N - q.natDegree))
      else 0) =
      0

Tactic:
simp +contextual
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
trans :
  eval₂ (algebraMap R S) t q' =
    t ^ N * q.sum fun (x1 : ℕ) (x2 : R[X]) ↦ HMul.hMul (β := S) (t ^ x1) ((φ.toRingHom : (a : R[X]) → S) x2 : S)
trans₁ :
  (t ^ N * q.sum fun (x1 : ℕ) (x2 : R[X]) ↦ HMul.hMul (β := S) (t ^ x1) ((φ.toRingHom : (a : R[X]) → S) x2 : S)) = 0
⊢ eval₂ (algebraMap R S) t q' = 0

Tactic:
trans t ^ N * q.sum (t ^ · * φ.toRingHom ·)

Premises used: HMul.hMul, Polynomial.sum, HPow.hPow, AlgHom.toRingHom, DFunLike.coe