awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : upperCrossingTime a b f N (k + 1) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
this : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω
h₁ : ∃ j ∈ Set.Ico (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ upperCrossingTime a b f N (k + 1) ω < N

Tactic:
rw [lowerCrossingTime, hittingBtwn_lt_iff _ le_rfl] at h

Premises used: le_rfl, MeasureTheory.lowerCrossingTime, MeasureTheory.hittingBtwn_lt_iff
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : upperCrossingTime a b f N (k + 1) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
this : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω
h₁ : ∃ j ∈ Set.Ico (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
h'₁ : upperCrossingTime a b f N (k + 1) ω < N
⊢ upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω

Tactic:
rw [lowerCrossingTime, hittingBtwn_lt_iff _ le_rfl] at h

Premises used: le_rfl, MeasureTheory.lowerCrossingTime, MeasureTheory.hittingBtwn_lt_iff
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : upperCrossingTime a b f N (k + 1) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
this : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω
h₁ : ∃ j ∈ Set.Ico (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
h'₁ : upperCrossingTime a b f N (k + 1) ω < N
ih₁ :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
⊢ upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω

Tactic:
rw [lowerCrossingTime, hittingBtwn_lt_iff _ le_rfl] at h

Premises used: le_rfl, MeasureTheory.lowerCrossingTime, MeasureTheory.hittingBtwn_lt_iff
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
h : ∃ j ∈ Set.Ico (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
h' : upperCrossingTime a b f N (k + 1) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
this : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω
succ :
  ∀ (j : ℕ) (hj₁ : j ∈ Set.Ico (upperCrossingTime a b f N (k + 1) ω) N) (hj₂ : f j ω ∈ Set.Iic a),
    ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := h
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
h' : upperCrossingTime a b f N (k + 1) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
this : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω
j : ℕ
hj₁ : j ∈ Set.Ico (upperCrossingTime a b f N (k + 1) ω) N
hj₂ : f j ω ∈ Set.Iic a
⊢ ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a

Tactic:
⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩

Premises used: LT.lt.le, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
h' : upperCrossingTime a b f N (k + 1) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
this : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω
j : ℕ
hj₁ : j ∈ Set.Ico (upperCrossingTime a b f N (k + 1) ω) N
hj₂ : f j ω ∈ Set.Iic a
⊢ ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a

Tactic:
exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : lowerCrossingTime a b f N n ω < N
h' : upperCrossingTime a b f N n ω < N
zero :
  ∀ (h : lowerCrossingTime a b f N 0 ω < N) (h' : upperCrossingTime a b f N 0 ω < N),
    upperCrossingTime a b f M 0 ω = upperCrossingTime a b f N 0 ω ∧
      lowerCrossingTime a b f M 0 ω = lowerCrossingTime a b f N 0 ω
succ :
  ∀ (k : ℕ)
    (ih :
      ∀ (h : lowerCrossingTime a b f N k ω < N) (h' : upperCrossingTime a b f N k ω < N),
        upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
          lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω)
    (h : lowerCrossingTime a b f N (k + 1) ω < N) (h' : upperCrossingTime a b f N (k + 1) ω < N),
    upperCrossingTime a b f M (k + 1) ω = upperCrossingTime a b f N (k + 1) ω ∧
      lowerCrossingTime a b f M (k + 1) ω = lowerCrossingTime a b f N (k + 1) ω
⊢ upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω ∧
    lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω

Tactic:
induction n with
  | zero =>
    simp only [upperCrossingTime_zero, bot_eq_zero',
      lowerCrossingTime_zero, true_and, eq_comm]
    refine hittingBtwn_eq_hittingBtwn_of_exists hNM ?_
    rw [lowerCrossingTime, hittingBtwn_lt_iff] at h
    · obtain ⟨j, hj₁, hj₂⟩ := h
      exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
    · exact le_rfl
  | succ k ih =>
    specialize ih (lt_of_le_of_lt (lowerCrossingTime_mono (Nat.le_succ _)) h)
      (lt_of_le_of_lt (upperCrossingTime_mono (Nat.le_succ _)) h')
    have : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω := by
      rw [upperCrossingTime_succ_eq, hittingBtwn_lt_iff] at h'
      · simp only [upperCrossingTime_succ_eq]
        obtain ⟨j, hj₁, hj₂⟩ := h'
        rw [eq_comm, ih.2]
        exact hittingBtwn_eq_hittingBtwn_of_exists hNM ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
      · exact le_rfl
    refine ⟨this, ?_⟩
    simp only [lowerCrossingTime, eq_comm, this, Nat.succ_eq_add_one]
    refine hittingBtwn_eq_hittingBtwn_of_exists hNM ?_
    rw [lowerCrossingTime, hittingBtwn_lt_iff _ le_rfl] at h
    obtain ⟨j, hj₁, hj₂⟩ := h
    exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩

Premises used: le_rfl, Nat.succ_eq_add_one, MeasureTheory.lowerCrossingTime, MeasureTheory.lowerCrossingTime_zero, eq_comm, MeasureTheory.upperCrossingTime_zero, MeasureTheory.hittingBtwn_lt_iff, true_and, bot_eq_zero', MeasureTheory.hittingBtwn_eq_hittingBtwn_of_exists
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
⊢ lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω

Tactic:
have := (crossing_eq_crossing_of_lowerCrossingTime_lt hNM
    (lt_of_le_of_lt lowerCrossingTime_le_upperCrossingTime_succ h)).2
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω ∧
    lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω

Tactic:
⟨?_, this⟩

Premises used: And.intro
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
refine : upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω
⊢ upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω ∧
    lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω

Tactic:
refine ⟨?_, this⟩
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
rw :
  hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) M ω
⊢ upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω

Tactic:
rw [upperCrossingTime_succ_eq, upperCrossingTime_succ_eq, eq_comm, this]

Premises used: MeasureTheory.upperCrossingTime_succ_eq, eq_comm
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) M ω

Tactic:
hittingBtwn_eq_hittingBtwn_of_exists hNM ?_

Premises used: MeasureTheory.hittingBtwn_eq_hittingBtwn_of_exists
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
refine : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
⊢ hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) M ω

Tactic:
refine hittingBtwn_eq_hittingBtwn_of_exists hNM ?_

Premises used: MeasureTheory.hittingBtwn_eq_hittingBtwn_of_exists
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
rw :
  ∀ (h : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b)
    (this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω),
    ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
hi :
  ∀ (h : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω < N)
    (this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω), N ≤ N
⊢ ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b

Tactic:
rw [upperCrossingTime_succ_eq, hittingBtwn_lt_iff] at h

Premises used: MeasureTheory.upperCrossingTime_succ_eq, MeasureTheory.hittingBtwn_lt_iff
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
obtain :
  ∀ (j : ℕ) (hj₁ : j ∈ Set.Ico (lowerCrossingTime a b f N n ω) N) (hj₂ : f j ω ∈ Set.Ici b),
    ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
⊢ ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := h
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
j : ℕ
hj₁ : j ∈ Set.Ico (lowerCrossingTime a b f N n ω) N
hj₂ : f j ω ∈ Set.Ici b
⊢ ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b

Tactic:
⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩

Premises used: LT.lt.le, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
j : ℕ
hj₁ : j ∈ Set.Ico (lowerCrossingTime a b f N n ω) N
hj₂ : f j ω ∈ Set.Ici b
⊢ ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b

Tactic:
exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ N ≤ N

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ N ≤ N

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N n ω < N
zero : ∀ (h : upperCrossingTime a b f N 0 ω < N), upperCrossingTime a b f M 0 ω = upperCrossingTime a b f N 0 ω
succ :
  ∀ (n : ℕ) (h : upperCrossingTime a b f N (n + 1) ω < N),
    upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω
⊢ upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω

Tactic:
cases n
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N 0 ω < N
⊢ upperCrossingTime a b f M 0 ω = upperCrossingTime a b f N 0 ω

Tactic:
simp
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
n : ℕ
h : upperCrossingTime a b f N (n + 1) ω < N
⊢ upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω

Tactic:
(crossing_eq_crossing_of_upperCrossingTime_lt hNM h).1

Premises used: MeasureTheory.crossing_eq_crossing_of_upperCrossingTime_lt, And.left
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
n : ℕ
h : upperCrossingTime a b f N (n + 1) ω < N
⊢ upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω

Tactic:
exact (crossing_eq_crossing_of_upperCrossingTime_lt hNM h).1

Premises used: MeasureTheory.crossing_eq_crossing_of_upperCrossingTime_lt, And.left
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
h₁ : BddAbove (α := ℕ) {n : ℕ | upperCrossingTime a b f M n ω < M}
h₂ : ∀ (n : ℕ), upperCrossingTime a b f N n ω < N → upperCrossingTime a b f M n ω < M
⊢ LE.le (α := ℕ) (sSup {n : ℕ | upperCrossingTime a b f N n ω < N}) (sSup {n : ℕ | upperCrossingTime a b f M n ω < M})

Tactic:
gcongr sSup {n | ?_} with n

Premises used: setOf, SupSet.sSup
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
⊢ BddAbove (α := ℕ) {n : ℕ | upperCrossingTime a b f M n ω < M}

Tactic:
upperCrossingTime_lt_bddAbove hab

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

Tactic:
exact upperCrossingTime_lt_bddAbove hab

Premises used: MeasureTheory.upperCrossingTime_lt_bddAbove
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
n : ℕ
hn : upperCrossingTime a b f N n ω < N
h₂ : upperCrossingTime a b f N n ω < M
⊢ upperCrossingTime a b f M n ω < M

Tactic:
rw [upperCrossingTime_eq_upperCrossingTime_of_lt hNM hn]

Premises used: MeasureTheory.upperCrossingTime_eq_upperCrossingTime_of_lt
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
n : ℕ
hn : upperCrossingTime a b f N n ω < N
⊢ upperCrossingTime a b f N n ω < M

Tactic:
lt_of_lt_of_le hn hNM

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
n : ℕ
hn : upperCrossingTime a b f N n ω < N
⊢ upperCrossingTime a b f N n ω < M

Tactic:
exact lt_of_lt_of_le hn hNM

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ upcrossingsBefore a b f N ω < upcrossingsBefore a b f (N₂ + 1) ω

Tactic:
lt_of_lt_of_le (Nat.lt_succ_self _) (le_csSup (upperCrossingTime_lt_bddAbove hab) ?_)

Premises used: Nat.lt_succ_self, MeasureTheory.upperCrossingTime_lt_bddAbove, le_csSup, lt_of_lt_of_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
refine :
  Membership.mem (γ := Set ℕ) {n : ℕ | upperCrossingTime a b f (N₂ + 1) n ω < N₂ + 1} (upcrossingsBefore a b f N ω).succ
⊢ upcrossingsBefore a b f N ω < upcrossingsBefore a b f (N₂ + 1) ω

Tactic:
refine lt_of_lt_of_le (Nat.lt_succ_self _) (le_csSup (upperCrossingTime_lt_bddAbove hab) ?_)

Premises used: Nat.lt_succ_self, MeasureTheory.upperCrossingTime_lt_bddAbove, le_csSup, lt_of_lt_of_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
rw : ∃ j ∈ Set.Ico (lowerCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) (N₂ + 1), f j ω ∈ Set.Ici b
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | upperCrossingTime a b f (N₂ + 1) n ω < N₂ + 1} (upcrossingsBefore a b f N ω).succ

Tactic:
rw [Set.mem_setOf_eq, upperCrossingTime_succ_eq, hittingBtwn_lt_iff _ le_rfl]

Premises used: MeasureTheory.upperCrossingTime_succ_eq, le_rfl, Set.mem_setOf_eq, MeasureTheory.hittingBtwn_lt_iff
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ ∃ j ∈ Set.Ico (lowerCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) (N₂ + 1), f j ω ∈ Set.Ici b

Tactic:
⟨N₂, ⟨?_, Nat.lt_succ_self _⟩, hN₂'.le⟩

Premises used: Nat.lt_succ_self, LT.lt.le, And.intro, Exists.intro
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
refine : lowerCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N₂
⊢ ∃ j ∈ Set.Ico (lowerCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) (N₂ + 1), f j ω ∈ Set.Ici b

Tactic:
refine ⟨N₂, ⟨?_, Nat.lt_succ_self _⟩, hN₂'.le⟩
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
rw : ∃ j ∈ Set.Icc (upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) N₂, f j ω ∈ Set.Iic a
⊢ lowerCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N₂

Tactic:
rw [lowerCrossingTime, hittingBtwn_le_iff_of_lt _ (Nat.lt_succ_self _)]

Premises used: MeasureTheory.lowerCrossingTime, Nat.lt_succ_self, MeasureTheory.hittingBtwn_le_iff_of_lt
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ ∃ j ∈ Set.Icc (upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) N₂, f j ω ∈ Set.Iic a

Tactic:
⟨N₁, ⟨le_trans ?_ hN₁, hN₂⟩, hN₁'.le⟩

Premises used: LT.lt.le, And.intro, Exists.intro, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
refine : upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
⊢ ∃ j ∈ Set.Icc (upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) N₂, f j ω ∈ Set.Iic a

Tactic:
refine ⟨N₁, ⟨le_trans ?_ hN₁, hN₂⟩, hN₁'.le⟩
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
pos : ∀ (hN : 0 < N), upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
neg : ∀ (hN : N ≤ 0), upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N

Tactic:
by_cases! hN : 0 < N
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : 0 < N
⊢ upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N

Tactic:
have : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N :=
      Nat.sSup_mem (upperCrossingTime_lt_nonempty hN) (upperCrossingTime_lt_bddAbove hab)
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : 0 < N
this : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N
pos : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω ≤ N
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N

Tactic:
rw [upperCrossingTime_eq_upperCrossingTime_of_lt (hN₁.trans (hN₂.trans <| Nat.le_succ _))
      this]

Premises used: MeasureTheory.upperCrossingTime_eq_upperCrossingTime_of_lt, Nat.le_succ, LE.le.trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : 0 < N
this : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N
⊢ upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω ≤ N

Tactic:
this.le

Premises used: LT.lt.le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : 0 < N
this : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N
⊢ upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω ≤ N

Tactic:
exact this.le

Premises used: LT.lt.le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : N ≤ 0
⊢ N = 0

Tactic:
rw [Nat.le_zero] at hN

Premises used: Nat.le_zero
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : N = 0
neg : upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f 0 ω) ω ≤ 0
neg₁ : upperCrossingTime a b f (N₂ + 1) 0 ω ≤ 0
neg₂ : LE.le (α := ℕ) (⊥ ω) 0
neg₃ : LE.le (α := ℕ) ⊥ 0
neg₄ neg₅ : LE.le (α := ℕ) 0 0
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N

Tactic:
rw [hN, upcrossingsBefore_zero, upperCrossingTime_zero, Pi.bot_apply, bot_eq_zero']

Premises used: Pi.bot_apply, MeasureTheory.upperCrossingTime_zero, MeasureTheory.upcrossingsBefore_zero, bot_eq_zero'
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hN : 0 < N
hab : a < b
hn : n < upcrossingsBefore a b f N ω
⊢ lowerCrossingTime a b f N n ω < N

Tactic:
lt_of_le_of_lt lowerCrossingTime_le_upperCrossingTime_succ
    (upperCrossingTime_lt_of_le_upcrossingsBefore hN hab hn)

Premises used: lt_of_le_of_lt, MeasureTheory.upperCrossingTime_lt_of_le_upcrossingsBefore, MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ