In the following, the rewrite fails because it "did not find instance of the pattern in the target expression":
example (l1:List Nat)(l2:List Nat)(n:Nat)(r:l1.length >= n)(p:l1.length = l2.length+1) : l2.length >= (n-1) :=
by
rw [Nat.sub_le_iff_le_add]
I'm confused why it doesn't bind given that the goal seems to be a perfect fit. (note: this is a simplified version of something larger, and I'm not interested in how to restate the example only in why rw fails).
After time wasted searching for a more suitable theorem, I ended up writing my own (which does work):
def Nat.succ_ge {m:Nat}{n:Nat} (h:m+1 >= n) : (n-1 <= m) :=
by
rw [Nat.sub_le_iff_le_add]
exact h
example (l1:List Nat)(l2:List Nat)(n:Nat)(r:l1.length >= n)(p:l1.length = l2.length+1) : l2.length >= (n-1) :=
by
apply Nat.succ_ge;
rw [p] at r
exact r
I find it strange since it just uses the original sub_le_iff_le_add theorem! I just don't understand why I can't apply it directly?
The problem is that rw is stumped by the difference between ≥ and ≤.
This is the reason that in Mathlib we always try writing things in terms of ≤.
One workaround is:
example {l1 l2 : List Nat} (r : l1.length ≥ n) (p : l1.length = l2.length + 1) : l2.length ≥ (n-1) := by
change _ ≤ _
rw [Nat.sub_le_iff_le_add]
sorry -- rest of proof