awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
h : r ≠ 0
hnN : n ≤ N
refine_2 :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      (x ^ (N - n) * x ^ n) =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₁ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
        x ^ (N - n) *
      x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₂ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n) * x ^ (N - n)) *
      x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₃ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        ((@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ * x) ^ (N - n)) *
      x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₄ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S) (HPow.hPow (α := S) 1 (N - n)) * x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₅ :
  HMul.hMul (α := S) (β := S) ((i : (a : R) → S) r : S) (1 : S) * x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₆ refine_2₇ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n) = HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
⊢ HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      x ^ (N - n + n) =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)

Tactic:
rw [pow_add, ← mul_assoc, mul_assoc (i r), ← mul_pow, invOf_mul_self, one_pow, mul_one]

Premises used: one_pow, mul_assoc, pow_add, invOf_mul_self, mul_one, mul_pow, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
f_1 g : R[X]
h : f_1.natDegree < g.natDegree
h_1 : g.natDegree ≤ N
h_2 : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f_1) * x ^ N = eval₂ i x f_1
h_3 : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N g) * x ^ N = eval₂ i x g
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N (f_1 + g)) * x ^ N =
    eval₂ i x (f_1 + g)

Tactic:
simp [*, add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
rw : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0
| eval₂ i x f = 0

Tactic:
rw [← eval₂_reflect_mul_pow i x N f hf]

Premises used: Polynomial.eval₂_reflect_mul_pow
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
conv_rhs :
  eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0 ↔
    eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0 ↔ eval₂ i x f = 0

Tactic:
conv_rhs => rw [← eval₂_reflect_mul_pow i x N f hf]

Premises used: Polynomial.eval₂_reflect_mul_pow
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
mp :
  eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0 →
    eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0
mpr :
  eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0 →
    eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0 ↔
    eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0
mp : 0 * x ^ N = 0
mp₁ mp₂ : Eq.{u_2 + 1} (α := S) 0 0
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0

Tactic:
rw [h, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0
mpr : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * 1 = 0
mpr₁ : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * HPow.hPow (α := S) 1 N = 0
mpr₂ :
  eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) *
      (x * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) ^ N =
    0
mpr₃ :
  eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) *
      (x ^ N * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ N) =
    0
mpr₄ :
  eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ N =
    0
mpr₅ : 0 * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ N = 0
mpr₆ mpr₇ : Eq.{u_2 + 1} (α := S) 0 0
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0

Tactic:
rw [← mul_one (eval₂ i (⅟x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h,
      zero_mul]

Premises used: one_pow, MulZeroClass.zero_mul, mul_assoc, Invertible.invOf, Polynomial.eval₂, mul_invOf_self, mul_one, mul_pow
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
n : ℕ
rw : (reflect f.natDegree f).coeff n = f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) n)
rw₁ rw₂ : f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) n) = f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) n)
⊢ f.reverse.coeff n = f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) n)

Tactic:
rw [reverse, coeff_reflect]

Premises used: Polynomial.coeff_reflect, Polynomial.reverse
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
rw : f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 0) = f.leadingCoeff
rw₁ : f.coeff (f.natDegree - 0) = f.leadingCoeff
rw₂ : f.coeff f.natDegree = f.leadingCoeff
rw₃ rw₄ : f.coeff f.natDegree = f.coeff f.natDegree
⊢ f.reverse.coeff 0 = f.leadingCoeff

Tactic:
rw [coeff_reverse, revAt_le zero_le, tsub_zero, leadingCoeff]

Premises used: zero_le, Polynomial.leadingCoeff, Polynomial.revAt_le, tsub_zero, Polynomial.coeff_reverse
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R[X]) (reverse 0) 0

Tactic:
rfl

Premises used: Multiset.map, List.map, Finset.map, Multiset.zero, Finset.empty, dite, Multiset.ofList, Polynomial.reflect, Finsupp.embDomain, Polynomial.reverse, rfl
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.reverse = 0 ↔ f = 0

Tactic:
simp [reverse]

Premises used: Polynomial.reverse
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
rw : ∀ (m : ℕ), LT.lt (α := WithBot ℕ) (↑f.natDegree : WithBot ℕ) (↑m : WithBot ℕ) → f.reverse.coeff m = 0
⊢ f.reverse.natDegree ≤ f.natDegree

Tactic:
rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero]

Premises used: Polynomial.degree_le_iff_coeff_zero, Polynomial.natDegree_le_iff_degree_le
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
n : ℕ
hn : LT.lt (α := WithBot ℕ) (↑f.natDegree : WithBot ℕ) (↑n : WithBot ℕ)
⊢ f.natDegree < n

Tactic:
rw [Nat.cast_lt] at hn

Premises used: Nat.cast_lt
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
n : ℕ
hn : f.natDegree < n
rw : f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) n) = 0
rw₁ :
  f.coeff
      (({ toFun := fun (i : ℕ) ↦ if i ≤ f.natDegree then f.natDegree - i else i, inj' := ⋯ : ℕ ↪ ℕ } : (a : ℕ) → ℕ) n) =
    0
rw₂ : f.coeff (if n ≤ f.natDegree then f.natDegree - n else n) = 0
rw₃ : f.coeff n = 0
rw₄ rw₅ : Eq.{u_1 + 1} (α := R) 0 0
⊢ f.reverse.coeff n = 0

Tactic:
rw [coeff_reverse, revAt, Function.Embedding.coeFn_mk, if_neg (not_le_of_gt hn),
    coeff_eq_zero_of_natDegree_lt hn]

Premises used: Polynomial.revAt, Function.Embedding.coeFn_mk, Polynomial.coeff_eq_zero_of_natDegree_lt, not_le_of_gt, Polynomial.coeff_reverse, if_neg
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
pos : ∀ (hf : f = 0), f.natDegree = f.reverse.natDegree + f.natTrailingDegree
neg : ∀ (hf : ¬f = 0), f.natDegree = f.reverse.natDegree + f.natTrailingDegree
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree

Tactic:
by_cases hf : f = 0
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f = 0
pos : natDegree.{u_1} (R := R) 0 = natDegree.{u_1} (R := R) (reverse 0) + natTrailingDegree.{u_1} (R := R) 0
pos₁ : natDegree.{u_1} (R := R) 0 = natDegree.{u_1} (R := R) 0 + natTrailingDegree.{u_1} (R := R) 0
pos₂ : 0 = 0 + natTrailingDegree.{u_1} (R := R) 0
pos₃ pos₄ : 0 = HAdd.hAdd (α := ℕ) 0 0
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree

Tactic:
rw [hf, reverse_zero, natDegree_zero, natTrailingDegree_zero]

Premises used: Polynomial.natDegree_zero, Polynomial.reverse_zero, Polynomial.natTrailingDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
neg : f.natDegree ≤ f.reverse.natDegree + f.natTrailingDegree
neg₁ : f.reverse.natDegree + f.natTrailingDegree ≤ f.natDegree
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natDegree ≤ f.reverse.natDegree + f.natTrailingDegree

Tactic:
tsub_le_iff_right.mp ?_

Premises used: tsub_le_iff_right, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
neg : f.natDegree - f.natTrailingDegree ≤ f.reverse.natDegree
⊢ f.natDegree ≤ f.reverse.natDegree + f.natTrailingDegree

Tactic:
refine tsub_le_iff_right.mp ?_

Premises used: tsub_le_iff_right, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
neg : f.reverse.coeff (f.natDegree - f.natTrailingDegree) ≠ 0
⊢ f.natDegree - f.natTrailingDegree ≤ f.reverse.natDegree

Tactic:
apply le_natDegree_of_ne_zero

Premises used: Polynomial.le_natDegree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
neg : f.coeff f.natTrailingDegree ≠ 0
⊢ f.reverse.coeff (f.natDegree - f.natTrailingDegree) ≠ 0

Tactic:
rw [reverse, coeff_reflect, ← revAt_le f.natTrailingDegree_le_natDegree, revAt_invol]

Premises used: Polynomial.coeff_reflect, Polynomial.revAt_le, Polynomial.natTrailingDegree_le_natDegree, Polynomial.revAt_invol, Polynomial.reverse
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.coeff f.natTrailingDegree ≠ 0

Tactic:
trailingCoeff_nonzero_iff_nonzero.mpr hf

Premises used: Iff.mpr, Polynomial.trailingCoeff_nonzero_iff_nonzero, Polynomial.trailingCoeff
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.coeff f.natTrailingDegree ≠ 0

Tactic:
exact trailingCoeff_nonzero_iff_nonzero.mpr hf

Premises used: Iff.mpr, Polynomial.trailingCoeff_nonzero_iff_nonzero
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
neg : f.natTrailingDegree ≤ f.natDegree - f.reverse.natDegree
⊢ f.reverse.natDegree + f.natTrailingDegree ≤ f.natDegree

Tactic:
rw [← le_tsub_iff_left f.reverse_natDegree_le]

Premises used: le_tsub_iff_left, Polynomial.reverse_natDegree_le
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
neg : f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0
⊢ f.natTrailingDegree ≤ f.natDegree - f.reverse.natDegree

Tactic:
apply natTrailingDegree_le_of_ne_zero

Premises used: Polynomial.natTrailingDegree_le_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
⊢ ¬f.reverse.leadingCoeff = 0

Tactic:
have key := mt leadingCoeff_eq_zero.mp (mt reverse_eq_zero.mp hf)
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
key : ¬f.reverse.leadingCoeff = 0
neg : ∀ (key : ¬f.reverse.coeff f.reverse.natDegree = 0), f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0
neg₁ :
  ∀ (key : ¬f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) f.reverse.natDegree) = 0),
    f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0
neg₂ neg₃ neg₄ neg₅ :
  ∀ (key : ¬f.coeff (f.natDegree - f.reverse.natDegree) = 0), f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0
⊢ f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0

Tactic:
rwa [leadingCoeff, coeff_reverse, revAt_le f.reverse_natDegree_le] at key

Premises used: Polynomial.leadingCoeff, Polynomial.revAt_le, Polynomial.reverse_natDegree_le, Polynomial.coeff_reverse
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
rw : f.reverse.natDegree = f.reverse.natDegree + f.natTrailingDegree - f.natTrailingDegree
rw₁ rw₂ : f.reverse.natDegree = f.reverse.natDegree
⊢ f.reverse.natDegree = f.natDegree - f.natTrailingDegree

Tactic:
rw [f.natDegree_eq_reverse_natDegree_add_natTrailingDegree, add_tsub_cancel_right]

Premises used: add_tsub_cancel_right, Polynomial.natDegree_eq_reverse_natDegree_add_natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
rw : f.reverse.coeff f.reverse.natDegree = f.trailingCoeff
rw₁ : f.reverse.coeff (f.natDegree - f.natTrailingDegree) = f.trailingCoeff
rw₂ : f.reverse.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) f.natTrailingDegree) = f.trailingCoeff
rw₃ :
  f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) ((revAt f.natDegree : (a : ℕ) → ℕ) f.natTrailingDegree : ℕ)) =
    f.trailingCoeff
rw₄ : f.coeff f.natTrailingDegree = f.trailingCoeff
rw₅ rw₆ : f.coeff f.natTrailingDegree = f.coeff f.natTrailingDegree
⊢ f.reverse.leadingCoeff = f.trailingCoeff

Tactic:
rw [leadingCoeff, reverse_natDegree, ← revAt_le f.natTrailingDegree_le_natDegree,
    coeff_reverse, revAt_invol, trailingCoeff]

Premises used: Polynomial.leadingCoeff, Polynomial.revAt_le, Polynomial.trailingCoeff, Polynomial.natTrailingDegree_le_natDegree, Polynomial.reverse_natDegree, Polynomial.revAt_invol, Polynomial.coeff_reverse
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
rw : f = 0 ∨ f ≠ 0
⊢ f.reverse.natTrailingDegree = 0

Tactic:
rw [natTrailingDegree_eq_zero, reverse_eq_zero, coeff_zero_reverse, leadingCoeff_ne_zero]

Premises used: Polynomial.reverse_eq_zero, Polynomial.natTrailingDegree_eq_zero, Polynomial.leadingCoeff_ne_zero, Polynomial.coeff_zero_reverse
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f = 0 ∨ f ≠ 0

Tactic:
eq_or_ne _ _

Premises used: eq_or_ne
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f = 0 ∨ f ≠ 0

Tactic:
exact eq_or_ne _ _

Premises used: eq_or_ne
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
rw : f.reverse.coeff f.reverse.natTrailingDegree = f.leadingCoeff
rw₁ : f.reverse.coeff 0 = f.leadingCoeff
rw₂ rw₃ : f.leadingCoeff = f.leadingCoeff
⊢ f.reverse.trailingCoeff = f.leadingCoeff

Tactic:
rw [trailingCoeff, natTrailingDegree_reverse, coeff_zero_reverse]

Premises used: Polynomial.trailingCoeff, Polynomial.natTrailingDegree_reverse, Polynomial.coeff_zero_reverse
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f g : R[X]
fg : f.leadingCoeff * g.leadingCoeff ≠ 0
rw : reflect (f.natDegree + g.natDegree) (f * g) = reflect f.natDegree f * reflect g.natDegree g
rw₁ rw₂ : reflect f.natDegree f * reflect g.natDegree g = reflect f.natDegree f * reflect g.natDegree g
⊢ reflect (f * g).natDegree (f * g) = reflect f.natDegree f * reflect g.natDegree g

Tactic:
rw [natDegree_mul' fg, reflect_mul f g rfl.le rfl.le]

Premises used: Polynomial.natDegree_mul', Eq.le, Polynomial.reflect_mul, rfl
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R[X]
pos : ∀ (f0 : f = 0), (f * g).reverse = f.reverse * g.reverse
neg : ∀ (f0 : ¬f = 0), (f * g).reverse = f.reverse * g.reverse
⊢ (f * g).reverse = f.reverse * g.reverse

Tactic:
by_cases f0 : f = 0
-- Module: Mathlib.Algebra.Polynomial.Reverse
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

Tactic:
simp only [f0, zero_mul, reverse_zero]

Premises used: MulZeroClass.zero_mul, Polynomial.reverse_zero
-- Module: Mathlib.Algebra.Polynomial.Reverse
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
neg : ∀ (g0 : ¬g = 0), (f * g).reverse = f.reverse * g.reverse
⊢ (f * g).reverse = f.reverse * g.reverse

Tactic:
by_cases g0 : g = 0
-- Module: Mathlib.Algebra.Polynomial.Reverse
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
pos₃ pos₄ : Eq.{u_2 + 1} (α := R[X]) 0 0
⊢ (f * g).reverse = f.reverse * g.reverse

Tactic:
rw [g0, mul_zero, reverse_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, Polynomial.reverse_zero
-- Module: Mathlib.Algebra.Polynomial.Reverse
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

Tactic:
simp [reverse_mul, *]

Premises used: Polynomial.reverse_mul
-- Module: Mathlib.Algebra.Polynomial.Reverse
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
rw₄ rw₅ : p.trailingCoeff * q.trailingCoeff = p.trailingCoeff * q.trailingCoeff
⊢ (p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff

Tactic:
rw [← reverse_leadingCoeff, reverse_mul_of_domain, leadingCoeff_mul, reverse_leadingCoeff,
    reverse_leadingCoeff]

Premises used: Polynomial.leadingCoeff_mul, Polynomial.reverse_mul_of_domain, Polynomial.reverse_leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
rw : f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 1) = if f.natDegree = 0 then 0 else f.coeff (f.natDegree - 1)
⊢ f.reverse.coeff 1 = f.nextCoeff

Tactic:
rw [coeff_reverse, nextCoeff]

Premises used: Polynomial.nextCoeff, Polynomial.coeff_reverse
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
pos : ∀ (hf : f.natDegree = 0), f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 1) = 0
neg : ∀ (hf : ¬f.natDegree = 0), f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 1) = f.coeff (f.natDegree - 1)
⊢ f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 1) = if f.natDegree = 0 then 0 else f.coeff (f.natDegree - 1)

Tactic:
split_ifs with hf
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.natDegree = 0
⊢ f.natDegree < 1

Tactic:
simp only [hf, zero_lt_one]

Premises used: zero_lt_one
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.natDegree = 0
⊢ f.coeff 1 = 0

Tactic:
have : coeff f 1 = 0 := coeff_eq_zero_of_natDegree_lt (by simp only [hf, zero_lt_one])
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.natDegree = 0
this : f.coeff 1 = 0
⊢ f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 1) = 0

Tactic:
simp [*, revAt]

Premises used: Polynomial.revAt
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f.natDegree = 0
neg : 1 ≤ f.natDegree
⊢ f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 1) = f.coeff (f.natDegree - 1)

Tactic:
rw [revAt_le]

Premises used: Polynomial.revAt_le
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f.natDegree = 0
⊢ 1 ≤ f.natDegree

Tactic:
Nat.succ_le_iff.2 (pos_iff_ne_zero.2 hf)

Premises used: Iff.mpr, Nat.succ_le_iff, pos_iff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f.natDegree = 0
⊢ 1 ≤ f.natDegree

Tactic:
exact Nat.succ_le_iff.2 (pos_iff_ne_zero.2 hf)

Premises used: Iff.mpr, Nat.succ_le_iff, pos_iff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
t : R
⊢ Eq.{u_1 + 1} (α := R[X]) (reverse ((C : (a : R) → R[X]) t)) ((C : (a : R) → R[X]) t)

Tactic:
simp [reverse]

Premises used: Polynomial.reverse
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
h : Nontrivial R
inl : (HMul.hMul (α := R[X]) 0 X).reverse = reverse 0
inr : ∀ (hp : p ≠ 0), (p * X).reverse = p.reverse
⊢ (p * X).reverse = p.reverse

Tactic:
rcases eq_or_ne p 0 with rfl | hp

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
h : Nontrivial R
⊢ (HMul.hMul (α := R[X]) 0 X).reverse = reverse 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
h : Nontrivial R
hp : p ≠ 0
⊢ (p * X).reverse = p.reverse

Tactic:
simp [reverse, hp]

Premises used: Polynomial.reverse
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
rw : (p * X).reverse = p.reverse
rw₁ rw₂ : p.reverse = p.reverse
⊢ (X * p).reverse = p.reverse

Tactic:
rw [commute_X p, reverse_mul_X]

Premises used: Polynomial.reverse_mul_X, Polynomial.commute_X
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ (p * HPow.hPow (α := R[X]) (β := ℕ) X 0).reverse = p.reverse

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Reverse
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
succ₃ succ₄ : p.reverse = p.reverse
⊢ (p * HPow.hPow (α := R[X]) X (n + 1)).reverse = p.reverse

Tactic:
rw [pow_succ, ← mul_assoc, reverse_mul_X, ih]

Premises used: pow_succ, mul_assoc, Polynomial.reverse_mul_X