Stopped Value predictable Part tau Mesh le

lemma stoppedValue_predictablePart_tauMesh_le {ι Ω : Type*} [TopologicalSpace ι]    [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {mΩ : MeasurableSpace Ω}    (S : ι → Ω → ℝ) (𝓕 : Filtration ι mΩ) (P : Measure Ω) (n : ℕ) {c : ℝ} (hc : 0 ≤ c) :    stoppedValue (predictablePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P)      (tauMesh S 𝓕 P n c) ≤ fun _ ↦ c := by  intro ω  let A := predictablePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P  let τ := hittingBtwn (fun t ω ↦ A (succ t) ω) (Set.Ioi c) ⊥ ⊤ ω  change A τ ω ≤ c  by_cases hτ_bot : τ = ⊥  · simpa [A, hτ_bot] using hc  · have hpred_lt : pred τ < τ := (pred_lt_iff_ne_bot).2 hτ_bot    have hnot_min : ¬ IsMin τ := by simpa [isMin_iff_eq_bot] using hτ_bot    simpa [succ_pred_of_not_isMin hnot_min] using notMem_of_lt_hittingBtwn hpred_lt bot_le