神秘化简问题, 仅仅是移项甚至只是对调了一下不等式的方向就不行了.
原问题是在一定条件下化简一个复杂的不等式, 预期结果是true或false, 没有达到预期结果, 结果是part1 > part2, 找不出原因的情况下, 我尝试直接化简part1 > part2, 并且将part1 > part2稍微变形或原样添加进assum, 也就是assum的第二部分.
原样添加进assum的时候, 可以得到true, 说明Simplify能够这样工作.
前两行的Simplify[expr,assum]的assum的第二部分是part1 > part2经过稍微简单移项得到的, 最后一行甚至只对调了不等式方向, 变成part2 < part1, 完全没有移项, 也得不出结果.
part1 = Sr t1 + a (1 + t1 + \[Gamma]);
part2 = c + t1 + a Sr t1 + \[Gamma] + a \[Lambda];
Simplify[
part1 > part2, {0 < a < 1,
c < (Sr t1 + a (1 + t1 + \[Gamma])) - (t1 + a Sr t1 + \[Gamma] +
a \[Lambda]), 0 < \[Lambda] < 1, t1 > 0, 1 > \[Gamma] > 0,
0 < Sr < 1}]
Simplify[
part1 > part2, {0 < a < 1,
a (1 + t1 + \[Gamma]) >
c + t1 + a Sr t1 + \[Gamma] + a \[Lambda] - Sr t1,
0 < \[Lambda] < 1, t1 > 0, 1 > \[Gamma] > 0, 0 < Sr < 1}]
Simplify[
part1 > part2, {0 < a < 1, part1 > part2, 0 < \[Lambda] < 1, t1 > 0,
1 > \[Gamma] > 0, 0 < Sr < 1}]
Simplify[
part1 > part2, {0 < a < 1, part2 < part1, 0 < \[Lambda] < 1, t1 > 0,
1 > \[Gamma] > 0, 0 < Sr < 1}]

https://www.wolframcloud.com/obj/97fd3116-0d9c-44ad-8f1b-b59dcaea2558

我个人的感觉是，以复杂的符号等式/不等式为假设的，基于Simplify（和它愉快的伙伴们）的化简，一直都不是太稳定（大致是个“有时候能行”的状态），相对而言，Reduce之类的函数表现相对而言会好很多：
Reduce[ForAll[{a, t1, γ, c, Sr, λ}, {0 < a < 1,
a (1 + t1 + γ) >
c + t1 + a Sr t1 + γ + a λ - Sr t1,
0 < λ < 1, t1 > 0, 1 > γ > 0, 0 < Sr < 1},
part1 > part2]]
Resolve[ForAll[{a, t1, γ, c, Sr, λ}, {0 < a < 1,
a (1 + t1 + γ) >
c + t1 + a Sr t1 + γ + a λ - Sr t1,
0 < λ < 1, t1 > 0, 1 > γ > 0, 0 < Sr < 1},
part1 > part2]]