\begin{lemma}\label{phi-first-estimate}\lean{I_one_le}\leanok
$I_1\le 2\eta d[X_1;X_2]$
\end{lemma}
\begin{proof}\leanok
  \uses{phi-min-def,first-fibre}
Similar to \Cref{first-estimate}: get upper bounds for $d[X_1;X_2]$ by $\phi[X_1;X_2]\le \phi[X_1+X_2;\tilde X_1+\tilde X_2]$ and $\phi[X_1;X_2]\le \phi[X_1|X_1+X_2;\tilde X_2|\tilde X_1+\tilde X_2]$, and then apply \Cref{first-fibre} to get an upper bound for $I_1$.
\end{proof}
/-- $I_1\le 2\eta d[X_1;X_2]$ -/
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₂, (IdentDistrib.refl hX₁.aemeasurable).rdist_eq h₂]
    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_eq (IdentDistrib.refl 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₂, (IdentDistrib.refl hX₁.aemeasurable).rdist_eq h₂]
    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_eq (IdentDistrib.refl hX₂.aemeasurable)]
    linarith
  nlinarith

/- *****************************************
Second estimate
********************************************* -/

include hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep in