import MyNat.Definition
import MyNat.Inequality -- le_iff_exists_add
import Mathlib.Tactic.Use -- use tactic
import AdditionWorld.Level4 -- add_comm
namespace MyNat
open MyNat

Inequality world.

Level 3: le_succ_of_le

We have seen how the use tactic makes progress on goals of the form ⊢ ∃ c, .... But what do we do when we have a hypothesis of the form h : ∃ c, ...? The hypothesis claims that there exists some natural number c with some property. How are we going to get to that natural number c? It turns out that the cases tactic can be used (just like it was used to extract information from ∧ and ∨ and ↔ hypotheses). Let me talk you through the proof of a ≤ b ⟹ a ≤ succ b.

The goal is an implication so we clearly want to start with

intro h

After this, if you want, you can do something like

rw [le_iff_exists_add] at h ⊢

(get the sideways T with \|- or \goal then space). This rw changes the ≤ into its ∃ form in h and the goal -- but if you are happy with just imagining the ∃ whenever you read a ≤ then you don't need to do this line.

Our hypothesis h is now ∃ (c : MyNat), b = a + c (or a ≤ b if you elected not to do the definitional rewriting) so

cases h with | _ c hc => ..

gives you the natural number c and the hypothesis hc : b = a + c. Now use use wisely and you're home.

Lemma : le_succ

For all naturals a, b, if a ≤ b then a ≤ succ b.

theorem 
le_succ: ∀ (a b : MyNat), a ≤ b → a ≤ succ b
le_succ (
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat) : 
a: MyNat
a ≤ 
b: MyNat
b → 
a: MyNat
a ≤ (
succ: MyNat → MyNat
succ 
b: MyNat
b) := by
a, b: MyNat
a ≤ b → a ≤ succ b
  intro 
h: a ≤ b
h
a, b: MyNat
h: a ≤ b
a ≤ succ b
  cases 
h: a ≤ b
h with
a, b: MyNat
h: a ≤ b
a ≤ succ b
  | 
_: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ 
c: MyNat
c 
hc: b = a + c
hc => -- a = 0, b = 0
a, b, c: MyNat
hc: b = a + c
intro
a ≤ succ b
    rw [
a, b, c: MyNat
hc: b = a + c
intro
a ≤ succ b
hc: b = a + c
hc
a, b, c: MyNat
hc: b = a + c
intro
a ≤ succ (a + c)]
a, b, c: MyNat
hc: b = a + c
intro
a ≤ succ (a + c)
    use 
c: MyNat
c + 
1: MyNat
1
Goals accomplished! 🐙

You can use succ c or c + 1 or 1 + c. Those numbers are all equal, right? Try these variations and see what happens.

Now what about if you do use 1 + c? Can you work out what is going on? Does it help if I tell you that the definition of 1 is succ 0?

Next up Level 4