import MyNat.Definition
import MyNat.Inequality -- le_iff_exists_add
import Mathlib.Tactic.Use -- use tactic
import AdditionWorld.Level6 -- add_right_comm
namespace MyNat
open MyNat

Inequality world.

Level 11: add_le_add_right

If you're faced with a goal of the form forall t, ..., then the next line is "so let t be arbitrary". The way to do this in Lean is intro t.

Lemma : add_le_add_right

For all naturals a and b, a ≤ b implies that for all naturals t, a+t ≤ b+t.

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

Next up Level 12