awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
⊢ (f * g).reverse = f.reverse * g.reverse
have pos : ∀ (g0 : g = 0), (f * g).reverse = f.reverse * g.reverse
Tactic: by_cases g0 : g = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
pos : ∀ (g0 : g = 0), (f * g).reverse = f.reverse * g.reverse
⊢ (f * g).reverse = f.reverse * g.reverse
have neg : ∀ (g0 : ¬g = 0), (f * g).reverse = f.reverse * g.reverse
Tactic: by_cases g0 : g = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : g = 0
⊢ (f * g).reverse = f.reverse * g.reverse
have pos : (f * 0).reverse = f.reverse * reverse 0
Tactic: rw [g0, mul_zero, reverse_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : g = 0
pos : (f * 0).reverse = f.reverse * reverse 0
⊢ (f * g).reverse = f.reverse * g.reverse
have pos₁ : reverse 0 = f.reverse * reverse 0
Tactic: rw [g0, mul_zero, reverse_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : g = 0
pos : (f * 0).reverse = f.reverse * reverse 0
pos₁ : reverse 0 = f.reverse * reverse 0
⊢ (f * g).reverse = f.reverse * g.reverse
have pos₂ : 0 = f.reverse * 0
Tactic: rw [g0, mul_zero, reverse_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : g = 0
pos : (f * 0).reverse = f.reverse * reverse 0
pos₁ : reverse 0 = f.reverse * reverse 0
pos₂ : 0 = f.reverse * 0
⊢ (f * g).reverse = f.reverse * g.reverse
have pos₃ : Eq.{u_2 + 1} (α := R[X]) 0 0
Tactic: rw [g0, mul_zero, reverse_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
⊢ (p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff
have rw : (p * q).reverse.leadingCoeff = p.trailingCoeff * q.trailingCoeff
Tactic: rw [← reverse_leadingCoeff, reverse_mul_of_domain, leadingCoeff_mul, reverse_leadingCoeff,
    reverse_leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
rw : (p * q).reverse.leadingCoeff = p.trailingCoeff * q.trailingCoeff
⊢ (p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff
have rw₁ : (p.reverse * q.reverse).leadingCoeff = p.trailingCoeff * q.trailingCoeff
Tactic: rw [← reverse_leadingCoeff, reverse_mul_of_domain, leadingCoeff_mul, reverse_leadingCoeff,
    reverse_leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
rw : (p * q).reverse.leadingCoeff = p.trailingCoeff * q.trailingCoeff
rw₁ : (p.reverse * q.reverse).leadingCoeff = p.trailingCoeff * q.trailingCoeff
⊢ (p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff
have rw₂ : p.reverse.leadingCoeff * q.reverse.leadingCoeff = p.trailingCoeff * q.trailingCoeff
Tactic: rw [← reverse_leadingCoeff, reverse_mul_of_domain, leadingCoeff_mul, reverse_leadingCoeff,
    reverse_leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
rw : (p * q).reverse.leadingCoeff = p.trailingCoeff * q.trailingCoeff
rw₁ : (p.reverse * q.reverse).leadingCoeff = p.trailingCoeff * q.trailingCoeff
rw₂ : p.reverse.leadingCoeff * q.reverse.leadingCoeff = p.trailingCoeff * q.trailingCoeff
⊢ (p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff
have rw₃ : p.trailingCoeff * q.reverse.leadingCoeff = p.trailingCoeff * q.trailingCoeff
Tactic: rw [← reverse_leadingCoeff, reverse_mul_of_domain, leadingCoeff_mul, reverse_leadingCoeff,
    reverse_leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
rw : (p * q).reverse.leadingCoeff = p.trailingCoeff * q.trailingCoeff
rw₁ : (p.reverse * q.reverse).leadingCoeff = p.trailingCoeff * q.trailingCoeff
rw₂ : p.reverse.leadingCoeff * q.reverse.leadingCoeff = p.trailingCoeff * q.trailingCoeff
rw₃ : p.trailingCoeff * q.reverse.leadingCoeff = p.trailingCoeff * q.trailingCoeff
⊢ (p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff
have rw₄ : p.trailingCoeff * q.trailingCoeff = p.trailingCoeff * q.trailingCoeff
Tactic: rw [← reverse_leadingCoeff, reverse_mul_of_domain, leadingCoeff_mul, reverse_leadingCoeff,
    reverse_leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.reverse.coeff 1 = f.nextCoeff
have rw : f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 1) = if f.natDegree = 0 then 0 else f.coeff (f.natDegree - 1)
Tactic: rw [coeff_reverse, nextCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 1) = if f.natDegree = 0 then 0 else f.coeff (f.natDegree - 1)
have pos : ∀ (hf : f.natDegree = 0), f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 1) = 0
Tactic: split_ifs with hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
pos : ∀ (hf : f.natDegree = 0), f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 1) = 0
⊢ f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 1) = if f.natDegree = 0 then 0 else f.coeff (f.natDegree - 1)
have neg : ∀ (hf : ¬f.natDegree = 0), f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 1) = f.coeff (f.natDegree - 1)
Tactic: split_ifs with hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.natDegree = 0
⊢ f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 1) = 0
have this : f.coeff 1 = 0
Tactic: have : coeff f 1 = 0 := coeff_eq_zero_of_natDegree_lt (by simp only [hf, zero_lt_one])
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f.natDegree = 0
⊢ f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 1) = f.coeff (f.natDegree - 1)
have neg : 1 ≤ f.natDegree
Tactic: rw [revAt_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ (p * X).reverse = p.reverse
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
h : Nontrivial R
⊢ (p * X).reverse = p.reverse
have inl : (HMul.hMul (α := R[X]) 0 X).reverse = reverse 0
Tactic: rcases eq_or_ne p 0 with rfl | hp
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
h : Nontrivial R
inl : (HMul.hMul (α := R[X]) 0 X).reverse = reverse 0
⊢ (p * X).reverse = p.reverse
have inr : ∀ (hp : p ≠ 0), (p * X).reverse = p.reverse
Tactic: rcases eq_or_ne p 0 with rfl | hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ (X * p).reverse = p.reverse
have rw : (p * X).reverse = p.reverse
Tactic: rw [commute_X p, reverse_mul_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
rw : (p * X).reverse = p.reverse
⊢ (X * p).reverse = p.reverse
have rw₁ : p.reverse = p.reverse
Tactic: rw [commute_X p, reverse_mul_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
ih : (p * HPow.hPow (α := R[X]) X n).reverse = p.reverse
⊢ (p * HPow.hPow (α := R[X]) X (n + 1)).reverse = p.reverse
have succ : (p * (HPow.hPow (α := R[X]) X n * X)).reverse = p.reverse
Tactic: rw [pow_succ, ← mul_assoc, reverse_mul_X, ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
ih : (p * HPow.hPow (α := R[X]) X n).reverse = p.reverse
succ : (p * (HPow.hPow (α := R[X]) X n * X)).reverse = p.reverse
⊢ (p * HPow.hPow (α := R[X]) X (n + 1)).reverse = p.reverse
have succ₁ : (p * HPow.hPow (α := R[X]) X n * X).reverse = p.reverse
Tactic: rw [pow_succ, ← mul_assoc, reverse_mul_X, ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
ih : (p * HPow.hPow (α := R[X]) X n).reverse = p.reverse
succ : (p * (HPow.hPow (α := R[X]) X n * X)).reverse = p.reverse
succ₁ : (p * HPow.hPow (α := R[X]) X n * X).reverse = p.reverse
succ₂ : (p * HPow.hPow (α := R[X]) X n).reverse = p.reverse
⊢ (p * HPow.hPow (α := R[X]) X (n + 1)).reverse = p.reverse
have succ₃ : p.reverse = p.reverse
Tactic: rw [pow_succ, ← mul_assoc, reverse_mul_X, ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
⊢ (p * HPow.hPow (α := R[X]) X n).reverse = p.reverse
have zero : (p * HPow.hPow (α := R[X]) (β := ℕ) X 0).reverse = p.reverse
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, ← mul_assoc, reverse_mul_X, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
zero : (p * HPow.hPow (α := R[X]) (β := ℕ) X 0).reverse = p.reverse
⊢ (p * HPow.hPow (α := R[X]) X n).reverse = p.reverse
have succ : ∀ (n : ℕ) (ih : (p * HPow.hPow (α := R[X]) X n).reverse = p.reverse),
  (p * HPow.hPow (α := R[X]) X (n + 1)).reverse = p.reverse
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, ← mul_assoc, reverse_mul_X, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n * p).reverse = p.reverse
have rw : (p * HPow.hPow (α := R[X]) X n).reverse = p.reverse
Tactic: rw [commute_X_pow p, reverse_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
rw : (p * HPow.hPow (α := R[X]) X n).reverse = p.reverse
⊢ (HPow.hPow (α := R[X]) X n * p).reverse = p.reverse
have rw₁ : p.reverse = p.reverse
Tactic: rw [commute_X_pow p, reverse_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
t : R
⊢ (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) p).reverse =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) + p.reverse
have rw : (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) t : R[X])).reverse =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) + p.reverse
Tactic: rw [add_comm, reverse_add_C, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
t : R
rw :
  (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) t : R[X])).reverse =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) + p.reverse
⊢ (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) p).reverse =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) + p.reverse
have rw₁ : p.reverse + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) + p.reverse
Tactic: rw [add_comm, reverse_add_C, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
t : R
rw :
  (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) t : R[X])).reverse =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) + p.reverse
rw₁ :
  p.reverse + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) + p.reverse
⊢ (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) p).reverse =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) + p.reverse
have rw₂ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) + p.reverse =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) + p.reverse
Tactic: rw [add_comm, reverse_add_C, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Ring R
f : R[X]
N : ℕ
⊢ reflect N (-f) = -reflect N f
have rw : reflect N (-1 * f) = -reflect N f
Tactic: rw [neg_eq_neg_one_mul, ← C_1, ← C_neg, reflect_C_mul, C_neg, C_1, ← neg_eq_neg_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Ring R
f : R[X]
N : ℕ
rw : reflect N (-1 * f) = -reflect N f
⊢ reflect N (-f) = -reflect N f
have rw₁ : reflect N (-(C : (a : R) → R[X]) 1 * f) = -reflect N f
Tactic: rw [neg_eq_neg_one_mul, ← C_1, ← C_neg, reflect_C_mul, C_neg, C_1, ← neg_eq_neg_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Ring R
f : R[X]
N : ℕ
rw : reflect N (-1 * f) = -reflect N f
rw₁ : reflect N (-(C : (a : R) → R[X]) 1 * f) = -reflect N f
⊢ reflect N (-f) = -reflect N f
have rw₂ : reflect N ((C : (a : R) → R[X]) (-1) * f) = -reflect N f
Tactic: rw [neg_eq_neg_one_mul, ← C_1, ← C_neg, reflect_C_mul, C_neg, C_1, ← neg_eq_neg_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Ring R
f : R[X]
N : ℕ
rw : reflect N (-1 * f) = -reflect N f
rw₁ : reflect N (-(C : (a : R) → R[X]) 1 * f) = -reflect N f
rw₂ : reflect N ((C : (a : R) → R[X]) (-1) * f) = -reflect N f
⊢ reflect N (-f) = -reflect N f
have rw₃ : (C : (a : R) → R[X]) (-1) * reflect N f = -reflect N f
Tactic: rw [neg_eq_neg_one_mul, ← C_1, ← C_neg, reflect_C_mul, C_neg, C_1, ← neg_eq_neg_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Ring R
f : R[X]
N : ℕ
rw : reflect N (-1 * f) = -reflect N f
rw₁ : reflect N (-(C : (a : R) → R[X]) 1 * f) = -reflect N f
rw₂ : reflect N ((C : (a : R) → R[X]) (-1) * f) = -reflect N f
rw₃ : (C : (a : R) → R[X]) (-1) * reflect N f = -reflect N f
⊢ reflect N (-f) = -reflect N f
have rw₄ : -(C : (a : R) → R[X]) 1 * reflect N f = -reflect N f
Tactic: rw [neg_eq_neg_one_mul, ← C_1, ← C_neg, reflect_C_mul, C_neg, C_1, ← neg_eq_neg_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Ring R
f : R[X]
N : ℕ
rw : reflect N (-1 * f) = -reflect N f
rw₁ : reflect N (-(C : (a : R) → R[X]) 1 * f) = -reflect N f
rw₂ : reflect N ((C : (a : R) → R[X]) (-1) * f) = -reflect N f
rw₃ : (C : (a : R) → R[X]) (-1) * reflect N f = -reflect N f
rw₄ : -(C : (a : R) → R[X]) 1 * reflect N f = -reflect N f
⊢ reflect N (-f) = -reflect N f
have rw₅ : -1 * reflect N f = -reflect N f
Tactic: rw [neg_eq_neg_one_mul, ← C_1, ← C_neg, reflect_C_mul, C_neg, C_1, ← neg_eq_neg_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Ring R
f : R[X]
N : ℕ
rw : reflect N (-1 * f) = -reflect N f
rw₁ : reflect N (-(C : (a : R) → R[X]) 1 * f) = -reflect N f
rw₂ : reflect N ((C : (a : R) → R[X]) (-1) * f) = -reflect N f
rw₃ : (C : (a : R) → R[X]) (-1) * reflect N f = -reflect N f
rw₄ : -(C : (a : R) → R[X]) 1 * reflect N f = -reflect N f
rw₅ : -1 * reflect N f = -reflect N f
⊢ reflect N (-f) = -reflect N f
have rw₆ : -reflect N f = -reflect N f
Tactic: rw [neg_eq_neg_one_mul, ← C_1, ← C_neg, reflect_C_mul, C_neg, C_1, ← neg_eq_neg_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Ring R
f g : R[X]
N : ℕ
⊢ reflect N (f - g) = reflect N f - reflect N g
have rw : reflect N (f + -g) = reflect N f - reflect N g
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, reflect_add, reflect_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Ring R
f g : R[X]
N : ℕ
rw : reflect N (f + -g) = reflect N f - reflect N g
⊢ reflect N (f - g) = reflect N f - reflect N g
have rw₁ : reflect N (f + -g) = reflect N f + -reflect N g
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, reflect_add, reflect_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Ring R
f g : R[X]
N : ℕ
rw : reflect N (f + -g) = reflect N f - reflect N g
rw₁ : reflect N (f + -g) = reflect N f + -reflect N g
⊢ reflect N (f - g) = reflect N f - reflect N g
have rw₂ : reflect N f + reflect N (-g) = reflect N f + -reflect N g
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, reflect_add, reflect_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Ring R
f g : R[X]
N : ℕ
rw : reflect N (f + -g) = reflect N f - reflect N g
rw₁ : reflect N (f + -g) = reflect N f + -reflect N g
rw₂ : reflect N f + reflect N (-g) = reflect N f + -reflect N g
⊢ reflect N (f - g) = reflect N f - reflect N g
have rw₃ : reflect N f + -reflect N g = reflect N f + -reflect N g
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, reflect_add, reflect_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Ring R
f : R[X]
⊢ (-f).reverse = -f.reverse
have rw : reflect (-f).natDegree (-f) = -f.reverse
Tactic: rw [reverse, reverse, reflect_neg, natDegree_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Ring R
f : R[X]
rw : reflect (-f).natDegree (-f) = -f.reverse
⊢ (-f).reverse = -f.reverse
have rw₁ : reflect (-f).natDegree (-f) = -reflect f.natDegree f
Tactic: rw [reverse, reverse, reflect_neg, natDegree_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Ring R
f : R[X]
rw : reflect (-f).natDegree (-f) = -f.reverse
rw₁ : reflect (-f).natDegree (-f) = -reflect f.natDegree f
⊢ (-f).reverse = -f.reverse
have rw₂ : -reflect (-f).natDegree f = -reflect f.natDegree f
Tactic: rw [reverse, reverse, reflect_neg, natDegree_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Ring R
f : R[X]
rw : reflect (-f).natDegree (-f) = -f.reverse
rw₁ : reflect (-f).natDegree (-f) = -reflect f.natDegree f
rw₂ : -reflect (-f).natDegree f = -reflect f.natDegree f
⊢ (-f).reverse = -f.reverse
have rw₃ : -reflect f.natDegree f = -reflect f.natDegree f
Tactic: rw [reverse, reverse, reflect_neg, natDegree_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
iR : DecidableEq R
p : R[X]
ip0 : Decidable (p = 0)
⊢ p.roots =
    if h : p = 0 then ∅
    else
      Classical.choose (p := fun (x : Multiset R) ↦
        (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯
have obtain : p.roots =
  if h : p = 0 then ∅
  else
    Classical.choose (p := fun (x : Multiset R) ↦
      (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) sorry
Tactic: obtain rfl := Subsingleton.elim iR (Classical.decEq R)
Cleared hypotheses: iR
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ip0 : Decidable (p = 0)
⊢ p.roots =
    if h : p = 0 then ∅
    else
      Classical.choose (p := fun (x : Multiset R) ↦
        (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯
have obtain : p.roots =
  if h : p = 0 then ∅
  else
    Classical.choose (p := fun (x : Multiset R) ↦
      (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) sorry
Tactic: obtain rfl := Subsingleton.elim ip0 (Classical.dec (p = 0))
Cleared hypotheses: ip0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ (↑(Multiset.card.{u} (α := R)
          (if h : p = 0 then ∅
          else
            Classical.choose (p := fun (x : Multiset R) ↦
              (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯)) :
      WithBot ℕ) ≤
    p.degree
have rw : (↑(Classical.choose (p := fun (x : Multiset R) ↦
          (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) sorry).card :
    WithBot ℕ) ≤
  p.degree
Tactic: rw [dif_neg hp0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ (↑p.roots.card : WithBot ℕ) ≤ p.degree
have unfold : (↑(Multiset.card.{u} (α := R)
        (if h : p = 0 then ∅
        else
          Classical.choose (p := fun (x : Multiset R) ↦
            (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) sorry)) :
    WithBot ℕ) ≤
  p.degree
Tactic: classical
  unfold roots
  rw [dif_neg hp0]
  exact (Classical.choose_spec (exists_multiset_roots hp0)).1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp0 : p ≠ 0
unfold :
  (↑(Multiset.card.{u} (α := R)
          (if h : p = 0 then ∅
          else
            Classical.choose (p := fun (x : Multiset R) ↦
              (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯)) :
      WithBot ℕ) ≤
    p.degree
⊢ (↑p.roots.card : WithBot ℕ) ≤ p.degree
have unfold₁ : (↑(Classical.choose (p := fun (x : Multiset R) ↦
          (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) sorry).card :
    WithBot ℕ) ≤
  p.degree
Tactic: classical
  unfold roots
  rw [dif_neg hp0]
  exact (Classical.choose_spec (exists_multiset_roots hp0)).1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
⊢ p.roots.card ≤ p.natDegree
have pos : ∀ (hp0 : p = 0), p.roots.card ≤ p.natDegree
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
pos : ∀ (hp0 : p = 0), p.roots.card ≤ p.natDegree
⊢ p.roots.card ≤ p.natDegree
have neg : ∀ (hp0 : ¬p = 0), p.roots.card ≤ p.natDegree
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
a : R
hp0 : 0 < p.degree
⊢ (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree
have rw : (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) (-a) : R[X])).degree = p.degree
Tactic: rw [sub_eq_add_neg, ← C_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
⊢ count a p.roots = rootMultiplicity a p
have pos : ∀ (hp : p = 0), count a p.roots = rootMultiplicity a p
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
pos : ∀ (hp : p = 0), count a p.roots = rootMultiplicity a p
⊢ count a p.roots = rootMultiplicity a p
have neg : ∀ (hp : ¬p = 0), count a p.roots = rootMultiplicity a p
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : ¬p = 0
⊢ count a p.roots = rootMultiplicity a p
have neg : count a
    (Classical.choose (p := fun (x : Multiset R) ↦
      (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) sorry) =
  rootMultiplicity a p
Tactic: rw [roots_def, dif_neg hp]