Type errors investigation

Stream: new members

[Pietro Lavino]

I am currently completing the following, and I get this confusing error: type mismatch
h'
has type
MeasurableSet (p.f i) : Prop
but is expected to have type
MeasurableSet (p.f i) : Prop (Lean 4). How am I supposed to understand in what way top the types not match?

import Mathlib.Analysis.Convolution

import Mathlib.MeasureTheory.Function.Jacobian

import Mathlib.MeasureTheory.Integral.Bochner

import Mathlib.MeasureTheory.Measure.Lebesgue.Basic

import Mathlib.Analysis.SpecialFunctions.Log.Basic

import Mathlib.Data.ENNReal.Real

import Init.Data.Fin.Basic

import Mathlib.Data.Set.Lattice

import Mathlib.Data.Set.Function

import Mathlib.Analysis.SpecialFunctions.Log.Basic

import Mathlib.Analysis.Convex.Basic

import Mathlib.Data.Real.Basic

import Mathlib.Algebra.BigOperators.Ring

import Mathlib.MeasureTheory.Measure.NullMeasurable

open MeasureTheory

open ENNReal

open Set

open Function

open scoped BigOperators

structure partition {α : Type*} (m : MeasurableSpace α) (μ : Measure α) [IsProbabilityMeasure μ] :=
  f : ℕ → Set α         -- A function from natural numbers to sets of terms in α
  measurable : ∀ n, MeasurableSet (f n)  -- Each set is measurable
  (disjoint : ∀ i j, i ≠ j → μ (f i ∩ f j) = 0)  -- The sets are pairwise disjoint
  (cover : (⋃ n, f n) = Set.univ)  -- The union of all sets covers the entire space

theorem addone {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
 (p : partition m μ) : (μ (⋃ i, p.f i)) = ∑' i , μ (p.f i) := by
  apply MeasureTheory.measure_iUnion₀
  · intro x y
    exact p.disjoint x y
  · intro i-- (h : MeasurableSet s) :
    have h': MeasurableSet (p.f i) := by
      exact p.measurable I
    simp[MeasureTheory.NullMeasurableSet]
    exact h'

[Kevin Buzzard]

Before the simp the goal is

h' : MeasurableSet (p.f i)
⊢ NullMeasurableSet (p.f i) μ

And simp seems to guess that the way you want to prove the set is nullmeasurable is to prove that it's measurable and that every measurable set is nullmeasurable, so this looks to me like a wrong turn (although I'm not an expert in this part of the library). If you change exact h' to convert h' you'll see where the terms don't match. But you look in trouble to me already by the simp?