Mix m Ensemble pure average

theorem mix_mEnsemble_pure_average {e : MEnsemble d α} {T : Type _} {U : Type*} [AddCommGroup U] [Module ℝ U] [inst : Mixable U T] (f : MState d → T) (hmix : mix e = pure ψ) :  average f e = f (pure ψ) := by  have hpure := mix_mEnsemble_pure_iff_pure.mp hmix  simp only [average, Functor.map, ProbDistribution.expect_val]  apply Mixable.to_U_inj  rw [MEnsemble.states] at hpure  simp only [Mixable.to_U_of_mkT, Function.comp_apply]  have h1 : ∀ i ∈ Finset.univ, (e.distr i : ℝ) • (Mixable.to_U (f (e.var i))) ≠ 0 → e.var i = pure ψ := fun i hi ↦ by    have h2 : e.distr i = 0 → (e.distr i : ℝ) • (Mixable.to_U (f (e.var i))) = 0 := fun h0 ↦ by      simp only [h0, Prob.coe_zero, zero_smul]    exact (hpure i) ∘ h2.mt  classical rw [←Finset.sum_filter_of_ne h1, Finset.sum_filter]  classical conv =>    enter [1, 2, a]    rw [←dite_eq_ite]    enter [2, hvar]    rw [hvar]  classical conv =>    enter [1, 2, a]    rw [dite_eq_ite]    rw [←ite_zero_smul]  have hpure' : ∀ i ∈ Finset.univ, (↑(e.distr i) : ℝ) ≠ 0 → e.var i = pure ψ := fun i hi hne0 ↦ by    apply hpure i    simpa using hne0  classical rw [← Finset.sum_smul, ← Finset.sum_filter, Finset.sum_filter_of_ne hpure', ProbDistribution.normalized, one_smul]