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
p : R[X]
n : ℕ
rw : p.mirror.coeff ((revAt (p.mirror.natDegree + p.mirror.natTrailingDegree) : (a : ℕ) → ℕ) n) = p.coeff n
rw₁ :
  p.coeff
      ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
        ((revAt (p.mirror.natDegree + p.mirror.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ)) =
    p.coeff n
⊢ p.mirror.mirror.coeff n = p.coeff n
have rw₂ : p.coeff
    ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
      ((revAt (p.natDegree + p.mirror.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ)) =
  p.coeff n
Tactic: rw [coeff_mirror, coeff_mirror, mirror_natDegree, mirror_natTrailingDegree, revAt_invol]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
rw : p.mirror.coeff ((revAt (p.mirror.natDegree + p.mirror.natTrailingDegree) : (a : ℕ) → ℕ) n) = p.coeff n
rw₁ :
  p.coeff
      ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
        ((revAt (p.mirror.natDegree + p.mirror.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ)) =
    p.coeff n
rw₂ :
  p.coeff
      ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
        ((revAt (p.natDegree + p.mirror.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ)) =
    p.coeff n
⊢ p.mirror.mirror.coeff n = p.coeff n
have rw₃ : p.coeff
    ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
      ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ)) =
  p.coeff n
Tactic: rw [coeff_mirror, coeff_mirror, mirror_natDegree, mirror_natTrailingDegree, revAt_invol]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
rw : p.mirror.coeff ((revAt (p.mirror.natDegree + p.mirror.natTrailingDegree) : (a : ℕ) → ℕ) n) = p.coeff n
rw₁ :
  p.coeff
      ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
        ((revAt (p.mirror.natDegree + p.mirror.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ)) =
    p.coeff n
rw₂ :
  p.coeff
      ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
        ((revAt (p.natDegree + p.mirror.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ)) =
    p.coeff n
rw₃ :
  p.coeff
      ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
        ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ)) =
    p.coeff n
⊢ p.mirror.mirror.coeff n = p.coeff n
have rw₄ : p.coeff n = p.coeff n
Tactic: rw [coeff_mirror, coeff_mirror, mirror_natDegree, mirror_natTrailingDegree, revAt_invol]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
h : p.mirror = 0
⊢ p = 0
have rw : p.mirror.mirror = 0
Tactic: rw [← p.mirror_mirror, h, mirror_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
h : p.mirror = 0
rw : p.mirror.mirror = 0
⊢ p = 0
have rw₁ : Eq.{u_1 + 1} (α := R[X]) (mirror 0) 0
Tactic: rw [← p.mirror_mirror, h, mirror_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
h : p.mirror = 0
rw : p.mirror.mirror = 0
rw₁ : Eq.{u_1 + 1} (α := R[X]) (mirror 0) 0
⊢ p = 0
have rw₂ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [← p.mirror_mirror, h, mirror_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
h : p = 0
⊢ p.mirror = 0
have rw : Eq.{u_1 + 1} (α := R[X]) (mirror 0) 0
Tactic: rw [h, mirror_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
h : p = 0
rw : Eq.{u_1 + 1} (α := R[X]) (mirror 0) 0
⊢ p.mirror = 0
have rw₁ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [h, mirror_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ p.mirror.trailingCoeff = p.leadingCoeff
have rw : p.mirror.trailingCoeff = p.coeff p.natDegree
Tactic: rw [leadingCoeff, trailingCoeff, mirror_natTrailingDegree, coeff_mirror,
    revAt_le (Nat.le_add_left _ _), add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
rw : p.mirror.trailingCoeff = p.coeff p.natDegree
⊢ p.mirror.trailingCoeff = p.leadingCoeff
have rw₁ : p.mirror.coeff p.mirror.natTrailingDegree = p.coeff p.natDegree
Tactic: rw [leadingCoeff, trailingCoeff, mirror_natTrailingDegree, coeff_mirror,
    revAt_le (Nat.le_add_left _ _), add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
rw : p.mirror.trailingCoeff = p.coeff p.natDegree
rw₁ : p.mirror.coeff p.mirror.natTrailingDegree = p.coeff p.natDegree
⊢ p.mirror.trailingCoeff = p.leadingCoeff
have rw₂ : p.mirror.coeff p.natTrailingDegree = p.coeff p.natDegree
Tactic: rw [leadingCoeff, trailingCoeff, mirror_natTrailingDegree, coeff_mirror,
    revAt_le (Nat.le_add_left _ _), add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
rw : p.mirror.trailingCoeff = p.coeff p.natDegree
rw₁ : p.mirror.coeff p.mirror.natTrailingDegree = p.coeff p.natDegree
rw₂ : p.mirror.coeff p.natTrailingDegree = p.coeff p.natDegree
⊢ p.mirror.trailingCoeff = p.leadingCoeff
have rw₃ : p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) p.natTrailingDegree) = p.coeff p.natDegree
Tactic: rw [leadingCoeff, trailingCoeff, mirror_natTrailingDegree, coeff_mirror,
    revAt_le (Nat.le_add_left _ _), add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
rw : p.mirror.trailingCoeff = p.coeff p.natDegree
rw₁ : p.mirror.coeff p.mirror.natTrailingDegree = p.coeff p.natDegree
rw₂ : p.mirror.coeff p.natTrailingDegree = p.coeff p.natDegree
rw₃ : p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) p.natTrailingDegree) = p.coeff p.natDegree
⊢ p.mirror.trailingCoeff = p.leadingCoeff
have rw₄ : p.coeff (p.natDegree + p.natTrailingDegree - p.natTrailingDegree) = p.coeff p.natDegree
Tactic: rw [leadingCoeff, trailingCoeff, mirror_natTrailingDegree, coeff_mirror,
    revAt_le (Nat.le_add_left _ _), add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
rw : p.mirror.trailingCoeff = p.coeff p.natDegree
rw₁ : p.mirror.coeff p.mirror.natTrailingDegree = p.coeff p.natDegree
rw₂ : p.mirror.coeff p.natTrailingDegree = p.coeff p.natDegree
rw₃ : p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) p.natTrailingDegree) = p.coeff p.natDegree
rw₄ : p.coeff (p.natDegree + p.natTrailingDegree - p.natTrailingDegree) = p.coeff p.natDegree
⊢ p.mirror.trailingCoeff = p.leadingCoeff
have rw₅ : p.coeff p.natDegree = p.coeff p.natDegree
Tactic: rw [leadingCoeff, trailingCoeff, mirror_natTrailingDegree, coeff_mirror,
    revAt_le (Nat.le_add_left _ _), add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ p.mirror.leadingCoeff = p.trailingCoeff
have rw : p.mirror.mirror.mirror.leadingCoeff = p.mirror.mirror.trailingCoeff
Tactic: rw [← p.mirror_mirror, mirror_trailingCoeff, p.mirror_mirror]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
rw : p.mirror.mirror.mirror.leadingCoeff = p.mirror.mirror.trailingCoeff
⊢ p.mirror.leadingCoeff = p.trailingCoeff
have rw₁ : p.mirror.mirror.mirror.leadingCoeff = p.mirror.leadingCoeff
Tactic: rw [← p.mirror_mirror, mirror_trailingCoeff, p.mirror_mirror]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
rw : p.mirror.mirror.mirror.leadingCoeff = p.mirror.mirror.trailingCoeff
rw₁ : p.mirror.mirror.mirror.leadingCoeff = p.mirror.leadingCoeff
⊢ p.mirror.leadingCoeff = p.trailingCoeff
have rw₂ : p.mirror.leadingCoeff = p.mirror.leadingCoeff
Tactic: rw [← p.mirror_mirror, mirror_trailingCoeff, p.mirror_mirror]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ (p * p.mirror).coeff (p.natDegree + p.natTrailingDegree) = p.sum fun (x : ℕ) (x_1 : R) ↦ HPow.hPow (β := ℕ) x_1 2
have rw : Eq (α := R)
  (∑ k ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ,
    p.coeff (k, p.natDegree + p.natTrailingDegree - k).1 * p.mirror.coeff (k, p.natDegree + p.natTrailingDegree - k).2)
  (p.sum fun (x : ℕ) (x_1 : R) ↦ HPow.hPow (β := ℕ) x_1 2)
Tactic: rw [coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ Eq (α := R)
    (∑ k ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ,
      p.coeff (k, p.natDegree + p.natTrailingDegree - k).1 *
        p.mirror.coeff (k, p.natDegree + p.natTrailingDegree - k).2)
    (p.sum fun (x : ℕ) (x_1 : R) ↦ HPow.hPow (β := ℕ) x_1 2)
have rfl : ∀ (n : ℕ) (hn : n ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ),
  p.coeff (n, p.natDegree + p.natTrailingDegree - n).1 * p.mirror.coeff (n, p.natDegree + p.natTrailingDegree - n).2 =
    HPow.hPow (β := ℕ) (p.coeff n) 2
Tactic: refine
    (Finset.sum_congr rfl fun n hn => ?_).trans
      (p.sum_eq_of_subset (fun _ ↦ (· ^ 2)) (fun _ ↦ zero_pow two_ne_zero) fun n hn ↦
          Finset.mem_range_succ_iff.mpr
            ((le_natDegree_of_mem_supp n hn).trans (Nat.le_add_right _ _))).symm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ
⊢ p.coeff (n, p.natDegree + p.natTrailingDegree - n).1 * p.mirror.coeff (n, p.natDegree + p.natTrailingDegree - n).2 =
    HPow.hPow (β := ℕ) (p.coeff n) 2
have rw : p.coeff (n, p.natDegree + p.natTrailingDegree - n).1 *
    p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) (n, p.natDegree + p.natTrailingDegree - n).2) =
  HPow.hPow (β := ℕ) (p.coeff n) 2
Tactic: rw [coeff_mirror, ← revAt_le (Finset.mem_range_succ_iff.mp hn), revAt_invol, ← sq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ
rw :
  p.coeff (n, p.natDegree + p.natTrailingDegree - n).1 *
      p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) (n, p.natDegree + p.natTrailingDegree - n).2) =
    HPow.hPow (β := ℕ) (p.coeff n) 2
⊢ p.coeff (n, p.natDegree + p.natTrailingDegree - n).1 * p.mirror.coeff (n, p.natDegree + p.natTrailingDegree - n).2 =
    HPow.hPow (β := ℕ) (p.coeff n) 2
have rw₁ : p.coeff ((n, (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n) : ℕ × ℕ).1 *
    p.coeff
      ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
        ((n, (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n).2 : ℕ)) =
  HPow.hPow (β := ℕ) (p.coeff n) 2
Tactic: rw [coeff_mirror, ← revAt_le (Finset.mem_range_succ_iff.mp hn), revAt_invol, ← sq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ
rw :
  p.coeff (n, p.natDegree + p.natTrailingDegree - n).1 *
      p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) (n, p.natDegree + p.natTrailingDegree - n).2) =
    HPow.hPow (β := ℕ) (p.coeff n) 2
rw₁ :
  p.coeff ((n, (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n) : ℕ × ℕ).1 *
      p.coeff
        ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
          ((n, (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n).2 : ℕ)) =
    HPow.hPow (β := ℕ) (p.coeff n) 2
⊢ p.coeff (n, p.natDegree + p.natTrailingDegree - n).1 * p.mirror.coeff (n, p.natDegree + p.natTrailingDegree - n).2 =
    HPow.hPow (β := ℕ) (p.coeff n) 2
have rw₂ : p.coeff ((n, (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n) : ℕ × ℕ).1 * p.coeff n =
  HPow.hPow (β := ℕ) (p.coeff n) 2
Tactic: rw [coeff_mirror, ← revAt_le (Finset.mem_range_succ_iff.mp hn), revAt_invol, ← sq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ
rw :
  p.coeff (n, p.natDegree + p.natTrailingDegree - n).1 *
      p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) (n, p.natDegree + p.natTrailingDegree - n).2) =
    HPow.hPow (β := ℕ) (p.coeff n) 2
rw₁ :
  p.coeff ((n, (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n) : ℕ × ℕ).1 *
      p.coeff
        ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
          ((n, (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n).2 : ℕ)) =
    HPow.hPow (β := ℕ) (p.coeff n) 2
rw₂ :
  p.coeff ((n, (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n) : ℕ × ℕ).1 * p.coeff n =
    HPow.hPow (β := ℕ) (p.coeff n) 2
⊢ p.coeff (n, p.natDegree + p.natTrailingDegree - n).1 * p.mirror.coeff (n, p.natDegree + p.natTrailingDegree - n).2 =
    HPow.hPow (β := ℕ) (p.coeff n) 2
have rw₃ : HPow.hPow (β := ℕ) (p.coeff ((n, (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n) : ℕ × ℕ).1) 2 =
  HPow.hPow (β := ℕ) (p.coeff n) 2
Tactic: rw [coeff_mirror, ← revAt_le (Finset.mem_range_succ_iff.mp hn), revAt_invol, ← sq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
⊢ (p * p.mirror).natDegree = 2 * p.natDegree
have pos : ∀ (hp : p = 0), (p * p.mirror).natDegree = 2 * 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]
inst_1 : NoZeroDivisors R
pos : ∀ (hp : p = 0), (p * p.mirror).natDegree = 2 * p.natDegree
⊢ (p * p.mirror).natDegree = 2 * p.natDegree
have neg : ∀ (hp : ¬p = 0), (p * p.mirror).natDegree = 2 * 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]
inst_1 : NoZeroDivisors R
hp : p = 0
⊢ (p * p.mirror).natDegree = 2 * p.natDegree
have pos : (HMul.hMul (α := R[X]) 0 (mirror 0)).natDegree = 2 * natDegree.{u_1} (R := R) 0
Tactic: rw [hp, zero_mul, natDegree_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
hp : p = 0
pos : (HMul.hMul (α := R[X]) 0 (mirror 0)).natDegree = 2 * natDegree.{u_1} (R := R) 0
⊢ (p * p.mirror).natDegree = 2 * p.natDegree
have pos₁ : natDegree.{u_1} (R := R) 0 = 2 * natDegree.{u_1} (R := R) 0
Tactic: rw [hp, zero_mul, natDegree_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
hp : p = 0
pos : (HMul.hMul (α := R[X]) 0 (mirror 0)).natDegree = 2 * natDegree.{u_1} (R := R) 0
pos₁ : natDegree.{u_1} (R := R) 0 = 2 * natDegree.{u_1} (R := R) 0
⊢ (p * p.mirror).natDegree = 2 * p.natDegree
have pos₂ : 0 = HMul.hMul (α := ℕ) 2 0
Tactic: rw [hp, zero_mul, natDegree_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
hp : p = 0
pos : (HMul.hMul (α := R[X]) 0 (mirror 0)).natDegree = 2 * natDegree.{u_1} (R := R) 0
pos₁ : natDegree.{u_1} (R := R) 0 = 2 * natDegree.{u_1} (R := R) 0
pos₂ : 0 = HMul.hMul (α := ℕ) 2 0
⊢ (p * p.mirror).natDegree = 2 * p.natDegree
have pos₃ : Eq (α := ℕ) 0 0
Tactic: rw [hp, zero_mul, natDegree_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * p.mirror).natDegree = 2 * p.natDegree
have neg : p.natDegree + p.mirror.natDegree = 2 * p.natDegree
Tactic: rw [natDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natDegree, two_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
neg : p.natDegree + p.mirror.natDegree = 2 * p.natDegree
⊢ (p * p.mirror).natDegree = 2 * p.natDegree
have neg₁ : p.natDegree + p.natDegree = 2 * p.natDegree
Tactic: rw [natDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natDegree, two_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
neg : p.natDegree + p.mirror.natDegree = 2 * p.natDegree
neg₁ : p.natDegree + p.natDegree = 2 * p.natDegree
⊢ (p * p.mirror).natDegree = 2 * p.natDegree
have neg₂ : p.natDegree + p.natDegree = p.natDegree + p.natDegree
Tactic: rw [natDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natDegree, two_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
have pos : ∀ (hp : p = 0), (p * p.mirror).natTrailingDegree = 2 * 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]
inst_1 : NoZeroDivisors R
pos : ∀ (hp : p = 0), (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
have neg : ∀ (hp : ¬p = 0), (p * p.mirror).natTrailingDegree = 2 * 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]
inst_1 : NoZeroDivisors R
hp : p = 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
have pos : (HMul.hMul (α := R[X]) 0 (mirror 0)).natTrailingDegree = 2 * natTrailingDegree.{u_1} (R := R) 0
Tactic: rw [hp, zero_mul, natTrailingDegree_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
hp : p = 0
pos : (HMul.hMul (α := R[X]) 0 (mirror 0)).natTrailingDegree = 2 * natTrailingDegree.{u_1} (R := R) 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
have pos₁ : natTrailingDegree.{u_1} (R := R) 0 = 2 * natTrailingDegree.{u_1} (R := R) 0
Tactic: rw [hp, zero_mul, natTrailingDegree_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
hp : p = 0
pos : (HMul.hMul (α := R[X]) 0 (mirror 0)).natTrailingDegree = 2 * natTrailingDegree.{u_1} (R := R) 0
pos₁ : natTrailingDegree.{u_1} (R := R) 0 = 2 * natTrailingDegree.{u_1} (R := R) 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
have pos₂ : 0 = HMul.hMul (α := ℕ) 2 0
Tactic: rw [hp, zero_mul, natTrailingDegree_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
hp : p = 0
pos : (HMul.hMul (α := R[X]) 0 (mirror 0)).natTrailingDegree = 2 * natTrailingDegree.{u_1} (R := R) 0
pos₁ : natTrailingDegree.{u_1} (R := R) 0 = 2 * natTrailingDegree.{u_1} (R := R) 0
pos₂ : 0 = HMul.hMul (α := ℕ) 2 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
have pos₃ : Eq (α := ℕ) 0 0
Tactic: rw [hp, zero_mul, natTrailingDegree_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
have neg : p.natTrailingDegree + p.mirror.natTrailingDegree = 2 * p.natTrailingDegree
Tactic: rw [natTrailingDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natTrailingDegree, two_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
neg : p.natTrailingDegree + p.mirror.natTrailingDegree = 2 * p.natTrailingDegree
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
have neg₁ : p.natTrailingDegree + p.natTrailingDegree = 2 * p.natTrailingDegree
Tactic: rw [natTrailingDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natTrailingDegree, two_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
neg : p.natTrailingDegree + p.mirror.natTrailingDegree = 2 * p.natTrailingDegree
neg₁ : p.natTrailingDegree + p.natTrailingDegree = 2 * p.natTrailingDegree
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
have neg₂ : p.natTrailingDegree + p.natTrailingDegree = p.natTrailingDegree + p.natTrailingDegree
Tactic: rw [natTrailingDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natTrailingDegree, two_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
⊢ (p * q).mirror = p.mirror * q.mirror
have pos : ∀ (hp : p = 0), (p * q).mirror = p.mirror * q.mirror
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 q : R[X]
inst_1 : NoZeroDivisors R
pos : ∀ (hp : p = 0), (p * q).mirror = p.mirror * q.mirror
⊢ (p * q).mirror = p.mirror * q.mirror
have neg : ∀ (hp : ¬p = 0), (p * q).mirror = p.mirror * q.mirror
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 q : R[X]
inst_1 : NoZeroDivisors R
hp : p = 0
⊢ (p * q).mirror = p.mirror * q.mirror
have pos : (0 * q).mirror = mirror 0 * q.mirror
Tactic: rw [hp, zero_mul, mirror_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : p = 0
pos : (0 * q).mirror = mirror 0 * q.mirror
⊢ (p * q).mirror = p.mirror * q.mirror
have pos₁ : mirror 0 = mirror 0 * q.mirror
Tactic: rw [hp, zero_mul, mirror_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : p = 0
pos : (0 * q).mirror = mirror 0 * q.mirror
pos₁ : mirror 0 = mirror 0 * q.mirror
⊢ (p * q).mirror = p.mirror * q.mirror
have pos₂ : 0 = 0 * q.mirror
Tactic: rw [hp, zero_mul, mirror_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : p = 0
pos : (0 * q).mirror = mirror 0 * q.mirror
pos₁ : mirror 0 = mirror 0 * q.mirror
pos₂ : 0 = 0 * q.mirror
⊢ (p * q).mirror = p.mirror * q.mirror
have pos₃ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [hp, zero_mul, mirror_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * q).mirror = p.mirror * q.mirror
have pos : ∀ (hq : q = 0), (p * q).mirror = p.mirror * q.mirror
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
pos : ∀ (hq : q = 0), (p * q).mirror = p.mirror * q.mirror
⊢ (p * q).mirror = p.mirror * q.mirror
have neg : ∀ (hq : ¬q = 0), (p * q).mirror = p.mirror * q.mirror
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ (p * q).mirror = p.mirror * q.mirror
have pos : (p * 0).mirror = p.mirror * mirror 0
Tactic: rw [hq, mul_zero, mirror_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
pos : (p * 0).mirror = p.mirror * mirror 0
⊢ (p * q).mirror = p.mirror * q.mirror
have pos₁ : mirror 0 = p.mirror * mirror 0
Tactic: rw [hq, mul_zero, mirror_zero, mul_zero]