gen_ineq_10

lemma gen_ineq_10 : d[Y # Z₃ + Z₄ | ⟨Z₁ + Z₃, Sum⟩] - d[Y # Z₁] ≤    (d[Z₁ # Z₂] + 2 * d[Z₁ # Z₃] + d[Z₂ # Z₄]) / 4    + (d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄] - d[Z₁ | Z₁ + Z₂ # Z₃ | Z₃ + Z₄]) / 4    + (H[Z₁ + Z₂] - H[Z₃ + Z₄] + H[Z₂] - H[Z₃] + H[Z₂ | Z₂ + Z₄] - H[Z₁ | Z₁ + Z₃]) / 8 := by  convert gen_ineq_00 Y hY Z₁ Z₂ Z₃ Z₄ hZ₁ hZ₂ hZ₃ hZ₄ h_indep using 2  have hS : Measurable Sum := by fun_prop  let e : G × G ≃ G × G := Equiv.prodComm G G  have A : e ∘ ⟨Z₁ + Z₃, Sum⟩ = ⟨Sum, Z₁ + Z₃⟩ := by ext p <;> rfl  rw [← condRuzsaDist_comp_right (ℙ : Measure Ω₀) (ℙ : Measure Ω) Y (Z₃ + Z₄) (⟨Z₁ + Z₃, Sum⟩)      e (by fun_prop) (by fun_prop) (by fun_prop) e.injective ,      ← condRuzsaDist_comp_right (ℙ : Measure Ω₀) (ℙ : Measure Ω) Y (Z₁ + Z₂)        (⟨Z₁ + Z₃, Sum⟩) e (by fun_prop) (by fun_prop) (by fun_prop) e.injective, A,      condRuzsaDist'_prod_eq_sum _ _ (by fun_prop) hS (by fun_prop),      condRuzsaDist'_prod_eq_sum _ _ (by fun_prop) hS (by fun_prop)]  congr with w  rcases eq_or_ne (Measure.real ℙ ((Z₁ + Z₃) ⁻¹' {w})) 0 with hw|hw  · simp [hw]  have : IsProbabilityMeasure (ℙ[|(Z₁ + Z₃) ⁻¹' {w}]) := cond_isProbabilityMeasure_of_real hw  have : Sum = (Z₁ + Z₂) + (Z₃ + Z₄) := by abel  rw [this, condRuzsaDist'_of_inj_map' hY (by fun_prop) (by fun_prop)]