Trouble feeding instances

Stream: general

[Abhimanyu Pallavi Sudhir]

In order.filter.filter_product, I'm trying to write:

@[simp] lemma of_div [division_ring β] (U : is_ultrafilter φ) (x y : β) :
  of (x / y) = (@division_ring_has_div β* (filter_product.division_ring U) (filter_product.division_ring U)).div
   (of x) (of y : β*) := sorry

[Abhimanyu Pallavi Sudhir]

(to try and bypass the problem of U not being an instance)

[Abhimanyu Pallavi Sudhir]

But Lean gives weird errors:

invalid field notation, function 'has_div.div' does not have explicit argument with type (has_div ...)

[Abhimanyu Pallavi Sudhir]

Which doesn't seem to make sense, as trying to access a field has_div out of has_div.div is certainly not what I'm doing.

[Chris Hughes]

In order to use the dot notation, you need the has_div argument to has_div.div to be explicit.

[Abhimanyu Pallavi Sudhir]

Oh, right -- of course.

[Abhimanyu Pallavi Sudhir]

Yes, this works.

@[simp] lemma of_div [division_ring β] (U : is_ultrafilter φ) (x y : β) :
  of (x / y) = @has_div.div _ (@division_ring_has_div β* (filter_product.division_ring U) (filter_product.division_ring U))
  (of x) (of y : β*)