Natural number game 4/8

Stream: new members

[Moti Ben-Ari]

Game 4/8 is to prove

theorem le_trans (x y z : ℕ) (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z

I almost solved it and then looked up @Anand Dyavanapalli solution which is

cases hab with k₁ h₁,
cases hbc with k₂ h₂,
rw h₂,
rw h₁,
use (k₁ + k₂),
rw add_assoc a k₁ k₂,
refl,

Translated to NNG this is

cases hxy with a ha
cases hyz with b hb
rw [hb]
rw [ha]
rw [add_assoc x a b]

The resulting goal is

x ≤ x + (a + b)

but nothing in NNG seems relevant. What is refl is equivalent to in NNG?

[Kevin Buzzard]

rfl?

[Kevin Buzzard]

But that won't prove the goal you post, although if you've got this far you should know how to take it from here. Note that you have skipped a use line in the lean 3 solution.

[Kevin Buzzard]

PS you can look up any solution to the lean 4 game by just looking at the github repository for the game.

[Moti Ben-Ari]

Thanks @Kevin Buzzard . It's obvious when you look up the answer ...

[Kevin Buzzard]

Yeah that's what I said when I read the proof of Fermat's Last Theorem. That's how maths works :-) (except I never finished the harmonic analysis part)