Reduction of operator classes

Stream: new members

[Soundwave]

Mathematical context: Adjoining a top element to a group to form a monoidal range for a valuation. I'm aware mathlib already has this construction.

I'm not understanding why the first case goes through by rfl but the second case is stubborn to reduce. Is there a better way to do this? Is it possible without a separate definition? My understanding is either an instance or a definition is required as valuationMonoid.add doesn't have a name inside the instance definition but the former seems to require an additional unfold with no way around it. I don't know why that is either.

class Monoid (M : Type) extends Add M where
  zero : M
  zero_add m : zero + m = m
  add_assoc (m n o : M) : m + n + o = m + (n + o)
  add_comm (m n : M) : m + n = n + m

instance Monoid.instOfNat [Monoid M] : OfNat M 0 where
  ofNat := zero

class Group (G : Type) extends Monoid G where
  add_inv : G → G
  add_left_inv g : add_inv g + g = zero

def Group.valuationMonoid.add [G : Group C] (g h : Option C) := do
  let a ← g
  let b ← h
  return a + b

instance Group.valuationMonoid [G : Group C] : Monoid (Option C) where
  add := valuationMonoid.add
  zero := .some 0
  zero_add g := by
    cases g with
    | none => rfl
    | some a => {
      show valuationMonoid.add _ _ = _
      unfold valuationMonoid.add
      simp
      exact G.zero_add a
    }
  add_assoc := by sorry
  add_comm := by sorry

[Ruben Van de Velde]

You can prove it with exact congrArg some (G.zero_add a)