mul_comm'

formal source

 388theorem mul_assoc' (a b c : LogicInt) : (a * b) * c = a * (b * c) := by
 389  rw [eq_iff_toInt_eq, toInt_mul, toInt_mul, toInt_mul, toInt_mul]; ring
 390
 391theorem mul_comm' (a b : LogicInt) : a * b = b * a := by
 392  rw [eq_iff_toInt_eq, toInt_mul, toInt_mul]; ring
 393
 394theorem one_mul' (a : LogicInt) : (1 : LogicInt) * a = a := by
 395  rw [eq_iff_toInt_eq, toInt_mul, toInt_one]; ring
 396
 397theorem mul_one' (a : LogicInt) : a * (1 : LogicInt) = a := by
 398  rw [eq_iff_toInt_eq, toInt_mul, toInt_one]; ring
 399
 400theorem mul_add' (a b c : LogicInt) : a * (b + c) = a * b + a * c := by
 401  rw [eq_iff_toInt_eq, toInt_mul, toInt_add, toInt_add, toInt_mul, toInt_mul]; ring
 402
 403theorem add_mul' (a b c : LogicInt) : (a + b) * c = a * c + b * c := by
 404  rw [eq_iff_toInt_eq, toInt_mul, toInt_add, toInt_add, toInt_mul, toInt_mul]; ring
 405
 406/-- `LogicInt` has no zero divisors: from `a * b = 0`, either `a = 0`
 407or `b = 0`. Forced by the ring isomorphism with `Int`. -/
 408theorem mul_eq_zero {a b : LogicInt} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
 409  constructor
 410  · intro h
 411    have hint : toInt a * toInt b = 0 := by
 412      rw [← toInt_mul]
 413      have := congrArg toInt h
 414      rwa [toInt_zero] at this
 415    rcases Int.mul_eq_zero.mp hint with ha | hb
 416    · left
 417      rw [eq_iff_toInt_eq, toInt_zero]; exact ha
 418    · right
 419      rw [eq_iff_toInt_eq, toInt_zero]; exact hb
 420  · rintro (ha | hb)
 421    · rw [ha, eq_iff_toInt_eq, toInt_mul, toInt_zero]; ring