import MyNat.Definition
import AdditionWorld.Level4 -- add_comm
import AdvancedAdditionWorld.Level5 -- add_right_cancel
namespace MyNat
open MyNat

Advanced Addition World

Level 7: add_right_cancel_iff

It's sometimes convenient to have the "if and only if" version of theorems like add_right_cancel. Remember that you can use constructor to split an ↔ goal into the → goal and the ← goal.

Pro tip:

Notice exact add_right_cancel _ _ _ means "let Lean figure out the missing inputs" so we don't have to spell it out like we did in Level 6.

Theorem

For all naturals a, b and t, a + t = b + t ↔ a = b.

theorem 
add_right_cancel_iff: ∀ (t a b : MyNat), a + t = b + t ↔ a = b
add_right_cancel_iff (
t: MyNat
t 
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat) :  
a: MyNat
a + 
t: MyNat
t = 
b: MyNat
b + 
t: MyNat
t ↔ 
a: MyNat
a = 
b: MyNat
b := by
t, a, b: MyNat
a + t = b + t ↔ a = b
  constructor
t, a, b: MyNat
mp
a + t = b + t → a = b
t, a, b: MyNat
mpr
a = b → a + t = b + t
  exact 
add_right_cancel: ∀ (a t b : MyNat), a + t = b + t → a = b
add_right_cancel 
_: MyNat
_ 
_: MyNat
_ 
_: MyNat
_
t, a, b: MyNat
mpr
a = b → a + t = b + t
  intro 
h: a = b
h
t, a, b: MyNat
h: a = b
mpr
a + t = b + t
  rw [
t, a, b: MyNat
h: a = b
mpr
a + t = b + t
h: a = b
h
t, a, b: MyNat
h: a = b
mpr
b + t = b + t]
Goals accomplished! 🐙

Next up Level 8