cond_construct_good

lemma cond_construct_good :    k ≤ δ' + (p.η/3) * (δ' + c[T₁ | R # T₁ | R] + c[T₂ | R # T₂ | R] + c[T₃ | R # T₃ | R]) := by  cases nonempty_fintype G  rw [delta'_eq_integral, cond_c_eq_integral _ _ _ hT₁ hR, cond_c_eq_integral _ _ _ hT₂ hR,    cond_c_eq_integral _ _ _ hT₃ hR]  simp_rw [integral_fintype .of_finite, ← Finset.sum_add_distrib, ← smul_add, Finset.mul_sum,    mul_smul_comm, ← Finset.sum_add_distrib, ← smul_add]  simp_rw [← integral_fintype .of_finite]  have : IsProbabilityMeasure (Measure.map R ℙ) := Measure.isProbabilityMeasure_map (by fun_prop)  calc    k = (Measure.map R ℙ)[fun _r => k] := by      rw [integral_const]; simp    _ ≤ _ := ?_  simp_rw [integral_fintype .of_finite]  apply Finset.sum_le_sum  intro r _  by_cases hr : ℙ (R⁻¹' {r}) = 0  · simp [Measure.real, Measure.map_apply hR (.singleton r), hr]  simp_rw [smul_eq_mul]  gcongr  have : IsProbabilityMeasure (ℙ[|R ⁻¹' {r}]) := cond_isProbabilityMeasure hr  apply construct_good' p X₁ X₂ h_min hT hT₁ hT₂ hT₃