awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯
refine :
  ∀ (m : ℕ) (hm : m < (Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯).pred),
    upperCrossingTime a b f N (m + 1) ω ≠ N
⊢ StrictMonoOn (β := ℕ) (fun (n : ℕ) ↦ upperCrossingTime a b f N n ω)
    (Set.Iic (Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯).pred)

Tactic:
refine strictMonoOn_Iic_of_lt_succ fun m hm => upperCrossingTime_lt_succ hab ?_

Premises used: MeasureTheory.upperCrossingTime_lt_succ, strictMonoOn_Iic_of_lt_succ
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯
m : ℕ
hm : m < (Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯).pred
⊢ m.succ < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯

Tactic:
rw [Nat.lt_pred_iff] at hm

Premises used: Nat.lt_pred_iff
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯
m : ℕ
hm : m.succ < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯
⊢ ¬upperCrossingTime a b f N m.succ ω = N

Tactic:
Nat.find_min _ hm

Premises used: Nat.find_min
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯
m : ℕ
hm : m.succ < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯
⊢ upperCrossingTime a b f N (m + 1) ω ≠ N

Tactic:
convert! Nat.find_min _ hm

Premises used: Nat.find_min
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯
⊢ StrictMonoOn (β := ℕ) (fun (n : ℕ) ↦ upperCrossingTime a b f N n ω)
    (Set.Iic (Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯).pred)

Tactic:
have hmono : StrictMonoOn (fun n => upperCrossingTime a b f N n ω)
        (Set.Iic (Nat.find (exists_upperCrossingTime_eq f N ω hab)).pred) := by
      refine strictMonoOn_Iic_of_lt_succ fun m hm => upperCrossingTime_lt_succ hab ?_
      rw [Nat.lt_pred_iff] at hm
      convert! Nat.find_min _ hm
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯
hmono :
  StrictMonoOn (β := ℕ) (fun (n : ℕ) ↦ upperCrossingTime a b f N n ω)
    (Set.Iic (Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯).pred)
⊢ N ≤ upperCrossingTime a b f N N ω

Tactic:
StrictMonoOn.Iic_id_le hmono N (Nat.le_sub_one_of_lt hN')

Premises used: StrictMonoOn.Iic_id_le, Nat.le_sub_one_of_lt
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯
hmono :
  StrictMonoOn (β := ℕ) (fun (n : ℕ) ↦ upperCrossingTime a b f N n ω)
    (Set.Iic (Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯).pred)
⊢ N ≤ upperCrossingTime a b f N N ω

Tactic:
convert! StrictMonoOn.Iic_id_le hmono N (Nat.le_sub_one_of_lt hN')

Premises used: StrictMonoOn.Iic_id_le, Nat.le_sub_one_of_lt
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : ¬N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯
⊢ Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯ ≤ N

Tactic:
rw [not_lt] at hN'

Premises used: not_lt
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯ ≤ N
⊢ upperCrossingTime a b f N N ω = N

Tactic:
upperCrossingTime_stabilize hN' (Nat.find_spec (exists_upperCrossingTime_eq f N ω hab))

Premises used: MeasureTheory.upperCrossingTime_stabilize, MeasureTheory.exists_upperCrossingTime_eq, Nat.find_spec
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯ ≤ N
⊢ upperCrossingTime a b f N N ω = N

Tactic:
exact upperCrossingTime_stabilize hN' (Nat.find_spec (exists_upperCrossingTime_eq f N ω hab))

Premises used: MeasureTheory.upperCrossingTime_stabilize, MeasureTheory.exists_upperCrossingTime_eq, Nat.find_spec
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : N ≤ n
⊢ upperCrossingTime a b f N n ω = N

Tactic:
le_antisymm upperCrossingTime_le
    (le_trans (upperCrossingTime_bound_eq f N ω hab).symm.le (upperCrossingTime_mono hn))

Premises used: MeasureTheory.upperCrossingTime_bound_eq, MeasureTheory.upperCrossingTime_mono, Eq.le, le_antisymm, MeasureTheory.upperCrossingTime_le, Eq.symm, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
⊢ (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N 0 ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N 0 ω) : WithTop ℕ)

Tactic:
⟨isStoppingTime_const _ 0, ?_⟩

Premises used: MeasureTheory.isStoppingTime_const, And.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
zero : IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N 0 ω) : WithTop ℕ)
⊢ (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N 0 ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N 0 ω) : WithTop ℕ)

Tactic:
refine ⟨isStoppingTime_const _ 0, ?_⟩
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
⊢ IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(hittingBtwn f (Set.Iic a) 0 N ω) : WithTop ℕ)

Tactic:
hf.adapted.isStoppingTime_hittingBtwn measurableSet_Iic

Premises used: MeasureTheory.Adapted.isStoppingTime_hittingBtwn, MeasureTheory.StronglyAdapted.adapted, measurableSet_Iic
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
⊢ IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(hittingBtwn f (Set.Iic a) 0 N ω) : WithTop ℕ)

Tactic:
exact hf.adapted.isStoppingTime_hittingBtwn measurableSet_Iic

Premises used: MeasureTheory.Adapted.isStoppingTime_hittingBtwn, MeasureTheory.StronglyAdapted.adapted, measurableSet_Iic
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n_1 : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N k ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)
n : ℕ
⊢ MeasurableSet.{u_1} (α := Ω)
    {ω : Ω | (↑(hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω) : WithTop ℕ) ≤ (↑n : WithTop ℕ)}

Tactic:
hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime ih.2 ?_ measurableSet_Ici _

Premises used: MeasureTheory.lowerCrossingTime, setOf, MeasureTheory.StronglyAdapted.adapted, MeasureTheory.hittingBtwn, And.right, WithTop.untopD, measurableSet_Ici, WithTop.recTopCoe, MeasureTheory.Adapted.isStoppingTime_hittingBtwn_isStoppingTime, ite
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n_1 : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N k ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)
n : ℕ
refine : ∀ (x : Ω), (↑(lowerCrossingTime a b f N k x) : WithTop ℕ) ≤ (↑N : WithTop ℕ)
⊢ MeasurableSet.{u_1} (α := Ω)
    {ω : Ω | (↑(hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω) : WithTop ℕ) ≤ (↑n : WithTop ℕ)}

Tactic:
refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime ih.2 ?_ measurableSet_Ici _

Premises used: MeasureTheory.StronglyAdapted.adapted, And.right, measurableSet_Ici, MeasureTheory.Adapted.isStoppingTime_hittingBtwn_isStoppingTime
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n_1 : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N k ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)
n : ℕ
⊢ ∀ (x : Ω), (↑(lowerCrossingTime a b f N k x) : WithTop ℕ) ≤ (↑N : WithTop ℕ)

Tactic:
simp [lowerCrossingTime_le]

Premises used: MeasureTheory.lowerCrossingTime_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N k ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)
⊢ IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)

Tactic:
have : IsStoppingTime ℱ (fun ω ↦ (upperCrossingTime a b f N (k + 1) ω : ℕ)) := by
      intro n
      simp_rw [upperCrossingTime_succ_eq]
      refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime ih.2 ?_ measurableSet_Ici _
      simp [lowerCrossingTime_le]
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N k ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)
this : IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)
⊢ (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N (k + 1) ω) : WithTop ℕ)

Tactic:
⟨this, fun n ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N k ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)
this : IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)
succ :
  ∀ (n : ℕ),
    MeasurableSet.{u_1} (α := Ω)
      {ω : Ω | (fun (ω : Ω) ↦ ((↑(lowerCrossingTime a b f N (k + 1) ω) : WithTop ℕ) : WithTop ℕ)) ω ≤ (↑n : WithTop ℕ)}
⊢ (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N (k + 1) ω) : WithTop ℕ)

Tactic:
refine ⟨this, fun n ↦ ?_⟩
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n_1 : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N k ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)
this : IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)
n : ℕ
⊢ MeasurableSet.{u_1} (α := Ω)
    {ω : Ω | (fun (ω : Ω) ↦ ((↑(lowerCrossingTime a b f N (k + 1) ω) : WithTop ℕ) : WithTop ℕ)) ω ≤ (↑n : WithTop ℕ)}

Tactic:
hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime this ?_ measurableSet_Iic _

Premises used: Set.Mem, MeasureTheory.lowerCrossingTime, setOf, MeasureTheory.StronglyAdapted.adapted, MeasureTheory.upperCrossingTime, MeasureTheory.hittingBtwn, measurableSet_Iic, WithTop.untopD, WithTop.recTopCoe, MeasureTheory.Adapted.isStoppingTime_hittingBtwn_isStoppingTime, ite
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n_1 : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N k ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)
this : IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)
n : ℕ
succ : ∀ (x : Ω), (↑(upperCrossingTime a b f N (k + 1) x) : WithTop ℕ) ≤ (↑N : WithTop ℕ)
⊢ MeasurableSet.{u_1} (α := Ω)
    {ω : Ω | (fun (ω : Ω) ↦ ((↑(lowerCrossingTime a b f N (k + 1) ω) : WithTop ℕ) : WithTop ℕ)) ω ≤ (↑n : WithTop ℕ)}

Tactic:
refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime this ?_ measurableSet_Iic _

Premises used: MeasureTheory.StronglyAdapted.adapted, measurableSet_Iic, MeasureTheory.Adapted.isStoppingTime_hittingBtwn_isStoppingTime
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n_1 : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N k ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)
this : IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)
n : ℕ
⊢ ∀ (x : Ω), (↑(upperCrossingTime a b f N (k + 1) x) : WithTop ℕ) ≤ (↑N : WithTop ℕ)

Tactic:
simp [upperCrossingTime_le]

Premises used: MeasureTheory.upperCrossingTime_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
zero :
  (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N 0 ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N 0 ω) : WithTop ℕ)
succ :
  ∀ (k : ℕ)
    (ih :
      (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N k ω) : WithTop ℕ)) ∧
        IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)),
    (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ∧
      IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N (k + 1) ω) : WithTop ℕ)
⊢ (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N n ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)

Tactic:
induction n with
  | zero =>
    refine ⟨isStoppingTime_const _ 0, ?_⟩
    simp only [lowerCrossingTime_zero, Nat.bot_eq_zero]
    exact hf.adapted.isStoppingTime_hittingBtwn measurableSet_Iic
  | succ k ih =>
    have : IsStoppingTime ℱ (fun ω ↦ (upperCrossingTime a b f N (k + 1) ω : ℕ)) := by
      intro n
      simp_rw [upperCrossingTime_succ_eq]
      refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime ih.2 ?_ measurableSet_Ici _
      simp [lowerCrossingTime_le]
    refine ⟨this, fun n ↦ ?_⟩
    refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime this ?_ measurableSet_Iic _
    simp [upperCrossingTime_le]

Premises used: MeasureTheory.Adapted.isStoppingTime_hittingBtwn, MeasureTheory.StronglyAdapted.adapted, MeasureTheory.lowerCrossingTime_zero, measurableSet_Iic, MeasureTheory.upperCrossingTime_le, Nat.bot_eq_zero
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
⊢ IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N n ω) : WithTop ℕ)

Tactic:
hf.isStoppingTime_crossing.1

Premises used: MeasureTheory.StronglyAdapted.isStoppingTime_crossing, And.left
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
⊢ IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)

Tactic:
hf.isStoppingTime_crossing.2

Premises used: MeasureTheory.StronglyAdapted.isStoppingTime_crossing, And.right
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
⊢ 0 ≤ upcrossingStrat a b f N n ω

Tactic:
Finset.sum_nonneg fun _ _ => Set.indicator_nonneg (fun _ _ => zero_le_one) _

Premises used: Finset.sum_nonneg, zero_le_one, MeasureTheory.upcrossingStrat, Set.indicator_nonneg
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
rw :
  LE.le (α := ℝ)
    (Set.indicator (⋃ i ∈ Finset.range N, Set.Ico (lowerCrossingTime a b f N i ω) (upperCrossingTime a b f N (i + 1) ω))
      1 n)
    1
h :
  (↑(Finset.range N) : Set ℕ).PairwiseDisjoint (α := Set ℕ) fun (k : ℕ) ↦
    Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)
⊢ upcrossingStrat a b f N n ω ≤ 1

Tactic:
rw [upcrossingStrat, ← Finset.indicator_biUnion_apply]

Premises used: Finset.indicator_biUnion_apply, MeasureTheory.upcrossingStrat
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
⊢ LE.le (α := ℝ)
    (Set.indicator (⋃ i ∈ Finset.range N, Set.Ico (lowerCrossingTime a b f N i ω) (upperCrossingTime a b f N (i + 1) ω))
      1 n)
    1

Tactic:
Set.indicator_le_self' (fun _ _ => zero_le_one) _

Premises used: Set.indicator_le_self', zero_le_one
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
⊢ LE.le (α := ℝ)
    (Set.indicator (⋃ i ∈ Finset.range N, Set.Ico (lowerCrossingTime a b f N i ω) (upperCrossingTime a b f N (i + 1) ω))
      1 n)
    1

Tactic:
exact Set.indicator_le_self' (fun _ _ => zero_le_one) _

Premises used: Set.indicator_le_self', zero_le_one
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
h :
  i ∈ (↑(Finset.range N) : Set ℕ) →
    ∀ ⦃y : ℕ⦄,
      y ∈ (↑(Finset.range N) : Set ℕ) →
        i ≠ y →
          Function.onFun (β := Set ℕ) Disjoint
            (fun (k : ℕ) ↦ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)) i y
⊢ i ∈ (↑(Finset.range N) : Set ℕ) →
    ∀ ⦃y : ℕ⦄,
      y ∈ (↑(Finset.range N) : Set ℕ) →
        i ≠ y →
          Function.onFun (β := Set ℕ) Disjoint
            (fun (k : ℕ) ↦ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)) i y

Tactic:
_
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
h_1 : i ∈ (↑(Finset.range N) : Set ℕ)
j : ℕ
h :
  j ∈ (↑(Finset.range N) : Set ℕ) →
    i ≠ j →
      Function.onFun (β := Set ℕ) Disjoint
        (fun (k : ℕ) ↦ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)) i j
⊢ j ∈ (↑(Finset.range N) : Set ℕ) →
    i ≠ j →
      Function.onFun (β := Set ℕ) Disjoint
        (fun (k : ℕ) ↦ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)) i j

Tactic:
_
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
h_1 : i ∈ (↑(Finset.range N) : Set ℕ)
j : ℕ
h_2 : j ∈ (↑(Finset.range N) : Set ℕ)
hij : i ≠ j
h :
  min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
    max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
⊢ Function.onFun (β := Set ℕ) Disjoint
    (fun (k : ℕ) ↦ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)) i j

Tactic:
simp only [Set.Ico_disjoint_Ico]

Premises used: Set.Ico_disjoint_Ico
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
h_1 : i ∈ (↑(Finset.range N) : Set ℕ)
j : ℕ
h_2 : j ∈ (↑(Finset.range N) : Set ℕ)
hij : i ≠ j
h :
  ∀ (hij' : i < j),
    min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
      max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
h₁ :
  ∀ (hij' : j < i),
    min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
      max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
⊢ min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
    max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)

Tactic:
obtain hij' | hij' := lt_or_gt_of_ne hij

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
h_1 : i ∈ (↑(Finset.range N) : Set ℕ)
j : ℕ
h_2 : j ∈ (↑(Finset.range N) : Set ℕ)
hij : i ≠ j
hij' : i < j
h : upperCrossingTime a b f N i.succ ω ≤ lowerCrossingTime a b f N j ω
⊢ min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
    max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)

Tactic:
rw [min_eq_left (upperCrossingTime_mono (Nat.succ_le_succ hij'.le) :
      upperCrossingTime a b f N _ ω ≤ upperCrossingTime a b f N _ ω),
      max_eq_right (lowerCrossingTime_mono hij'.le :
        lowerCrossingTime a b f N _ _ ≤ lowerCrossingTime _ _ _ _ _ _)]

Premises used: MeasureTheory.upperCrossingTime_mono, LT.lt.le, max_eq_right, min_eq_left, MeasureTheory.lowerCrossingTime_mono, Nat.succ_le_succ
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
h : i ∈ (↑(Finset.range N) : Set ℕ)
j : ℕ
h_1 : j ∈ (↑(Finset.range N) : Set ℕ)
hij : i ≠ j
hij' : i < j
⊢ upperCrossingTime a b f N i.succ ω ≤ lowerCrossingTime a b f N j ω

Tactic:
le_trans upperCrossingTime_le_lowerCrossingTime
      (lowerCrossingTime_mono (Nat.succ_le_of_lt hij'))

Premises used: Nat.succ_le_of_lt, MeasureTheory.upperCrossingTime_le_lowerCrossingTime, MeasureTheory.lowerCrossingTime_mono, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
h : i ∈ (↑(Finset.range N) : Set ℕ)
j : ℕ
h_1 : j ∈ (↑(Finset.range N) : Set ℕ)
hij : i ≠ j
hij' : i < j
⊢ upperCrossingTime a b f N i.succ ω ≤ lowerCrossingTime a b f N j ω

Tactic:
refine le_trans upperCrossingTime_le_lowerCrossingTime
      (lowerCrossingTime_mono (Nat.succ_le_of_lt hij'))

Premises used: Nat.succ_le_of_lt, MeasureTheory.upperCrossingTime_le_lowerCrossingTime, MeasureTheory.lowerCrossingTime_mono, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
h_1 : i ∈ (↑(Finset.range N) : Set ℕ)
j : ℕ
h_2 : j ∈ (↑(Finset.range N) : Set ℕ)
hij : i ≠ j
hij' : j < i
h : upperCrossingTime a b f N j.succ ω ≤ lowerCrossingTime a b f N i ω
⊢ min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
    max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)

Tactic:
rw [min_eq_right (upperCrossingTime_mono (Nat.succ_le_succ hij'.le) :
      upperCrossingTime a b f N _ ω ≤ upperCrossingTime a b f N _ ω),
      max_eq_left (lowerCrossingTime_mono hij'.le :
        lowerCrossingTime a b f N _ _ ≤ lowerCrossingTime _ _ _ _ _ _)]

Premises used: MeasureTheory.upperCrossingTime_mono, LT.lt.le, max_eq_left, min_eq_right, MeasureTheory.lowerCrossingTime_mono, Nat.succ_le_succ