awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
A : Type u_1
inst_1 : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
inj : ∀ (x : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) x : A) (0 : A) → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
hz₁ : Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) (p.coeff 0) : A) (0 : A)
h₃ : Commute ((f : (a : R) → A) p.leadingCoeff) z
h₄ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
inj₁ : ∀ (x : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) x : A) (0 : A) → x = 0
⊢ p.natDegree = 0

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

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, Polynomial.eval₂_C
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
A : Type u_1
inst_1 : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
inj : ∀ (x : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) x : A) (0 : A) → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
hz₁ : Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) (p.coeff 0) : A) (0 : A)
h₃ : Commute ((f : (a : R) → A) p.leadingCoeff) z
h₄ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
inj₁ : ∀ (x : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) x : A) (0 : A) → x = 0
h₅ : p.natDegree = 0
⊢ ¬p.coeff 0 = 0

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

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, Polynomial.eval₂_C
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
A : Type u_1
inst_1 : Semiring A
p : R[X]
f : R →+* A
z : A
hz : Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) (p.coeff 0) : A) (0 : A)
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
inj : ∀ (x : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) x : A) (0 : A) → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0

Tactic:
absurd (inj _ hz) h0

Premises used: absurd
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
A : Type u_1
inst_1 : Semiring A
p : R[X]
f : R →+* A
z : A
hz : Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) (p.coeff 0) : A) (0 : A)
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
inj : ∀ (x : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) x : A) (0 : A) → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0

Tactic:
exact absurd (inj _ hz) h0

Premises used: absurd
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
A : Type u_1
inst_1 : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
inj : ∀ (x : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) x : A) (0 : A) → x = 0
h : p.natDegree > 0
inr : HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) * eval₂ f z p = 0
inr₁ : HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) * 0 = 0
inr₂ inr₃ : Eq.{u_1 + 1} (α := A) 0 0
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0

Tactic:
rw [integralNormalization_eval₂_leadingCoeff_mul_of_commute h _ _ h₁ h₂, hz, mul_zero]

Premises used: MulZeroClass.mul_zero, Polynomial.integralNormalization_eval₂_leadingCoeff_mul_of_commute
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
⊢ eval₂ f (HMul.hMul (α := S) ((f : (a : R) → S) p.leadingCoeff : S) z) p.integralNormalization = 0

Tactic:
integralNormalization_eval₂_eq_zero_of_commute _ hz (.all _ _) (.all _ _) inj

Premises used: Commute.all, DFunLike.coe, Polynomial.integralNormalization_eval₂_eq_zero_of_commute
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
S : Type v
A : Type u_1
inst : CommSemiring S
inst_1 : Semiring A
inst_2 : Algebra S A
f : S[X]
z : A
hz : Eq.{u_1 + 1} (α := A) ((aeval z : (a : S[X]) → A) f : A) (0 : A)
inj : ∀ (x : S), Eq.{u_1 + 1} (α := A) ((algebraMap S A : (a : S) → A) x : A) (0 : A) → x = 0
⊢ Eq.{u_1 + 1} (α := A)
    ((aeval (HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) f.leadingCoeff : A) z) : (a : S[X]) → A)
        f.integralNormalization :
      A)
    (0 : A)

Tactic:
integralNormalization_eval₂_eq_zero_of_commute (algebraMap S A) hz
    (Algebra.commute_algebraMap_left _ _) (.map (.all _ _) _) inj

Premises used: Algebra.algebraMap, MonoidHomClass.toMonoidHom, Algebra.commute_algebraMap_left, RingHomClass.toRingHom, Commute.map, Commute.all, Polynomial.integralNormalization_eval₂_eq_zero_of_commute
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
A : Type u_1
inst_1 : Semiring A
f : R →+* A
p : R[X]
H : Ne.{u_1 + 1} (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (0 : A)
a : ∀ (i : ℕ), (map f p).integralNormalization.coeff i = (map f p.integralNormalization).coeff i
⊢ (map f p).integralNormalization = map f p.integralNormalization

Tactic:
ext i
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
A : Type u_1
inst_1 : Semiring A
f : R →+* A
p : R[X]
H : Ne.{u_1 + 1} (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (0 : A)
i : ℕ
⊢ (map f p).integralNormalization.coeff i = (map f p.integralNormalization).coeff i

Tactic:
simp [integralNormalization_coeff, degree_map_eq_of_leadingCoeff_ne_zero _ H, apply_ite f,
    leadingCoeff_map_of_leadingCoeff_ne_zero _ H, natDegree_map_eq_iff.mpr (.inl H)]

Premises used: Iff.mpr, Polynomial.natDegree_map_eq_iff, apply_ite, Polynomial.degree_map_eq_of_leadingCoeff_ne_zero, Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero, Polynomial.integralNormalization_coeff, Or.inl, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
inst_1 : IsCancelMulZero R
f : R[X]
⊢ Nontrivial R

Tactic:
nontriviality R using Subsingleton.eq_zero

Premises used: Subsingleton.eq_zero
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
inst_1 : IsCancelMulZero R
f : R[X]
h : Nontrivial R
⊢ IsDomain R

Tactic:
have : IsDomain R := {}
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
inst_1 : IsCancelMulZero R
f : R[X]
h : Nontrivial R
this : IsDomain R
pos : ∀ (hf : f = 0), f.integralNormalization.support = f.support
neg : ∀ (hf : ¬f = 0), f.integralNormalization.support = f.support
⊢ f.integralNormalization.support = f.support

Tactic:
by_cases hf : f = 0
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
inst_1 : IsCancelMulZero R
f : R[X]
h : Nontrivial R
this : IsDomain R
hf : f = 0
⊢ f.integralNormalization.support = f.support

Tactic:
simp [hf]
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
inst_1 : IsCancelMulZero R
f : R[X]
h : Nontrivial R
this : IsDomain R
hf : ¬f = 0
neg : ∀ (i : ℕ), i ∈ f.integralNormalization.support ↔ i ∈ f.support
⊢ f.integralNormalization.support = f.support

Tactic:
ext i
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
inst_1 : IsCancelMulZero R
f : R[X]
h : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
⊢ i ∈ f.integralNormalization.support ↔ i ∈ f.support

Tactic:
⟨fun h => support_integralNormalization_subset h, ?_⟩

Premises used: Polynomial.support_integralNormalization_subset, Iff.intro
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
inst_1 : IsCancelMulZero R
f : R[X]
h : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
neg : i ∈ f.support → i ∈ f.integralNormalization.support
⊢ i ∈ f.integralNormalization.support ↔ i ∈ f.support

Tactic:
refine ⟨fun h => support_integralNormalization_subset h, ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
inst_1 : IsCancelMulZero R
f : R[X]
h : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
neg :
  f.coeff i ≠ 0 → (if f.degree = (↑i : WithBot ℕ) then 1 else f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)) ≠ 0
⊢ i ∈ f.support → i ∈ f.integralNormalization.support

Tactic:
simp only [integralNormalization_coeff, mem_support_iff]

Premises used: Polynomial.mem_support_iff, Polynomial.integralNormalization_coeff
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
inst_1 : IsCancelMulZero R
f : R[X]
h : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
hfi : f.coeff i ≠ 0
pos : ∀ (hi : f.degree = (↑i : WithBot ℕ)), Ne.{u + 1} (α := R) 1 0
neg : ∀ (hi : ¬f.degree = (↑i : WithBot ℕ)), f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i) ≠ 0
⊢ (if f.degree = (↑i : WithBot ℕ) then 1 else f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)) ≠ 0

Tactic:
split_ifs with hi
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
inst_1 : IsCancelMulZero R
f : R[X]
h : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
hfi : f.coeff i ≠ 0
hi : f.degree = (↑i : WithBot ℕ)
⊢ Ne.{u + 1} (α := R) 1 0

Tactic:
simp [hf, hfi]
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
inst_1 : IsCancelMulZero R
f : R[X]
h : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
hfi : f.coeff i ≠ 0
hi : ¬f.degree = (↑i : WithBot ℕ)
⊢ f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i) ≠ 0

Tactic:
simp [hf, hfi]
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
hi : Irreducible (Polynomial.map φ f)
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
⊢ Irreducible (Polynomial.map ψ (Polynomial.map ι f))

Tactic:
rw [show φ = ψ.comp ι from rfl, ← map_map] at hi

Premises used: Polynomial.map_map, rfl
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ψ (Polynomial.map ι f))
⊢ Irreducible (Polynomial.map ι f)

Tactic:
replace hi := hm.map ι |>.irreducible_of_irreducible_map _ _ hi
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
⊢ Irreducible f

Tactic:
⟨fun h ↦ hi.1 <| (mapRingHom ι).isUnit_map h, fun a b h ↦ ?_⟩

Premises used: Irreducible.not_isUnit, Irreducible.mk, Polynomial.mapRingHom, RingHom.isUnit_map
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
refine : ∀ (a b : R[X]) (h : f = a * b), IsUnit a ∨ IsUnit b
⊢ Irreducible f

Tactic:
refine ⟨fun h ↦ hi.1 <| (mapRingHom ι).isUnit_map h, fun a b h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
inr :
  ∀ (this : ∀ (a b : R[X]) (h : f = a * b) (hb : IsUnit (Polynomial.map ι b)), IsUnit a ∨ IsUnit b)
    (hb : ¬IsUnit (Polynomial.map ι b)), IsUnit a ∨ IsUnit b
wlog : ∀ (a b : R[X]) (h : f = a * b) (hb : IsUnit (Polynomial.map ι b)), IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
wlog hb : IsUnit (b.map ι) generalizing a b

Premises used: IsUnit, Polynomial.map
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
this : ∀ (a b : R[X]) (h : f = a * b) (hb : IsUnit (Polynomial.map ι b)), IsUnit a ∨ IsUnit b
hb : ¬IsUnit (Polynomial.map ι b)
rw : Polynomial.map ι (a * b) = Polynomial.map ι a * Polynomial.map ι b
rw₁ rw₂ : Polynomial.map ι a * Polynomial.map ι b = Polynomial.map ι a * Polynomial.map ι b
⊢ Polynomial.map ι f = Polynomial.map ι a * Polynomial.map ι b

Tactic:
rw [h, Polynomial.map_mul]

Premises used: Polynomial.map_mul
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
this : ∀ (a b : R[X]) (h : f = a * b) (hb : IsUnit (Polynomial.map ι b)), IsUnit a ∨ IsUnit b
hb : ¬IsUnit (Polynomial.map ι b)
⊢ IsUnit a ∨ IsUnit b

Tactic:
exact (this b a (mul_comm a b ▸ h)
      (hi.2 (by rw [h, Polynomial.map_mul]) |>.resolve_right hb)).symm

Premises used: Eq.rec, Or.symm, Irreducible.isUnit_or_isUnit, mul_comm, Or.resolve_right
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi_1 : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
i : ℕ
hi : i ≠ 0
obtain : ∀ (w : R'), IsUnit w → ∀ (h : (C : (a : R') → R'[X]) w = Polynomial.map ι b), IsNilpotent (b.coeff i)
⊢ IsNilpotent (b.coeff i)

Tactic:
obtain ⟨_, _, h⟩ := Polynomial.isUnit_iff.1 hb

Premises used: Polynomial.isUnit_iff, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi_1 : Irreducible (Polynomial.map ι f)
a b : R[X]
h_1 : f = a * b
hb : IsUnit (Polynomial.map ι b)
i : ℕ
hi : i ≠ 0
w : R'
left : IsUnit w
h : (C : (a : R') → R'[X]) w = Polynomial.map ι b
⊢ IsNilpotent (b.coeff i)

Tactic:
simpa only [coeff_map, coeff_C, hi, ite_false, ← RingHom.mem_ker,
      show RingHom.ker ι = nilradical R from Ideal.mk_ker] using congr(coeff $(h.symm) i)

Premises used: Polynomial.coeff_map, ite_false, RingHom.mem_ker, Polynomial.coeff_C, Ideal.mk_ker
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
⊢ ∀ (i : ℕ) (hi : i ≠ 0), IsNilpotent (b.coeff i)

Tactic:
have hn (i : ℕ) (hi : i ≠ 0) : IsNilpotent (b.coeff i) := by
    obtain ⟨_, _, h⟩ := Polynomial.isUnit_iff.1 hb
    simpa only [coeff_map, coeff_C, hi, ite_false, ← RingHom.mem_ker,
      show RingHom.ker ι = nilradical R from Ideal.mk_ker] using congr(coeff $(h.symm) i)
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ) (hi : i ≠ 0), IsNilpotent (b.coeff i)
⊢ IsUnit a ∨ IsUnit b

Tactic:
.inr <| isUnit_of_coeff_isUnit_isNilpotent (isUnit_of_mul_isUnit_right
    (x := a.coeff f.natDegree) <| (IsUnit.neg_iff _).1 ?_) hn

Premises used: Polynomial.isUnit_of_coeff_isUnit_isNilpotent, isUnit_of_mul_isUnit_right, IsUnit.neg_iff, Iff.mp, Or.inr
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ) (hi : i ≠ 0), IsNilpotent (b.coeff i)
refine : IsUnit (-(a.coeff f.natDegree * b.coeff 0))
⊢ IsUnit a ∨ IsUnit b

Tactic:
refine .inr <| isUnit_of_coeff_isUnit_isNilpotent (isUnit_of_mul_isUnit_right
    (x := a.coeff f.natDegree) <| (IsUnit.neg_iff _).1 ?_) hn

Premises used: Polynomial.isUnit_of_coeff_isUnit_isNilpotent, isUnit_of_mul_isUnit_right, IsUnit.neg_iff, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ) (hi : i ≠ 0), IsNilpotent (b.coeff i)
⊢ f.leadingCoeff = coeff (a * b) f.natDegree

Tactic:
have hc : f.leadingCoeff = _ := congr(coeff $h f.natDegree)
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ) (hi : i ≠ 0), IsNilpotent (b.coeff i)
hc : f.leadingCoeff = coeff (a * b) f.natDegree
⊢ 1 - a.coeff f.natDegree * b.coeff 0 = ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)

Tactic:
rw [hm, coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j ↦ a.coeff i * b.coeff j,
    Finset.sum_range_succ, ← sub_eq_iff_eq_add, Nat.sub_self] at hc

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ, HMul.hMul, Polynomial.coeff_mul, Polynomial.coeff, Nat.sub_self, sub_eq_iff_eq_add, Finset.sum_range_succ
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ) (hi : i ≠ 0), IsNilpotent (b.coeff i)
hc : 1 - a.coeff f.natDegree * b.coeff 0 = ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)
rw : IsUnit (HSub.hSub (α := R) (∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)) 1)
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))

Tactic:
rw [← add_sub_cancel_left 1 (-(_ * _)), ← sub_eq_add_neg, hc]

Premises used: HMul.hMul, add_sub_cancel_left, sub_eq_add_neg, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ) (hi : i ≠ 0), IsNilpotent (b.coeff i)
hc : 1 - a.coeff f.natDegree * b.coeff 0 = ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)
⊢ IsUnit (HSub.hSub (α := R) (∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)) 1)

Tactic:
IsNilpotent.isUnit_sub_one <| show _ ∈ nilradical R from sum_mem fun i hi ↦
    Ideal.mul_mem_left _ _ <| hn _ <| Nat.sub_ne_zero_of_lt (List.mem_range.1 hi)

Premises used: IsNilpotent.isUnit_sub_one, List.mem_range, HSub.hSub, Polynomial.coeff, Nat.sub_ne_zero_of_lt, Iff.mp, Polynomial.natDegree, Ideal.mul_mem_left, sum_mem, nilradical
-- Module: Mathlib.RingTheory.Polynomial.IrreducibleRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ) (hi : i ≠ 0), IsNilpotent (b.coeff i)
hc : 1 - a.coeff f.natDegree * b.coeff 0 = ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)
⊢ IsUnit (HSub.hSub (α := R) (∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)) 1)

Tactic:
exact IsNilpotent.isUnit_sub_one <| show _ ∈ nilradical R from sum_mem fun i hi ↦
    Ideal.mul_mem_left _ _ <| hn _ <| Nat.sub_ne_zero_of_lt (List.mem_range.1 hi)

Premises used: IsNilpotent.isUnit_sub_one, List.mem_range, HSub.hSub, Nat.sub_ne_zero_of_lt, Iff.mp, Ideal.mul_mem_left, sum_mem, nilradical
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : ι → S[X]
H : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ (j : ℕ), IsIntegral R ((p i).coeff j)
j : ℕ
⊢ IsIntegral R ((Finset.prod ∅ p).coeff j)

Tactic:
simp [coeff_one, apply_ite, isIntegral_zero, isIntegral_one]

Premises used: Polynomial.coeff_one, apply_ite, isIntegral_one, isIntegral_zero