awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
this : Monotone.{0, u_2} (β := ι) fun (n : ℕ) ↦ lowerCrossingTime a b f N n ω
⊢ lowerCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N m ω

Tactic:
this hnm
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
this : Monotone.{0, u_2} (β := ι) fun (n : ℕ) ↦ lowerCrossingTime a b f N n ω
⊢ lowerCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N m ω

Tactic:
exact this hnm
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
suffices : Monotone.{0, u_2} (β := ι) fun (n : ℕ) ↦ lowerCrossingTime a b f N n ω
⊢ lowerCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N m ω

Tactic:
suffices Monotone fun n => lowerCrossingTime a b f N n ω by exact this hnm
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ Monotone.{0, u_2} (β := ι) fun (n : ℕ) ↦ lowerCrossingTime a b f N n ω

Tactic:
monotone_nat_of_le_succ fun n =>
    le_trans lowerCrossingTime_le_upperCrossingTime_succ upperCrossingTime_le_lowerCrossingTime

Premises used: MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ, MeasureTheory.upperCrossingTime_le_lowerCrossingTime, le_trans, monotone_nat_of_le_succ
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ Monotone.{0, u_2} (β := ι) fun (n : ℕ) ↦ lowerCrossingTime a b f N n ω

Tactic:
exact monotone_nat_of_le_succ fun n =>
    le_trans lowerCrossingTime_le_upperCrossingTime_succ upperCrossingTime_le_lowerCrossingTime

Premises used: MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ, MeasureTheory.upperCrossingTime_le_lowerCrossingTime, le_trans, monotone_nat_of_le_succ
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
this : Monotone.{0, u_2} (β := ι) fun (n : ℕ) ↦ upperCrossingTime a b f N n ω
⊢ upperCrossingTime a b f N n ω ≤ upperCrossingTime a b f N m ω

Tactic:
this hnm
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
this : Monotone.{0, u_2} (β := ι) fun (n : ℕ) ↦ upperCrossingTime a b f N n ω
⊢ upperCrossingTime a b f N n ω ≤ upperCrossingTime a b f N m ω

Tactic:
exact this hnm
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
suffices : Monotone.{0, u_2} (β := ι) fun (n : ℕ) ↦ upperCrossingTime a b f N n ω
⊢ upperCrossingTime a b f N n ω ≤ upperCrossingTime a b f N m ω

Tactic:
suffices Monotone fun n => upperCrossingTime a b f N n ω by exact this hnm
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ Monotone.{0, u_2} (β := ι) fun (n : ℕ) ↦ upperCrossingTime a b f N n ω

Tactic:
monotone_nat_of_le_succ fun n =>
    le_trans upperCrossingTime_le_lowerCrossingTime lowerCrossingTime_le_upperCrossingTime_succ

Premises used: MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ, MeasureTheory.upperCrossingTime_le_lowerCrossingTime, le_trans, monotone_nat_of_le_succ
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ Monotone.{0, u_2} (β := ι) fun (n : ℕ) ↦ upperCrossingTime a b f N n ω

Tactic:
exact monotone_nat_of_le_succ fun n =>
    le_trans upperCrossingTime_le_lowerCrossingTime lowerCrossingTime_le_upperCrossingTime_succ

Premises used: MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ, MeasureTheory.upperCrossingTime_le_lowerCrossingTime, le_trans, monotone_nat_of_le_succ
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
h : lowerCrossingTime a b f N n ω ≠ N
obtain :
  ∀ (j : ℕ) (hj₁ : j ∈ Set.Icc (upperCrossingTime a b f N n ω) (lowerCrossingTime a b f N n ω))
    (hj₂ : f j ω ∈ Set.Iic a), stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)) ω ≤ a
⊢ stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)) ω ≤ a

Tactic:
obtain ⟨j, hj₁, hj₂⟩ :=
    (hittingBtwn_le_iff_of_lt _ (lt_of_le_of_ne lowerCrossingTime_le h)).1 le_rfl

Premises used: le_rfl, MeasureTheory.lowerCrossingTime_le, MeasureTheory.hittingBtwn_le_iff_of_lt, Iff.mp, lt_of_le_of_ne
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
h : lowerCrossingTime a b f N n ω ≠ N
j : ℕ
hj₁ : j ∈ Set.Icc (upperCrossingTime a b f N n ω) (lowerCrossingTime a b f N n ω)
hj₂ : f j ω ∈ Set.Iic a
⊢ stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)) ω ≤ a

Tactic:
stoppedValue_hittingBtwn_mem ⟨j, ⟨hj₁.1, le_trans hj₁.2 lowerCrossingTime_le⟩, hj₂⟩

Premises used: MeasureTheory.stoppedValue, MeasureTheory.lowerCrossingTime_le, Set.Mem, MeasureTheory.lowerCrossingTime, MeasureTheory.stoppedValue_hittingBtwn_mem, setOf, MeasureTheory.hittingBtwn, WithTop.some, Set.Icc, And.right, And.left, And.intro, Exists.intro, Set.Iic, Not, le_trans, ite
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
h : lowerCrossingTime a b f N n ω ≠ N
j : ℕ
hj₁ : j ∈ Set.Icc (upperCrossingTime a b f N n ω) (lowerCrossingTime a b f N n ω)
hj₂ : f j ω ∈ Set.Iic a
⊢ stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)) ω ≤ a

Tactic:
exact stoppedValue_hittingBtwn_mem ⟨j, ⟨hj₁.1, le_trans hj₁.2 lowerCrossingTime_le⟩, hj₂⟩

Premises used: MeasureTheory.lowerCrossingTime_le, MeasureTheory.stoppedValue_hittingBtwn_mem, And.right, And.left, And.intro, Exists.intro, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
h : upperCrossingTime a b f N (n + 1) ω ≠ N
obtain :
  ∀ (j : ℕ)
    (hj₁ :
      j ∈ Set.Icc (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) (upperCrossingTime a b f N (n + 1) ω))
    (hj₂ : f j ω ∈ Set.Ici b), b ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω
⊢ b ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω

Tactic:
obtain ⟨j, hj₁, hj₂⟩ :=
    (hittingBtwn_le_iff_of_lt _ (lt_of_le_of_ne upperCrossingTime_le h)).1 le_rfl

Premises used: le_rfl, MeasureTheory.hittingBtwn_le_iff_of_lt, Iff.mp, MeasureTheory.upperCrossingTime_le, lt_of_le_of_ne
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
h : upperCrossingTime a b f N (n + 1) ω ≠ N
j : ℕ
hj₁ : j ∈ Set.Icc (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) (upperCrossingTime a b f N (n + 1) ω)
hj₂ : f j ω ∈ Set.Ici b
⊢ b ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω

Tactic:
stoppedValue_hittingBtwn_mem ⟨j, ⟨hj₁.1, le_trans hj₁.2 (hittingBtwn_le _)⟩, hj₂⟩

Premises used: MeasureTheory.stoppedValue, Set.Ici, Set.Mem, MeasureTheory.stoppedValue_hittingBtwn_mem, setOf, MeasureTheory.upperCrossingTime, MeasureTheory.hittingBtwn, WithTop.some, MeasureTheory.lowerCrossingTimeAux, Set.Icc, And.right, And.left, And.intro, MeasureTheory.hittingBtwn_le, Exists.intro, Not, le_trans, ite
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
h : upperCrossingTime a b f N (n + 1) ω ≠ N
j : ℕ
hj₁ : j ∈ Set.Icc (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) (upperCrossingTime a b f N (n + 1) ω)
hj₂ : f j ω ∈ Set.Ici b
⊢ b ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω

Tactic:
exact stoppedValue_hittingBtwn_mem ⟨j, ⟨hj₁.1, le_trans hj₁.2 (hittingBtwn_le _)⟩, hj₂⟩

Premises used: MeasureTheory.stoppedValue_hittingBtwn_mem, And.right, And.left, And.intro, MeasureTheory.hittingBtwn_le, Exists.intro, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
⊢ upperCrossingTime a b f N (n + 1) ω < lowerCrossingTime a b f N (n + 1) ω

Tactic:
lt_of_le_of_ne upperCrossingTime_le_lowerCrossingTime fun h =>
    not_le.2 hab <| le_trans ?_ (stoppedValue_lowerCrossingTime hn)

Premises used: not_le, Iff.mpr, MeasureTheory.stoppedValue_lowerCrossingTime, MeasureTheory.upperCrossingTime_le_lowerCrossingTime, lt_of_le_of_ne, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
refine :
  ∀ (h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω),
    b ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω
⊢ upperCrossingTime a b f N (n + 1) ω < lowerCrossingTime a b f N (n + 1) ω

Tactic:
refine lt_of_le_of_ne upperCrossingTime_le_lowerCrossingTime fun h =>
    not_le.2 hab <| le_trans ?_ (stoppedValue_lowerCrossingTime hn)

Premises used: not_le, Iff.mpr, MeasureTheory.stoppedValue_lowerCrossingTime, MeasureTheory.upperCrossingTime_le_lowerCrossingTime, lt_of_le_of_ne, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
simp : b ≤ f (WithTop.untopA (↑(lowerCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω
⊢ b ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω

Tactic:
simp only [stoppedValue]

Premises used: MeasureTheory.stoppedValue
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
rw : b ≤ f (WithTop.untopA (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω
⊢ b ≤ f (WithTop.untopA (↑(lowerCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω

Tactic:
rw [← h]
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
⊢ b ≤ f (WithTop.untopA (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω

Tactic:
stoppedValue_upperCrossingTime (h.symm ▸ hn)

Premises used: MeasureTheory.stoppedValue, Eq.rec, MeasureTheory.stoppedValue_upperCrossingTime, Eq.symm
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
⊢ b ≤ f (WithTop.untopA (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω

Tactic:
exact stoppedValue_upperCrossingTime (h.symm ▸ hn)

Premises used: MeasureTheory.stoppedValue_upperCrossingTime
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
⊢ lowerCrossingTime a b f N n ω < upperCrossingTime a b f N (n + 1) ω

Tactic:
lt_of_le_of_ne lowerCrossingTime_le_upperCrossingTime_succ fun h =>
    not_le.2 hab <| le_trans (stoppedValue_upperCrossingTime hn) ?_

Premises used: not_le, Iff.mpr, MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ, MeasureTheory.stoppedValue_upperCrossingTime, lt_of_le_of_ne, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
refine :
  ∀ (h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω),
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω ≤ a
⊢ lowerCrossingTime a b f N n ω < upperCrossingTime a b f N (n + 1) ω

Tactic:
refine lt_of_le_of_ne lowerCrossingTime_le_upperCrossingTime_succ fun h =>
    not_le.2 hab <| le_trans (stoppedValue_upperCrossingTime hn) ?_

Premises used: not_le, Iff.mpr, MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ, MeasureTheory.stoppedValue_upperCrossingTime, lt_of_le_of_ne, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
simp : f (WithTop.untopA (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω ≤ a
⊢ stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω ≤ a

Tactic:
simp only [stoppedValue]

Premises used: MeasureTheory.stoppedValue
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
rw : f (WithTop.untopA (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)) ω ≤ a
⊢ f (WithTop.untopA (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω ≤ a

Tactic:
rw [← h]
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
⊢ f (WithTop.untopA (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)) ω ≤ a

Tactic:
stoppedValue_lowerCrossingTime (h.symm ▸ hn)

Premises used: MeasureTheory.stoppedValue, MeasureTheory.stoppedValue_lowerCrossingTime, Eq.rec, Eq.symm
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
⊢ f (WithTop.untopA (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)) ω ≤ a

Tactic:
exact stoppedValue_lowerCrossingTime (h.symm ▸ hn)

Premises used: MeasureTheory.stoppedValue_lowerCrossingTime
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
⊢ upperCrossingTime a b f N n ω < upperCrossingTime a b f N (n + 1) ω

Tactic:
lt_of_le_of_lt upperCrossingTime_le_lowerCrossingTime
    (lowerCrossingTime_lt_upperCrossingTime hab hn)

Premises used: lt_of_le_of_lt, MeasureTheory.lowerCrossingTime_lt_upperCrossingTime, MeasureTheory.upperCrossingTime_le_lowerCrossingTime
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
hnm : n ≤ m
hn : lowerCrossingTime a b f N n ω = N
⊢ lowerCrossingTime a b f N m ω = N

Tactic:
le_antisymm lowerCrossingTime_le (le_trans (le_of_eq hn.symm) (lowerCrossingTime_mono hnm))

Premises used: MeasureTheory.lowerCrossingTime_le, le_antisymm, MeasureTheory.lowerCrossingTime_mono, le_of_eq, Eq.symm, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
hnm : n ≤ m
hn : upperCrossingTime a b f N n ω = N
⊢ upperCrossingTime a b f N m ω = N

Tactic:
le_antisymm upperCrossingTime_le (le_trans (le_of_eq hn.symm) (upperCrossingTime_mono hnm))

Premises used: MeasureTheory.upperCrossingTime_mono, le_antisymm, MeasureTheory.upperCrossingTime_le, le_of_eq, Eq.symm, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
hnm : n ≤ m
hn : N ≤ lowerCrossingTime a b f N n ω
⊢ lowerCrossingTime a b f N m ω = N

Tactic:
lowerCrossingTime_stabilize hnm (le_antisymm lowerCrossingTime_le hn)

Premises used: MeasureTheory.lowerCrossingTime_le, MeasureTheory.lowerCrossingTime_stabilize, le_antisymm
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
hnm : n ≤ m
hn : N ≤ upperCrossingTime a b f N n ω
⊢ upperCrossingTime a b f N m ω = N

Tactic:
upperCrossingTime_stabilize hnm (le_antisymm upperCrossingTime_le hn)

Premises used: MeasureTheory.upperCrossingTime_stabilize, le_antisymm, MeasureTheory.upperCrossingTime_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
by_contra! : ∀ (h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N), False
⊢ ∃ (n : ℕ), upperCrossingTime a b f N n ω = N

Tactic:
by_contra! h
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
⊢ StrictMono (β := ℕ) fun (n : ℕ) ↦ upperCrossingTime a b f N n ω

Tactic:
have : StrictMono fun n => upperCrossingTime a b f N n ω :=
    strictMono_nat_of_lt_succ fun n => upperCrossingTime_lt_succ hab (h _)
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
this : StrictMono (β := ℕ) fun (n : ℕ) ↦ upperCrossingTime a b f N n ω
⊢ ∃ (m : ℕ) (_ : Membership.mem (γ := Set ℕ) (Set.range fun (n : ℕ) ↦ upperCrossingTime a b f N n ω) m), N < m

Tactic:
⟨upperCrossingTime a b f N (N + 1) ω, ⟨N + 1, rfl⟩,
      lt_of_lt_of_le N.lt_succ_self (StrictMono.id_le this (N + 1))⟩

Premises used: MeasureTheory.upperCrossingTime, Nat.lt_succ_self, HAdd.hAdd, Exists.intro, StrictMono.id_le, OfNat.ofNat, rfl, lt_of_lt_of_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
this : StrictMono (β := ℕ) fun (n : ℕ) ↦ upperCrossingTime a b f N n ω
obtain : ∀ (k : ℕ) (hk : N < (fun (n : ℕ) ↦ upperCrossingTime a b f N n ω) k), False
⊢ False

Tactic:
obtain ⟨_, ⟨k, rfl⟩, hk⟩ :
      ∃ (m : _) (_ : m ∈ Set.range fun n => upperCrossingTime a b f N n ω), N < m :=
    ⟨upperCrossingTime a b f N (N + 1) ω, ⟨N + 1, rfl⟩,
      lt_of_lt_of_le N.lt_succ_self (StrictMono.id_le this (N + 1))⟩

Premises used: MeasureTheory.upperCrossingTime, Set.range, rfl
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
this : StrictMono (β := ℕ) fun (n : ℕ) ↦ upperCrossingTime a b f N n ω
k : ℕ
hk : N < (fun (n : ℕ) ↦ upperCrossingTime a b f N n ω) k
⊢ False

Tactic:
not_le.2 hk upperCrossingTime_le

Premises used: not_le, Iff.mpr, MeasureTheory.upperCrossingTime_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
this : StrictMono (β := ℕ) fun (n : ℕ) ↦ upperCrossingTime a b f N n ω
k : ℕ
hk : N < (fun (n : ℕ) ↦ upperCrossingTime a b f N n ω) k
⊢ False

Tactic:
exact not_le.2 hk upperCrossingTime_le

Premises used: not_le, Iff.mpr, MeasureTheory.upperCrossingTime_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
obtain :
  ∀ (k : ℕ) (hk : upperCrossingTime a b f N k ω = N), BddAbove (α := ℕ) {n : ℕ | upperCrossingTime a b f N n ω < N}
⊢ BddAbove (α := ℕ) {n : ℕ | upperCrossingTime a b f N n ω < N}

Tactic:
obtain ⟨k, hk⟩ := exists_upperCrossingTime_eq f N ω hab

Premises used: MeasureTheory.exists_upperCrossingTime_eq
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
⊢ BddAbove (α := ℕ) {n : ℕ | upperCrossingTime a b f N n ω < N}

Tactic:
⟨k, fun n (hn : upperCrossingTime a b f N n ω < N) => ?_⟩

Premises used: BddAbove, Set.Nonempty, Exists.intro
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
refine : ∀ (n : ℕ) (hn : upperCrossingTime a b f N n ω < N), n ≤ k
⊢ BddAbove (α := ℕ) {n : ℕ | upperCrossingTime a b f N n ω < N}

Tactic:
refine ⟨k, fun n (hn : upperCrossingTime a b f N n ω < N) => ?_⟩
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
n : ℕ
hn : upperCrossingTime a b f N n ω < N
by_contra : ∀ (hn' : ¬n ≤ k), False
⊢ n ≤ k

Tactic:
by_contra hn'
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
n : ℕ
hn : upperCrossingTime a b f N n ω < N
hn' : ¬n ≤ k
⊢ False

Tactic:
hn.ne (upperCrossingTime_stabilize (not_le.1 hn').le hk)

Premises used: not_le, LT.lt.le, MeasureTheory.upperCrossingTime_stabilize, Iff.mp, LT.lt.ne
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
n : ℕ
hn : upperCrossingTime a b f N n ω < N
hn' : ¬n ≤ k
⊢ False

Tactic:
exact hn.ne (upperCrossingTime_stabilize (not_le.1 hn').le hk)

Premises used: not_le, LT.lt.le, MeasureTheory.upperCrossingTime_stabilize, Iff.mp, LT.lt.ne
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hN : 0 < N
⊢ Set.Nonempty (α := ℕ) {n : ℕ | upperCrossingTime a b f N n ω < N}

Tactic:
⟨0, hN⟩

Premises used: Set.Nonempty, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
pos : ∀ (hN' : N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯), upperCrossingTime a b f N N ω = N
neg :
  ∀ (hN' : ¬N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯), upperCrossingTime a b f N N ω = N
⊢ upperCrossingTime a b f N N ω = N

Tactic:
by_cases hN' : N < Nat.find (exists_upperCrossingTime_eq f N ω hab)

Premises used: Nat.find, MeasureTheory.exists_upperCrossingTime_eq
-- 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) ⋯
⊢ upperCrossingTime a b f N N ω = N

Tactic:
le_antisymm upperCrossingTime_le ?_

Premises used: le_antisymm, MeasureTheory.upperCrossingTime_le
-- 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) ⋯
pos : N ≤ upperCrossingTime a b f N N ω
⊢ upperCrossingTime a b f N N ω = N

Tactic:
refine le_antisymm upperCrossingTime_le ?_

Premises used: le_antisymm, MeasureTheory.upperCrossingTime_le
-- 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:
strictMonoOn_Iic_of_lt_succ fun m hm => upperCrossingTime_lt_succ hab ?_

Premises used: MeasureTheory.upperCrossingTime_lt_succ, strictMonoOn_Iic_of_lt_succ