import MyNat.Definition
import MultiplicationWorld.Level1 -- zero_mul
import AdvancedMultiplicationWorld.Level2 -- eq_zero_or_eq_zero_of_mul_eq_zero
import Mathlib.Tactic.LeftRight
namespace MyNat
open MyNat

Advanced Multiplication World

Level 3: mul_eq_zero_iff

Now you have eq_zero_or_eq_zero_of_mul_eq_zero this is pretty straightforward.

Theorem

ab = 0, if and only if at least one of a or b is equal to zero.

theorem 
mul_eq_zero_iff: ∀ (a b : MyNat), a * b = 0 ↔ a = 0 ∨ b = 0
mul_eq_zero_iff (
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat): 
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
a * b = 0 ↔ a = 0 ∨ b = 0
  constructor
a, b: MyNat
mp
a * b = 0 → a = 0 ∨ b = 0
a, b: MyNat
mpr
a = 0 ∨ b = 0 → a * b = 0
  {
a, b: MyNat
mp
a * b = 0 → a = 0 ∨ b = 0
     intro 
h: a * b = 0
h
a, b: MyNat
h: a * b = 0
mp
a = 0 ∨ b = 0
     exact 
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 
h: a * b = 0
h
Goals accomplished! 🐙
  }
a, b: MyNat
mpr
a = 0 ∨ b = 0 → a * b = 0
  {
a, b: MyNat
mpr
a = 0 ∨ b = 0 → a * b = 0
    intro 
hab: a = 0 ∨ b = 0
hab
a, b: MyNat
hab: a = 0 ∨ b = 0
mpr
a * b = 0
    cases 
hab: a = 0 ∨ b = 0
hab with
a, b: MyNat
hab: a = 0 ∨ b = 0
mpr
a * b = 0
    | 
inl: ∀ {a b : Prop}, a → a ∨ b
inl 
ha: a = 0
ha =>
a, b: MyNat
ha: a = 0
mpr.inl
a * b = 0
      rw [
a, b: MyNat
ha: a = 0
mpr.inl
a * b = 0
ha: a = 0
ha
a, b: MyNat
ha: a = 0
mpr.inl
0 * b = 0]
a, b: MyNat
ha: a = 0
mpr.inl
0 * b = 0
      rw [
a, b: MyNat
ha: a = 0
mpr.inl
0 * b = 0
zero_mul: ∀ (m : MyNat), 0 * m = 0
zero_mul
a, b: MyNat
ha: a = 0
mpr.inl
0 = 0]
Goals accomplished! 🐙
    | 
inr: ∀ {a b : Prop}, b → a ∨ b
inr 
hb: b = 0
hb =>
a, b: MyNat
hb: b = 0
mpr.inr
a * b = 0
      rw [
a, b: MyNat
hb: b = 0
mpr.inr
a * b = 0
hb: b = 0
hb
a, b: MyNat
hb: b = 0
mpr.inr
a * 0 = 0]
a, b: MyNat
hb: b = 0
mpr.inr
a * 0 = 0
      rw [
a, b: MyNat
hb: b = 0
mpr.inr
a * 0 = 0
mul_zero: ∀ (a : MyNat), a * 0 = 0
mul_zero
a, b: MyNat
hb: b = 0
mpr.inr
0 = 0]
Goals accomplished! 🐙
  }
Goals accomplished! 🐙

Next up Level 4