awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
h : Nontrivial S
p : R[X]
hpm : p.Monic
hp : ∃ (a : ℕ), r ^ a * eval₂ (algebraMap R S) x p = 0
⊢ ∃ (n : ℕ), IsIntegral R (r ^ n * x)
have obtain : ∀ (m : ℕ) (hm : r ^ m * eval₂ (algebraMap R S) x p = 0), ∃ (n : ℕ), IsIntegral R (r ^ n * x)
Tactic: obtain ⟨m, hm⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
h : Nontrivial S
p : R[X]
hpm : p.Monic
m : ℕ
hm : r ^ m * eval₂ (algebraMap R S) x p = 0
⊢ ∃ (n : ℕ), IsIntegral R (r ^ n * x)
have this : IsIntegral R
  ((HPow.hPow (α := (↥(integralClosure R S))[X])
          ((C : (a : ↥(integralClosure R S)) → (↥(integralClosure R S))[X])
              (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) r hr) :
            (↥(integralClosure R S))[X])
          m *
        Polynomial.map (algebraMap R ↥(integralClosure R S)) p).leadingCoeff •
    x)
Tactic: have := isIntegral_trans (R := R) _ (isIntegral_leadingCoeff_smul (R := integralClosure R S)
    (C ⟨r, hr⟩ ^ m * p.map (algebraMap _ _)) x (by simpa [← aeval_def] using hm))
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
h : Nontrivial S
p : R[X]
hpm : p.Monic
m : ℕ
hm : r ^ m * eval₂ (algebraMap R S) x p = 0
this :
  IsIntegral R
    ((HPow.hPow (α := (↥(integralClosure R S))[X])
            ((C : (a : ↥(integralClosure R S)) → (↥(integralClosure R S))[X])
                (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) r hr) :
              (↥(integralClosure R S))[X])
            m *
          Polynomial.map (algebraMap R ↥(integralClosure R S)) p).leadingCoeff •
      x)
⊢ ∃ (n : ℕ), IsIntegral R (r ^ n * x)
have this₁ : IsIntegral R (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) r hr ^ m • x)
Tactic: rw [← map_pow, (hpm.map _).leadingCoeff_C_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
a : ↥(Submonoid.powers r)
hx : IsIntegral R (mk' Sₘ x a)
⊢ ∃ (n : ℕ), IsIntegral R (r ^ n * x)
have refine : IsIntegral.{u_5, u_7} R (A := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
Tactic: refine IsLocalization.Away.exists_isIntegral_mul_of_isIntegral_algebraMap (Sₘ := Sₘ) hr ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
a : ↥(Submonoid.powers r)
hx : IsIntegral R (mk' Sₘ x a)
⊢ IsIntegral.{u_5, u_7} R (A := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
have obtain : ∀ (n : ℕ)
  (hx :
    IsIntegral R
      (mk' Sₘ x
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers r) x)
          ((fun (x : ℕ) ↦ r ^ x) n) sorry))),
  IsIntegral.{u_5, u_7} R (A := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
Tactic: obtain ⟨_, ⟨n, rfl⟩⟩ := a
Cleared hypotheses: a, hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst_7 : Away r Sₘ
x : S
n : ℕ
hx :
  IsIntegral R
    (mk' Sₘ x
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers r) x)
        ((fun (x : ℕ) ↦ r ^ x) n) ⋯))
⊢ IsIntegral.{u_5, u_7} R (A := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
have h : (algebraMap S Sₘ : (a : S) → Sₘ) x =
  HMul.hMul (α := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) (r ^ n) : Sₘ)
    (mk' Sₘ x
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers r) x)
        ((fun (x : ℕ) ↦ r ^ x) n) sorry))
Tactic: convert! (hr.pow n).algebraMap.mul hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
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
⊢ IsIntegral R t
have a : Nontrivial S
Tactic: nontriviality S
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ φ.IsIntegralElem t
have obtain : ∀ (p : (↥R[s])[X]) (hpm : p.Monic) (hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0), φ.IsIntegralElem t
Tactic: obtain ⟨p, hpm, hpt⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
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
⊢ φ.IsIntegralElem t
have this : Polynomial.map (algebraMap (↥R[s]) S) p ∈ lifts φ.toRingHom
Tactic: have : p.map (algebraMap _ S) ∈ lifts φ.toRingHom := (lifts_iff_coeff_lifts _).mpr
      (by simp [← AlgHom.mem_range, φ, ← Algebra.adjoin_singleton_eq_range_aeval])
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ φ.IsIntegralElem t
have 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
Tactic: obtain ⟨q, hqp, hqd, hqm⟩ := lifts_and_degree_eq_and_monic this (hpm.map _)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ eval₂ φ.toRingHom t q = 0
have rw : eval t (Polynomial.map φ.toRingHom q) = 0
Tactic: rw [← eval_map, hqp, eval_map, hpt]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ eval₂ φ.toRingHom t q = 0
have rw₁ : eval t (Polynomial.map (algebraMap (↥R[s]) S) p) = 0
Tactic: rw [← eval_map, hqp, eval_map, hpt]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ eval₂ φ.toRingHom t q = 0
have rw₃ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [← eval_map, hqp, eval_map, hpt]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ IsIntegral R t
have obtain : ∀ (q : R[X][X]) (hqm : q.Monic) (hqt : eval₂ φ.toRingHom t q = 0), 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]⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
have pos : ∀ (hi : i ∈ q.support), (q.coeff i).natDegree ≤ N
Tactic: by_cases hi : i ∈ q.support
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ (q.coeff i).natDegree ≤ N
have neg : ∀ (hi : i ∉ q.support), (q.coeff i).natDegree ≤ N
Tactic: by_cases hi : i ∈ q.support
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
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
⊢ IsIntegral R t
have hN : ∀ (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
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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 := ⋯ }
⊢ (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)
have 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)
Tactic: rw [aeval_def, ← eval₂_reflect_mul_pow _ _ N _ ((natDegree_reflect_le ..).trans (by simp [hN]))]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
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
⊢ IsIntegral R t
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
have refine_1 : q'.Monic
Tactic: refine ⟨q', ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ IsIntegral R t
have refine_2 : eval₂ (algebraMap R S) t q' = 0
Tactic: refine ⟨q', ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
have refine_1 : q'.natDegree ≤ q.natDegree + N
Tactic: refine monic_of_natDegree_le_of_coeff_eq_one (q.natDegree + N) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ q'.Monic
have refine_1₁ : q'.coeff (q.natDegree + N) = 1
Tactic: refine monic_of_natDegree_le_of_coeff_eq_one (q.natDegree + N) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
have 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
Tactic: refine natDegree_sum_le_of_forall_le _ _ fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ 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
have refine_1 : i * 1 + max N (q.coeff i).natDegree ≤ q.natDegree + N
Tactic: grw [natDegree_mul_le, natDegree_pow_le, natDegree_X_le, natDegree_reflect_le]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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'.coeff (q.natDegree + N) = 1
have 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
Tactic: simp only [sum, finsetSum_coeff, coeff_X_pow_mul', coeff_reflect, q']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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)
⊢ 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
have 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
Tactic: rw [Finset.sum_eq_single q.natDegree]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ 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
have 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
Tactic: rw [Finset.sum_eq_single q.natDegree]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ 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
have 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
Tactic: rw [Finset.sum_eq_single q.natDegree]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
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
⊢ (if i ≤ q.natDegree + N then (q.coeff i).coeff ((revAt N : (a : ℕ) → ℕ) (q.natDegree + N - i)) else 0) = 0
have this₁ : 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₂) _