construct_good_prelim'

lemma construct_good_prelim' : k ≤ δ + p.η * c[T₁ | T₃ # T₂ | T₃] := by  let sum1 : ℝ := (Measure.map T₃ ℙ)[fun t ↦ d[T₁; ℙ[|T₃ ⁻¹' {t}] # T₂; ℙ[|T₃ ⁻¹' {t}]]]  let sum2 : ℝ := (Measure.map T₃ ℙ)[fun t ↦ d[p.X₀₁; ℙ # T₁; ℙ[|T₃ ⁻¹' {t}]] - d[p.X₀₁ # X₁]]  let sum3 : ℝ := (Measure.map T₃ ℙ)[fun t ↦ d[p.X₀₂; ℙ # T₂; ℙ[|T₃ ⁻¹' {t}]] - d[p.X₀₂ # X₂]]  let sum4 : ℝ := (Measure.map T₃ ℙ)[fun t ↦ ψ[T₁; ℙ[|T₃ ⁻¹' {t}] # T₂; ℙ[|T₃ ⁻¹' {t}]]]  have h2T₃ : T₃ = T₁ + T₂ := by    calc T₃ = T₁ + T₂ + T₃ - T₃ := by simp [hT, ZModModule.neg_eq_self]      _ = T₁ + T₂ := by rw [add_sub_cancel_right]  have hP : IsProbabilityMeasure (Measure.map T₃ ℙ) :=    Measure.isProbabilityMeasure_map hT₃.aemeasurable  -- control sum1 with entropic BSG  have h1 : sum1 ≤ δ := by    have h1 : sum1 ≤ 3 * I[T₁ : T₂] + 2 * H[T₃] - H[T₁] - H[T₂] := by      subst h2T₃; exact ent_bsg hT₁ hT₂    have h2 : H[⟨T₂, T₃⟩] = H[⟨T₁, T₂⟩] := by      rw [h2T₃, entropy_add_right', entropy_comm] <;> assumption    have h3 : H[⟨T₁, T₂⟩] = H[⟨T₃, T₁⟩] := by      rw [h2T₃, entropy_add_left, entropy_comm] <;> assumption    simp_rw [mutualInfo_def] at h1 ⊢; linarith  -- rewrite sum2 and sum3 as Rusza distances  have h2 : sum2 = d[p.X₀₁ # T₁ | T₃] - d[p.X₀₁ # X₁] := by    simp only [sum2, integral_sub .of_finite .of_finite, integral_const, smul_eq_mul]    simp [condRuzsaDist'_eq_sum hT₁ hT₃,      integral_eq_setIntegral (FiniteRange.ae_mem_toFinset _ T₃), setIntegral_finset _ .finset,      map_measureReal_apply hT₃ (.singleton _), smul_eq_mul]  have h3 : sum3 = d[p.X₀₂ # T₂ | T₃] - d[p.X₀₂ # X₂] := by    simp only [sum3, integral_sub .of_finite .of_finite, integral_const, smul_eq_mul]    simp [condRuzsaDist'_eq_sum hT₂ hT₃,      integral_eq_setIntegral (FiniteRange.ae_mem_toFinset _ T₃), setIntegral_finset _ .finset,      map_measureReal_apply hT₃ (.singleton _)]  -- put all these estimates together to bound sum4  have h4 : sum4 ≤ δ + p.η * ((d[p.X₀₁ # T₁ | T₃] - d[p.X₀₁ # X₁])      + (d[p.X₀₂ # T₂ | T₃] - d[p.X₀₂ # X₂])) := by    have : sum4 = sum1 + p.η * (sum2 + sum3) := by      simp only [sum1, sum2, sum3, sum4, integral_add .of_finite .of_finite, integral_const_mul]    rw [this, h2, h3, add_assoc, mul_add]    linarith  have hk : k ≤ sum4 := by    suffices (Measure.map T₃ ℙ)[fun _ ↦ k] ≤ sum4 by simpa using this    refine integral_mono_ae .of_finite .of_finite <| ae_iff_of_countable.2 fun t ht ↦ ?_    have : IsProbabilityMeasure (ℙ[|T₃ ⁻¹' {t}]) :=      cond_isProbabilityMeasure (by simpa [hT₃] using ht)    dsimp only    linarith only [distance_ge_of_min' (μ := ℙ[|T₃ ⁻¹' {t}]) (μ' := ℙ[|T₃ ⁻¹' {t}]) p h_min hT₁ hT₂]  exact hk.trans h4