R : Type ?u.164
inst✝ : Semiring R
f : R[X]
N i : ℕ
⊢ (if (if i ≤ N then N - i else i) ≤ N then N - if i ≤ N then N - i else i else if i ≤ N then N - i else i) = i
R : Type ?u.164
inst✝ : Semiring R
f : R[X]
N i : ℕ
⊢ revAtFun N (revAtFun N i) = i
unfold revAtFun
case inl.inl
R : Type ?u.164
inst✝ : Semiring R
f : R[X]
N i : ℕ
h : i ≤ N
j : N - i ≤ N
⊢ N - (N - i) = i

case inl.inr
R : Type ?u.164
inst✝ : Semiring R
f : R[X]
N i : ℕ
h : i ≤ N
j : ¬N - i ≤ N
⊢ N - i = i

case inr
R : Type ?u.164
inst✝ : Semiring R
f : R[X]
N i : ℕ
h : ¬i ≤ N
⊢ i = i
R : Type ?u.164
inst✝ : Semiring R
f : R[X]
N i : ℕ
⊢ (if (if i ≤ N then N - i else i) ≤ N then N - if i ≤ N then N - i else i else if i ≤ N then N - i else i) = i
split_ifs with h j
no goals
case inl.inl
R : Type ?u.164
inst✝ : Semiring R
f : R[X]
N i : ℕ
h : i ≤ N
j : N - i ≤ N
⊢ N - (N - i) = i
exact tsub_tsub_cancel_of_le h
case inl.inr.h
R : Type ?u.164
inst✝ : Semiring R
f : R[X]
N i : ℕ
h : i ≤ N
j : ¬N - i ≤ N
⊢ False
case inl.inr
R : Type ?u.164
inst✝ : Semiring R
f : R[X]
N i : ℕ
h : i ≤ N
j : ¬N - i ≤ N
⊢ N - i = i
exfalso
case inl.inr.h
R : Type ?u.164
inst✝ : Semiring R
f : R[X]
N i : ℕ
h : i ≤ N
j : ¬N - i ≤ N
⊢ N - i ≤ N
case inl.inr.h
R : Type ?u.164
inst✝ : Semiring R
f : R[X]
N i : ℕ
h : i ≤ N
j : ¬N - i ≤ N
⊢ False
apply j
no goals
case inl.inr.h
R : Type ?u.164
inst✝ : Semiring R
f : R[X]
N i : ℕ
h : i ≤ N
j : ¬N - i ≤ N
⊢ N - i ≤ N
exact Nat.sub_le N i
no goals
case inr
R : Type ?u.164
inst✝ : Semiring R
f : R[X]
N i : ℕ
h : ¬i ≤ N
⊢ i = i
rfl