Stopped Value min ae eq cond Exp of discrete Approx Sequence

theorem stoppedValue_min_ae_eq_condExp_of_discreteApproxSequence    (h : Martingale X 𝓕 μ) (hRC : ∀ ω, IsRightContinuous (X · ω))    (hτ : IsStoppingTime 𝓕 τ) (hσ : IsStoppingTime 𝓕 σ) {n : ι} (hτ_le : ∀ x, τ x ≤ n)    (τn : DiscreteApproxSequence 𝓕 τ μ) (σn : DiscreteApproxSequence 𝓕 σ μ) :    (stoppedValue X fun x ↦ min (τ x) (σ x)) =ᵐ[μ] μ[stoppedValue X τ|hσ.measurableSpace] := by  set τn' := (discreteApproxSequence_of 𝓕 hτ_le τn).inf σn  have hint (m : ℕ) : stoppedValue X (τn' m) =ᵐ[μ]      μ[stoppedValue X (discreteApproxSequence_of 𝓕 hτ_le τn m) |        (σn.isStoppingTime m).measurableSpace] := by    refine EventuallyEq.trans (Eq.eventuallyEq ?_)      (h.stoppedValue_min_ae_eq_condExp_of_countable_range hRC        ((discreteApproxSequence_of 𝓕 hτ_le τn).isStoppingTime m)        (σn.isStoppingTime m) (discreteApproxSequence_of_le hτ_le τn m)        (DiscreteApproxSequence.countable _ _) (σn.countable m))    congr 1; ext ω; rw [min_comm]; rfl  have hintgbl : Integrable (stoppedValue X τ) μ :=    integrable_stoppedValue_of_discreteApproxSequence' h hRC hτ_le τn  refine ae_eq_condExp_of_forall_setIntegral_eq _ hintgbl ?_ ?_    ((measurable_stoppedValue (h.stronglyAdapted.isStronglyProgressive_of_rightContinuous hRC)      (hτ.min hσ)).mono ((hτ.min hσ).measurableSpace_mono hσ <| fun ω ↦ min_le_right _ _)      le_rfl).aestronglyMeasurable  · exact fun s hs _ ↦ (integrable_stoppedValue_of_discreteApproxSequence' h hRC      (fun _ ↦ min_le_of_left_le <| hτ_le _) <| τn.inf σn).integrableOn  rintro s hs -  have : (fun m ↦ ∫ ω in s, stoppedValue X (τn' m) ω ∂μ) =    fun m ↦ ∫ ω in s, stoppedValue X (discreteApproxSequence_of 𝓕 hτ_le τn m) ω ∂μ := by    ext m    rw [setIntegral_congr_ae (g := μ[stoppedValue X (discreteApproxSequence_of 𝓕 hτ_le τn m) |        (σn.isStoppingTime m).measurableSpace]) (hσ.measurableSpace_le _ hs)        (by filter_upwards [hint m] with ω hω _ using hω)]    exact setIntegral_condExp _      (h.integrable_stoppedValue_of_countable_range _        (DiscreteApproxSequence.isStoppingTime _ _) (discreteApproxSequence_of_le hτ_le τn m)        (DiscreteApproxSequence.countable _ m))      (hσ.measurableSpace_mono (σn.isStoppingTime m) (σn.le m) _ hs)  refine tendsto_nhds_unique (f := (fun m ↦ ∫ (ω : Ω) in s, stoppedValue X (τn' m) ω ∂μ))    (l := atTop) ?_ (this ▸ ?_)  · refine tendsto_setIntegral_of_L1' _ (integrable_stoppedValue_of_discreteApproxSequence' h hRC        (fun _ ↦ min_le_of_left_le <| hτ_le _) τn').aestronglyMeasurable ?_      (tendsto_eLpNorm_stoppedValue_of_discreteApproxSequence_of_le h hRC τn'        (τn.discreteApproxSequence_of_le_inf_le_of_left σn hτ_le)) _    rw [eventually_atTop]    exact ⟨0, fun m _ ↦ (h.integrable_stoppedValue_of_countable_range _      (DiscreteApproxSequence.isStoppingTime _ _)      (τn.discreteApproxSequence_of_le_inf_le_of_left σn hτ_le m)      (DiscreteApproxSequence.countable _ m))⟩  · refine tendsto_setIntegral_of_L1' _ hintgbl.aestronglyMeasurable ?_      (tendsto_eLpNorm_stoppedValue_of_discreteApproxSequence h hRC hτ_le τn) _    rw [eventually_atTop]    exact ⟨0, fun m _ ↦ (h.integrable_stoppedValue_of_countable_range _        (DiscreteApproxSequence.isStoppingTime _ _) (discreteApproxSequence_of_le hτ_le τn m)        (DiscreteApproxSequence.countable _ m))⟩