dist_of_min_eq_zero

theorem dist_of_min_eq_zero (hA : A.Nonempty) (hη' : η < 1 / 8) : d[X₁ # X₂] = 0 := by  let ⟨Ω', m', μ, Y₁, Y₂, Y₁', Y₂', hμ, h_indep, hY₁, hY₂, hY₁', hY₂', h_id1, h_id2, h_id1', h_id2'⟩    := independent_copies4_nondep hX₁ hX₂ hX₁ hX₂ ℙ ℙ ℙ ℙ  rw [← h_id1.rdist_congr h_id2]  let _ : MeasureSpace Ω' := ⟨μ⟩  have : IsProbabilityMeasure (ℙ : Measure Ω') := hμ  have h'_min : phiMinimizes Y₁ Y₂ η A ℙ := phiMinimizes_of_identDistrib h_min h_id1.symm h_id2.symm  exact dist_of_min_eq_zero' hη h'_min (h_id1.trans h_id1'.symm) (h_id2.trans h_id2'.symm)     h_indep hY₁ hY₂ hY₁' hY₂'  hA hη'