[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ mirror 0 = 0
[PROOFSTEP]
simp [mirror]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ mirror (↑(monomial n) a) = ↑(monomial n) a
[PROOFSTEP]
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]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ mirror (↑(monomial n) a) = ↑(monomial n) a
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
ha : a = 0
⊢ mirror (↑(monomial n) a) = ↑(monomial n) a
[PROOFSTEP]
rw [ha, monomial_zero_right, mirror_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
ha : ¬a = 0
⊢ mirror (↑(monomial n) a) = ↑(monomial n) a
[PROOFSTEP]
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]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ natDegree (mirror p) = natDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : p = 0
⊢ natDegree (mirror p) = natDegree p
[PROOFSTEP]
rw [hp, mirror_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : ¬p = 0
⊢ natDegree (mirror p) = natDegree p
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : ¬p = 0
✝ : Nontrivial R
⊢ natDegree (mirror p) = natDegree p
[PROOFSTEP]
rw [mirror, natDegree_mul', reverse_natDegree, natDegree_X_pow, tsub_add_cancel_of_le p.natTrailingDegree_le_natDegree]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : ¬p = 0
✝ : Nontrivial R
⊢ leadingCoeff (reverse p) * leadingCoeff (X ^ natTrailingDegree p) ≠ 0
[PROOFSTEP]
rwa [leadingCoeff_X_pow, mul_one, reverse_leadingCoeff, Ne, trailingCoeff_eq_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ natTrailingDegree (mirror p) = natTrailingDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : p = 0
⊢ natTrailingDegree (mirror p) = natTrailingDegree p
[PROOFSTEP]
rw [hp, mirror_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : ¬p = 0
⊢ natTrailingDegree (mirror p) = natTrailingDegree p
[PROOFSTEP]
rw [mirror, natTrailingDegree_mul_X_pow ((mt reverse_eq_zero.mp) hp), reverse_natTrailingDegree, zero_add]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ coeff (mirror p) n = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) n)
[PROOFSTEP]
by_cases h2 : p.natDegree < n
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : natDegree p < n
⊢ coeff (mirror p) n = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) n)
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt (by rwa [mirror_natDegree])]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : natDegree p < n
⊢ natDegree (mirror p) < n
[PROOFSTEP]
rwa [mirror_natDegree]
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : natDegree p < n
⊢ 0 = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) n)
[PROOFSTEP]
by_cases h1 : n ≤ p.natDegree + p.natTrailingDegree
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : natDegree p < n
h1 : n ≤ natDegree p + natTrailingDegree p
⊢ 0 = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) n)
[PROOFSTEP]
rw [revAt_le h1, coeff_eq_zero_of_lt_natTrailingDegree]
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : natDegree p < n
h1 : n ≤ natDegree p + natTrailingDegree p
⊢ natDegree p + natTrailingDegree p - n < natTrailingDegree p
[PROOFSTEP]
exact (tsub_lt_iff_left h1).mpr (Nat.add_lt_add_right h2 _)
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : natDegree p < n
h1 : ¬n ≤ natDegree p + natTrailingDegree p
⊢ 0 = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) n)
[PROOFSTEP]
rw [← revAtFun_eq, revAtFun, if_neg h1, coeff_eq_zero_of_natDegree_lt h2]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : ¬natDegree p < n
⊢ coeff (mirror p) n = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) n)
[PROOFSTEP]
rw [not_lt] at h2 
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : n ≤ natDegree p
⊢ coeff (mirror p) n = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) n)
[PROOFSTEP]
rw [revAt_le (h2.trans (Nat.le_add_right _ _))]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : n ≤ natDegree p
⊢ coeff (mirror p) n = coeff p (natDegree p + natTrailingDegree p - n)
[PROOFSTEP]
by_cases h3 : p.natTrailingDegree ≤ n
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : n ≤ natDegree p
h3 : natTrailingDegree p ≤ n
⊢ coeff (mirror p) n = coeff p (natDegree p + natTrailingDegree p - n)
[PROOFSTEP]
rw [← tsub_add_eq_add_tsub h2, ← tsub_tsub_assoc h2 h3, mirror, coeff_mul_X_pow', if_pos h3, coeff_reverse,
  revAt_le (tsub_le_self.trans h2)]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : n ≤ natDegree p
h3 : ¬natTrailingDegree p ≤ n
⊢ coeff (mirror p) n = coeff p (natDegree p + natTrailingDegree p - n)
[PROOFSTEP]
rw [not_le] at h3 
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : n ≤ natDegree p
h3 : n < natTrailingDegree p
⊢ coeff (mirror p) n = coeff p (natDegree p + natTrailingDegree p - n)
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt (lt_tsub_iff_right.mpr (Nat.add_lt_add_left h3 _))]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : n ≤ natDegree p
h3 : n < natTrailingDegree p
⊢ coeff (mirror p) n = 0
[PROOFSTEP]
exact coeff_eq_zero_of_lt_natTrailingDegree (by rwa [mirror_natTrailingDegree])
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : n ≤ natDegree p
h3 : n < natTrailingDegree p
⊢ n < natTrailingDegree (mirror p)
[PROOFSTEP]
rwa [mirror_natTrailingDegree]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ eval 1 (mirror p) = eval 1 p
[PROOFSTEP]
simp_rw [eval_eq_sum_range, one_pow, mul_one, mirror_natDegree]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ (Finset.sum (Finset.range (natDegree p + 1)) fun x => coeff (mirror p) x) =
    Finset.sum (Finset.range (natDegree p + 1)) fun x => coeff p x
[PROOFSTEP]
refine' Finset.sum_bij_ne_zero _ _ _ _ _
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ (a : ℕ) → a ∈ Finset.range (natDegree p + 1) → coeff (mirror p) a ≠ 0 → ℕ
[PROOFSTEP]
exact fun n _ _ => revAt (p.natDegree + p.natTrailingDegree) n
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (a : ℕ),
    a ∈ Finset.range (natDegree p + 1) →
      coeff (mirror p) a ≠ 0 → ↑(revAt (natDegree p + natTrailingDegree p)) a ∈ Finset.range (natDegree p + 1)
[PROOFSTEP]
intro n hn hp
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ Finset.range (natDegree p + 1)
hp : coeff (mirror p) n ≠ 0
⊢ ↑(revAt (natDegree p + natTrailingDegree p)) n ∈ Finset.range (natDegree p + 1)
[PROOFSTEP]
rw [Finset.mem_range_succ_iff] at *
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ≤ natDegree p
hp : coeff (mirror p) n ≠ 0
⊢ ↑(revAt (natDegree p + natTrailingDegree p)) n ≤ natDegree p
[PROOFSTEP]
rw [revAt_le (hn.trans (Nat.le_add_right _ _))]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ≤ natDegree p
hp : coeff (mirror p) n ≠ 0
⊢ natDegree p + natTrailingDegree p - n ≤ natDegree p
[PROOFSTEP]
rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right, ← mirror_natTrailingDegree]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ≤ natDegree p
hp : coeff (mirror p) n ≠ 0
⊢ natTrailingDegree (mirror p) ≤ n
[PROOFSTEP]
exact natTrailingDegree_le_of_ne_zero hp
[GOAL]
case refine'_3
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (a₁ a₂ : ℕ),
    a₁ ∈ Finset.range (natDegree p + 1) →
      coeff (mirror p) a₁ ≠ 0 →
        a₂ ∈ Finset.range (natDegree p + 1) →
          coeff (mirror p) a₂ ≠ 0 →
            ↑(revAt (natDegree p + natTrailingDegree p)) a₁ = ↑(revAt (natDegree p + natTrailingDegree p)) a₂ → a₁ = a₂
[PROOFSTEP]
exact fun n₁ n₂ _ _ _ _ h => by rw [← @revAt_invol _ n₁, h, revAt_invol]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n₁ n₂ : ℕ
x✝³ : n₁ ∈ Finset.range (natDegree p + 1)
x✝² : coeff (mirror p) n₁ ≠ 0
x✝¹ : n₂ ∈ Finset.range (natDegree p + 1)
x✝ : coeff (mirror p) n₂ ≠ 0
h : ↑(revAt (natDegree p + natTrailingDegree p)) n₁ = ↑(revAt (natDegree p + natTrailingDegree p)) n₂
⊢ n₁ = n₂
[PROOFSTEP]
rw [← @revAt_invol _ n₁, h, revAt_invol]
[GOAL]
case refine'_4
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (b : ℕ),
    b ∈ Finset.range (natDegree p + 1) → coeff p b ≠ 0 → ∃ a h₁ h₂, b = ↑(revAt (natDegree p + natTrailingDegree p)) a
[PROOFSTEP]
intro n hn hp
[GOAL]
case refine'_4
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ Finset.range (natDegree p + 1)
hp : coeff p n ≠ 0
⊢ ∃ a h₁ h₂, n = ↑(revAt (natDegree p + natTrailingDegree p)) a
[PROOFSTEP]
use revAt (p.natDegree + p.natTrailingDegree) n
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ Finset.range (natDegree p + 1)
hp : coeff p n ≠ 0
⊢ ∃ h₁ h₂, n = ↑(revAt (natDegree p + natTrailingDegree p)) (↑(revAt (natDegree p + natTrailingDegree p)) n)
[PROOFSTEP]
refine' ⟨_, _, revAt_invol.symm⟩
[GOAL]
case h.refine'_1
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ Finset.range (natDegree p + 1)
hp : coeff p n ≠ 0
⊢ ↑(revAt (natDegree p + natTrailingDegree p)) n ∈ Finset.range (natDegree p + 1)
[PROOFSTEP]
rw [Finset.mem_range_succ_iff] at *
[GOAL]
case h.refine'_1
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ≤ natDegree p
hp : coeff p n ≠ 0
⊢ ↑(revAt (natDegree p + natTrailingDegree p)) n ≤ natDegree p
[PROOFSTEP]
rw [revAt_le (hn.trans (Nat.le_add_right _ _))]
[GOAL]
case h.refine'_1
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ≤ natDegree p
hp : coeff p n ≠ 0
⊢ natDegree p + natTrailingDegree p - n ≤ natDegree p
[PROOFSTEP]
rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right]
[GOAL]
case h.refine'_1
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ≤ natDegree p
hp : coeff p n ≠ 0
⊢ natTrailingDegree p ≤ n
[PROOFSTEP]
exact natTrailingDegree_le_of_ne_zero hp
[GOAL]
case h.refine'_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ Finset.range (natDegree p + 1)
hp : coeff p n ≠ 0
⊢ coeff (mirror p) (↑(revAt (natDegree p + natTrailingDegree p)) n) ≠ 0
[PROOFSTEP]
change p.mirror.coeff _ ≠ 0
[GOAL]
case h.refine'_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ Finset.range (natDegree p + 1)
hp : coeff p n ≠ 0
⊢ coeff (mirror p) (↑(revAt (natDegree p + natTrailingDegree p)) n) ≠ 0
[PROOFSTEP]
rwa [coeff_mirror, revAt_invol]
[GOAL]
case refine'_5
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (a : ℕ),
    a ∈ Finset.range (natDegree p + 1) →
      coeff (mirror p) a ≠ 0 → coeff (mirror p) a = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) a)
[PROOFSTEP]
exact fun n _ _ => p.coeff_mirror n
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ coeff (mirror (mirror p)) n = coeff p n
[PROOFSTEP]
rw [coeff_mirror, coeff_mirror, mirror_natDegree, mirror_natTrailingDegree, revAt_invol]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
h : mirror p = 0
⊢ p = 0
[PROOFSTEP]
rw [← p.mirror_mirror, h, mirror_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
h : p = 0
⊢ mirror p = 0
[PROOFSTEP]
rw [h, mirror_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ trailingCoeff (mirror p) = leadingCoeff p
[PROOFSTEP]
rw [leadingCoeff, trailingCoeff, mirror_natTrailingDegree, coeff_mirror, revAt_le (Nat.le_add_left _ _),
  add_tsub_cancel_right]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ leadingCoeff (mirror p) = trailingCoeff p
[PROOFSTEP]
rw [← p.mirror_mirror, mirror_trailingCoeff, p.mirror_mirror]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ coeff (p * mirror p) (natDegree p + natTrailingDegree p) = sum p fun n x => x ^ 2
[PROOFSTEP]
rw [coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ (Finset.sum (Finset.range (Nat.succ (natDegree p + natTrailingDegree p))) fun k =>
      coeff p (k, natDegree p + natTrailingDegree p - k).fst *
        coeff (mirror p) (k, natDegree p + natTrailingDegree p - k).snd) =
    sum p fun n x => x ^ 2
[PROOFSTEP]
refine'
  (Finset.sum_congr rfl fun n hn => _).trans
    (p.sum_eq_of_subset (fun _ => (· ^ 2)) (fun _ => zero_pow zero_lt_two) fun n hn =>
        Finset.mem_range_succ_iff.mpr ((le_natDegree_of_mem_supp n hn).trans (Nat.le_add_right _ _))).symm
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ Finset.range (Nat.succ (natDegree p + natTrailingDegree p))
⊢ coeff p (n, natDegree p + natTrailingDegree p - n).fst *
      coeff (mirror p) (n, natDegree p + natTrailingDegree p - n).snd =
    coeff p n ^ 2
[PROOFSTEP]
rw [coeff_mirror, ← revAt_le (Finset.mem_range_succ_iff.mp hn), revAt_invol, ← sq]
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ natDegree (p * mirror p) = 2 * natDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ natDegree (p * mirror p) = 2 * natDegree p
[PROOFSTEP]
rw [hp, zero_mul, natDegree_zero, mul_zero]
[GOAL]
case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ natDegree (p * mirror p) = 2 * natDegree p
[PROOFSTEP]
rw [natDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natDegree, two_mul]
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ natTrailingDegree (p * mirror p) = 2 * natTrailingDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ natTrailingDegree (p * mirror p) = 2 * natTrailingDegree p
[PROOFSTEP]
rw [hp, zero_mul, natTrailingDegree_zero, mul_zero]
[GOAL]
case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ natTrailingDegree (p * mirror p) = 2 * natTrailingDegree p
[PROOFSTEP]
rw [natTrailingDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natTrailingDegree, two_mul]
[GOAL]
R : Type u_1
inst✝ : Ring R
p q : R[X]
⊢ mirror (-p) = -mirror p
[PROOFSTEP]
rw [mirror, mirror, reverse_neg, natTrailingDegree_neg, neg_mul_eq_neg_mul]
[GOAL]
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ mirror (p * q) = mirror p * mirror q
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ mirror (p * q) = mirror p * mirror q
[PROOFSTEP]
rw [hp, zero_mul, mirror_zero, zero_mul]
[GOAL]
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ mirror (p * q) = mirror p * mirror q
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ mirror (p * q) = mirror p * mirror q
[PROOFSTEP]
rw [hq, mul_zero, mirror_zero, mul_zero]
[GOAL]
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ mirror (p * q) = mirror p * mirror q
[PROOFSTEP]
rw [mirror, mirror, mirror, reverse_mul_of_domain, natTrailingDegree_mul hp hq, pow_add]
[GOAL]
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ reverse p * reverse q * (X ^ natTrailingDegree p * X ^ natTrailingDegree q) =
    reverse p * X ^ natTrailingDegree p * (reverse q * X ^ natTrailingDegree q)
[PROOFSTEP]
rw [mul_assoc, ← mul_assoc q.reverse, ← X_pow_mul (p := reverse q)]
[GOAL]
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ reverse p * (X ^ natTrailingDegree p * reverse q * X ^ natTrailingDegree q) =
    reverse p * X ^ natTrailingDegree p * (reverse q * X ^ natTrailingDegree q)
[PROOFSTEP]
repeat' rw [mul_assoc]
[GOAL]
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ reverse p * (X ^ natTrailingDegree p * reverse q * X ^ natTrailingDegree q) =
    reverse p * X ^ natTrailingDegree p * (reverse q * X ^ natTrailingDegree q)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ reverse p * (X ^ natTrailingDegree p * (reverse q * X ^ natTrailingDegree q)) =
    reverse p * X ^ natTrailingDegree p * (reverse q * X ^ natTrailingDegree q)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
a : R
⊢ mirror (a • p) = a • mirror p
[PROOFSTEP]
rw [← C_mul', ← C_mul', mirror_mul_of_domain, mirror_C]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
⊢ Irreducible f
[PROOFSTEP]
constructor
[GOAL]
case not_unit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
⊢ ¬IsUnit f
[PROOFSTEP]
exact h1
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
⊢ ∀ (a b : R[X]), f = a * b → IsUnit a ∨ IsUnit b
[PROOFSTEP]
intro g h fgh
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
let k := g * h.mirror
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
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]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
⊢ f * mirror f = k * mirror k
[PROOFSTEP]
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]
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
have g_dvd_f : g ∣ f := by
  rw [fgh]
  exact dvd_mul_right g h
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
⊢ g ∣ f
[PROOFSTEP]
rw [fgh]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
⊢ g ∣ g * h
[PROOFSTEP]
exact dvd_mul_right g h
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
have h_dvd_f : h ∣ f := by
  rw [fgh]
  exact dvd_mul_left h g
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
⊢ h ∣ f
[PROOFSTEP]
rw [fgh]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
⊢ h ∣ g * h
[PROOFSTEP]
exact dvd_mul_left h g
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
have g_dvd_k : g ∣ k := dvd_mul_right g h.mirror
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
have h_dvd_k_rev : h ∣ k.mirror := by
  rw [mirror_mul_of_domain, mirror_mirror]
  exact dvd_mul_left h g.mirror
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ h ∣ mirror k
[PROOFSTEP]
rw [mirror_mul_of_domain, mirror_mirror]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ h ∣ mirror g * h
[PROOFSTEP]
exact dvd_mul_left h g.mirror
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
have hk := h2 k key
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
rcases hk with (hk | hk | hk | hk)
[GOAL]
case isUnit_or_isUnit'.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = f
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
exact Or.inr (h3 h h_dvd_f (by rwa [← hk]))
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = f
⊢ h ∣ mirror f
[PROOFSTEP]
rwa [← hk]
[GOAL]
case isUnit_or_isUnit'.inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = -f
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
exact Or.inr (h3 h h_dvd_f (by rwa [← neg_eq_iff_eq_neg.mpr hk, mirror_neg, dvd_neg]))
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = -f
⊢ h ∣ mirror f
[PROOFSTEP]
rwa [← neg_eq_iff_eq_neg.mpr hk, mirror_neg, dvd_neg]
[GOAL]
case isUnit_or_isUnit'.inr.inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = mirror f
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
exact Or.inl (h3 g g_dvd_f (by rwa [← hk]))
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = mirror f
⊢ g ∣ mirror f
[PROOFSTEP]
rwa [← hk]
[GOAL]
case isUnit_or_isUnit'.inr.inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = -mirror f
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
exact Or.inl (h3 g g_dvd_f (by rwa [← neg_eq_iff_eq_neg.mpr hk, dvd_neg]))
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = -mirror f
⊢ g ∣ mirror f
[PROOFSTEP]
rwa [← neg_eq_iff_eq_neg.mpr hk, dvd_neg]
