case intro
R : Type ?u.51822
inst✝ : Semiring R
f : R[X]
O n o : ℕ
ho : o ≤ O
n' : ℕ
hn : n ≤ n + n'
⊢ ↑(revAt (n + n' + O)) (n + o) = ↑(revAt (n + n')) n + ↑(revAt O) o
R : Type ?u.51822
inst✝ : Semiring R
f : R[X]
N O n o : ℕ
hn : n ≤ N
ho : o ≤ O
⊢ ↑(revAt (N + O)) (n + o) = ↑(revAt N) n + ↑(revAt O) o
rcases Nat.le.dest hn with ⟨n', rfl⟩
case intro.intro
R : Type ?u.51822
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ ↑(revAt (n + n' + (o + o'))) (n + o) = ↑(revAt (n + n')) n + ↑(revAt (o + o')) o
case intro
R : Type ?u.51822
inst✝ : Semiring R
f : R[X]
O n o : ℕ
ho : o ≤ O
n' : ℕ
hn : n ≤ n + n'
⊢ ↑(revAt (n + n' + O)) (n + o) = ↑(revAt (n + n')) n + ↑(revAt O) o
rcases Nat.le.dest ho with ⟨o', rfl⟩
case intro.intro
R : Type ?u.51822
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ ↑(revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)
case intro.intro
R : Type ?u.51822
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ ↑(revAt (n + n' + (o + o'))) (n + o) = ↑(revAt (n + n')) n + ↑(revAt (o + o')) o
repeat' rw [revAt_le (le_add_right rfl.le)]
case intro.intro
R : Type ?u.51822
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)
case intro.intro
R : Type ?u.51822
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ ↑(revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)
rw [add_assoc, add_left_comm n' o, ← add_assoc, revAt_le (le_add_right rfl.le)]
no goals
case intro.intro
R : Type ?u.51822
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)
repeat' rw [add_tsub_cancel_left]
case intro.intro
R : Type ?u.51822
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ ↑(revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)
case intro.intro
R : Type ?u.51822
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ ↑(revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)
rw [revAt_le (le_add_right rfl.le)]
no goals
case intro.intro
R : Type ?u.51822
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n' + o' = n' + (o + o' - o)
rw [add_tsub_cancel_left]