new_gen_ineq_aux1

lemma new_gen_ineq_aux1 {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₄]          + I[Y₁ + Y₂ : Y₁ + Y₃ | Y₁ + Y₂ + Y₃ + Y₄]) / 2 := by  set S := Y₁ + Y₂ + Y₃ + Y₄  set T₁ := Y₁ + Y₂  set T₂ := Y₁ + Y₃  set T₁' := Y₃ + Y₄  set T₂' := Y₂ + Y₄  have : ρ[T₁ | ⟨T₂, S⟩ # A] ≤ ρ[T₁ | S # A] + I[T₁ : T₂ | S] / 2 := by    rw [condMutualInfo_eq' (by fun_prop) (by fun_prop) (by fun_prop)]    exact condRho_prod_le (by fun_prop) (by fun_prop) (by fun_prop) hA  have : ρ[T₁ | S # A] ≤ (ρ[T₁ # A] + ρ[T₁' # A] + d[T₁ # T₁']) / 2 := by    have S_eq : S = T₁ + T₁' := by simp only [S, T₁, T₁']; abel    rw [S_eq]    apply condRho_of_sum_le (by fun_prop) (by fun_prop) hA    exact h_indep.indepFun_add_add (ι := Fin 4) (by intro i; fin_cases i <;> assumption) 0 1 2 3      (by decide) (by decide) (by decide) (by decide)  have : ρ[T₁ # A] ≤ (ρ[Y₁ # A] + ρ[Y₂ # A] + d[Y₁ # Y₂]) / 2 :=    rho_of_sum_le hY₁ hY₂ hA (h_indep.indepFun (i := 0) (j := 1) (by decide))  have : ρ[T₁' # A] ≤ (ρ[Y₃ # A] + ρ[Y₄ # A] + d[Y₃ # Y₄]) / 2 :=    rho_of_sum_le hY₃ hY₄ hA (h_indep.indepFun (i := 2) (j := 3) (by decide))  linarith