Lean4
/-- Define a `CommRing` structure on a Type by proving a minimized set of axioms.
Note that this uses the default definitions for `npow`, `nsmul`, `zsmul` and `sub`
See note [reducible non-instances]. -/
abbrev ofMinimalAxioms {R : Type u} [Add R] [Mul R] [Neg R] [Zero R] [One R]
(add_assoc : ∀ a b c : R, a + b + c = a + (b + c)) (zero_add : ∀ a : R, 0 + a = a)
(neg_add_cancel : ∀ a : R, -a + a = 0) (mul_assoc : ∀ a b c : R, a * b * c = a * (b * c))
(mul_comm : ∀ a b : R, a * b = b * a) (one_mul : ∀ a : R, 1 * a = a)
(left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c) : CommRing R :=
haveI mul_one : ∀ a : R, a * 1 = a := fun a => by rw [mul_comm, one_mul]
haveI right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c := fun a b c => by
rw [mul_comm, left_distrib, mul_comm, mul_comm b c]
letI := Ring.ofMinimalAxioms add_assoc zero_add neg_add_cancel mul_assoc one_mul mul_one left_distrib right_distrib
{ mul_comm := mul_comm }
