Open paulch42 opened 1 year ago
The following proof works (only change is in the last few lines):
theorem mul_left_cancel (a b c : MyNat) (ha : a ≠ 0) : a * b = a * c → b = c := by
induction c generalizing b with
| zero =>
rw [zero_is_0]
rw [mul_zero]
intro h
cases (eq_zero_or_eq_zero_of_mul_eq_zero _ _ h) with
| inl h1 =>
exfalso
apply ha
assumption
| inr h2 =>
assumption
| succ d hd =>
intro hb
cases b with
| zero =>
rw [zero_is_0] at hb
rw [mul_zero] at hb
rw [zero_is_0]
exfalso
apply ha
have hb := hb.symm
cases (eq_zero_or_eq_zero_of_mul_eq_zero _ _ hb) with
| inl h =>
exact h
| inr h =>
exfalso
exact succ_ne_zero _ h
| succ c =>
rw [mul_succ] at hb
rw [mul_succ] at hb
have aceqad := add_right_cancel _ _ _ hb
have ceqd := hd c aceqad
rw [ceqd]
There is also a missing import for add_right_cancel
- AdvancedAdditionWorld.Level5
.
In level 4 of Advanced Multiplication World there is a proof of:
Near the end of the proof is the line
apply hd
which is flagged in VS Code as an error with the message:Using a clone of the latest
lean4-samples
from GitHub.