I_two_le

lemma I_two_le (hA : A.Nonempty) (h'η : η < 1) :    I₂ ≤ 2 * η * k + (η / (1 - η)) * (2 * η * k - I₁) := by  have W : 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 W' : 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₂ (hX₁.add hX₁') (hX₂.add hX₂')  have Z : 2 * k = d[X₁ + X₁' # X₂ + X₂'] + d[X₁ | X₁ + X₁' # X₂ | X₂ + X₂'] + I₂ :=    I_two_aux' h₁ h₂ h_indep hX₁ hX₂ hX₁' hX₂'  have : ρ[X₁ + X₁' # A] ≤ (ρ[X₁ # A] + ρ[X₁ # A] + d[ X₁ # X₁ ]) / 2 := by    refine (rho_of_sum_le hX₁ hX₁' hA      (by simpa using h_indep.indepFun (show (0 : Fin 4) ≠ 2 by decide))).trans_eq ?_    rw [rho_eq_of_identDistrib h₁.symm, h₁.rdist_congr_right hX₁.aemeasurable]  have : ρ[X₂ + X₂' # A] ≤ (ρ[X₂ # A] + ρ[X₂ # A] + d[ X₂ # X₂ ]) / 2 := by    refine (rho_of_sum_le hX₂ hX₂' hA      (by simpa using h_indep.indepFun (show (1 : Fin 4) ≠ 3 by decide))).trans_eq ?_    rw [rho_eq_of_identDistrib h₂.symm, h₂.rdist_congr_right hX₂.aemeasurable]  have : ρ[X₁ | X₁ + X₁' # A] ≤ (ρ[X₁ # A] + ρ[X₁ # A] + d[ X₁ # X₁ ]) / 2 := by    refine (condRho_of_sum_le hX₁ hX₁' hA      (by simpa using h_indep.indepFun (show (0 : Fin 4) ≠ 2 by decide))).trans_eq ?_    rw [rho_eq_of_identDistrib h₁.symm, h₁.rdist_congr_right hX₁.aemeasurable]  have : ρ[X₂ | X₂ + X₂' # A] ≤ (ρ[X₂ # A] + ρ[X₂ # A] + d[ X₂ # X₂ ]) / 2 := by    refine (condRho_of_sum_le hX₂ hX₂' hA      (by simpa using h_indep.indepFun (show (1 : Fin 4) ≠ 3 by decide))).trans_eq ?_    rw [rho_eq_of_identDistrib h₂.symm, h₂.rdist_congr_right hX₂.aemeasurable]  have : I₂ ≤ η * (d[X₁ # X₁] + d[X₂ # X₂]) := by nlinarith  rw [rdist_add_rdist_eq h₁ h₂ h_indep hX₁ hX₂ hX₁' hX₂'] at this  have one_eta : 0 < 1 - η := by linarith  apply (mul_le_mul_iff_of_pos_left one_eta).1  have : (1 - η) * I₂ ≤ 2 * η * k - I₁ * η := by linarith  apply this.trans_eq  field_simp  ring