awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0
have mpr₃ : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) *
    (x ^ N * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ N) =
  0
Tactic: rw [← mul_one (eval₂ i (⅟x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h,
      zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0
have mpr₄ : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ N =
  0
Tactic: rw [← mul_one (eval₂ i (⅟x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h,
      zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0
have mpr₅ : 0 * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ N = 0
Tactic: rw [← mul_one (eval₂ i (⅟x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h,
      zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0
have mpr₆ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [← mul_one (eval₂ i (⅟x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h,
      zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
n : ℕ
⊢ f.reverse.coeff n = f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) n)
have rw : (reflect f.natDegree f).coeff n = f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) n)
Tactic: rw [reverse, coeff_reflect]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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)
⊢ f.reverse.coeff n = f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) n)
have rw₁ : f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) n) = f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) n)
Tactic: rw [reverse, coeff_reflect]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.reverse.coeff 0 = f.leadingCoeff
have rw : f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 0) = f.leadingCoeff
Tactic: rw [coeff_reverse, revAt_le zero_le, tsub_zero, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
rw : f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 0) = f.leadingCoeff
⊢ f.reverse.coeff 0 = f.leadingCoeff
have rw₁ : f.coeff (f.natDegree - 0) = f.leadingCoeff
Tactic: rw [coeff_reverse, revAt_le zero_le, tsub_zero, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ f.reverse.coeff 0 = f.leadingCoeff
have rw₂ : f.coeff f.natDegree = f.leadingCoeff
Tactic: rw [coeff_reverse, revAt_le zero_le, tsub_zero, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ f.reverse.coeff 0 = f.leadingCoeff
have rw₃ : f.coeff f.natDegree = f.coeff f.natDegree
Tactic: rw [coeff_reverse, revAt_le zero_le, tsub_zero, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.reverse.natDegree ≤ f.natDegree
have rw : ∀ (m : ℕ), LT.lt (α := WithBot ℕ) (↑f.natDegree : WithBot ℕ) (↑m : WithBot ℕ) → f.reverse.coeff m = 0
Tactic: rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
n : ℕ
hn : LT.lt (α := WithBot ℕ) (↑f.natDegree : WithBot ℕ) (↑n : WithBot ℕ)
⊢ f.reverse.coeff n = 0
have hn₁ : f.natDegree < n
Tactic: rw [Nat.cast_lt] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
n : ℕ
hn : f.natDegree < n
⊢ f.reverse.coeff n = 0
have rw : f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ f.reverse.coeff n = 0
have rw₁ : f.coeff
    (({ toFun := fun (i : ℕ) ↦ if i ≤ f.natDegree then f.natDegree - i else i, inj' := sorry : ℕ ↪ ℕ } : (a : ℕ) → ℕ) 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ f.reverse.coeff n = 0
have rw₂ : f.coeff (if n ≤ f.natDegree then f.natDegree - n else 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ f.reverse.coeff n = 0
have rw₃ : f.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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ f.reverse.coeff n = 0
have rw₄ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [coeff_reverse, revAt, Function.Embedding.coeFn_mk, if_neg (not_le_of_gt hn),
    coeff_eq_zero_of_natDegree_lt hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree
have pos : ∀ (hf : f = 0), f.natDegree = f.reverse.natDegree + f.natTrailingDegree
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
pos : ∀ (hf : f = 0), f.natDegree = f.reverse.natDegree + f.natTrailingDegree
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree
have neg : ∀ (hf : ¬f = 0), f.natDegree = f.reverse.natDegree + f.natTrailingDegree
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f = 0
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree
have pos : natDegree.{u_1} (R := R) 0 = natDegree.{u_1} (R := R) (reverse 0) + natTrailingDegree.{u_1} (R := R) 0
Tactic: rw [hf, reverse_zero, natDegree_zero, natTrailingDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree
have pos₁ : natDegree.{u_1} (R := R) 0 = natDegree.{u_1} (R := R) 0 + natTrailingDegree.{u_1} (R := R) 0
Tactic: rw [hf, reverse_zero, natDegree_zero, natTrailingDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree
have pos₂ : 0 = 0 + natTrailingDegree.{u_1} (R := R) 0
Tactic: rw [hf, reverse_zero, natDegree_zero, natTrailingDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree
have pos₃ : 0 = HAdd.hAdd (α := ℕ) 0 0
Tactic: rw [hf, reverse_zero, natDegree_zero, natTrailingDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree
have neg : f.natDegree ≤ f.reverse.natDegree + f.natTrailingDegree
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
neg : f.natDegree ≤ f.reverse.natDegree + f.natTrailingDegree
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree
have neg₁ : f.reverse.natDegree + f.natTrailingDegree ≤ f.natDegree
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natDegree ≤ f.reverse.natDegree + f.natTrailingDegree
have neg : f.natDegree - f.natTrailingDegree ≤ f.reverse.natDegree
Tactic: refine tsub_le_iff_right.mp ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natDegree - f.natTrailingDegree ≤ f.reverse.natDegree
have neg : f.reverse.coeff (f.natDegree - f.natTrailingDegree) ≠ 0
Tactic: apply le_natDegree_of_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.reverse.coeff (f.natDegree - f.natTrailingDegree) ≠ 0
have neg : f.coeff f.natTrailingDegree ≠ 0
Tactic: rw [reverse, coeff_reflect, ← revAt_le f.natTrailingDegree_le_natDegree, revAt_invol]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.reverse.natDegree + f.natTrailingDegree ≤ f.natDegree
have neg : f.natTrailingDegree ≤ f.natDegree - f.reverse.natDegree
Tactic: rw [← le_tsub_iff_left f.reverse_natDegree_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natTrailingDegree ≤ f.natDegree - f.reverse.natDegree
have neg : f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0
Tactic: apply natTrailingDegree_le_of_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0
have key : ¬f.reverse.leadingCoeff = 0
Tactic: have key := mt leadingCoeff_eq_zero.mp (mt reverse_eq_zero.mp hf)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
key : ¬f.reverse.leadingCoeff = 0
⊢ f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0
have neg : ∀ (key : ¬f.reverse.coeff 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
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0
have neg₁ : ∀ (key : ¬f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) 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
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0
have neg₂ : ∀ (key : ¬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
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.reverse.natDegree = f.natDegree - f.natTrailingDegree
have rw : f.reverse.natDegree = f.reverse.natDegree + f.natTrailingDegree - f.natTrailingDegree
Tactic: rw [f.natDegree_eq_reverse_natDegree_add_natTrailingDegree, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
rw : f.reverse.natDegree = f.reverse.natDegree + f.natTrailingDegree - f.natTrailingDegree
⊢ f.reverse.natDegree = f.natDegree - f.natTrailingDegree
have rw₁ : f.reverse.natDegree = f.reverse.natDegree
Tactic: rw [f.natDegree_eq_reverse_natDegree_add_natTrailingDegree, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.reverse.leadingCoeff = f.trailingCoeff
have rw : f.reverse.coeff f.reverse.natDegree = f.trailingCoeff
Tactic: rw [leadingCoeff, reverse_natDegree, ← revAt_le f.natTrailingDegree_le_natDegree,
    coeff_reverse, revAt_invol, trailingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
rw : f.reverse.coeff f.reverse.natDegree = f.trailingCoeff
⊢ f.reverse.leadingCoeff = f.trailingCoeff
have rw₁ : f.reverse.coeff (f.natDegree - f.natTrailingDegree) = f.trailingCoeff
Tactic: rw [leadingCoeff, reverse_natDegree, ← revAt_le f.natTrailingDegree_le_natDegree,
    coeff_reverse, revAt_invol, trailingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ f.reverse.leadingCoeff = f.trailingCoeff
have rw₂ : f.reverse.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) f.natTrailingDegree) = f.trailingCoeff
Tactic: rw [leadingCoeff, reverse_natDegree, ← revAt_le f.natTrailingDegree_le_natDegree,
    coeff_reverse, revAt_invol, trailingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ f.reverse.leadingCoeff = f.trailingCoeff
have rw₃ : f.coeff ((revAt f.natDegree : (a : ℕ) → ℕ) ((revAt f.natDegree : (a : ℕ) → ℕ) f.natTrailingDegree : ℕ)) =
  f.trailingCoeff
Tactic: rw [leadingCoeff, reverse_natDegree, ← revAt_le f.natTrailingDegree_le_natDegree,
    coeff_reverse, revAt_invol, trailingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ f.reverse.leadingCoeff = f.trailingCoeff
have rw₄ : f.coeff f.natTrailingDegree = f.trailingCoeff
Tactic: rw [leadingCoeff, reverse_natDegree, ← revAt_le f.natTrailingDegree_le_natDegree,
    coeff_reverse, revAt_invol, trailingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ f.reverse.leadingCoeff = f.trailingCoeff
have rw₅ : f.coeff f.natTrailingDegree = f.coeff f.natTrailingDegree
Tactic: rw [leadingCoeff, reverse_natDegree, ← revAt_le f.natTrailingDegree_le_natDegree,
    coeff_reverse, revAt_invol, trailingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.reverse.natTrailingDegree = 0
have rw : f = 0 ∨ f ≠ 0
Tactic: rw [natTrailingDegree_eq_zero, reverse_eq_zero, coeff_zero_reverse, leadingCoeff_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.reverse.trailingCoeff = f.leadingCoeff
have rw : f.reverse.coeff f.reverse.natTrailingDegree = f.leadingCoeff
Tactic: rw [trailingCoeff, natTrailingDegree_reverse, coeff_zero_reverse]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
rw : f.reverse.coeff f.reverse.natTrailingDegree = f.leadingCoeff
⊢ f.reverse.trailingCoeff = f.leadingCoeff
have rw₁ : f.reverse.coeff 0 = f.leadingCoeff
Tactic: rw [trailingCoeff, natTrailingDegree_reverse, coeff_zero_reverse]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ f.reverse.trailingCoeff = f.leadingCoeff
have rw₂ : f.leadingCoeff = f.leadingCoeff
Tactic: rw [trailingCoeff, natTrailingDegree_reverse, coeff_zero_reverse]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f g : R[X]
fg : f.leadingCoeff * g.leadingCoeff ≠ 0
⊢ reflect (f * g).natDegree (f * g) = reflect f.natDegree f * reflect g.natDegree g
have rw : reflect (f.natDegree + 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ reflect (f * g).natDegree (f * g) = reflect f.natDegree f * reflect g.natDegree g
have rw₁ : reflect f.natDegree f * reflect g.natDegree g = reflect f.natDegree f * reflect g.natDegree g
Tactic: rw [natDegree_mul' fg, reflect_mul f g rfl.le rfl.le]
-- 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]
⊢ (f * g).reverse = f.reverse * g.reverse
have pos : ∀ (f0 : f = 0), (f * g).reverse = f.reverse * g.reverse
Tactic: by_cases f0 : f = 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]
pos : ∀ (f0 : f = 0), (f * g).reverse = f.reverse * g.reverse
⊢ (f * g).reverse = f.reverse * g.reverse
have neg : ∀ (f0 : ¬f = 0), (f * g).reverse = f.reverse * g.reverse
Tactic: by_cases f0 : f = 0