adding one inside a function

Stream: new members

[Alex Kontorovich]

More noob questions. Please help to make this work? (tried library_search, simp, hint, cc, suggest...) Thank you!

lemma z (F:ℕ→ℝ)(G:ℕ→ℝ) (i:ℕ) (fg: ∀ k, G(k)= F (k+i))
: ∀ k, (F(k + nat.succ i)= G (k+1))
:=
begin
    intros k,
    sorry,
end,

[Johan Commelin]

Try symmetry and then convert fg (k+1) using 1

[Johan Commelin]

Or maybe better symmetry, rw show k + nat.succ i = (k+1) + i,

[Johan Commelin]

suffices : k + nat.succ i = (k+1) + i,
{ sorry },
rw this,
symmetry,
apply fg

[Patrick Massot]

Why suffices?

[Patrick Massot]

Don't you mean have?

[Patrick Massot]

And probably rw fg can replace the last two lines.

[Patrick Massot]

I say λ k, by rw [show k + nat.succ i = (k+1) + i, by ring, fg]

[Patrick Massot]

(But I can see comma haters coming)

[Kenny Lau]

import tactic data.real.basic

lemma z (F : ℕ → ℝ) (G : ℕ → ℝ) (i : ℕ) (fg : ∀ k, G k = F (k+i)) (k : ℕ) :
  F (k + nat.succ i) = G (k + 1) :=
by rw fg; congr' 1; omega

[Sebastien Gouezel]

The new mathlib style is

by { rw fg, congr' 1, omega }

[Kenny Lau]

oh I didn't know that

[Patrick Massot]

Kenny cheated by moving k left of the colon

[Patrick Massot]

And ring is shorter than omega, I'm very disappointed by Kenny's golf.

[Kevin Buzzard]

That's great to hear that that's the new mathlib style, I had independently come up with it, I know it costs some extra bytes with the brackets but it was getting silly with all the semicolons

[Reid Barton]

At least they're not some unicode brackets, so they only cost 1 byte each.