awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S T : Subalgebra R A
⊢ Algebra.IsIntegral.{u_1, u_2} R ↥(S ⊔ T) ↔ Algebra.IsIntegral.{u_1, u_2} R ↥S ∧ Algebra.IsIntegral.{u_1, u_2} R ↥T
have simp_rw : S ⊔ T ≤ integralClosure R A ↔ S ≤ integralClosure R A ∧ T ≤ integralClosure R A
Tactic: simp_rw [← le_integralClosure_iff_isIntegral, sup_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
ι : Sort u_5
S : ι → Subalgebra R A
⊢ Algebra.IsIntegral.{u_1, u_2} R ↥(iSup S) ↔ ∀ (i : ι), Algebra.IsIntegral.{u_1, u_2} R ↥(S i)
have simp_rw : iSup S ≤ integralClosure R A ↔ ∀ (i : ι), S i ≤ integralClosure R A
Tactic: simp_rw [← le_integralClosure_iff_isIntegral, iSup_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
f : A ≃ₐ[R] S
⊢ Subalgebra.map (↑f : A →ₐ[R] S) (integralClosure R A) = integralClosure R S
have h : ∀ (y : S),
  y ∈ Subalgebra.map (↑f : A →ₐ[R] S) (integralClosure R A) ↔
    Membership.mem (γ := Subalgebra R S) (integralClosure R S) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
f : A ≃ₐ[R] S
y : S
⊢ y ∈ Subalgebra.map (↑f : A →ₐ[R] S) (integralClosure R A) ↔
    Membership.mem (γ := Subalgebra R S) (integralClosure R S) y
have h : (∃ (x : A), Membership.mem (γ := Subalgebra R A) (integralClosure R A) x ∧ ((↑f : A →ₐ[R] S) : (a : A) → S) x = y) ↔
  Membership.mem (γ := Subalgebra R S) (integralClosure R S) y
Tactic: rw [Subalgebra.mem_map]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
f : A ≃ₐ[R] S
y : S
⊢ (∃ (x : A), Membership.mem (γ := Subalgebra R A) (integralClosure R A) x ∧ ((↑f : A →ₐ[R] S) : (a : A) → S) x = y) ↔
    Membership.mem (γ := Subalgebra R S) (integralClosure R S) y
have h : (∃ (x : A), Membership.mem (γ := Subalgebra R A) (integralClosure R A) x ∧ ((↑f : A →ₐ[R] S) : (a : A) → S) x = y) →
  Membership.mem (γ := Subalgebra R S) (integralClosure R S) y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
f : A ≃ₐ[R] S
y : S
h :
  (∃ (x : A), Membership.mem (γ := Subalgebra R A) (integralClosure R A) x ∧ ((↑f : A →ₐ[R] S) : (a : A) → S) x = y) →
    Membership.mem (γ := Subalgebra R S) (integralClosure R S) y
⊢ (∃ (x : A), Membership.mem (γ := Subalgebra R A) (integralClosure R A) x ∧ ((↑f : A →ₐ[R] S) : (a : A) → S) x = y) ↔
    Membership.mem (γ := Subalgebra R S) (integralClosure R S) y
have h₁ : Membership.mem (γ := Subalgebra R S) (integralClosure R S) y →
  ∃ (x : A), Membership.mem (γ := Subalgebra R A) (integralClosure R A) x ∧ ((↑f : A →ₐ[R] S) : (a : A) → S) x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
f : A ≃ₐ[R] S
y : S
hy : Membership.mem (γ := Subalgebra R S) (integralClosure R S) y
⊢ ∃ (x : A), Membership.mem (γ := Subalgebra R A) (integralClosure R A) x ∧ ((↑f : A →ₐ[R] S) : (a : A) → S) x = y
have right : ((↑f : A →ₐ[R] S) : (a : A) → S) ((f.symm : (a : S) → A) y : A) = y
Tactic: use f.symm y, hy.map (f.symm : S →ₐ[R] A)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x : ↥(integralClosure R A)
p : R[X]
hpm : p.Monic
hpx : eval₂ (algebraMap R A) (↑x : A) p = 0
⊢ (↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) : A) = (↑0 : A)
have rwa : ∀ (hpx : Eq.{u_2 + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A)),
  (↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) : A) = (↑0 : A)
Tactic: rwa [← aeval_def, ← Subalgebra.val_apply, aeval_algHom_apply] at hpx
Cleared hypotheses: hpx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x : ↥(integralClosure R A)
p : R[X]
hpm : p.Monic
hpx : eval₂ (algebraMap R A) (↑x : A) p = 0
rwa :
  ∀ (hpx : Eq.{u_2 + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A)),
    (↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) : A) = (↑0 : A)
⊢ (↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) : A) = (↑0 : A)
have rwa₁ : ∀
  (hpx :
    Eq.{u_2 + 1} (α := A)
      (((aeval ((Subalgebra.val (integralClosure R A) : (a : ↥(integralClosure R A)) → A) x) : R[X] →ₐ[R] A) :
            (a : R[X]) → A)
          p :
        A)
      (0 : A)),
  (↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) : A) = (↑0 : A)
Tactic: rwa [← aeval_def, ← Subalgebra.val_apply, aeval_algHom_apply] at hpx
Cleared hypotheses: hpx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x : ↥(integralClosure R A)
p : R[X]
hpm : p.Monic
hpx : eval₂ (algebraMap R A) (↑x : A) p = 0
rwa :
  ∀ (hpx : Eq.{u_2 + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A)),
    (↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) : A) = (↑0 : A)
rwa₁ :
  ∀
    (hpx :
      Eq.{u_2 + 1} (α := A)
        (((aeval ((Subalgebra.val (integralClosure R A) : (a : ↥(integralClosure R A)) → A) x) : R[X] →ₐ[R] A) :
              (a : R[X]) → A)
            p :
          A)
        (0 : A)),
    (↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) : A) = (↑0 : A)
⊢ (↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) : A) = (↑0 : A)
have rwa₂ : ∀
  (hpx :
    Eq (α := A)
      ((Subalgebra.val (integralClosure R A) : (a : ↥(integralClosure R A)) → A)
          ((aeval x : (a : R[X]) → ↥(integralClosure R A)) p : ↥(integralClosure R A)) :
        A)
      (0 : A)),
  (↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) : A) = (↑0 : A)
Tactic: rwa [← aeval_def, ← Subalgebra.val_apply, aeval_algHom_apply] at hpx
Cleared hypotheses: hpx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
hx : IsIntegral R (x * y)
⊢ IsIntegral R x
have obtain : ∀ (p : R[X]) (p_monic : p.Monic) (hp : eval₂ (algebraMap R B) (x * y) p = 0), IsIntegral R x
Tactic: obtain ⟨p, p_monic, hp⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ IsIntegral R x
have refine : eval₂ (algebraMap R B) x (p.scaleRoots r) = 0
Tactic: refine ⟨scaleRoots p r, (monic_scaleRoots_iff r).2 p_monic, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ eval₂ (algebraMap R B) x (p.scaleRoots r) = 0
have h : 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: convert! scaleRoots_aeval_eq_zero hp
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [Algebra.commutes] at hr ⊢
Cleared hypotheses: hr, p, p_monic, hp
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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 (HMul.hMul (β := B) (x * y) ((algebraMap R B : (a : R) → B) r : B))) : (a : R[X]) → B)
have h : Eq (α := (p : R[X]) → B) (eval₂ (algebraMap R B) x) (⇑(aeval x) : (a : R[X]) → B)
Tactic: rw [mul_assoc, hr, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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 R M.det
have 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))
Tactic: rw [Matrix.det_apply]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
have pos : ∀ (h' : 1 ≤ p.natDegree), f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
Tactic: by_cases h' : 1 ≤ p.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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)
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
have neg : ∀ (h' : ¬1 ≤ p.natDegree), f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
Tactic: by_cases h' : 1 ≤ p.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
have h₁ : p.integralNormalization.Monic ∧
  eval₂ f (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x) p.integralNormalization = 0
Tactic: use integralNormalization p
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (hypothesis)
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
⊢ False
have h'₁ : LE.le (α := ℕ) 1 0
Tactic: rw [h'', natDegree_zero] at h'
Cleared hypotheses: h', h''
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (hypothesis)
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.integralNormalization.Monic ∧
    eval₂ f (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x) p.integralNormalization = 0
have this : p ≠ 0
Tactic: have : p ≠ 0 := fun h'' => by
      rw [h'', natDegree_zero] at h'
      exact Nat.not_succ_le_zero 0 h'
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ p.integralNormalization.Monic ∧
    eval₂ f (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x) p.integralNormalization = 0
have right : eval₂ f (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x) p.integralNormalization = 0
Tactic: use monic_integralNormalization this
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ eval₂ f (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x) p.integralNormalization = 0
have right : HPow.hPow (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (p.natDegree - 1) * eval₂ f x p = 0
Tactic: rw [integralNormalization_eval₂_leadingCoeff_mul h' f x, h, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ eval₂ f (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x) p.integralNormalization = 0
have right₁ : HPow.hPow (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (p.natDegree - 1) * 0 = 0
Tactic: rw [integralNormalization_eval₂_leadingCoeff_mul h' f x, h, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ eval₂ f (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x) p.integralNormalization = 0
have right₂ : Eq.{u_4 + 1} (α := S) 0 0
Tactic: rw [integralNormalization_eval₂_leadingCoeff_mul h' f x, h, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
have pos : ∀ (hp : Polynomial.map f p = 0), f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
Tactic: by_cases hp : p.map f = 0
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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)
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
have neg : ∀ (hp : ¬Polynomial.map f p = 0), f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
Tactic: by_cases hp : p.map f = 0
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (hypothesis)
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
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
have hp₁ : (Polynomial.map f p).coeff p.natDegree = coeff 0 p.natDegree
Tactic: apply_fun fun q => coeff q p.natDegree at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (hypothesis)
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
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
have hp₁ : Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
Tactic: rw [coeff_map, coeff_zero, coeff_natDegree] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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 (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
have pos : f.IsIntegralElem 0
Tactic: rw [hp, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (hypothesis)
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
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
have h'₁ : p.natDegree = 0
Tactic: rw [Nat.one_le_iff_ne_zero, Classical.not_not] at h'
Cleared hypotheses: h', hp
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (hypothesis)
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
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
have h₁ : 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
Cleared hypotheses: h, h', hp
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ f.IsIntegralElem (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) x)
have neg : Polynomial.map f p = 0
Tactic: suffices p.map f = 0 by exact (hp this).elim
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ Polynomial.map f p = 0
have neg : Polynomial.map f ((C : (a : R) → R[X]) (p.coeff 0)) = 0
Tactic: rw [eq_C_of_natDegree_eq_zero h', map_C, h, C_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ Polynomial.map f p = 0
have neg₁ : Eq.{u_4 + 1} (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) (p.coeff 0)) : S[X]) (0 : S[X])
Tactic: rw [eq_C_of_natDegree_eq_zero h', map_C, h, C_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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])
⊢ Polynomial.map f p = 0
have neg₂ : Eq.{u_4 + 1} (α := S[X]) ((C : (a : S) → S[X]) 0) 0
Tactic: rw [eq_C_of_natDegree_eq_zero h', map_C, h, C_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ Polynomial.map f p = 0
have neg₃ : Eq.{u_4 + 1} (α := S) 0 0
Tactic: rw [eq_C_of_natDegree_eq_zero h', map_C, h, C_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (hypothesis)
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)
⊢ IsIntegral R (p.leadingCoeff • x)
have h₁ : eval₂ (algebraMap R S) x p = 0
Tactic: rw [aeval_def] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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 (p.leadingCoeff • x)
have rw : IsIntegral R (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) x)
Tactic: rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
S : Type u_4
inst : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ 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
have 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)
Tactic: rw [← (Ideal.Quotient.eq_zero_iff_mem.mpr h), eval₂_eq_sum_range]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
S : Type u_4
inst : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ 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)
have nth_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))
  ((Ideal.Quotient.mk I : (a : S[X]) → S[X] ⧸ I)
    (∑ i ∈ Finset.range (g.natDegree + 1),
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (g.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)))
Tactic: nth_rw 3 [(as_sum_range_C_mul_X_pow g)]