RS_prime.pre_413_measure_inter

lemma pre_413_measure_inter {x : ℝ} (hx : 2 ≤ x) (y : Finset.Ico 1 ⌊x⌋₊) :    «θ».Stieltjes.measure.real (Set.Ioc (↑↑y) (↑↑y + 1) ∩ Set.Icc 2 x) = if Nat.Prime (y + 1) then Real.log (↑y + 1) else 0 := by  by_cases y_eq: y.val = 1  · simp only [y_eq, cast_one, reduceAdd]    norm_num    conv =>      arg 1      arg 2      equals Set.Icc 2 2 =>        ext a        simp        have foo := y.prop        rw [Finset.mem_Ico] at foo        grind    rw [Measure.real_def]    simp only [«θ».Stieltjes, Set.Icc_self, StieltjesFunction.measure_singleton,      theta_two]    conv =>      lhs      arg 1      arg 1      rhs      arg 2      equals ↑(1: ℕ) + (1: ℝ) => norm_num    rw [leftLim_theta_succ]    simp [Real.log_nonneg]  · rw [Measure.real_def, MeasureTheory.measure_eq_measure_of_null_sdiff (t := Set.Ioc (↑↑y) (↑↑y + 1))]    · simp only [«θ».Stieltjes, StieltjesFunction.measure_Ioc, theta_succ_sub,      ENNReal.toReal_ofReal_eq_iff]      split_ifs      · simp [Real.log_nonneg]      · simp    · simp    · simp      conv =>        arg 1        arg 2        equals ∅ =>          ext a          simp only [Set.mem_sdiff, Set.mem_Ioc, Set.mem_Icc, not_and, not_le,            Set.mem_empty_iff_false, iff_false, Classical.not_imp, not_lt, and_imp]          intro ha hb          have y_prop := y.property          rw [Finset.mem_Ico] at y_prop           have y_lt: (2: ℝ) ≤ y.val := by            norm_cast            omega          refine ⟨?_, ?_⟩          · grw [y_lt]            linarith          · grw [hb]            have bar := y_prop.2            rw [← Nat.add_one_le_iff] at bar            norm_cast            grw [bar]            apply Nat.floor_le            linarith      simp