\begin{lemma}[Entropy bound on quadruple sum]\label{foursum-bound}
  \lean{ent_ofsum_le}\leanok
  With the same notation, we have
  \begin{equation}
    \label{HS-bound}
    \bbH[X_1+X_2+\tilde X_1+\tilde X_2] \le \tfrac{1}{2} \bbH[X_1]+\tfrac{1}{2} \bbH[X_2] + (2 + \eta) k - I_1.
  \end{equation}
\end{lemma}
\begin{proof}\uses{first-cond, first-fibre, first-upper, ruz-indep}\leanok
  Subtracting \Cref{first-cond} from \Cref{first-fibre}, and combining the resulting inequality with \Cref{first-upper} gives the bound
\[
  d[X_1+\tilde X_2;X_2+\tilde X_1] \le (1 + \eta) k - I_1,
\]
and the claim follows from \Cref{ruz-indep} and the definition of $k$.
\end{proof}
lemma ent_ofsum_le
    [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] [IsProbabilityMeasure (ℙ : Measure Ω₀₂)] :
    H[X₁ + X₂ + X₁' + X₂'] ≤ H[X₁]/2 + H[X₂]/2 + (2+p.η)*k - I₁ := by
  let D := d[X₁ + X₂' # X₂ + X₁']
  let Dcc := d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁']
  let D1 := d[p.X₀₁ # X₁]
  let Dc1 := d[p.X₀₁ # X₁ | X₁ + X₂']
  let D2 := d[p.X₀₂ # X₂]
  let Dc2 := d[p.X₀₂ # X₂ | X₂ + X₁']
  have lem68 : D + Dcc + I₁ = 2 * k :=
    rdist_add_rdist_add_condMutual_eq _ _ _ _ hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep
  have lem610 : Dcc ≥ k - p.η * (Dc1 - D1) - p.η * (Dc2 - D2) :=
    condRuzsaDist_of_sums_ge p X₁ X₂ X₁' X₂' hX₁ hX₂ (by fun_prop) (by aesop) h_min
  have lem611c : Dc1 - D1 ≤ k / 2 + H[X₁] / 4 - H[X₂] / 4 :=
    diff_rdist_le_3 p X₁ X₂ X₁' X₂' hX₁ hX₂' h₂ h_indep
  have lem611d : Dc2 - D2 ≤ k / 2 + H[X₂] / 4 - H[X₁] / 4 :=
    diff_rdist_le_4 p X₁ X₂ X₁' X₂' hX₂ hX₁' h₁ h_indep
  have aux : D + I₁ ≤ (1 + p.η) * k := by
    calc D + I₁
       ≤ k + p.η * (Dc1 - D1) + p.η * (Dc2 - D2) := ?_
     _ ≤ k + p.η * (k / 2 + H[X₁] / 4 - H[X₂] / 4) + p.η * (k / 2 + H[X₂] / 4 - H[X₁] / 4) := ?_
     _ = (1 + p.η) * k := by ring
    · convert add_le_add lem68.le (neg_le_neg lem610) using 1 <;> ring
    · refine add_le_add (add_le_add (le_refl _) ?_) ?_
      · apply (mul_le_mul_left p.hη).mpr lem611c
      · apply (mul_le_mul_left p.hη).mpr lem611d
  have ent_sub_eq_ent_add : H[X₁ + X₂' - (X₂ + X₁')] = H[X₁ + X₂' + (X₂ + X₁')] := by
    simp [ZModModule.sub_eq_add]
  have rw₁ : X₁ + X₂' + (X₂ + X₁') = X₁ + X₂ + X₁' + X₂' := by abel
  have ind_aux : IndepFun (X₁ + X₂') (X₂ + X₁') := by
    exact iIndepFun.indepFun_add_add h_indep (fun i ↦ by fin_cases i <;> assumption) 0 2 1 3
      (by decide) (by decide) (by decide) (by decide)
  have ind : D = H[X₁ + X₂' - (X₂ + X₁')] - H[X₁ + X₂'] / 2 - H[X₂ + X₁'] / 2 :=
    ind_aux.rdist_eq (by fun_prop) (by fun_prop)
  rw [ind, ent_sub_eq_ent_add, rw₁] at aux
  have obs : H[X₁ + X₂ + X₁' + X₂'] ≤ H[X₁ + X₂'] / 2 + H[X₂ + X₁'] / 2 + (1 + p.η) * k - I₁ := by
    linarith
  have rw₂ : H[X₁ + X₂'] = k + H[X₁]/2 + H[X₂]/2 := by
    have HX₂_eq : H[X₂] = H[X₂'] :=
      congr_arg (fun (μ : Measure G) ↦ measureEntropy (μ := μ)) h₂.map_eq
    have k_eq : k = H[X₁ - X₂'] - H[X₁] / 2 - H[X₂'] / 2 := by
      have k_eq_aux : k = d[X₁ # X₂'] := (IdentDistrib.refl hX₁.aemeasurable).rdist_eq h₂
      rw [k_eq_aux]
      exact (h_indep.indepFun (show (0 : Fin 4) ≠ 2 by decide)).rdist_eq hX₁ hX₂'
    rw [k_eq, ← ZModModule.sub_eq_add, ← HX₂_eq]
    ring
  have rw₃ : H[X₂ + X₁'] = k + H[X₁]/2 + H[X₂]/2 := by
    have HX₁_eq : H[X₁] = H[X₁'] :=
      congr_arg (fun (μ : Measure G) ↦ measureEntropy (μ := μ)) h₁.map_eq
    have k_eq' : k = H[X₁' - X₂] - H[X₁'] / 2 - H[X₂] / 2 := by
      have k_eq_aux : k = d[X₁' # X₂] :=
        IdentDistrib.rdist_eq h₁ (IdentDistrib.refl hX₂.aemeasurable)
      rw [k_eq_aux]
      exact IndepFun.rdist_eq (h_indep.indepFun (show (3 : Fin 4) ≠ 1 by decide)) hX₁' hX₂
    rw [add_comm X₂ X₁', k_eq', ← ZModModule.sub_eq_add, ← HX₁_eq]
    ring
  calc H[X₁ + X₂ + X₁' + X₂']
      ≤ H[X₁ + X₂'] / 2 + H[X₂ + X₁'] / 2 + (1 + p.η) * k - I₁  := obs
    _ = (k + H[X₁] / 2 + H[X₂] / 2) / 2
        + (k + H[X₁] / 2 + H[X₂] / 2) / 2 + (1 + p.η) * k - I₁  := by rw [rw₂, rw₃]
    _ = H[X₁] / 2 + H[X₂] / 2 + (2 + p.η) * k - I₁              := by ring