Maximal ineq finset

lemma maximal_ineq_finset (hsub : Submartingale Y 𝓕 P) (hnonneg : 0 ≤ Y) (ε : ℝ≥0) {n : ι}    {J : Finset ι} (hJn : ∀ i ∈ J, i ≤ n) (hnJ : n ∈ J) :    ε • P.real {ω | (ε : ℝ) ≤ J.sup' ⟨n, hnJ⟩ fun i ↦ Y i ω} ≤     ∫ ω in {ω | (ε : ℝ) ≤ J.sup' ⟨n, hnJ⟩ fun i ↦ Y i ω}, Y n ω ∂P := by  -- Convert to ℕ-indexed submartingale defined by (Y(j₁), ⋯, Y(jₘ), Y(n), Y(n), ⋯)  -- where J = {j₁, ⋯, jₘ, n}, and j₁ < ⋯ < jₘ = n  classical  let toι (k : ℕ) : ι := if hn : k < #J then J.orderEmbOfFin rfl ⟨k, hn⟩ else n  have toι_mono : Monotone toι := fun k l hkl ↦ by    unfold toι    split_ifs with hk hl hl    exacts [(J.orderEmbOfFin rfl).monotone hkl, hJn _ (orderEmbOfFin_mem ..), by omega, le_refl _]  have hcongr (ω : Ω) : J.sup' ⟨n, hnJ⟩ (fun i ↦ Y i ω) =      (range (#J + 1)).sup' nonempty_range_add_one fun k ↦ Y (toι k) ω := by    unfold toι    apply le_antisymm    · refine sup'_le _ _ fun i hi ↦ ?_      refine le_sup'_of_le _ (b := ((J.orderIsoOfFin rfl).symm ⟨i, hi⟩ : ℕ)) ?_ ?_      · simp      · simp [orderEmbOfFin]    · refine sup'_le _ _ fun k hk ↦ ?_      apply le_sup' fun i ↦ Y i ω      split_ifs      exacts [orderEmbOfFin_mem .., hnJ]  calc    _ = ε • P.real        {ω | (ε : ℝ) ≤ (range (#J + 1)).sup' nonempty_range_add_one fun k ↦ Y (toι k) ω} := by      simp_rw [hcongr]    _ ≤ ∫ ω in {ω | (ε : ℝ) ≤ (range (#J + 1)).sup' nonempty_range_add_one fun k ↦ Y (toι k) ω},        Y n ω ∂P := by      convert maximal_ineq' (hsub.indexComap toι_mono) (fun _ ↦ hnonneg _) ε #J      · rfl      · rfl      · simp [toι]    _ = _ := by      congr! with ω      simp_rw [hcongr]