eq_iff_toInt_eq

formal source

 357/-- Transfer principle: an equation in `LogicInt` holds iff it holds
 358under `toInt`. The workhorse for proving ring identities on
 359`LogicInt` by reduction to `Int`. -/
 360theorem eq_iff_toInt_eq {a b : LogicInt} : a = b ↔ toInt a = toInt b := by
 361  constructor
 362  · exact congrArg toInt
 363  · intro h
 364    have := congrArg fromInt h
 365    rw [fromInt_toInt, fromInt_toInt] at this
 366    exact this
 367
 368/-! ## 7. Ring Axioms on `LogicInt`
 369
 370By transfer through `toInt`, every ring identity on `LogicInt`
 371reduces to one on `Int` and is closed by `ring`. -/
 372
 373theorem add_assoc' (a b c : LogicInt) : (a + b) + c = a + (b + c) := by
 374  rw [eq_iff_toInt_eq, toInt_add, toInt_add, toInt_add, toInt_add]; ring
 375
 376theorem add_comm' (a b : LogicInt) : a + b = b + a := by
 377  rw [eq_iff_toInt_eq, toInt_add, toInt_add]; ring
 378
 379theorem zero_add' (a : LogicInt) : (0 : LogicInt) + a = a := by
 380  rw [eq_iff_toInt_eq, toInt_add, toInt_zero]; ring
 381
 382theorem add_zero' (a : LogicInt) : a + (0 : LogicInt) = a := by
 383  rw [eq_iff_toInt_eq, toInt_add, toInt_zero]; ring
 384
 385theorem add_left_neg' (a : LogicInt) : -a + a = 0 := by
 386  rw [eq_iff_toInt_eq, toInt_add, toInt_neg, toInt_zero]; ring
 387
 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