dist_of_min_eq_zero'

lemma dist_of_min_eq_zero' (hA : A.Nonempty) (hη' : η < 1 / 8) : d[X₁ # X₂] = 0 := by  let T₁ := X₁ + X₂  let T₂ := X₁ + X₁'  let T₃ := X₁' + X₂  have hsum : T₁ + T₂ + T₃ = 0 := by    have : T₁ + T₂ + T₃ = 2 • (X₁ + X₁' + X₂) := by simp only [T₁, T₂, T₃]; abel    rwa [ZModModule.char_nsmul_eq_zero 2 (X₁ + X₁' + X₂)] at this  let S := X₁ + X₂ + X₁' + X₂'  have J₁ : k ≤ I₁ + 2 * I₂ + η / 3 *      (ρ[T₁ | ⟨T₂, S⟩ # A] + ρ[T₂ | ⟨T₁, S⟩ # A] + ρ[T₁ | ⟨T₃, S⟩ # A] + ρ[T₃ | ⟨T₁, S⟩ # A]        + ρ[T₂ | ⟨T₃, S⟩ # A] + ρ[T₃ | ⟨T₂, S⟩ # A] - 3 * (ρ[X₁ # A] + ρ[X₂ # A])) := by    have K := dist_le_of_sum_zero_cond' h_min S hsum      (by fun_prop) (by fun_prop) (by fun_prop) (by fun_prop)    have : I[T₂ : T₃ | S] = I₂ := by      rw [condMutualInfo_comm (by fun_prop) (by fun_prop)]      have : X₁ + X₁' = X₁' + X₁ := by abel      convert I₃_eq _ _ _ _ hX₁ hX₂ hX₁' hX₂' h₁ h_indep using 2    linarith  have J₂ : k ≤ I₁ + 2 * I₂ +      η / 3 * (k + d[X₁ # X₁'] + d[X₁ # X₂'] + d[X₂ # X₁'] + d[X₂ # X₂'] + d[X₁' # X₂']) := by    apply J₁.trans    gcongr    have W : X₂ + X₁' = X₁' + X₂ := by abel    have := condRho_sum_le' hX₁ hX₂ hX₁' hX₂' h_indep hA    simp only [W] at this    have : ρ[X₁' # A] = ρ[X₁ # A] := rho_eq_of_identDistrib h₁.symm    have : ρ[X₂' # A] = ρ[X₂ # A] := rho_eq_of_identDistrib h₂.symm    linarith  have J₃ : k ≤ I₁ + 2 * I₂ + η / 3 * (6 * k + I₂ - I₁) := by    apply J₂.trans_eq    congr 2    have : d[X₁ # X₁'] = d[X₁ # X₁] := h₁.symm.rdist_congr_right hX₁.aemeasurable    have : d[X₁ # X₂'] = d[X₁ # X₂] := h₂.symm.rdist_congr_right hX₁.aemeasurable    have : d[X₂ # X₁'] = d[X₁ # X₂] := by      rw [rdist_symm]; exact h₁.symm.rdist_congr_left hX₂.aemeasurable    have : d[X₂ # X₂'] = d[X₂ # X₂] := h₂.symm.rdist_congr_right hX₂.aemeasurable    have : d[X₁' # X₂'] = d[X₁ # X₂] := h₁.symm.rdist_congr h₂.symm    have := rdist_add_rdist_eq h₁ h₂ h_indep hX₁ hX₂ hX₁' hX₂'    linarith  let D := 2 * η * k - I₁  have J₄ : k ≤ 8 * η * k - (3 - 10 * η) / (3 * (1 - η)) * D := by    have I₁_eq : I₁ = 2 * η * k - D := by simp only [D]; abel    have : I₂ ≤ 2 * η * k + η / (1 - η) * D :=      I_two_le hη h_min h₁ h₂ h_indep hX₁ hX₂ hX₁' hX₂' hA (by linarith)    calc    k ≤ I₁ + 2 * I₂ + η / 3 * (6 * k + I₂ - I₁) := J₃    _ = 2 * η * k + I₁ + 2 * I₂ + η / 3 * (I₂ - I₁) := by ring    _ ≤ 2 * η * k + (2 * η * k - D) + 2 * (2 * η * k + η / (1 - η) * D)        + η / 3 * ((2 * η * k + η / (1 - η) * D) - (2 * η * k - D)) := by      rw [I₁_eq]      gcongr    _ = 8 * η * k - (3 - 10 * η) / (3 * (1 - η)) * D := by      have : 1 - η ≠ 0 := ne_of_gt (by linarith)      field_simp      ring  have J₅ : k ≤ 8 * η * k - 0 := by    apply J₄.trans    gcongr    have : 0 ≤ D := sub_nonneg_of_le (I_one_le hη h_min h₁ h₂ h_indep hX₁ hX₂ hX₁' hX₂' hA)    apply mul_nonneg _ this    exact div_nonneg (by linarith) (by linarith)  have : k ≤ 0 := by nlinarith  exact le_antisymm this (rdist_nonneg hX₁ hX₂)