Unfold Multiplication in Group

Stream: maths

[Charles Murphy]

I am trying to prove that a something is a group and I am wondering if there is a way to get Lean to unfold the definition of multiplication that for the given group.

@[reducible] def C : Type := {n : ℚ // n ≠ -1}

instance : has_mul C :=
{
  mul := λ a b, ⟨a.val + b.val + a.val * b.val, sorry⟩,
}

theorem C_mul_one : ∀ a : C, a * 1 = a :=
begin
  intros a,
  cases a,

end

For instance, in the theorem C_mul_one, I get

⟨a_val, a_property⟩ * 1 = ⟨a_val, a_property⟩

and would like to be able to use the definition of multiplication for C to continue the proof. Thanks.