\begin{lemma}[First estimate]\label{first-estimate}
  \lean{first_estimate}\leanok We have $I_1 \leq 2 \eta k$.
\end{lemma}
\begin{proof}\uses{first-fibre, first-dist-sum, first-cond, first-upper}\leanok  Take a suitable linear combination of \Cref{first-fibre}, \Cref{first-dist-sum}, \Cref{first-cond}, and \Cref{first-upper}.
\end{proof}
/-- We have $I_1 \leq 2 \eta k$ -/
lemma first_estimate
    [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] [IsProbabilityMeasure (ℙ : Measure Ω₀₂)] :
    I₁ ≤ 2 * p.η * k := by
  have v1 := rdist_add_rdist_add_condMutual_eq X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_› ‹_› ‹_› ‹_›
  have v2 := rdist_of_sums_ge p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_› ‹_›
  have v3 := condRuzsaDist_of_sums_ge p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› (by fun_prop) (by aesop)
  have v4 := (mul_le_mul_left p.hη).2 (diff_rdist_le_1 p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_›)
  have v5 := (mul_le_mul_left p.hη).2 (diff_rdist_le_2 p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_›)
  have v6 := (mul_le_mul_left p.hη).2 (diff_rdist_le_3 p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_›)
  have v7 := (mul_le_mul_left p.hη).2 (diff_rdist_le_4 p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_›)
  simp only [inv_eq_one_div] at *
  linarith [v1, v2, v3, v4, v5, v6, v7]

include hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_min in
/--
$$\mathbb{H}[X_1+X_2+\tilde X_1+\tilde X_2] \le \tfrac{1}{2} \mathbb{H}[X_1]+\tfrac{1}{2} \mathbb{H}[X_2] + (2 + \eta) k - I_1.$$
-/