∀ {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {ι : Type u_3} [inst_3 : LinearOrder ι] [LocallyFiniteOrder ι]
  [inst_5 : OrderBot ι] [inst_6 : TopologicalSpace ι] [DiscreteTopology ι] [inst_8 : MeasurableSpace ι] [BorelSpace ι]
  [inst_10 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {ℱ : MeasureTheory.Filtration ι m}
  {τ σ : Ω → WithTop ι} {f : ι → Ω → E} {i : ι},
  MeasureTheory.Martingale f ℱ μ →
    MeasureTheory.IsStoppingTime ℱ τ →
      ∀ (hσ : MeasureTheory.IsStoppingTime ℱ σ) [MeasureTheory.SigmaFinite (μ.trim ⋯)],
        (∀ (x : Ω), τ x ≤ ↑i) →
          μ[MeasureTheory.stoppedValue f τ | hσ.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}]
            MeasureTheory.stoppedValue f τ