import MyNat.Definition
import MyNat.Addition
import AdditionWorld.Level6
import AdvancedAdditionWorld.Level1 -- succ_inj
import AdvancedAdditionWorld.Level3 -- succ_eq_succ_of_eq
namespace MyNat
open MyNat

Advanced Addition World

Level 4: eq_iff_succ_eq_succ

Here is an iff goal. You can split it into two goals (the implications in both directions) using the constructor tactic, which is how you're going to have to start.

constructor

Now you have two goals. The first is exactly succ_inj so you can close it with

exact succ_inj

and the second one you could solve by looking up the name of the theorem you proved in the last level and doing exact <that name>, or alternatively you could get some more intro practice and seeing if you can prove it using intro and rw.

Remember that succ_inj is succ a = succ b → a = b.

Theorem

Two natural numbers are equal if and only if their successors are equal.

theorem 
succ_eq_succ_iff: ∀ (a b : MyNat), succ a = succ b ↔ a = b
succ_eq_succ_iff (
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat) : 
succ: MyNat → MyNat
succ 
a: MyNat
a = 
succ: MyNat → MyNat
succ 
b: MyNat
b ↔ 
a: MyNat
a = 
b: MyNat
b := by
a, b: MyNat
succ a = succ b ↔ a = b
  constructor
a, b: MyNat
mp
succ a = succ b → a = b
a, b: MyNat
mpr
a = b → succ a = succ b
  exact 
succ_inj: ∀ {a b : MyNat}, succ a = succ b → a = b
succ_inj
a, b: MyNat
mpr
a = b → succ a = succ b
  exact 
succ_eq_succ_of_eq: ∀ {a b : MyNat}, a = b → succ a = succ b
succ_eq_succ_of_eq
Goals accomplished! 🐙

Next up Level 5