## Stream: new members

### Topic: adding one inside a function

#### Alex Kontorovich (Apr 14 2020 at 20:53):

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 (Apr 14 2020 at 20:58):

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

#### Johan Commelin (Apr 14 2020 at 20:59):

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

#### Johan Commelin (Apr 14 2020 at 21:00):

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


Why suffices?

#### Patrick Massot (Apr 14 2020 at 21:01):

Don't you mean have?

#### Patrick Massot (Apr 14 2020 at 21:01):

And probably rw fg can replace the last two lines.

#### Patrick Massot (Apr 14 2020 at 21:02):

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

#### Patrick Massot (Apr 14 2020 at 21:03):

(But I can see comma haters coming)

#### Kenny Lau (Apr 14 2020 at 21:04):

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 (Apr 14 2020 at 21:05):

The new mathlib style is

by { rw fg, congr' 1, omega }


#### Kenny Lau (Apr 14 2020 at 21:05):

oh I didn't know that

#### Patrick Massot (Apr 14 2020 at 21:05):

Kenny cheated by moving k left of the colon

#### Patrick Massot (Apr 14 2020 at 21:06):

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

#### Kevin Buzzard (Apr 14 2020 at 22:43):

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 (Apr 14 2020 at 22:44):

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

Last updated: Dec 20 2023 at 11:08 UTC