awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
h_1 : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
rw : (p.comp q).leadingCoeff = 1
rw₁ : (p.comp q).coeff (p.comp q).natDegree = 1
rw₂ : (p.comp q).coeff (p.natDegree * q.natDegree) = 1
rw₃ : p.leadingCoeff * q.leadingCoeff ^ p.natDegree = 1
rw₄ : 1 * q.leadingCoeff ^ p.natDegree = 1
rw₅ : 1 * HPow.hPow (α := R) 1 p.natDegree = 1
⊢ (p.comp q).Monic
have rw₆ : HMul.hMul (α := R) 1 1 = 1
Tactic: rw [Monic.def, Polynomial.leadingCoeff, this, coeff_comp_degree_mul_degree h, hp.leadingCoeff,
    hq.leadingCoeff, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
h_1 : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
rw : (p.comp q).leadingCoeff = 1
rw₁ : (p.comp q).coeff (p.comp q).natDegree = 1
rw₂ : (p.comp q).coeff (p.natDegree * q.natDegree) = 1
rw₃ : p.leadingCoeff * q.leadingCoeff ^ p.natDegree = 1
rw₄ : 1 * q.leadingCoeff ^ p.natDegree = 1
rw₅ : 1 * HPow.hPow (α := R) 1 p.natDegree = 1
rw₆ : HMul.hMul (α := R) 1 1 = 1
⊢ (p.comp q).Monic
have rw₇ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [Monic.def, Polynomial.leadingCoeff, this, coeff_comp_degree_mul_degree h, hp.leadingCoeff,
    hq.leadingCoeff, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R
⊢ (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))).Monic
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R
h : Nontrivial R
⊢ (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))).Monic
have refine : ∀ (ha : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree = 0), False
Tactic: refine hp.comp (monic_X_add_C _) fun ha ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R
h : Nontrivial R
ha : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree = 0
⊢ False
have ha₁ : Eq (α := ℕ) 1 0
Tactic: rw [natDegree_X_add_C] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
⊢ p.degree ≤ 0 ↔ p = 1
have rw : p.degree ≤ 0 ↔ p.natDegree = 0
Tactic: rw [← hp.natDegree_eq_zero, natDegree_eq_zero_iff_degree_le_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
rw : p.degree ≤ 0 ↔ p.natDegree = 0
⊢ p.degree ≤ 0 ↔ p = 1
have rw₁ : p.degree ≤ 0 ↔ p.degree ≤ 0
Tactic: rw [← hp.natDegree_eq_zero, natDegree_eq_zero_iff_degree_le_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
⊢ (p * q).natDegree = p.natDegree + q.natDegree
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : Nontrivial R
⊢ (p * q).natDegree = p.natDegree + q.natDegree
have h : p.leadingCoeff * q.leadingCoeff ≠ 0
Tactic: apply natDegree_mul'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
⊢ (p * q).degree = (q * p).degree
have pos : ∀ (h : q = 0), (p * q).degree = (q * p).degree
Tactic: by_cases h : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
pos : ∀ (h : q = 0), (p * q).degree = (q * p).degree
⊢ (p * q).degree = (q * p).degree
have neg : ∀ (h : ¬q = 0), (p * q).degree = (q * p).degree
Tactic: by_cases h : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ (p * q).degree = (q * p).degree
have neg : p.degree + q.degree = q.degree + p.degree
Tactic: rw [degree_mul', hp.degree_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
neg : p.degree + q.degree = q.degree + p.degree
⊢ (p * q).degree = (q * p).degree
have neg₁ : p.leadingCoeff * q.leadingCoeff ≠ 0
Tactic: rw [degree_mul', hp.degree_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
have neg : 1 * q.leadingCoeff ≠ 0
Tactic: rwa [hp.leadingCoeff, one_mul, leadingCoeff_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
neg : 1 * q.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
have neg₁ : q.leadingCoeff ≠ 0
Tactic: rwa [hp.leadingCoeff, one_mul, leadingCoeff_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
neg : 1 * q.leadingCoeff ≠ 0
neg₁ : q.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
have neg₂ : q ≠ 0
Tactic: rwa [hp.leadingCoeff, one_mul, leadingCoeff_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q ≠ 0
⊢ (p * q).natDegree = p.natDegree + q.natDegree
have rw : p.leadingCoeff * q.leadingCoeff ≠ 0
Tactic: rw [natDegree_mul']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
⊢ (p * q).natDegree = (q * p).natDegree
have pos : ∀ (h : q = 0), (p * q).natDegree = (q * p).natDegree
Tactic: by_cases h : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
pos : ∀ (h : q = 0), (p * q).natDegree = (q * p).natDegree
⊢ (p * q).natDegree = (q * p).natDegree
have neg : ∀ (h : ¬q = 0), (p * q).natDegree = (q * p).natDegree
Tactic: by_cases h : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ (p * q).natDegree = (q * p).natDegree
have neg : q.leadingCoeff * p.leadingCoeff ≠ 0
Tactic: rw [hp.natDegree_mul' h, Polynomial.natDegree_mul', add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
a : R
g : R[X]
hfg : HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * g = 1
hgf : g * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = 1
⊢ False
have h : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * g).natDegree =
  (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree + g.natDegree
Tactic: have h := (monic_X_add_C a).natDegree_mul' (right_ne_zero_of_mul_eq_one hfg)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
a : R
g : R[X]
hfg : HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * g = 1
hgf : g * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = 1
h :
  (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * g).natDegree =
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree + g.natDegree
⊢ False
have h₁ : 0 = 1 + g.natDegree
Tactic: rw [hfg, natDegree_one, natDegree_X_add_C] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
h0 : p * r ≠ 0
hl : (p * r).natDegree < p.natDegree
⊢ False
have hl₁ : p.natDegree + r.natDegree < p.natDegree
Tactic: rw [hp.natDegree_mul' <| right_ne_zero_of_mul h0] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
⊢ (p * q).nextCoeff = p.nextCoeff + q.nextCoeff
have a : Nontrivial R
Tactic: nontriviality
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : Nontrivial R
⊢ (p * q).nextCoeff = p.nextCoeff + q.nextCoeff
have simp : (p * q).reverse.coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1
Tactic: simp only [← coeff_one_reverse]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : Nontrivial R
⊢ (p * q).reverse.coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1
have rw : (p.reverse * q.reverse).coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1
Tactic: rw [reverse_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : Nontrivial R
rw : (p.reverse * q.reverse).coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1
⊢ (p * q).reverse.coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1
have rw₁ : p.leadingCoeff * q.leadingCoeff ≠ 0
Tactic: rw [reverse_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
⊢ (HPow.hPow (β := ℕ) p 0).nextCoeff = HSMul.hSMul (α := ℕ) 0 p.nextCoeff
have zero : nextCoeff 1 = HSMul.hSMul (α := ℕ) 0 p.nextCoeff
Tactic: rw [pow_zero, zero_smul, ← map_one (f := C), nextCoeff_C_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
zero : nextCoeff 1 = HSMul.hSMul (α := ℕ) 0 p.nextCoeff
⊢ (HPow.hPow (β := ℕ) p 0).nextCoeff = HSMul.hSMul (α := ℕ) 0 p.nextCoeff
have zero₁ : Eq.{u + 1} (α := R) (nextCoeff 1) 0
Tactic: rw [pow_zero, zero_smul, ← map_one (f := C), nextCoeff_C_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
zero : nextCoeff 1 = HSMul.hSMul (α := ℕ) 0 p.nextCoeff
zero₁ : Eq.{u + 1} (α := R) (nextCoeff 1) 0
⊢ (HPow.hPow (β := ℕ) p 0).nextCoeff = HSMul.hSMul (α := ℕ) 0 p.nextCoeff
have zero₂ : Eq.{u + 1} (α := R) (nextCoeff ((C : (a : R) → R[X]) 1)) 0
Tactic: rw [pow_zero, zero_smul, ← map_one (f := C), nextCoeff_C_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
zero : nextCoeff 1 = HSMul.hSMul (α := ℕ) 0 p.nextCoeff
zero₁ : Eq.{u + 1} (α := R) (nextCoeff 1) 0
zero₂ : Eq.{u + 1} (α := R) (nextCoeff ((C : (a : R) → R[X]) 1)) 0
⊢ (HPow.hPow (β := ℕ) p 0).nextCoeff = HSMul.hSMul (α := ℕ) 0 p.nextCoeff
have zero₃ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [pow_zero, zero_smul, ← map_one (f := C), nextCoeff_C_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
ih : (p ^ n).nextCoeff = n • p.nextCoeff
⊢ (p ^ (n + 1)).nextCoeff = (n + 1) • p.nextCoeff
have succ : (p ^ n * p).nextCoeff = (n + 1) • p.nextCoeff
Tactic: rw [pow_succ, (hp.pow n).nextCoeff_mul hp, ih, succ_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
ih : (p ^ n).nextCoeff = n • p.nextCoeff
succ : (p ^ n * p).nextCoeff = (n + 1) • p.nextCoeff
⊢ (p ^ (n + 1)).nextCoeff = (n + 1) • p.nextCoeff
have succ₁ : (p ^ n).nextCoeff + p.nextCoeff = (n + 1) • p.nextCoeff
Tactic: rw [pow_succ, (hp.pow n).nextCoeff_mul hp, ih, succ_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
ih : (p ^ n).nextCoeff = n • p.nextCoeff
succ : (p ^ n * p).nextCoeff = (n + 1) • p.nextCoeff
succ₁ : (p ^ n).nextCoeff + p.nextCoeff = (n + 1) • p.nextCoeff
⊢ (p ^ (n + 1)).nextCoeff = (n + 1) • p.nextCoeff
have succ₂ : n • p.nextCoeff + p.nextCoeff = (n + 1) • p.nextCoeff
Tactic: rw [pow_succ, (hp.pow n).nextCoeff_mul hp, ih, succ_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
ih : (p ^ n).nextCoeff = n • p.nextCoeff
succ : (p ^ n * p).nextCoeff = (n + 1) • p.nextCoeff
succ₁ : (p ^ n).nextCoeff + p.nextCoeff = (n + 1) • p.nextCoeff
succ₂ : n • p.nextCoeff + p.nextCoeff = (n + 1) • p.nextCoeff
⊢ (p ^ (n + 1)).nextCoeff = (n + 1) • p.nextCoeff
have succ₃ : n • p.nextCoeff + p.nextCoeff = n • p.nextCoeff + p.nextCoeff
Tactic: rw [pow_succ, (hp.pow n).nextCoeff_mul hp, ih, succ_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
⊢ (p ^ n).nextCoeff = n • p.nextCoeff
have zero : (HPow.hPow (β := ℕ) p 0).nextCoeff = HSMul.hSMul (α := ℕ) 0 p.nextCoeff
Tactic: induction n with
  | zero => rw [pow_zero, zero_smul, ← map_one (f := C), nextCoeff_C_eq_zero]
  | succ n ih => rw [pow_succ, (hp.pow n).nextCoeff_mul hp, ih, succ_nsmul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
zero : (HPow.hPow (β := ℕ) p 0).nextCoeff = HSMul.hSMul (α := ℕ) 0 p.nextCoeff
⊢ (p ^ n).nextCoeff = n • p.nextCoeff
have succ : ∀ (n : ℕ) (ih : (p ^ n).nextCoeff = n • p.nextCoeff), (p ^ (n + 1)).nextCoeff = (n + 1) • p.nextCoeff
Tactic: induction n with
  | zero => rw [pow_zero, zero_smul, ← map_one (f := C), nextCoeff_C_eq_zero]
  | succ n ih => rw [pow_succ, (hp.pow n).nextCoeff_mul hp, ih, succ_nsmul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
⊢ p = 1
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h : Nontrivial R
⊢ p.degree = 0
have rw : Ne.{u_1 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
Tactic: rw [← degree_map_eq_of_leadingCoeff_ne_zero f _, map_eq, degree_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h : Nontrivial R
⊢ Ne.{u_1 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
have rw : Ne.{u_1 + 1} (α := S) 1 0
Tactic: rw [hp.leadingCoeff, f.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h : Nontrivial R
⊢ p = 1
have hdeg : p.degree = 0
Tactic: have hdeg : p.degree = 0 := by
    rw [← degree_map_eq_of_leadingCoeff_ne_zero f _, map_eq, degree_one]
    · rw [hp.leadingCoeff, f.map_one]
      exact one_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h : Nontrivial R
hdeg : p.degree = 0
⊢ p = 1
have hndeg : p.natDegree = 0
Tactic: have hndeg : p.natDegree = 0 :=
    WithBot.coe_eq_coe.mp ((degree_eq_natDegree hp.ne_zero).symm.trans hdeg)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h : Nontrivial R
hdeg : p.degree = 0
hndeg : p.natDegree = 0
⊢ p = 1
have h : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
Tactic: convert! eq_C_of_degree_eq_zero hdeg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h : Nontrivial R
hdeg : p.degree = 0
hndeg : p.natDegree = 0
⊢ Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
have h : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X])
Tactic: rw [← hndeg, ← Polynomial.leadingCoeff, hp.leadingCoeff, C.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h_1 : Nontrivial R
hdeg : p.degree = 0
hndeg : p.natDegree = 0
h : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X])
⊢ Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
have h₁ : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
Tactic: rw [← hndeg, ← Polynomial.leadingCoeff, hp.leadingCoeff, C.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h_1 : Nontrivial R
hdeg : p.degree = 0
hndeg : p.natDegree = 0
h : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X])
h₁ : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
⊢ Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
have h₂ : Eq.{u + 1} (α := R[X]) 1 ((C : (a : R) → R[X]) 1)
Tactic: rw [← hndeg, ← Polynomial.leadingCoeff, hp.leadingCoeff, C.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h_1 : Nontrivial R
hdeg : p.degree = 0
hndeg : p.natDegree = 0
h : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X])
h₁ : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
h₂ : Eq.{u + 1} (α := R[X]) 1 ((C : (a : R) → R[X]) 1)
⊢ Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
have h₃ : Eq.{u + 1} (α := R[X]) 1 1
Tactic: rw [← hndeg, ← Polynomial.leadingCoeff, hp.leadingCoeff, C.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
hn : (p ^ n).natDegree = n * p.natDegree
⊢ (p ^ (n + 1)).natDegree = (n + 1) * p.natDegree
have succ : (p ^ n * p).natDegree = (n + 1) * p.natDegree
Tactic: rw [pow_succ, (hp.pow n).natDegree_mul hp, hn, Nat.succ_mul, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
hn : (p ^ n).natDegree = n * p.natDegree
succ : (p ^ n * p).natDegree = (n + 1) * p.natDegree
⊢ (p ^ (n + 1)).natDegree = (n + 1) * p.natDegree
have succ₁ : (p ^ n).natDegree + p.natDegree = (n + 1) * p.natDegree
Tactic: rw [pow_succ, (hp.pow n).natDegree_mul hp, hn, Nat.succ_mul, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
hn : (p ^ n).natDegree = n * p.natDegree
succ : (p ^ n * p).natDegree = (n + 1) * p.natDegree
succ₁ : (p ^ n).natDegree + p.natDegree = (n + 1) * p.natDegree
⊢ (p ^ (n + 1)).natDegree = (n + 1) * p.natDegree
have succ₂ : n * p.natDegree + p.natDegree = (n + 1) * p.natDegree
Tactic: rw [pow_succ, (hp.pow n).natDegree_mul hp, hn, Nat.succ_mul, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
hn : (p ^ n).natDegree = n * p.natDegree
succ : (p ^ n * p).natDegree = (n + 1) * p.natDegree
succ₁ : (p ^ n).natDegree + p.natDegree = (n + 1) * p.natDegree
succ₂ : n * p.natDegree + p.natDegree = (n + 1) * p.natDegree
⊢ (p ^ (n + 1)).natDegree = (n + 1) * p.natDegree
have succ₃ : n * p.natDegree + p.natDegree = n * p.natDegree + p.natDegree
Tactic: rw [pow_succ, (hp.pow n).natDegree_mul hp, hn, Nat.succ_mul, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
hn : (p ^ n).natDegree = n * p.natDegree
succ : (p ^ n * p).natDegree = (n + 1) * p.natDegree
succ₁ : (p ^ n).natDegree + p.natDegree = (n + 1) * p.natDegree
succ₂ : n * p.natDegree + p.natDegree = (n + 1) * p.natDegree
succ₃ : n * p.natDegree + p.natDegree = n * p.natDegree + p.natDegree
⊢ (p ^ (n + 1)).natDegree = (n + 1) * p.natDegree
have succ₄ : p.natDegree + n * p.natDegree = p.natDegree + n * p.natDegree
Tactic: rw [pow_succ, (hp.pow n).natDegree_mul hp, hn, Nat.succ_mul, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
⊢ (p ^ n).natDegree = n * p.natDegree
have zero : (HPow.hPow (β := ℕ) p 0).natDegree = 0 * p.natDegree
Tactic: induction n with
  | zero => simp
  | succ n hn => rw [pow_succ, (hp.pow n).natDegree_mul hp, hn, Nat.succ_mul, add_comm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
zero : (HPow.hPow (β := ℕ) p 0).natDegree = 0 * p.natDegree
⊢ (p ^ n).natDegree = n * p.natDegree
have succ : ∀ (n : ℕ) (hn : (p ^ n).natDegree = n * p.natDegree), (p ^ (n + 1)).natDegree = (n + 1) * p.natDegree
Tactic: induction n with
  | zero => simp
  | succ n hn => rw [pow_succ, (hp.pow n).natDegree_mul hp, hn, Nat.succ_mul, add_comm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
r : R
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ n).natDegree = n
have rw : n * (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree = n
Tactic: rw [(monic_X_add_C r).natDegree_pow, natDegree_X_add_C, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
r : R
rw : n * (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree = n
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ n).natDegree = n
have rw₁ : n * 1 = n
Tactic: rw [(monic_X_add_C r).natDegree_pow, natDegree_X_add_C, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
r : R
rw : n * (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree = n
rw₁ : n * 1 = n
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ n).natDegree = n
have rw₂ : n = n
Tactic: rw [(monic_X_add_C r).natDegree_pow, natDegree_X_add_C, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
⊢ p = 1
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
h : Nontrivial R
⊢ p = 1
have obtain : ∀ (q : R[X]) (h : p * q = 1), p = 1
Tactic: obtain ⟨q, h⟩ := hpu.exists_right_inv
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
h_1 : Nontrivial R
q : R[X]
h : p * q = 1
⊢ p = 1
have this : (p * q).natDegree = p.natDegree + q.natDegree
Tactic: have := hm.natDegree_mul' (right_ne_zero_of_mul_eq_one h)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
h_1 : Nontrivial R
q : R[X]
h : p * q = 1
this : (p * q).natDegree = p.natDegree + q.natDegree
⊢ p = 1
have this₁ : p.natDegree = 0 ∧ q.natDegree = 0
Tactic: rw [h, natDegree_one, eq_comm, add_eq_zero] at this
Cleared hypotheses: this