import MyNat.Definition
import MyNat.Addition -- add_succ
import MyNat.Multiplication -- mul_succ
import AdvancedAdditionWorld.Level9 -- succ_ne_zero
import Mathlib.Tactic.LeftRight
namespace MyNat
open MyNat

Advanced Multiplication World

Level 2: eq_zero_or_eq_zero_of_mul_eq_zero

A variant on the previous level.

Theorem

If ab = 0, then at least one of a or b is equal to zero.

theorem 
eq_zero_or_eq_zero_of_mul_eq_zero: ∀ (a b : MyNat), a * b = 0 → a = 0 ∨ b = 0
eq_zero_or_eq_zero_of_mul_eq_zero (
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat) (
h: a * b = 0
h : 
a: MyNat
a * 
b: MyNat
b = 
0: MyNat
0) :
  
a: MyNat
a = 
0: MyNat
0 ∨ 
b: MyNat
b = 
0: MyNat
0 := by
a, b: MyNat
h: a * b = 0
a = 0 ∨ b = 0
  cases 
a: MyNat
a with
a, b: MyNat
h: a * b = 0
a = 0 ∨ b = 0
  | 
zero: MyNat
zero =>
b: MyNat
h: zero * b = 0
zero
zero = 0 ∨ b = 0
    left
b: MyNat
h: zero * b = 0
zero.h
zero = 0
    rfl
Goals accomplished! 🐙
  | 
succ: MyNat → MyNat
succ 
a': MyNat
a' =>
b, a': MyNat
h: succ a' * b = 0
succ
succ a' = 0 ∨ b = 0
    cases 
b: MyNat
b with
b, a': MyNat
h: succ a' * b = 0
succ
succ a' = 0 ∨ b = 0
    | 
zero: MyNat
zero =>
a': MyNat
h: succ a' * zero = 0
succ.zero
succ a' = 0 ∨ zero = 0
      right
a': MyNat
h: succ a' * zero = 0
succ.zero.h
zero = 0
      rfl
Goals accomplished! 🐙
    | 
succ: MyNat → MyNat
succ 
b': MyNat
b' =>
a', b': MyNat
h: succ a' * succ b' = 0
succ.succ
succ a' = 0 ∨ succ b' = 0
      exfalso
a', b': MyNat
h: succ a' * succ b' = 0
succ.succ.h
False
      rw [
a', b': MyNat
h: succ a' * succ b' = 0
succ.succ.h
False
mul_succ: ∀ (a b : MyNat), a * succ b = a * b + a
mul_succ
a', b': MyNat
h: succ a' * b' + succ a' = 0
succ.succ.h
False]
a', b': MyNat
h: succ a' * b' + succ a' = 0
succ.succ.h
False at 
h: succ a' * succ b' = 0
h
a', b': MyNat
h: succ a' * b' + succ a' = 0
succ.succ.h
False
      rw [
a', b': MyNat
h: succ a' * b' + succ a' = 0
succ.succ.h
False
add_succ: ∀ (a d : MyNat), a + succ d = succ (a + d)
add_succ
a', b': MyNat
h: succ (succ a' * b' + a') = 0
succ.succ.h
False]
a', b': MyNat
h: succ (succ a' * b' + a') = 0
succ.succ.h
False at 
h: succ a' * b' + succ a' = 0
h
a', b': MyNat
h: succ (succ a' * b' + a') = 0
succ.succ.h
False
      exact 
succ_ne_zero: ∀ (a : MyNat), succ a ≠ 0
succ_ne_zero 
_: MyNat
_ 
h: succ (succ a' * b' + a') = 0
h
Goals accomplished! 🐙

Next up Level 3