awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
A : Type u_1
inst_1 : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
n : ℕ
_hn : n ∈ Finset.range (p.natDegree + 1)
a :
  HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff n) : A)
      (HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) n * x ^ n) =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₁ :
  HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff n) : A)
        (HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) n) *
      x ^ n =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₂ :
  HMul.hMul (α := A) (β := A) ((f : (a : R) → A) (p.integralNormalization.coeff n) : A)
        ((f : (a : R) → A) (p.leadingCoeff ^ n) : A) *
      x ^ n =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₃ :
  HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff n * p.leadingCoeff ^ n) : A) (x ^ n) =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₄ :
  HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n * p.leadingCoeff ^ (p.natDegree - 1)) : A) (x ^ n) =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
⊢ HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff n) : A)
      (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) x ^ n) =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
have a₅ : HMul.hMul (α := A) (β := A) ((f : (a : R) → A) (p.coeff n) : A)
      ((f : (a : R) → A) (p.leadingCoeff ^ (p.natDegree - 1)) : A) *
    x ^ n =
  HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
    HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
Tactic: rw [h₁.mul_pow, ← mul_assoc, ← f.map_pow, ← f.map_mul,
    integralNormalization_coeff_mul_leadingCoeff_pow _ h, f.map_mul, h₂.eq, f.map_pow, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
A : Type u_1
inst_1 : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
n : ℕ
_hn : n ∈ Finset.range (p.natDegree + 1)
a :
  HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff n) : A)
      (HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) n * x ^ n) =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₁ :
  HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff n) : A)
        (HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) n) *
      x ^ n =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₂ :
  HMul.hMul (α := A) (β := A) ((f : (a : R) → A) (p.integralNormalization.coeff n) : A)
        ((f : (a : R) → A) (p.leadingCoeff ^ n) : A) *
      x ^ n =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₃ :
  HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff n * p.leadingCoeff ^ n) : A) (x ^ n) =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₄ :
  HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n * p.leadingCoeff ^ (p.natDegree - 1)) : A) (x ^ n) =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₅ :
  HMul.hMul (α := A) (β := A) ((f : (a : R) → A) (p.coeff n) : A)
        ((f : (a : R) → A) (p.leadingCoeff ^ (p.natDegree - 1)) : A) *
      x ^ n =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
⊢ HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff n) : A)
      (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) x ^ n) =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
have a₆ : HMul.hMul (α := A) (β := A) ((f : (a : R) → A) (p.leadingCoeff ^ (p.natDegree - 1)) : A)
      ((f : (a : R) → A) (p.coeff n) : A) *
    x ^ n =
  HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
    HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
Tactic: rw [h₁.mul_pow, ← mul_assoc, ← f.map_pow, ← f.map_mul,
    integralNormalization_coeff_mul_leadingCoeff_pow _ h, f.map_mul, h₂.eq, f.map_pow, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
have inl : ∀ (h : p.natDegree = 0),
  eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
Tactic: obtain (h | h) := p.natDegree.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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
inl :
  ∀ (h : p.natDegree = 0),
    eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
have inr : ∀ (h : p.natDegree > 0),
  eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
Tactic: obtain (h | h) := p.natDegree.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
have pos : ∀ (h0 : p.coeff 0 = 0),
  eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
Tactic: by_cases h0 : coeff p 0 = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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
pos :
  ∀ (h0 : p.coeff 0 = 0),
    eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
have neg : ∀ (h0 : ¬p.coeff 0 = 0),
  eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
Tactic: by_cases h0 : coeff p 0 = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
have pos : eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) (leadingCoeff ((C : (a : R) → R[X]) (p.coeff 0))) : A) z)
    (integralNormalization ((C : (a : R) → R[X]) (p.coeff 0))) =
  0
Tactic: rw [eq_C_of_natDegree_eq_zero h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (hypothesis)
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
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
have hz₁ : Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) (p.coeff 0) : A) (0 : A)
Tactic: rw [eq_C_of_natDegree_eq_zero h, eval₂_C] at hz
Cleared hypotheses: hz, h₁, h₂, inj, h, h0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
have inr : HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) * eval₂ f z p = 0
Tactic: rw [integralNormalization_eval₂_leadingCoeff_mul_of_commute h _ _ h₁ h₂, hz, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
have inr₁ : HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) * 0 = 0
Tactic: rw [integralNormalization_eval₂_leadingCoeff_mul_of_commute h _ _ h₁ h₂, hz, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) z) p.integralNormalization = 0
have inr₂ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [integralNormalization_eval₂_leadingCoeff_mul_of_commute h _ _ h₁ h₂, hz, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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)
⊢ (map f p).integralNormalization = map f p.integralNormalization
have a : ∀ (i : ℕ), (map f p).integralNormalization.coeff i = (map f p.integralNormalization).coeff i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsCancelMulZero R
f : R[X]
⊢ f.integralNormalization.support = f.support
have a : Nontrivial R
Tactic: nontriviality R using Subsingleton.eq_zero
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsCancelMulZero R
f : R[X]
h : Nontrivial R
⊢ f.integralNormalization.support = f.support
have this : IsDomain R
Tactic: have : IsDomain R := {}
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsCancelMulZero R
f : R[X]
h : Nontrivial R
this : IsDomain R
⊢ f.integralNormalization.support = f.support
have pos : ∀ (hf : f = 0), f.integralNormalization.support = f.support
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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
⊢ f.integralNormalization.support = f.support
have neg : ∀ (hf : ¬f = 0), f.integralNormalization.support = f.support
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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
have neg : ∀ (i : ℕ), i ∈ f.integralNormalization.support ↔ i ∈ f.support
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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
have neg : i ∈ f.support → i ∈ f.integralNormalization.support
Tactic: refine ⟨fun h => support_integralNormalization_subset h, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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.support → i ∈ f.integralNormalization.support
have neg : f.coeff i ≠ 0 → (if f.degree = (↑i : WithBot ℕ) then 1 else f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)) ≠ 0
Tactic: simp only [integralNormalization_coeff, mem_support_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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
⊢ (if f.degree = (↑i : WithBot ℕ) then 1 else f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)) ≠ 0
have pos : ∀ (hi : f.degree = (↑i : WithBot ℕ)), Ne.{u + 1} (α := R) 1 0
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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
⊢ (if f.degree = (↑i : WithBot ℕ) then 1 else f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)) ≠ 0
have neg : ∀ (hi : ¬f.degree = (↑i : WithBot ℕ)), f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i) ≠ 0
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IrreducibleRing (hypothesis)
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 f
have hi₁ : Irreducible (Polynomial.map ψ (Polynomial.map ι f))
Tactic: rw [show φ = ψ.comp ι from rfl, ← map_map] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IrreducibleRing (hypothesis)
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 f
have hi₁ : Irreducible (Polynomial.map ι f)
Tactic: replace hi := hm.map ι |>.irreducible_of_irreducible_map _ _ hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IrreducibleRing (goal)
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
have refine : ∀ (a b : R[X]) (h : f = a * b), IsUnit a ∨ IsUnit b
Tactic: refine ⟨fun h ↦ hi.1 <| (mapRingHom ι).isUnit_map h, fun a b h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IrreducibleRing (goal)
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
⊢ IsUnit a ∨ IsUnit b
have 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
Tactic: wlog hb : IsUnit (b.map ι) generalizing a b
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IrreducibleRing (goal)
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
⊢ IsUnit a ∨ IsUnit b
have wlog : ∀ (a b : R[X]) (h : f = a * b) (hb : IsUnit (Polynomial.map ι b)), IsUnit a ∨ IsUnit b
Tactic: wlog hb : IsUnit (b.map ι) generalizing a b
Cleared hypotheses: a, b, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IrreducibleRing (goal)
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)
⊢ Polynomial.map ι f = Polynomial.map ι a * Polynomial.map ι b
have rw : Polynomial.map ι (a * b) = Polynomial.map ι a * Polynomial.map ι b
Tactic: rw [h, Polynomial.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IrreducibleRing (goal)
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
⊢ Polynomial.map ι f = Polynomial.map ι a * Polynomial.map ι b
have rw₁ : Polynomial.map ι a * Polynomial.map ι b = Polynomial.map ι a * Polynomial.map ι b
Tactic: rw [h, Polynomial.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IrreducibleRing (goal)
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
⊢ IsNilpotent (b.coeff i)
have obtain : ∀ (w : R'), IsUnit w → ∀ (h : (C : (a : R') → R'[X]) w = Polynomial.map ι b), IsNilpotent (b.coeff i)
Tactic: obtain ⟨_, _, h⟩ := Polynomial.isUnit_iff.1 hb
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IrreducibleRing (hypothesis)
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)
⊢ IsUnit a ∨ IsUnit b
have hn : ∀ (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)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IrreducibleRing (goal)
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
have refine : IsUnit (-(a.coeff f.natDegree * b.coeff 0))
Tactic: refine .inr <| isUnit_of_coeff_isUnit_isNilpotent (isUnit_of_mul_isUnit_right
    (x := a.coeff f.natDegree) <| (IsUnit.neg_iff _).1 ?_) hn