awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
ha : ¬a = 0
neg :
  reverse ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₁ :
  reflect (natDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₂ :
  reflect (if a = 0 then 0 else n) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₃ :
  reflect n ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
have neg₄ : reflect n ((monomial n : (a : R) → R[X]) a) * HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) a
Tactic: rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
ha : ¬a = 0
neg :
  reverse ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₁ :
  reflect (natDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₂ :
  reflect (if a = 0 then 0 else n) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₃ :
  reflect n ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₄ : reflect n ((monomial n : (a : R) → R[X]) a) * HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) a
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
have neg₅ : reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) *
    HPow.hPow (α := R[X]) X n =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
Tactic: rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
ha : ¬a = 0
neg :
  reverse ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₁ :
  reflect (natDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₂ :
  reflect (if a = 0 then 0 else n) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₃ :
  reflect n ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₄ : reflect n ((monomial n : (a : R) → R[X]) a) * HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) a
neg₅ :
  reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) *
      HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
have neg₆ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt n : (a : ℕ) → ℕ) n : ℕ)) *
    HPow.hPow (α := R[X]) X n =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
Tactic: rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
ha : ¬a = 0
neg :
  reverse ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₁ :
  reflect (natDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₂ :
  reflect (if a = 0 then 0 else n) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₃ :
  reflect n ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₄ : reflect n ((monomial n : (a : R) → R[X]) a) * HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) a
neg₅ :
  reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) *
      HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
neg₆ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt n : (a : ℕ) → ℕ) n : ℕ)) *
      HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
have neg₇ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n - n)) * HPow.hPow (α := R[X]) X n =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
Tactic: rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
ha : ¬a = 0
neg :
  reverse ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₁ :
  reflect (natDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₂ :
  reflect (if a = 0 then 0 else n) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₃ :
  reflect n ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₄ : reflect n ((monomial n : (a : R) → R[X]) a) * HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) a
neg₅ :
  reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) *
      HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
neg₆ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt n : (a : ℕ) → ℕ) n : ℕ)) *
      HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
neg₇ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n - n)) * HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
have neg₈ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 0) * HPow.hPow (α := R[X]) X n =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
Tactic: rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
ha : ¬a = 0
neg :
  reverse ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₁ :
  reflect (natDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₂ :
  reflect (if a = 0 then 0 else n) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₃ :
  reflect n ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₄ : reflect n ((monomial n : (a : R) → R[X]) a) * HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) a
neg₅ :
  reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) *
      HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
neg₆ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt n : (a : ℕ) → ℕ) n : ℕ)) *
      HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
neg₇ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n - n)) * HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
neg₈ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 0) *
      HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
have neg₉ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (1 : R[X]) * HPow.hPow (α := R[X]) X n =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
Tactic: rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
ha : ¬a = 0
neg :
  reverse ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₁ :
  reflect (natDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₂ :
  reflect (if a = 0 then 0 else n) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₃ :
  reflect n ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₄ : reflect n ((monomial n : (a : R) → R[X]) a) * HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) a
neg₅ :
  reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) *
      HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
neg₆ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt n : (a : ℕ) → ℕ) n : ℕ)) *
      HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
neg₇ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n - n)) * HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
neg₈ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 0) *
      HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
neg₉ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (1 : R[X]) * HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
have neg₁₀ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
Tactic: rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
have pos : ∀ (ha : a = 0), Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
Tactic: classical
    by_cases ha : a = 0
    · rw [ha, monomial_zero_right, mirror_zero]
    · rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
pos :
  ∀ (ha : a = 0), Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
have neg : ∀ (ha : ¬a = 0), Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
Tactic: classical
    by_cases ha : a = 0
    · rw [ha, monomial_zero_right, mirror_zero]
    · rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ p.mirror.natDegree = p.natDegree
have pos : ∀ (hp : p = 0), p.mirror.natDegree = p.natDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
pos : ∀ (hp : p = 0), p.mirror.natDegree = p.natDegree
⊢ p.mirror.natDegree = p.natDegree
have neg : ∀ (hp : ¬p = 0), p.mirror.natDegree = p.natDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : p = 0
⊢ p.mirror.natDegree = p.natDegree
have pos : natDegree.{u_1} (R := R) (mirror 0) = natDegree.{u_1} (R := R) 0
Tactic: rw [hp, mirror_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : p = 0
pos : natDegree.{u_1} (R := R) (mirror 0) = natDegree.{u_1} (R := R) 0
⊢ p.mirror.natDegree = p.natDegree
have pos₁ : natDegree.{u_1} (R := R) 0 = natDegree.{u_1} (R := R) 0
Tactic: rw [hp, mirror_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.mirror.natDegree = p.natDegree
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : ¬p = 0
h : Nontrivial R
⊢ p.mirror.natDegree = p.natDegree
have rw : p.reverse.leadingCoeff * (HPow.hPow (α := R[X]) X p.natTrailingDegree).leadingCoeff ≠ 0
Tactic: rw [mirror, natDegree_mul', reverse_natDegree, natDegree_X_pow,
    tsub_add_cancel_of_le p.natTrailingDegree_le_natDegree]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : ¬p = 0
h : Nontrivial R
⊢ p.reverse.leadingCoeff * (HPow.hPow (α := R[X]) X p.natTrailingDegree).leadingCoeff ≠ 0
have rwa : p.reverse.leadingCoeff * 1 ≠ 0
Tactic: rwa [leadingCoeff_X_pow, mul_one, reverse_leadingCoeff, Ne, trailingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : ¬p = 0
h : Nontrivial R
rwa : p.reverse.leadingCoeff * 1 ≠ 0
⊢ p.reverse.leadingCoeff * (HPow.hPow (α := R[X]) X p.natTrailingDegree).leadingCoeff ≠ 0
have rwa₁ : p.reverse.leadingCoeff ≠ 0
Tactic: rwa [leadingCoeff_X_pow, mul_one, reverse_leadingCoeff, Ne, trailingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : ¬p = 0
h : Nontrivial R
rwa : p.reverse.leadingCoeff * 1 ≠ 0
rwa₁ : p.reverse.leadingCoeff ≠ 0
⊢ p.reverse.leadingCoeff * (HPow.hPow (α := R[X]) X p.natTrailingDegree).leadingCoeff ≠ 0
have rwa₂ : p.trailingCoeff ≠ 0
Tactic: rwa [leadingCoeff_X_pow, mul_one, reverse_leadingCoeff, Ne, trailingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : ¬p = 0
h : Nontrivial R
rwa : p.reverse.leadingCoeff * 1 ≠ 0
rwa₁ : p.reverse.leadingCoeff ≠ 0
rwa₂ : p.trailingCoeff ≠ 0
⊢ p.reverse.leadingCoeff * (HPow.hPow (α := R[X]) X p.natTrailingDegree).leadingCoeff ≠ 0
have rwa₃ : ¬p.trailingCoeff = 0
Tactic: rwa [leadingCoeff_X_pow, mul_one, reverse_leadingCoeff, Ne, trailingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree
have pos : ∀ (hp : p = 0), p.mirror.natTrailingDegree = p.natTrailingDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
pos : ∀ (hp : p = 0), p.mirror.natTrailingDegree = p.natTrailingDegree
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree
have neg : ∀ (hp : ¬p = 0), p.mirror.natTrailingDegree = p.natTrailingDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : p = 0
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree
have pos : natTrailingDegree.{u_1} (R := R) (mirror 0) = natTrailingDegree.{u_1} (R := R) 0
Tactic: rw [hp, mirror_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : p = 0
pos : natTrailingDegree.{u_1} (R := R) (mirror 0) = natTrailingDegree.{u_1} (R := R) 0
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree
have pos₁ : natTrailingDegree.{u_1} (R := R) 0 = natTrailingDegree.{u_1} (R := R) 0
Tactic: rw [hp, mirror_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree
have neg : (p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree).natTrailingDegree = p.natTrailingDegree
Tactic: rw [mirror, natTrailingDegree_mul_X_pow ((mt reverse_eq_zero.mp) hp),
      natTrailingDegree_reverse, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : ¬p = 0
neg : (p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree).natTrailingDegree = p.natTrailingDegree
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree
have neg₁ : p.reverse.natTrailingDegree + p.natTrailingDegree = p.natTrailingDegree
Tactic: rw [mirror, natTrailingDegree_mul_X_pow ((mt reverse_eq_zero.mp) hp),
      natTrailingDegree_reverse, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : ¬p = 0
neg : (p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree).natTrailingDegree = p.natTrailingDegree
neg₁ : p.reverse.natTrailingDegree + p.natTrailingDegree = p.natTrailingDegree
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree
have neg₂ : 0 + p.natTrailingDegree = p.natTrailingDegree
Tactic: rw [mirror, natTrailingDegree_mul_X_pow ((mt reverse_eq_zero.mp) hp),
      natTrailingDegree_reverse, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : ¬p = 0
neg : (p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree).natTrailingDegree = p.natTrailingDegree
neg₁ : p.reverse.natTrailingDegree + p.natTrailingDegree = p.natTrailingDegree
neg₂ : 0 + p.natTrailingDegree = p.natTrailingDegree
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree
have neg₃ : p.natTrailingDegree = p.natTrailingDegree
Tactic: rw [mirror, natTrailingDegree_mul_X_pow ((mt reverse_eq_zero.mp) hp),
      natTrailingDegree_reverse, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
have pos : ∀ (h2 : p.natDegree < n), p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
Tactic: by_cases h2 : p.natDegree < n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
pos : ∀ (h2 : p.natDegree < n), p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
have neg : ∀ (h2 : ¬p.natDegree < n), p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
Tactic: by_cases h2 : p.natDegree < n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
have pos : 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
Tactic: rw [coeff_eq_zero_of_natDegree_lt (by rwa [mirror_natDegree])]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
⊢ 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
have pos : ∀ (h1 : n ≤ p.natDegree + p.natTrailingDegree),
  0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
Tactic: by_cases h1 : n ≤ p.natDegree + p.natTrailingDegree