I_one_le

lemma I_one_le (hA : A.Nonempty) : I₁ ≤ 2 * η * d[ X₁ # X₂ ] := by  have : d[X₁ + X₂' # X₂ + X₁'] + d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁'] + I₁ = 2 * k :=    rdist_add_rdist_add_condMutual_eq _ _ _ _ hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep.reindex_four_abdc  have : k - η * (ρ[X₁ | X₁ + X₂' # A] - ρ[X₁ # A])      - η * (ρ[X₂ | X₂ + X₁' # A] - ρ[X₂ # A]) ≤ d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁'] :=    condRho_le_condRuzsaDist_of_phiMinimizes h_min hX₁ hX₂ (by fun_prop) (by fun_prop)  have : k - η * (ρ[X₁ + X₂' # A] - ρ[X₁ # A])      - η * (ρ[X₂ + X₁' # A] - ρ[X₂ # A]) ≤ d[X₁ + X₂' # X₂ + X₁'] :=    le_rdist_of_phiMinimizes h_min (hX₁.add hX₂') (hX₂.add hX₁')  have : ρ[X₁ + X₂' # A] ≤ (ρ[X₁ # A] + ρ[X₂ # A] + d[ X₁ # X₂ ]) / 2 := by    rw [rho_eq_of_identDistrib h₂, h₂.rdist_congr_right hX₁.aemeasurable]    apply rho_of_sum_le hX₁ hX₂' hA    simpa using h_indep.indepFun (show (0 : Fin 4) ≠ 3 by decide)  have : ρ[X₂ + X₁' # A] ≤ (ρ[X₁ # A] + ρ[X₂ # A] + d[ X₁ # X₂ ]) / 2 := by    rw [add_comm, rho_eq_of_identDistrib h₁, h₁.rdist_congr_left hX₂.aemeasurable]    apply rho_of_sum_le hX₁' hX₂ hA    simpa using h_indep.indepFun (show (2 : Fin 4) ≠ 1 by decide)  have : ρ[X₁ | X₁ + X₂' # A] ≤ (ρ[X₁ # A] + ρ[X₂ # A] + d[ X₁ # X₂ ]) / 2 := by    rw [rho_eq_of_identDistrib h₂, h₂.rdist_congr_right hX₁.aemeasurable]    apply condRho_of_sum_le hX₁ hX₂' hA    simpa using h_indep.indepFun (show (0 : Fin 4) ≠ 3 by decide)  have : ρ[X₂ | X₂ + X₁' # A] ≤ (ρ[X₁ # A] + ρ[X₂ # A] + d[ X₁ # X₂ ]) / 2 := by    have : ρ[X₂ | X₂ + X₁' # A] ≤ (ρ[X₂ # A] + ρ[X₁' # A] + d[ X₂ # X₁' ]) / 2 := by      apply condRho_of_sum_le hX₂ hX₁' hA      simpa using h_indep.indepFun (show (1 : Fin 4) ≠ 2 by decide)    have I : ρ[X₁' # A] = ρ[X₁ # A] := rho_eq_of_identDistrib h₁.symm    have J : d[X₂ # X₁'] = d[X₁ # X₂] := by      rw [rdist_symm, h₁.rdist_congr_left hX₂.aemeasurable]    linarith  nlinarith