-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem mirror_eval_one : p.mirror.eval 1 = p.eval 1

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ p.mirror.natTrailingDegree ≤ n

Tactic:
exact natTrailingDegree_le_of_ne_zero hp

Result:
no goals

Proof state:
case refine_3
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a₁ ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a₁ ≠ 0 →
      ∀ a₂ ∈ Finset.range (p.natDegree + 1),
        p.mirror.coeff a₂ ≠ 0 →
          (revAt (p.natDegree + p.natTrailingDegree)) a₁ = (revAt (p.natDegree + p.natTrailingDegree)) a₂ → a₁ = a₂

Tactic:
exact fun n₁ _ _ _ _ _ h => by rw [← @revAt_invol _ n₁, h, revAt_invol]

Result:
no goals

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.mirror.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ∈ Finset.range (p.natDegree + 1)

Tactic:
rw [Finset.mem_range_succ_iff] at *

Result:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ≤ p.natDegree

Proof state:
case h.refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n) ≠ 0

Tactic:
rwa [coeff_mirror, revAt_invol]

Result:
no goals

Proof state:
case refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (a : ℕ) → a ∈ Finset.range (p.natDegree + 1) → p.mirror.coeff a ≠ 0 → ℕ

Tactic:
exact fun n _ _ => revAt (p.natDegree + p.natTrailingDegree) n

Result:
no goals

Proof state:
case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ b ∈ Finset.range (p.natDegree + 1),
    p.coeff b ≠ 0 →
      ∃ a,
        ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
          (revAt (p.natDegree + p.natTrailingDegree)) a = b

Tactic:
intro n hn hp

Result:
case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ ∃ a,
    ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
      (revAt (p.natDegree + p.natTrailingDegree)) a = n

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ≤ p.natDegree

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

Result:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ p.natDegree + p.natTrailingDegree - n ≤ p.natDegree

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ ∃ (_ : (revAt (p.natDegree + p.natTrailingDegree)) n ∈ Finset.range (p.natDegree + 1)) (_ :
    p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n) ≠ 0),
    (revAt (p.natDegree + p.natTrailingDegree)) ((revAt (p.natDegree + p.natTrailingDegree)) n) = n

Tactic:
refine ⟨?_, ?_, revAt_invol⟩

Result:
case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ∈ Finset.range (p.natDegree + 1)

case h.refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n) ≠ 0

Proof state:
case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ≤ p.natDegree

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

Result:
case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natDegree + p.natTrailingDegree - n ≤ p.natDegree

Proof state:
case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natDegree + p.natTrailingDegree - n ≤ p.natDegree

Tactic:
rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right]

Result:
case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natTrailingDegree ≤ n

Proof state:
case refine_5
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → p.mirror.coeff a = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) a)

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

Result:
no goals

Proof state:
case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ∈ Finset.range (p.natDegree + 1)

Tactic:
rw [Finset.mem_range_succ_iff] at *

Result:
case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ≤ p.natDegree

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → (revAt (p.natDegree + p.natTrailingDegree)) a ∈ Finset.range (p.natDegree + 1)

Tactic:
intro n hn hp

Result:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.mirror.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ∈ Finset.range (p.natDegree + 1)

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ p.natDegree + p.natTrailingDegree - n ≤ p.natDegree

Tactic:
rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right, ← mirror_natTrailingDegree]

Result:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ p.mirror.natTrailingDegree ≤ n

Proof state:
case h.refine_1
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

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ eval 1 p.mirror = eval 1 p

Tactic:
simp_rw [eval_eq_sum_range, one_pow, mul_one, mirror_natDegree]

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ x ∈ Finset.range (p.natDegree + 1), p.mirror.coeff x = ∑ x ∈ Finset.range (p.natDegree + 1), p.coeff x

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ x ∈ Finset.range (p.natDegree + 1), p.mirror.coeff x = ∑ x ∈ Finset.range (p.natDegree + 1), p.coeff x

Tactic:
refine Finset.sum_bij_ne_zero ?_ ?_ ?_ ?_ ?_

Result:
case refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (a : ℕ) → a ∈ Finset.range (p.natDegree + 1) → p.mirror.coeff a ≠ 0 → ℕ

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

case refine_3
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ (a₁ : ℕ) (h₁₁ : a₁ ∈ Finset.range (p.natDegree + 1)) (h₁₂ : p.mirror.coeff a₁ ≠ 0) (a₂ : ℕ)
    (h₂₁ : a₂ ∈ Finset.range (p.natDegree + 1)) (h₂₂ : p.mirror.coeff 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 : R[X]
⊢ ∀ b ∈ Finset.range (p.natDegree + 1),
    p.coeff b ≠ 0 → ∃ a, ∃ (h₁ : a ∈ Finset.range (p.natDegree + 1)) (h₂ : p.mirror.coeff a ≠ 0), ?refine_1 a h₁ h₂ = b

case refine_5
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 (?refine_1 a h₁ h₂)