dist_diff_bound_2

lemma dist_diff_bound_2 :      ((d[p.X₀₂ # U | ⟨V, S⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # U | ⟨W, S⟩] - d[p.X₀₂ # X₂])    + (d[p.X₀₂ # V | ⟨U, S⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # V | ⟨W, S⟩] - d[p.X₀₂ # X₂])    + (d[p.X₀₂ # W | ⟨U, S⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # W | ⟨V, S⟩] - d[p.X₀₂ # X₂]))    ≤ (16 * k + 6 * d[X₂ # X₂] + 2 * d[X₁ # X₁]) / 4 + (H[X₂ + X₂'] - H[X₁ + X₁']) / 4      + (H[X₁ | X₁ + X₁'] - H[X₂ | X₂ + X₂']) / 4 := by  have I1 := gen_ineq_01 p.X₀₂ p.hmeas2 X₂ X₁ X₂' X₁' hX₂ hX₁ hX₂' hX₁' h_indep.reindex_four_bacd  have I2 := gen_ineq_00 p.X₀₂ p.hmeas2 X₂ X₁ X₁' X₂' hX₂ hX₁ hX₁' hX₂' h_indep.reindex_four_badc  have I3 := gen_ineq_10 p.X₀₂ p.hmeas2 X₂ X₂' X₁ X₁' hX₂ hX₂' hX₁ hX₁' h_indep.reindex_four_bcad  have I4 := gen_ineq_10 p.X₀₂ p.hmeas2 X₂ X₂' X₁' X₁ hX₂ hX₂' hX₁' hX₁ h_indep.reindex_four_bcda  have I5 := gen_ineq_00 p.X₀₂ p.hmeas2 X₂ X₁' X₁ X₂' hX₂ hX₁' hX₁ hX₂' h_indep.reindex_four_bdac  have I6 := gen_ineq_01 p.X₀₂ p.hmeas2 X₂ X₁' X₂' X₁ hX₂ hX₁' hX₂' hX₁ h_indep.reindex_four_bdca  have C1 : X₂ + X₁ = X₁ + X₂ := by abel  have C2 : X₁ + X₁' = W := by abel  have C3 : U + X₂' + X₁' = S := by abel  have C4 : X₂ + X₁' = V := by abel  have C5 : X₂ + X₂' + X₁ + X₁' = S := by abel  have C6 : X₂ + X₂' + X₁' + X₁ = S := by abel  have C7 : V + X₁ + X₂' = S := by abel  have C8 : V + X₂' + X₁ = S := by abel  have C9 : d[X₂ # X₁] = d[X₁ # X₂] := rdist_symm  have C10 : d[X₁ # X₂'] = d[X₁ # X₂] := h₂.symm.rdist_congr_right hX₁.aemeasurable  have C11 : d[X₂ # X₁'] = d[X₁ # X₂] := by    rw [rdist_symm]    exact h₁.symm.rdist_congr_left hX₂.aemeasurable  have C12 : d[X₂' # X₁'] = d[X₁' # X₂'] := rdist_symm  have C13 : d[X₂' # X₁] = d[X₁ # X₂'] := rdist_symm  have C14 : d[X₁' # X₁] = d[X₁ # X₁'] := rdist_symm  have C15 : d[X₁' # X₂'] = d[X₁ # X₂] := h₁.symm.rdist_congr h₂.symm  have C16 : H[X₁' + X₂'] = H[X₁ + X₂] := by    apply ProbabilityTheory.IdentDistrib.entropy_congr    have I : IdentDistrib (⟨X₁, X₂⟩) (⟨X₁', X₂'⟩) := h₁.prodMk h₂ (h_indep.indepFun zero_ne_one)        (h_indep.indepFun (show 3 ≠ 2 by decide))    exact I.symm.comp measurable_add  have C17 : H[X₂' + X₁'] = H[X₁ + X₂] := by rw [add_comm]; exact C16  have C18 : H[X₁'] = H[X₁] := h₁.symm.entropy_congr  have C19 : H[X₂'] = H[X₂] := h₂.symm.entropy_congr  have C20 : H[X₁ + X₂'] = H[X₁ + X₂] := by    apply ProbabilityTheory.IdentDistrib.entropy_congr    have I : IdentDistrib (⟨X₁, X₂'⟩) (⟨X₁, X₂⟩) :=      (IdentDistrib.refl hX₁.aemeasurable).prodMk h₂.symm      (h_indep.indepFun (show 0 ≠ 2 by decide)) (h_indep.indepFun zero_ne_one)    exact I.comp measurable_add  have C21 : H[X₁' | W] = H[X₁ | W] := by    conv_rhs => rw [add_comm]    apply IdentDistrib.condEntropy_eq hX₁' (hX₁'.add hX₁) hX₁ (hX₁.add hX₁')    have I : IdentDistrib (⟨X₁', X₁⟩) (⟨X₁, X₁'⟩) := h₁.symm.prodMk h₁        (h_indep.indepFun (show 3 ≠ 0 by decide)) (h_indep.indepFun (show 0 ≠ 3 by decide))    exact I.comp (measurable_fst.prodMk measurable_add)  have C22 : H[X₂' | X₂' + X₁] = H[X₂ | X₁ + X₂] := by    rw [add_comm]    apply IdentDistrib.condEntropy_eq hX₂' (hX₁.add hX₂') hX₂ (hX₁.add hX₂)    have I : IdentDistrib (⟨X₁, X₂'⟩) (⟨X₁, X₂⟩) :=      (IdentDistrib.refl hX₁.aemeasurable).prodMk h₂.symm      (h_indep.indepFun (show 0 ≠ 2 by decide)) (h_indep.indepFun zero_ne_one)    exact I.comp (measurable_snd.prodMk measurable_add)  have C23 : H[X₁ | X₁ + X₂'] = H[X₁ | X₁ + X₂] := by    apply IdentDistrib.condEntropy_eq hX₁ (hX₁.add hX₂') hX₁ (hX₁.add hX₂)    have I : IdentDistrib (⟨X₁, X₂'⟩) (⟨X₁, X₂⟩) :=      (IdentDistrib.refl hX₁.aemeasurable).prodMk h₂.symm      (h_indep.indepFun (show 0 ≠ 2 by decide)) (h_indep.indepFun zero_ne_one)    exact I.comp (measurable_fst.prodMk measurable_add)  have C24 : H[X₂ | V] = H[X₂ | X₁ + X₂] := by    apply IdentDistrib.condEntropy_eq hX₂ (hX₁'.add hX₂) hX₂ (hX₁.add hX₂)    have I : IdentDistrib (⟨X₁', X₂⟩) (⟨X₁, X₂⟩) :=      h₁.symm.prodMk (IdentDistrib.refl hX₂.aemeasurable)      (h_indep.indepFun (show 3 ≠ 1 by decide)) (h_indep.indepFun zero_ne_one)    exact I.comp (measurable_snd.prodMk measurable_add)  have C25 : H[X₂' | X₂' + X₁'] = H[X₂ | X₁ + X₂] := by    rw [add_comm]    apply IdentDistrib.condEntropy_eq hX₂' (hX₁'.add hX₂') hX₂ (hX₁.add hX₂)    have I : IdentDistrib (⟨X₁', X₂'⟩) (⟨X₁, X₂⟩) := h₁.symm.prodMk h₂.symm        (h_indep.indepFun (show 3 ≠ 2 by decide)) (h_indep.indepFun zero_ne_one)    exact I.comp (measurable_snd.prodMk measurable_add)  have C26 : H[X₁' | X₁' + X₂'] = H[X₁ | X₁ + X₂] := by    apply IdentDistrib.condEntropy_eq hX₁' (hX₁'.add hX₂') hX₁ (hX₁.add hX₂)    have I : IdentDistrib (⟨X₁', X₂'⟩) (⟨X₁, X₂⟩) := h₁.symm.prodMk h₂.symm      (h_indep.indepFun (show 3 ≠ 2 by decide)) (h_indep.indepFun zero_ne_one)    exact I.comp (measurable_fst.prodMk measurable_add)  have C27 : H[X₂ | X₁ + X₂] = H[X₁ | X₁ + X₂] := by    have := condEntropy_of_injective ℙ hX₁ (hX₁.add hX₂) _ (fun p ↦ add_right_injective p)    convert! this with ω    simp [add_comm (X₁ ω), add_assoc (X₂ ω), ZModModule.add_self]  have C28 : H[V] = H[U] := by    apply ProbabilityTheory.IdentDistrib.entropy_congr    have I : IdentDistrib (⟨X₁', X₂⟩) (⟨X₁, X₂⟩) :=      h₁.symm.prodMk (IdentDistrib.refl hX₂.aemeasurable)      (h_indep.indepFun (show 3 ≠ 1 by decide)) (h_indep.indepFun zero_ne_one)    exact I.comp measurable_add  have C29 : H[X₂' + X₁] = H[X₁ + X₂] := by    rw [add_comm]    apply ProbabilityTheory.IdentDistrib.entropy_congr    have I : IdentDistrib (⟨X₁, X₂'⟩) (⟨X₁, X₂⟩) :=      (IdentDistrib.refl hX₁.aemeasurable).prodMk h₂.symm      (h_indep.indepFun (show 0 ≠ 2 by decide)) (h_indep.indepFun zero_ne_one)    exact I.comp measurable_add  have C30 : d[X₁ # X₁'] = d[X₁ # X₁] := h₁.symm.rdist_congr_right hX₁.aemeasurable  have C31 : d[X₂ # X₂'] = d[X₂ # X₂] := h₂.symm.rdist_congr_right hX₂.aemeasurable  simp only [C1, C2, C3, C4, C5, C6, C7, C8, C9, C10, C11, C12, C13, C14, C15, C16, C17, C18, C19,    C20, C21, C22, C23, C24, C25, C26, C27, C28, C29, C30, C31]    at I1 I2 I3 I4 I5 I6 ⊢  linarith only [I1, I2, I3, I4, I5, I6]