\begin{lemma}\label{phi-second-estimate}\lean{I_two_le}\leanok
$I_2\le 2\eta d[X_1;X_2] + \frac{\eta}{1-\eta}(2\eta d[X_1;X_2]-I_1)$.
\end{lemma}
\begin{proof}\leanok
  \uses{phi-min-def,cor-fibre,I1-I2-diff}
First of all, by $\phi[X_1;X_2]\le \phi[X_1+\tilde X_1;X_2+\tilde X_2]$, $\phi[X_1;X_2]\le \phi[X_1|X_1+\tilde X_1;X_2|X_2+\tilde X_2]$, and the fibring identity obtained by applying \Cref{cor-fibre} on $(X_1,X_2,\tilde X_1,\tilde X_2)$,
we have $I_2\le \eta (d[X_1;X_1]+d[X_2;X_2])$. Then apply \Cref{I1-I2-diff} to get $I_2\le 2\eta d[X_1;X_2] +\eta(I_2-I_1)$, and rearrange.
\end{proof}
/-- $I_2\le 2\eta d[X_1;X_2] + \frac{\eta}{1-\eta}(2\eta d[X_1;X_2]-I_1)$. -/
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,
      IdentDistrib.rdist_eq (IdentDistrib.refl hX₁.aemeasurable) h₁]
  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,
      IdentDistrib.rdist_eq (IdentDistrib.refl hX₂.aemeasurable) h₂]
  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,
      IdentDistrib.rdist_eq (IdentDistrib.refl hX₁.aemeasurable) h₁]
  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,
      IdentDistrib.rdist_eq (IdentDistrib.refl hX₂.aemeasurable) h₂]
  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

/- ****************************************
End Game
******************************************* -/

include h_min in
omit [IsProbabilityMeasure (ℙ : Measure Ω)] in
/-- If $G$-valued random variables $T_1,T_2,T_3$ satisfy $T_1+T_2+T_3=0$, then
  $$d[X_1;X_2]\le 3\bbI[T_1:T_2\mid T_3] + (2\bbH[T_3]-\bbH[T_1]-\bbH[T_2])+ \eta(\rho(T_1|T_3)+\rho(T_2|T_3)-\rho(X_1)-\rho(X_2)).$$ -/