awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
h : p.natDegree + p.natTrailingDegree - n ≤ p.natDegree
⊢ (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n ≤ p.natDegree

Tactic:
rw [revAt_le (hn.trans (Nat.le_add_right _ _))]

Premises used: Nat.le_add_right, Polynomial.revAt_le, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
h : p.natTrailingDegree ≤ n
⊢ p.natDegree + p.natTrailingDegree - n ≤ p.natDegree

Tactic:
rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right]

Premises used: add_comm, add_tsub_cancel_right, tsub_le_iff_tsub_le
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natTrailingDegree ≤ n

Tactic:
natTrailingDegree_le_of_ne_zero hp

Premises used: Polynomial.natTrailingDegree_le_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natTrailingDegree ≤ n

Tactic:
exact natTrailingDegree_le_of_ne_zero hp

Premises used: Polynomial.natTrailingDegree_le_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
h : p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n) ≠ 0
⊢ p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n) ≠ 0

Tactic:
change p.mirror.coeff _ ≠ 0

Premises used: Polynomial.mirror, Polynomial.coeff
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
h :
  p.coeff
      ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
        ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ)) ≠
    0
h₁ h₂ h₃ h₄ : p.coeff n ≠ 0
⊢ p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n) ≠ 0

Tactic:
rwa [coeff_mirror, revAt_invol]

Premises used: Polynomial.coeff_mirror, Polynomial.revAt_invol
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ ∀ (a : ℕ) (h₁ : a ∈ Finset.range (p.natDegree + 1)) (h₂ : p.mirror.coeff a ≠ 0),
    p.mirror.coeff a = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) a)

Tactic:
fun n _ _ => p.coeff_mirror n

Premises used: Polynomial.coeff_mirror
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ ∀ (a : ℕ) (h₁ : a ∈ Finset.range (p.natDegree + 1)) (h₂ : p.mirror.coeff a ≠ 0),
    p.mirror.coeff a = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) a)

Tactic:
exact fun n _ _ => p.coeff_mirror n

Premises used: Polynomial.coeff_mirror
-- Module: Mathlib.Algebra.Polynomial.Mirror
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
rw₄ rw₅ : p.coeff n = p.coeff n
⊢ p.mirror.mirror.coeff n = p.coeff n

Tactic:
rw [coeff_mirror, coeff_mirror, mirror_natDegree, mirror_natTrailingDegree, revAt_invol]

Premises used: Polynomial.mirror_natDegree, Polynomial.coeff_mirror, Polynomial.mirror_natTrailingDegree, Polynomial.revAt_invol
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
⊢ Function.Involutive.{u_1 + 1} (α := R[X]) mirror

Tactic:
mirror_mirror

Premises used: Function.Involutive, Polynomial.mirror_mirror
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
⊢ p.mirror = q ↔ p = q.mirror

Tactic:
mirror_involutive.eq_iff

Premises used: Polynomial.mirror_involutive, Function.Involutive.eq_iff
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
⊢ p.mirror = q.mirror ↔ p = q

Tactic:
mirror_involutive.injective.eq_iff

Premises used: Function.Injective.eq_iff, Polynomial.mirror_involutive, Function.Involutive.injective
-- Module: Mathlib.Algebra.Polynomial.Mirror
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ p = 0

Tactic:
rw [← p.mirror_mirror, h, mirror_zero]

Premises used: Polynomial.mirror_zero, Polynomial.mirror_mirror
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
h : p = 0
rw : Eq.{u_1 + 1} (α := R[X]) (mirror 0) 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ p.mirror = 0

Tactic:
rw [h, mirror_zero]

Premises used: Polynomial.mirror_zero
-- Module: Mathlib.Algebra.Polynomial.Mirror
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
rw₅ rw₆ : p.coeff p.natDegree = p.coeff p.natDegree
⊢ p.mirror.trailingCoeff = p.leadingCoeff

Tactic:
rw [leadingCoeff, trailingCoeff, mirror_natTrailingDegree, coeff_mirror,
    revAt_le (Nat.le_add_left _ _), add_tsub_cancel_right]

Premises used: Nat.le_add_left, Polynomial.leadingCoeff, Polynomial.revAt_le, Polynomial.trailingCoeff, Polynomial.coeff_mirror, Polynomial.mirror_natTrailingDegree, add_tsub_cancel_right
-- Module: Mathlib.Algebra.Polynomial.Mirror
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
rw₂ rw₃ : p.mirror.leadingCoeff = p.mirror.leadingCoeff
⊢ p.mirror.leadingCoeff = p.trailingCoeff

Tactic:
rw [← p.mirror_mirror, mirror_trailingCoeff, p.mirror_mirror]

Premises used: Polynomial.mirror_trailingCoeff, Polynomial.mirror_mirror
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
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)
⊢ (p * p.mirror).coeff (p.natDegree + p.natTrailingDegree) = 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]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, Polynomial.coeff_mul
-- Module: Mathlib.Algebra.Polynomial.Mirror
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)

Tactic:
(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

Premises used: Iff.mpr, Polynomial.le_natDegree_of_mem_supp, Nat.le_add_right, Finset.mem_range_succ_iff, Polynomial.sum_eq_of_subset, two_ne_zero, HPow.hPow, LE.le.trans, Polynomial.natDegree, OfNat.ofNat, Eq.symm, Finset.sum_congr, zero_pow, rfl, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
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
⊢ 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:
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

Premises used: Iff.mpr, Polynomial.le_natDegree_of_mem_supp, Nat.le_add_right, Finset.mem_range_succ_iff, Polynomial.sum_eq_of_subset, two_ne_zero, HPow.hPow, LE.le.trans, Polynomial.natDegree, OfNat.ofNat, Eq.symm, Finset.sum_congr, zero_pow, rfl, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Mirror
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
rw₃ rw₄ :
  HPow.hPow (β := ℕ) (p.coeff ((n, (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n) : ℕ × ℕ).1) 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

Tactic:
rw [coeff_mirror, ← revAt_le (Finset.mem_range_succ_iff.mp hn), revAt_invol, ← sq]

Premises used: Finset.mem_range_succ_iff, sq, Polynomial.revAt_le, Iff.mp, Polynomial.coeff_mirror, Polynomial.revAt_invol
-- Module: Mathlib.Algebra.Polynomial.Mirror
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
neg : ∀ (hp : ¬p = 0), (p * p.mirror).natDegree = 2 * p.natDegree
⊢ (p * p.mirror).natDegree = 2 * p.natDegree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Mirror
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
pos₃ pos₄ : Eq (α := ℕ) 0 0
⊢ (p * p.mirror).natDegree = 2 * p.natDegree

Tactic:
rw [hp, zero_mul, natDegree_zero, mul_zero]

Premises used: MulZeroClass.zero_mul, Polynomial.natDegree_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.Mirror
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
neg₂ neg₃ : p.natDegree + p.natDegree = p.natDegree + p.natDegree
⊢ (p * p.mirror).natDegree = 2 * p.natDegree

Tactic:
rw [natDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natDegree, two_mul]

Premises used: Polynomial.natDegree_mul, two_mul, mt, Polynomial.mirror_natDegree, Iff.mp, Polynomial.mirror_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Mirror
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
neg : ∀ (hp : ¬p = 0), (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Mirror
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
pos₃ pos₄ : Eq (α := ℕ) 0 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

Tactic:
rw [hp, zero_mul, natTrailingDegree_zero, mul_zero]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, Polynomial.natTrailingDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Mirror
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
neg₂ neg₃ : p.natTrailingDegree + p.natTrailingDegree = p.natTrailingDegree + p.natTrailingDegree
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

Tactic:
rw [natTrailingDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natTrailingDegree, two_mul]

Premises used: two_mul, mt, Iff.mp, Polynomial.natTrailingDegree_mul, Polynomial.mirror_eq_zero, Polynomial.mirror_natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Mirror
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
neg : ∀ (hp : ¬p = 0), (p * q).mirror = p.mirror * q.mirror
⊢ (p * q).mirror = p.mirror * q.mirror

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Mirror
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
pos₃ pos₄ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ (p * q).mirror = p.mirror * q.mirror

Tactic:
rw [hp, zero_mul, mirror_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, Polynomial.mirror_zero
-- Module: Mathlib.Algebra.Polynomial.Mirror
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
neg : ∀ (hq : ¬q = 0), (p * q).mirror = p.mirror * q.mirror
⊢ (p * q).mirror = p.mirror * q.mirror

Tactic:
by_cases hq : q = 0
-- Module: Mathlib.Algebra.Polynomial.Mirror
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
pos₁ : mirror 0 = p.mirror * mirror 0
pos₂ : 0 = p.mirror * 0
pos₃ pos₄ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ (p * q).mirror = p.mirror * q.mirror

Tactic:
rw [hq, mul_zero, mirror_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, Polynomial.mirror_zero
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
neg :
  p.reverse * q.reverse * (HPow.hPow (α := R[X]) X p.natTrailingDegree * HPow.hPow (α := R[X]) X q.natTrailingDegree) =
    p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)
⊢ (p * q).mirror = p.mirror * q.mirror

Tactic:
rw [mirror, mirror, mirror, reverse_mul_of_domain, natTrailingDegree_mul hp hq, pow_add]

Premises used: Polynomial.reverse_mul_of_domain, pow_add, Polynomial.mirror, Polynomial.natTrailingDegree_mul
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
neg :
  p.reverse * (HPow.hPow (α := R[X]) X p.natTrailingDegree * q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree) =
    p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)
⊢ p.reverse * q.reverse * (HPow.hPow (α := R[X]) X p.natTrailingDegree * HPow.hPow (α := R[X]) X q.natTrailingDegree) =
    p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)

Tactic:
rw [mul_assoc, ← mul_assoc q.reverse, ← X_pow_mul (p := reverse q)]

Premises used: mul_assoc, Polynomial.reverse, Polynomial.X_pow_mul
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
neg :
  p.reverse *
      (HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)) =
    p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)
⊢ p.reverse * (HPow.hPow (α := R[X]) X p.natTrailingDegree * q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree) =
    p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
neg neg₁ :
  p.reverse *
      (HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)) =
    p.reverse *
      (HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree))
⊢ p.reverse *
      (HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)) =
    p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
neg neg₁ neg₂ :
  p.reverse *
      (HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)) =
    p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)
⊢ p.reverse * (HPow.hPow (α := R[X]) X p.natTrailingDegree * q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree) =
    p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)

Tactic:
repeat' rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
a : R
rw : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).mirror = a • p.mirror
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).mirror =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p.mirror
rw₂ : mirror ((C : (a : R) → R[X]) a) * p.mirror = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p.mirror
rw₃ rw₄ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p.mirror =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p.mirror
⊢ (a • p).mirror = a • p.mirror

Tactic:
rw [← C_mul', ← C_mul', mirror_mul_of_domain, mirror_C]

Premises used: Polynomial.C_mul', Polynomial.mirror_mul_of_domain, Polynomial.mirror_C
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Ring R
p : R[X]
rw : (-p).reverse * HPow.hPow (α := R[X]) X (-p).natTrailingDegree = -p.mirror
rw₁ :
  (-p).reverse * HPow.hPow (α := R[X]) X (-p).natTrailingDegree =
    -(p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree)
rw₂ :
  -p.reverse * HPow.hPow (α := R[X]) X (-p).natTrailingDegree =
    -(p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree)
rw₃ :
  -p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree = -(p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree)
rw₄ rw₅ :
  -p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree = -p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree
⊢ (-p).mirror = -p.mirror

Tactic:
rw [mirror, mirror, reverse_neg, natTrailingDegree_neg, neg_mul_eq_neg_mul]

Premises used: Polynomial.mirror, Polynomial.natTrailingDegree_neg, Polynomial.reverse_neg, neg_mul_eq_neg_mul
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
not_isUnit : ¬IsUnit f
isUnit_or_isUnit : ∀ ⦃a b : R[X]⦄, f = a * b → IsUnit a ∨ IsUnit b
⊢ Irreducible f

Tactic:
constructor
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
⊢ ¬IsUnit f

Tactic:
h1
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
⊢ ¬IsUnit f

Tactic:
exact h1
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
rw : g * h * (g * h).mirror = k * k.mirror
rw₁ : g * h * (g.mirror * h.mirror) = k * k.mirror
rw₂ : g * h * (g.mirror * h.mirror) = k * (g.mirror * h.mirror.mirror)
rw₃ : g * h * (g.mirror * h.mirror) = k * (g.mirror * h)
rw₄ : g * (h * (g.mirror * h.mirror)) = k * (g.mirror * h)
rw₅ : g * (g.mirror * h.mirror * h) = k * (g.mirror * h)
rw₆ : g * (h.mirror * g.mirror * h) = k * (g.mirror * h)
rw₇ : g * (h.mirror * (g.mirror * h)) = k * (g.mirror * h)
rw₈ rw₉ : g * h.mirror * (g.mirror * h) = k * (g.mirror * h)
⊢ f * f.mirror = k * k.mirror

Tactic:
rw [fgh, mirror_mul_of_domain, mirror_mul_of_domain, mirror_mirror, mul_assoc, mul_comm h,
        mul_comm g.mirror, mul_assoc, ← mul_assoc]

Premises used: mul_assoc, Polynomial.mirror, Polynomial.mirror_mul_of_domain, mul_comm, Polynomial.mirror_mirror
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
⊢ f * f.mirror = k * k.mirror

Tactic:
have key : f * f.mirror = k * k.mirror := by
      rw [fgh, mirror_mul_of_domain, mirror_mul_of_domain, mirror_mirror, mul_assoc, mul_comm h,
        mul_comm g.mirror, mul_assoc, ← mul_assoc]
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
rw : g ∣ g * h
⊢ g ∣ f

Tactic:
rw [fgh]
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
⊢ g ∣ g * h

Tactic:
dvd_mul_right g h

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
⊢ g ∣ g * h

Tactic:
exact dvd_mul_right g h

Premises used: dvd_mul_right