gen_ineq_aux2

lemma gen_ineq_aux2 :    d[Y # Z₁ + Z₂ | ⟨Z₁ + Z₃, Sum⟩] ≤ d[Y # Z₁]      + (d[Z₁ # Z₃] + d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄]) / 2      + (H[Z₂ | Z₂ + Z₄] - H[Z₁ | Z₁ + Z₃] + H[Z₁] - H[Z₃]) / 4 := by  cases nonempty_fintype G  have hS : Measurable Sum := by fun_prop  have I : IndepFun (⟨Z₁, Z₃⟩) (⟨Z₂, Z₄⟩) := by    refine (h_indep.indepFun_prodMk_prodMk ?_ 0 2 1 3      (by decide) (by decide) (by decide) (by decide))    intro i; fin_cases i <;> assumption  calc  d[Y # Z₁ + Z₂ | ⟨Z₁ + Z₃, Sum⟩]    = d[Y # Z₁ + Z₂ | ⟨Z₁ + Z₃, Z₂ + Z₄⟩] := by      let e : G × G ≃ G × G :=        { toFun p := ⟨p.1, p.2 - p.1⟩          invFun p := ⟨p.1, p.2 + p.1⟩          left_inv := by intro ⟨a, b⟩; simp          right_inv := by intro ⟨a, b⟩; simp }      convert! (condRuzsaDist_comp_right (ℙ : Measure Ω₀) (ℙ : Measure Ω) Y (Z₁ + Z₂)        (⟨Z₁ + Z₃, Sum⟩) e (hZ₁.add hZ₂) ((hZ₁.add hZ₃).prodMk hS)        (.of_discrete (f := e)) e.injective).symm      simp only [e, Pi.add_apply, Equiv.coe_fn_mk, Function.comp_apply]      abel  _ = ∑ w, (Measure.real ℙ (⟨Z₁ + Z₃, Z₂ + Z₄⟩ ⁻¹' {w})) *        d[Y ; ℙ # Z₁ + Z₂ ; ℙ[|⟨Z₁ + Z₃, Z₂ + Z₄⟩ ← w]] := by    rw [condRuzsaDist'_eq_sum']    · exact hZ₁.add hZ₂    · exact (hZ₁.add hZ₃).prodMk (hZ₂.add hZ₄)  _ ≤ ∑ w, Measure.real ℙ (⟨Z₁ + Z₃, Z₂ + Z₄⟩ ⁻¹' {w}) * (d[Y ; ℙ # Z₁ ; ℙ[|⟨Z₁ + Z₃, Z₂ + Z₄⟩ ← w]]      + d[Z₁ ; ℙ[|⟨Z₁ + Z₃, Z₂ + Z₄⟩ ⁻¹' {w}] # Z₂ ; ℙ[|⟨Z₁ + Z₃, Z₂ + Z₄⟩ ⁻¹' {w}]] / 2      + H[Z₂ | ⟨Z₁ + Z₃, Z₂ + Z₄⟩ ← w] / 4 - H[Z₁ | ⟨Z₁ + Z₃, Z₂ + Z₄⟩ ← w] / 4) := by    apply Finset.sum_le_sum (fun w _h'w ↦ ?_)    rcases eq_or_ne (Measure.real ℙ (⟨Z₁ + Z₃, Z₂ + Z₄⟩ ⁻¹' {w})) 0 with hw|hw    · simp [hw]    gcongr    have : IsProbabilityMeasure (ℙ[|⟨Z₁ + Z₃, Z₂ + Z₄⟩ ← w]) := cond_isProbabilityMeasure_of_real hw    have : IndepFun Z₁ Z₂ (ℙ[|⟨Z₁ + Z₃, Z₂ + Z₄⟩ ⁻¹' {w}]) := by      have E : (⟨Z₁, Z₃⟩)⁻¹' {p | p.1 + p.2 = w.1} ∩ (⟨Z₂, Z₄⟩)⁻¹' {p | p.1 + p.2 = w.2}        = ⟨Z₁ + Z₃, Z₂ + Z₄⟩ ⁻¹' {w} := by aesop      have I : IndepFun (⟨Z₁, Z₃⟩) (⟨Z₂, Z₄⟩) (ℙ[|(⟨Z₁, Z₃⟩)⁻¹' {p | p.1 + p.2 = w.1}          ∩ (⟨Z₂, Z₄⟩)⁻¹' {p | p.1 + p.2 = w.2}]) :=        I.cond (measurable_add (.singleton w.1))          (measurable_add (.singleton w.2)) (hZ₁.prodMk hZ₃) (hZ₂.prodMk hZ₄)      rw [E] at I      exact I.comp measurable_fst measurable_fst    have := condRuzsaDist_diff_le' (ℙ : Measure Ω₀) (μ' := ℙ[|⟨Z₁ + Z₃, Z₂ + Z₄⟩ ← w])      hY hZ₁ hZ₂ this    linarith  _ = d[Y # Z₁ | Z₁ + Z₃] + d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄]/2      + H[Z₂ | Z₂ + Z₄] / 4 - H[Z₁ | Z₁ + Z₃] / 4 := by    simp only [mul_sub, mul_add, Finset.sum_sub_distrib, Finset.sum_add_distrib]    congr    · rw [← condRuzsaDist'_eq_sum' hZ₁ (by fun_prop)]      apply condRuszaDist_prod_eq_of_indepFun hY hZ₁ (by fun_prop) (by fun_prop)      exact I.comp (measurable_fst.prodMk measurable_add) measurable_add    · simp_rw [← mul_div_assoc, ← Finset.sum_div]      rw [condRuzsaDist_eq_sum' hZ₁ (by fun_prop) hZ₂ (by fun_prop), Fintype.sum_prod_type]      congr with x      congr with y      have : (⟨Z₁ + Z₃, Z₂ + Z₄⟩) ⁻¹' {(x, y)} = (Z₁ + Z₃) ⁻¹' {x} ∩ (Z₂ + Z₄) ⁻¹' {y} := by        ext p; simp      rw [this]      have J : IndepFun (Z₁ + Z₃) (Z₂ + Z₄) := by exact I.comp measurable_add measurable_add      rw [J.measureReal_inter_preimage_eq_mul (.singleton x) (.singleton y)]      rcases eq_or_ne (Measure.real ℙ ((Z₁ + Z₃) ⁻¹' {x})) 0 with h1|h1      · simp [h1]      rcases eq_or_ne (Measure.real ℙ ((Z₂ + Z₄) ⁻¹' {y})) 0 with h2|h2      · simp [h2]      congr 1      have A : IdentDistrib Z₁ Z₁ (ℙ[|(Z₁ + Z₃) ⁻¹' {x} ∩ (Z₂ + Z₄) ⁻¹' {y}])          (ℙ[|(Z₁ + Z₃) ⁻¹' {x}]) := by        rw [← cond_cond_eq_cond_inter' (by exact hZ₁.add hZ₃ (.singleton _))          (by exact hZ₂.add hZ₄ (.singleton _)) (by finiteness)]        have : IsProbabilityMeasure (ℙ[|(Z₁ + Z₃) ⁻¹' {x}]) := cond_isProbabilityMeasure_of_real h1        apply (IndepFun.identDistrib_cond _ (.singleton _) hZ₁ (by fun_prop) _).symm        · have : IndepFun (⟨Z₁, Z₃⟩) (⟨Z₂, Z₄⟩) (ℙ[|(⟨Z₁, Z₃⟩) ⁻¹' {p | p.1 + p.2 = x}]) :=            I.cond_left (measurable_add (.singleton x))              (hZ₁.prodMk hZ₃)          exact this.comp measurable_fst measurable_add        · rw [cond_apply, J.measure_inter_preimage_eq_mul _ _ (.singleton x) (.singleton y)]          · simp only [ne_eq, measure_ne_top, not_false_eq_true, measureReal_eq_zero_iff] at h1 h2            simp [h1, h2]          · exact hZ₁.add hZ₃ (.singleton _)      have B : IdentDistrib Z₂ Z₂ (ℙ[|(Z₁ + Z₃) ⁻¹' {x} ∩ (Z₂ + Z₄) ⁻¹' {y}])          (ℙ[|(Z₂ + Z₄) ⁻¹' {y}]) := by        rw [Set.inter_comm, ← cond_cond_eq_cond_inter' (by exact hZ₂.add hZ₄ (.singleton _))          (by exact hZ₁.add hZ₃ (.singleton _)) (by finiteness)]        have : IsProbabilityMeasure (ℙ[|(Z₂ + Z₄) ⁻¹' {y}]) := cond_isProbabilityMeasure_of_real h2        apply (IndepFun.identDistrib_cond _ (.singleton _) hZ₂ (hZ₁.add hZ₃) _).symm        · have : IndepFun (⟨Z₂, Z₄⟩) (⟨Z₁, Z₃⟩) (ℙ[|(⟨Z₂, Z₄⟩) ⁻¹' {p | p.1 + p.2 = y}]) :=            I.symm.cond_left (measurable_add (.singleton y))              (hZ₂.prodMk hZ₄)          exact this.comp measurable_fst measurable_add        · rw [cond_apply (hZ₂.add hZ₄ (.singleton y)),            J.symm.measure_inter_preimage_eq_mul _ _ (.singleton _) (.singleton _)]          simp only [ne_eq, measure_ne_top, not_false_eq_true, measureReal_eq_zero_iff] at h1 h2          simp [h1, h2]      exact A.rdist_congr B    · have I1 : H[Z₂ | Z₂ + Z₄] = H[Z₂ | ⟨Z₂ + Z₄, Z₁ + Z₃⟩] := by        apply (condEntropy_prod_eq_of_indepFun hZ₂ (by fun_prop) (by fun_prop) _).symm        exact I.symm.comp (measurable_fst.prodMk measurable_add) measurable_add      have I2 : H[Z₂ | ⟨Z₂ + Z₄, Z₁ + Z₃⟩] = H[Z₂ | ⟨Z₁ + Z₃, Z₂ + Z₄⟩] :=        condEntropy_of_injective' _ hZ₂ ((hZ₁.add hZ₃).prodMk (hZ₂.add hZ₄))          _ (Equiv.prodComm G G).injective ((hZ₂.add hZ₄).prodMk (hZ₁.add hZ₃))      rw [I1, I2, condEntropy_eq_sum_fintype _ _ _ (by fun_prop)]      simp_rw [← mul_div_assoc, Finset.sum_div]    · have : H[Z₁ | Z₁ + Z₃] = H[Z₁ | ⟨Z₁ + Z₃, Z₂ + Z₄⟩] := by        apply (condEntropy_prod_eq_of_indepFun hZ₁ (hZ₁.add hZ₃) (hZ₂.add hZ₄) _).symm        exact I.comp (measurable_fst.prodMk measurable_add) measurable_add      rw [this, condEntropy_eq_sum_fintype _ _ _ (by fun_prop)]      simp_rw [← mul_div_assoc, Finset.sum_div]  _ ≤ (d[Y # Z₁] + d[Z₁ # Z₃]/2 + H[Z₁]/4 - H[Z₃]/4) + d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄]/2      + H[Z₂ | Z₂ + Z₄] / 4 - H[Z₁ | Z₁ + Z₃] / 4 := by    gcongr    have I : IndepFun Z₁ Z₃ := by exact h_indep.indepFun (show 0 ≠ 2 by decide)    have := condRuzsaDist_diff_le''' (ℙ : Measure Ω₀) (μ' := (ℙ : Measure Ω)) hY hZ₁ hZ₃ I    linarith  _ = _ := by ring