\begin{lemma}\label{second-estimate-aux}\lean{second_estimate_aux}\leanok
We have
\[d[X_1;X_1] + d[X_2;X_2] \leq 2 k + \frac{2(2 \eta k - I_1)}{1-\eta}. \]
\end{lemma}
\begin{proof}
\uses{ruz-indep, foursum-bound, dist-sums}\leanok
We may use \Cref{ruz-indep} to expand
  \begin{align*}
   & d[X_1+\tilde X_1;X_2+\tilde X_2] \\ &= \bbH[X_1+\tilde X_1 + X_2 + \tilde X_2]  - \tfrac{1}{2} \bbH[X_1+\tilde X_1] - \tfrac{1}{2} \bbH[X_2+\tilde X_2] \\
    &= \bbH[X_1+\tilde X_1 + X_2 + \tilde X_2]  - \tfrac{1}{2} \bbH[X_1] - \tfrac{1}{2} \bbH[X_2]  \\ & \qquad\qquad\qquad   - \tfrac{1}{2} \left( d[X_1;X_1] + d[X_2; X_2] \right),
  \end{align*}
  and hence by \Cref{foursum-bound}
  \[
    d[X_1+\tilde X_1; X_2+\tilde X_2] \leq (2+\eta) k - \tfrac{1}{2} \left( d[X_1;X_1] + d[X_2;X_2] \right) - I_1.
  \]
  Combining this bound with \Cref{dist-sums} we obtain
  the result.
\end{proof}
lemma second_estimate_aux :
    d[X₁ # X₁] + d[X₂ # X₂] ≤ 2 * (k + (2 * p.η * k - I₁) / (1 - p.η)) := by
  have hX₁_indep : IndepFun X₁ X₁' (μ := ℙ) := h_indep.indepFun (show 0 ≠ 2 by decide)
  have hX₂_indep : IndepFun X₂ X₂' (μ := ℙ) := h_indep.indepFun (show 1 ≠ 3 by decide)
  have hX_indep : IndepFun (X₁ + X₁') (X₂ + X₂') := by
    exact h_indep.indepFun_add_add (ι := Fin 4) (by intro i; fin_cases i <;> assumption) 0 2 1 3
      (by decide) (by decide) (by decide) (by decide)
  have h : d[X₁ + X₁' # X₂+ X₂'] ≤ (2 + p.η) * k - (d[X₁# X₁] + d[X₂ # X₂]) / 2 - I₁ := by
    have h := hX_indep.rdist_eq (hX₁.add hX₁') (hX₂.add hX₂')
    rw [ZModModule.sub_eq_add (X₁ + X₁') (X₂ + X₂'), ← ZModModule.sub_eq_add X₁ X₁',
      ← ZModModule.sub_eq_add X₂ X₂',
      sub_eq_iff_eq_add.mp (sub_eq_iff_eq_add.mp (hX₁_indep.rdist_eq hX₁ hX₁').symm),
      sub_eq_iff_eq_add.mp (sub_eq_iff_eq_add.mp (hX₂_indep.rdist_eq hX₂ hX₂').symm),
      ← h₁.entropy_eq, ← h₂.entropy_eq, add_assoc, add_assoc, add_halves, add_halves,
      ← (IdentDistrib.refl hX₁.aemeasurable).rdist_eq h₁,
      ← (IdentDistrib.refl hX₂.aemeasurable).rdist_eq h₂,
      ZModModule.sub_eq_add X₁ X₁', ZModModule.sub_eq_add X₂ X₂', ← add_assoc, add_right_comm _ X₁']
        at h
    have h_indep' : iIndepFun ![X₁, X₂, X₂', X₁'] :=
      by exact h_indep.reindex_four_abdc
    have h' := ent_ofsum_le p X₁ X₂ X₁' X₂' hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep' h_min
    convert (h.symm ▸ (sub_le_sub_right (sub_le_sub_right h' _) _)) using 1; ring
  have h' := (rdist_of_sums_ge' p X₁ X₂ X₁' X₂' hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep h_min).le.trans h
  rw [← div_le_iff₀' two_pos, ← sub_le_iff_le_add', le_div_iff₀ (by linarith [p.hη'])]
  linarith

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