has_mul instance for option?

Stream: maths

[Koundinya Vajjha]

Does option have a has_mul instance?

I've been trying to prove the following:

lemma to_nnreal_mul (a b : ennreal) : ennreal.to_nnreal (a * b) = (ennreal.to_nnreal a)*(ennreal.to_nnreal b) := sorry

But after cases on both a and b I want to simplify the none * some term and the others, but I am stuck. Any suggetions?

[Chris Hughes]

none is defeq to \top, and there should be lemmas about that. Probably rfl will prove it. There might be a special version of cases for ennreal

[Koundinya Vajjha]

I'm stuck on ennreal.to_nnreal (some a * some b) = a * b.

[Sebastien Gouezel]

lemma to_nnreal_mul (a b : ennreal) :
  ennreal.to_nnreal (a * b) = (ennreal.to_nnreal a) * (ennreal.to_nnreal b) :=
begin
  cases a; cases b,
  { simp [none_eq_top] },
  { by_cases h : b = 0; simp [none_eq_top, some_eq_coe, h, top_mul] },
  { by_cases h : a = 0; simp [none_eq_top, some_eq_coe, h, mul_top] },
  { simp [some_eq_coe, coe_mul.symm, -coe_mul] }
end

We should probably add a simp attribute to none_eq_top and some_eq_coe, by the way.