import Mathlib.Tactic.ToAdditive
import Mathlib.Init.ZeroOne

-- to_additive doesn't attach `simp`
@[simp, to_additive]
theorem One.foo [One α] [Mul α] (a : α) : (1 : α) * a = 1 := sorry

example [One α] [Mul α] (a : α) : (1 : α) * a = 1 := by simp

#check @Zero.foo -- exists

example [Zero α] [Add α] : (0 : α) + a = 0 := by simp -- fails (note: zero_add doesn't fire because it's not imported)

import Mathlib.Algebra.Hom.Group

-- `simps` doesn't run on additivised declaration
@[to_additive, simps]
def OneHom.id' (M : Type _) [One M] : OneHom M M where
  toFun x := x
  map_one' := rfl

#check OneHom.id'_apply -- exists
#check ZeroHom.id' -- exists
#check ZeroHom.id'_apply -- doesn't exist

import Mathlib.Algebra.Group.Units

@[ext, to_additive]
theorem Units.ext' [Monoid α] : Function.Injective (fun (u : αˣ) => (u : α))
  | ⟨v, i₁, vi₁, iv₁⟩, ⟨v', i₂, vi₂, iv₂⟩, e => by
    simp only at e; subst v'; congr;
    simpa only [iv₂, vi₁, one_mul, mul_one] using mul_assoc i₂ v i₁

example [Monoid α] (a b : αˣ) : a = b := by
  ext -- does something
  sorry

example [AddMonoid α] (a b : AddUnits α) : a = b := by
  ext -- fails