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
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ eval 1 (mirror p) = eval 1 p
simp_rw [eval_eq_sum_range, one_pow, mul_one, mirror_natDegree]
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 → ℕ

case refine'_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (a : ℕ) (h₁ : a ∈ Finset.range (natDegree p + 1)) (h₂ : coeff (mirror p) a ≠ 0),
    ?refine'_1 a h₁ h₂ ∈ Finset.range (natDegree p + 1)

case refine'_3
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (a₁ a₂ : ℕ) (h₁₁ : a₁ ∈ Finset.range (natDegree p + 1)) (h₁₂ : coeff (mirror p) a₁ ≠ 0)
    (h₂₁ : a₂ ∈ Finset.range (natDegree p + 1)) (h₂₂ : coeff (mirror p) a₂ ≠ 0),
    ?refine'_1 a₁ h₁₁ h₁₂ = ?refine'_1 a₂ h₂₁ h₂₂ → a₁ = a₂

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 = ?refine'_1 a h₁ h₂

case refine'_5
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (a : ℕ) (h₁ : a ∈ Finset.range (natDegree p + 1)) (h₂ : coeff (mirror p) a ≠ 0),
    coeff (mirror p) a = coeff p (?refine'_1 a h₁ h₂)
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
refine' Finset.sum_bij_ne_zero _ _ _ _ _
no goals
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 → ℕ
exact fun n _ _ => revAt (p.natDegree + p.natTrailingDegree) n
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)
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)
intro n hn hp
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
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)
rw [Finset.mem_range_succ_iff] at *
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
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
rw [revAt_le (hn.trans (Nat.le_add_right _ _))]
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
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
rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right, ← mirror_natTrailingDegree]
no goals
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
exact natTrailingDegree_le_of_ne_zero hp
no goals
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₂
exact fun n₁ n₂ _ _ _ _ h => by rw [← @revAt_invol _ n₁, h, revAt_invol]
no goals
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₂
rw [← @revAt_invol _ n₁, h, revAt_invol]
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
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
intro n hn hp
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
⊢ ∃ h₁ h₂, n = ↑(revAt (natDegree p + natTrailingDegree p)) (↑(revAt (natDegree p + natTrailingDegree p)) n)
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
use revAt (p.natDegree + p.natTrailingDegree) n
case refine'_4.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)

case refine'_4.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
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
⊢ ∃ h₁ h₂, n = ↑(revAt (natDegree p + natTrailingDegree p)) (↑(revAt (natDegree p + natTrailingDegree p)) n)
refine' ⟨_, _, revAt_invol.symm⟩
case refine'_4.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
case refine'_4.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)
rw [Finset.mem_range_succ_iff] at *
case refine'_4.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
case refine'_4.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
rw [revAt_le (hn.trans (Nat.le_add_right _ _))]
case refine'_4.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
case refine'_4.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
rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right]
no goals
case refine'_4.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
exact natTrailingDegree_le_of_ne_zero hp
case refine'_4.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
case refine'_4.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
change p.mirror.coeff _ ≠ 0
no goals
case refine'_4.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
rwa [coeff_mirror, revAt_invol]
no goals
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)
exact fun n _ _ => p.coeff_mirror n