new_gen_ineq_aux2

lemma new_gen_ineq_aux2 {Y₁ Y₂ Y₃ Y₄ : Ω → G}    (hY₁ : Measurable Y₁) (hY₂ : Measurable Y₂) (hY₃ : Measurable Y₃) (hY₄ : Measurable Y₄)    (h_indep : iIndepFun ![Y₁, Y₂, Y₃, Y₄]) (hA : A.Nonempty) :    ρ[Y₁ + Y₂ | ⟨Y₁ + Y₃, Y₁ + Y₂ + Y₃ + Y₄⟩ # A] ≤       (ρ[Y₁ # A] + ρ[Y₂ # A] + ρ[Y₃ # A] + ρ[Y₄ # A]) / 4        + (d[Y₁ # Y₃] + d[Y₂ # Y₄]) / 4 + d[Y₁ | Y₁ + Y₃ # Y₂ | Y₂ + Y₄] / 2 := by  cases nonempty_fintype G  set S := Y₁ + Y₂ + Y₃ + Y₄  set T₁ := Y₁ + Y₂  set T₂ := Y₁ + Y₃  set T₁' := Y₃ + Y₄  set T₂' := Y₂ + Y₄  have I : IndepFun (⟨Y₁, Y₃⟩) (⟨Y₂, Y₄⟩) := 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  ρ[Y₁ + Y₂ | ⟨T₂, S⟩ # A]    = ρ[Y₁ + Y₂ | ⟨T₂, T₂'⟩ # A] := by      have : S = T₂ + T₂' := by simp only [S, T₂, T₂']; abel      rw [this]      let e : G × G ≃ G × G :=        { toFun p := ⟨p.1, p.1 + p.2⟩          invFun p := ⟨p.1, p.2 - p.1⟩          left_inv := by intro ⟨a, b⟩; simp          right_inv := by intro ⟨a, b⟩; simp }      exact condRho_of_injective T₁ (⟨T₂, T₂'⟩) (f := e) (A := A) e.injective  _ = ∑ w, (Measure.real ℙ (⟨T₂, T₂'⟩ ⁻¹' {w})) * ρ[Y₁ + Y₂ ; ℙ[|⟨T₂, T₂'⟩ ← w] # A] := by    rw [condRho, tsum_fintype]  _ ≤ ∑ w, (Measure.real ℙ (⟨T₂, T₂'⟩ ⁻¹' {w})) * ((ρ[Y₁ ; ℙ[|⟨T₂, T₂'⟩ ← w] # A] +      ρ[Y₂ ; ℙ[|⟨T₂, T₂'⟩ ← w] # A] + d[Y₁ ; ℙ[|⟨T₂, T₂'⟩ ← w] # Y₂ ; ℙ[|⟨T₂, T₂'⟩ ← w]]) / 2) := by    gcongr with w hw    have : IndepFun Y₁ Y₂ (ℙ[|⟨T₂, T₂'⟩ ⁻¹' {w}]) := by      have E : (⟨Y₁, Y₃⟩)⁻¹' {p | p.1 + p.2 = w.1} ∩ (⟨Y₂, Y₄⟩)⁻¹' {p | p.1 + p.2 = w.2}        = ⟨T₂, T₂'⟩ ⁻¹' {w} := by aesop      have I : IndepFun (⟨Y₁, Y₃⟩) (⟨Y₂, Y₄⟩) (ℙ[|(⟨Y₁, Y₃⟩)⁻¹' {p | p.1 + p.2 = w.1}          ∩ (⟨Y₂, Y₄⟩)⁻¹' {p | p.1 + p.2 = w.2}]) :=        I.cond (measurable_add (.singleton w.1))          (measurable_add (.singleton w.2)) (hY₁.prodMk hY₃) (hY₂.prodMk hY₄)      rw [E] at I      exact I.comp measurable_fst measurable_fst    exact rho_of_sum_le hY₁ hY₂ hA this  _ = (ρ[Y₁ | ⟨T₂, T₂'⟩ # A] + ρ[Y₂ | ⟨T₂, T₂'⟩ # A] + d[Y₁ | T₂ # Y₂ | T₂']) / 2 := by    simp_rw [← mul_div_assoc, ← Finset.sum_div, mul_add, Finset.sum_add_distrib, condRho,      tsum_fintype]    congr    rw [condRuzsaDist_eq_sum' hY₁ (by fun_prop) hY₂ (by fun_prop), Fintype.sum_prod_type]    congr with x    congr with y    have : (⟨T₂, T₂'⟩) ⁻¹' {(x, y)} = (Y₁ + Y₃) ⁻¹' {x} ∩ (Y₂ + Y₄) ⁻¹' {y} := by      ext p; simp [T₂, T₂']    rw [this]    have J : IndepFun (Y₁ + Y₃) (Y₂ + Y₄) := 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 ℙ ((Y₁ + Y₃) ⁻¹' {x})) 0 with h1|h1    · simp [h1, T₂]    rcases eq_or_ne (Measure.real ℙ ((Y₂ + Y₄) ⁻¹' {y})) 0 with h2|h2    · simp [h2, T₂']    congr 1    have A : IdentDistrib Y₁ Y₁ (ℙ[|(Y₁ + Y₃) ⁻¹' {x} ∩ (Y₂ + Y₄) ⁻¹' {y}])        (ℙ[|(Y₁ + Y₃) ⁻¹' {x}]) := by      rw [← cond_cond_eq_cond_inter' (by exact hY₁.add hY₃ (.singleton _))        (by exact hY₂.add hY₄ (.singleton _)) (by finiteness)]      have : IsProbabilityMeasure (ℙ[|(Y₁ + Y₃) ⁻¹' {x}]) := cond_isProbabilityMeasure_of_real h1      apply (IndepFun.identDistrib_cond _ (.singleton _) hY₁ (by fun_prop) _).symm      · have : IndepFun (⟨Y₁, Y₃⟩) (⟨Y₂, Y₄⟩) (ℙ[|(⟨Y₁, Y₃⟩) ⁻¹' {p | p.1 + p.2 = x}]) :=          I.cond_left (measurable_add (.singleton x)) (hY₁.prodMk hY₃)        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 hY₁.add hY₃ (.singleton _)    refine A.rdist_congr ?_    rw [Set.inter_comm, ← cond_cond_eq_cond_inter' (by exact hY₂.add hY₄ (.singleton _))      (by exact hY₁.add hY₃ (.singleton _)) (by finiteness)]    have : IsProbabilityMeasure (ℙ[|(Y₂ + Y₄) ⁻¹' {y}]) := cond_isProbabilityMeasure_of_real h2    apply (IndepFun.identDistrib_cond _ (.singleton _) hY₂ (hY₁.add hY₃) _).symm    · have : IndepFun (⟨Y₂, Y₄⟩) (⟨Y₁, Y₃⟩) (ℙ[|(⟨Y₂, Y₄⟩) ⁻¹' {p | p.1 + p.2 = y}]) :=        I.symm.cond_left (measurable_add (.singleton y)) (hY₂.prodMk hY₄)      exact this.comp measurable_fst measurable_add    · rw [cond_apply (hY₂.add hY₄ (.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]  _ = (ρ[Y₁ | T₂ # A] + ρ[Y₂ | T₂' # A] + d[Y₁ | T₂ # Y₂ | T₂']) / 2 := by    congr 3    · apply condRho_prod_eq_of_indepFun hY₁ (by fun_prop) (by fun_prop)      exact I.comp (measurable_fst.prodMk measurable_add) measurable_add    · have : ρ[Y₂ | ⟨T₂, T₂'⟩ # A] = ρ[Y₂ | ⟨T₂', T₂⟩ # A] :=        condRho_of_injective Y₂ (⟨T₂', T₂⟩) (f := Prod.swap) Prod.swap_injective      rw [this]      apply condRho_prod_eq_of_indepFun hY₂ (by fun_prop) (by fun_prop)      exact I.symm.comp (measurable_fst.prodMk measurable_add) measurable_add  _ ≤ ((ρ[Y₁ # A] + ρ[Y₃ # A] + d[Y₁ # Y₃]) / 2 +       (ρ[Y₂ # A] + ρ[Y₄ # A] + d[Y₂ # Y₄]) / 2 + d[Y₁ | T₂ # Y₂ | T₂']) / 2 := by    gcongr    · exact condRho_of_sum_le hY₁ hY₃ hA (h_indep.indepFun (i := 0) (j := 2) (by decide))    · exact condRho_of_sum_le hY₂ hY₄ hA (h_indep.indepFun (i := 1) (j := 3) (by decide))  _ = (ρ[Y₁ # A] + ρ[Y₂ # A] + ρ[Y₃ # A] + ρ[Y₄ # A]) / 4        + (d[Y₁ # Y₃] + d[Y₂ # Y₄]) / 4 + d[Y₁ | Y₁ + Y₃ # Y₂ | Y₂ + Y₄] / 2 := by ring