Cexp eq cexp cexp

lemma cexp_eq_cexp_cexp (g : α → β) (h : ∀ x y, f.prob x ≠ 0 → g x = g y → (q x ↔ q y)) :    f.cexp u q = (g <$> f).cexp (fun k ↦ f.cexp u (fun y ↦ g y = k))      (fun k ↦ ∃ x, g x = k ∧ q x) := by  rw [cexp, cexp]  refine congr_arg₂ _ ?_ ?_  · rw [exp_eq_exp_cexp g]    refine exp_congr fun k _ ↦ ?_    by_cases qk : ∃ z, g z = k ∧ q z    · simp only [qk, ite_true]      rcases qk with ⟨z,zk,qz⟩      refine cexp_congr fun w m e ↦ ?_      simp only [(h w z m (e.trans zk.symm)).mpr qz, ite_true]    · simp only [qk, ite_false]      refine cexp_eq_zero fun _ _ e ↦ ?_      simp only [not_exists, not_and] at qk      simp only [qk _ e, ite_false]  · simp only [pr_map]    refine pr_congr fun x m ↦ ⟨?_,?_⟩    · intro _; use x    · intro ⟨y,gyx,qy⟩; rwa [h x y m gyx.symm]