case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
⊢ coeff (reflect N (↑C c * X ^ n)) n✝ = coeff (↑C c * X ^ ↑(revAt N) n) n✝
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
⊢ reflect N (↑C c * X ^ n) = ↑C c * X ^ ↑(revAt N) n
ext
case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
⊢ c * coeff (X ^ n) (↑(revAt N) n✝) = c * if n✝ = ↑(revAt N) n then 1 else 0
case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
⊢ coeff (reflect N (↑C c * X ^ n)) n✝ = coeff (↑C c * X ^ ↑(revAt N) n) n✝
rw [reflect_C_mul, coeff_C_mul, coeff_C_mul, coeff_X_pow, coeff_reflect]
case a.inl
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : n✝ = ↑(revAt N) n
⊢ c * coeff (X ^ n) (↑(revAt N) n✝) = c * 1

case a.inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = ↑(revAt N) n
⊢ c * coeff (X ^ n) (↑(revAt N) n✝) = c * 0
case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
⊢ c * coeff (X ^ n) (↑(revAt N) n✝) = c * if n✝ = ↑(revAt N) n then 1 else 0
split_ifs with h
no goals
case a.inl
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : n✝ = ↑(revAt N) n
⊢ c * coeff (X ^ n) (↑(revAt N) n✝) = c * 1
rw [h, revAt_invol, coeff_X_pow_self]
case a.inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = ↑(revAt N) n
⊢ ¬↑(revAt N) n✝ ∈ support (X ^ n)
case a.inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = ↑(revAt N) n
⊢ c * coeff (X ^ n) (↑(revAt N) n✝) = c * 0
rw [not_mem_support_iff.mp]
case a.inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = ↑(revAt N) n
a : ↑(revAt N) n✝ ∈ support (X ^ n)
⊢ False
case a.inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = ↑(revAt N) n
⊢ ¬↑(revAt N) n✝ ∈ support (X ^ n)
intro a
case a.inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = ↑(revAt N) n
a : ↑(revAt N) n✝ ∈ support (↑C 1 * X ^ n)
⊢ False
case a.inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = ↑(revAt N) n
a : ↑(revAt N) n✝ ∈ support (X ^ n)
⊢ False
rw [← one_mul (X ^ n), ← C_1] at a
case a.inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = ↑(revAt N) n
a : ↑(revAt N) n✝ ∈ support (↑C 1 * X ^ n)
⊢ n✝ = ↑(revAt N) n
case a.inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = ↑(revAt N) n
a : ↑(revAt N) n✝ ∈ support (↑C 1 * X ^ n)
⊢ False
apply h
no goals
case a.inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = ↑(revAt N) n
a : ↑(revAt N) n✝ ∈ support (↑C 1 * X ^ n)
⊢ n✝ = ↑(revAt N) n
rw [← mem_support_C_mul_X_pow a, revAt_invol]