le_sub_iff_add_le error

Stream: new members

[Calle Sönne]

I have following code, which gives an error on the last line:

lemma limit_start_irrelevant (a : ℕ → ℝ) (k : ℕ) (l : ℝ) (h : M1P1.is_limit (λ n, a (n+k)) l) : M1P1.is_limit a l :=
begin
intros ε Hε, cases h ε Hε with N H, use N + k, intros n Hn, simp only at H, rw ←le_sub_iff_add_le N k n at Hn,
end

Tactic state:

function expected at
  le_sub_iff_add_le
term has type
  ?m_3 ≤ ?m_4 - ?m_5 ↔ ?m_3 + ?m_5 ≤ ?m_4
state:
a : ℕ → ℝ,
k : ℕ,
l : ℝ,
h : M1P1.is_limit (λ (n : ℕ), a (n + k)) l,
ε : ℝ,
Hε : ε > 0,
N n : ℕ,
Hn : n ≥ N + k,
H : ∀ (n : ℕ), n ≥ N → |a (n + k) - l| < ε
⊢ |a n - l| < ε

I can't seem to figure out what the problem is, subtracting naturals is fishy but lean seems to be complaining about something else. Any help would be appreciated :)

[Mario Carneiro]

you wrote le_sub_iff_add_le N k n but it takes no explicit arguments

[Calle Sönne]

Right, without arguments I get this error:

rewrite tactic failed, did not find instance of the pattern in the target expression
  _ ≤ ?m_5
state:
a : ℕ → ℝ,
k : ℕ,
l : ℝ,
h : M1P1.is_limit (λ (n : ℕ), a (n + k)) l,
ε : ℝ,
Hε : ε > 0,
N n : ℕ,
Hn : n ≥ N + k,
H : ∀ (n : ℕ), n ≥ N → |a (n + k) - l| < ε
⊢ |a n - l| < ε

Do I need to "flip" the inequality? I thought both sides were treated as equal.

[Kenny Lau]

try erw

[Mario Carneiro]

try rw ge at Hn?

[Kenny Lau]

wait I know why

[Kenny Lau]

you're dealing with natural numbers.

[Kenny Lau]

:face_palm:

[Mario Carneiro]

There are similar theorems explicitly for nat

[Mario Carneiro]

you can't use the general theorem

[Kenny Lau]

but it still won't match the le with ge I guess

[Kenny Lau]

so you need to use erw or replace Hn := _

[Mario Carneiro]

I think you want replace Hn := nat.le_sub_right_of_add_le Hn

[Calle Sönne]

that worked. Thank you :)