∀ {α : Type u_5} {E : Type u_6} (m m_1 : MeasurableSpace α),
  m = m_1 →
    ∀ {m₀ : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : CompleteSpace E] [inst_2 : NormedSpace ℝ E]
      (μ μ_1 : MeasureTheory.Measure α),
      μ = μ_1 → ∀ (f f_1 : α → E), f = f_1 → ∀ (a a_1 : α), a = a_1 → μ[f | m] a = μ_1[f_1 | m_1] a_1