How can I concretize this particular _ type?

Stream: new members

[Lars Ericson]

I have one _ in this declaration:

noncomputable def μ_M1 : @measure_theory.measure X M1 :=
@measure_theory.measure.of_measurable X M1
  (λ (s: set X) _, finset.card s.to_finset)
  (by simp)
  (λ x h a, begin simp, sorry end)

If I hover over the "_", it tells me

_x: is_measurable s

If I replace _ with z: is_measurable s as follows:

noncomputable def μ_M1 : @measure_theory.measure X M1 :=
@measure_theory.measure.of_measurable X M1
  (λ (s: set X) (z: is_measurable s), finset.card s.to_finset)
  (by simp)
  (λ x h a, begin simp, sorry end)

Lean gives me a long sequence of errors, for the line with the z on it:

foo.lean:24:20
failed to synthesize type class instance for
s : set X
⊢ measurable_space X
foo.lean:24:20
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  ⁇
inferred
  M1
Additional information:
/home/catskills/Desktop/grundbegriffe/src/foo.lean:24:38: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch, term
    ?m_2.card
  has type
    ℕ
  but is expected to have type
    ennreal
foo.lean:24:20
failed to synthesize type class instance for
s : set X
⊢ measurable_space X
foo.lean:24:20
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  ⁇
inferred
  M1
foo.lean:24:20
failed to synthesize type class instance for
s : set X
⊢ measurable_space X
foo.lean:24:20
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  ⁇
inferred
  M1
foo.lean:24:20
failed to synthesize type class instance for
s : set X
⊢ measurable_space X
foo.lean:24:20
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  ⁇
inferred
  M1
foo.lean:24:20
failed to synthesize type class instance for
s : set X
⊢ measurable_space X
foo.lean:24:20
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  ⁇
inferred
  M1
foo.lean:24:20
failed to synthesize type class instance for
s : set X
⊢ measurable_space X
foo.lean:24:20
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  ⁇
inferred
  M1
foo.lean:24:20
failed to synthesize type class instance for
s : set X
⊢ measurable_space X
foo.lean:24:20
failed to synthesize type class instance for
s : set X
⊢ measurable_space X

Is there a way to get Lean to allow me to concretize the type to the type it ascribes to the _?

[Lars Ericson]

DONE

import measure_theory.measure_space

instance inhabitant : fintype (fin 1) := fin.fintype 1

def A :=  λ a, a ∈ (𝒫 ⊤ : set (set (fin 1)))

def M : measurable_space (fin 1) := { is_measurable_empty := by {rw A, finish},
  is_measurable' := A,
  is_measurable_compl := assume a h, by {rw A at *, finish},
  is_measurable_Union := assume f hf, by {rw A at *, simp },
}

noncomputable abbreviation qlbrdl (s: set (fin 1)) (z: @is_measurable (fin 1) M s) : ennreal :=
  finset.card s.to_finset

noncomputable def μ : @measure_theory.measure (fin 1) M :=
@measure_theory.measure.of_measurable _ M
  (qlbrdl)
  (by simp)
  (λ x h a, begin
    simp,
    sorry
  end)