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)

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)
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ coeff (mirror p) n = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) n)
by_cases h2 : p.natDegree < n
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)
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)
rw [not_lt] at h2
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)
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)
rw [revAt_le (h2.trans (Nat.le_add_right _ _))]
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)

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)
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)
by_cases h3 : p.natTrailingDegree ≤ n
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)
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)
rw [not_le] at h3
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
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)
rw [coeff_eq_zero_of_natDegree_lt (lt_tsub_iff_right.mpr (Nat.add_lt_add_left h3 _))]
no goals
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
exact coeff_eq_zero_of_lt_natTrailingDegree (by rwa [mirror_natTrailingDegree])
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)
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)
rw [coeff_eq_zero_of_natDegree_lt (by rwa [mirror_natDegree])]
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)

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)
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)
by_cases h1 : n ≤ p.natDegree + p.natTrailingDegree
no goals
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : natDegree p < n
⊢ natDegree (mirror p) < n
rwa [mirror_natDegree]
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
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)
rw [revAt_le h1, coeff_eq_zero_of_lt_natTrailingDegree]
no goals
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
exact (tsub_lt_iff_left h1).mpr (Nat.add_lt_add_right h2 _)
no goals
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)
rw [← revAtFun_eq, revAtFun, if_neg h1, coeff_eq_zero_of_natDegree_lt h2]
no goals
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)
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)]
no goals
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : n ≤ natDegree p
h3 : n < natTrailingDegree p
⊢ n < natTrailingDegree (mirror p)
rwa [mirror_natTrailingDegree]