toInt_mul

formal source

 341    rw [toInt_mk, toInt_mk]
 342    ring
 343
 344theorem toInt_mul (a b : LogicInt) : toInt (a * b) = toInt a * toInt b := by
 345  induction a using Quotient.inductionOn with
 346  | h p =>
 347    induction b using Quotient.inductionOn with
 348    | h q =>
 349      rcases p with ⟨a, b⟩
 350      rcases q with ⟨c, d⟩
 351      show toInt (mk (a * c + b * d) (a * d + b * c)) = toInt (mk a b) * toInt (mk c d)
 352      rw [toInt_mk, toInt_mk, toInt_mk]
 353      rw [toNat_add, toNat_add, toNat_mul, toNat_mul, toNat_mul, toNat_mul]
 354      push_cast
 355      ring
 356
 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