no goals
ι : Type ?u.104315
α : Type u_1
β : Type ?u.104321
inst✝ : LinearOrderedSemifield α
a✝ b c d e : α
m n : ℤ
a : α
⊢ a / 3 + a / 3 + a / 3 = a
rw [div_add_div_same, div_add_div_same, ← two_mul, ← add_one_mul 2 a, two_add_one_eq_three,
  mul_div_cancel_left a three_ne_zero]