awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ :
  LE.le (α := ℝ) (∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ)
    (∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ)
h₂ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    HSub.hSub (α := ℝ) (∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ)
      (∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ)
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ ≤
    HSub.hSub (α := ℝ) (∫ (x : Ω), f n x ∂μ) (∫ (x : Ω), f 0 x ∂μ)
have simp_rw : ∫ (x : Ω), (f n - f 0) x ∂μ ≤ HSub.hSub (α := ℝ) (∫ (x : Ω), f n x ∂μ) (∫ (x : Ω), f 0 x ∂μ)
Tactic: simp_rw [Finset.sum_range_sub, integral_sub' (hf.integrable _) (hf.integrable _), le_refl]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ :
  LE.le (α := ℝ) (∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ)
    (∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ)
h₂ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    HSub.hSub (α := ℝ) (∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ)
      (∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ)
simp_rw : ∫ (x : Ω), (f n - f 0) x ∂μ ≤ HSub.hSub (α := ℝ) (∫ (x : Ω), f n x ∂μ) (∫ (x : Ω), f 0 x ∂μ)
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ ≤
    HSub.hSub (α := ℝ) (∫ (x : Ω), f n x ∂μ) (∫ (x : Ω), f 0 x ∂μ)
have simp_rw₁ : HSub.hSub (α := ℝ) (∫ (a : Ω), f n a ∂μ) (∫ (a : Ω), f 0 a ∂μ) ≤
  HSub.hSub (α := ℝ) (∫ (a : Ω), f n a ∂μ) (∫ (a : Ω), f 0 a ∂μ)
Tactic: simp_rw [Finset.sum_range_sub, integral_sub' (hf.integrable _) (hf.integrable _), le_refl]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
⊢ upcrossingsBefore a b f 0 = 0
have h : ∀ (ω : Ω), upcrossingsBefore a b f 0 ω = 0 ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ upperCrossingTime a b f N n ω = N
have refine : ¬upperCrossingTime a b f N n ω < N
Tactic: refine le_antisymm upperCrossingTime_le (not_lt.1 ?_)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
⊢ upcrossingsBefore a b f N ω ≤ N
have pos : ∀ (hN : N = 0), upcrossingsBefore a b f N ω ≤ N
Tactic: by_cases hN : N = 0
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
pos : ∀ (hN : N = 0), upcrossingsBefore a b f N ω ≤ N
⊢ upcrossingsBefore a b f N ω ≤ N
have neg : ∀ (hN : ¬N = 0), upcrossingsBefore a b f N ω ≤ N
Tactic: by_cases hN : N = 0
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : N = 0
⊢ upcrossingsBefore a b f N ω ≤ N
have pos : upcrossingsBefore a b f 0 ω ≤ 0
Tactic: subst hN
Cleared hypotheses: N, hN
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
⊢ upcrossingsBefore a b f 0 ω ≤ 0
have pos : LE.le (α := ℕ) 0 0
Tactic: rw [upcrossingsBefore_zero]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
⊢ upcrossingsBefore a b f N ω ≤ N
have neg : ∀ (n : ℕ) (hn : upperCrossingTime a b f N n ω < N), n ≤ N
Tactic: refine csSup_le ⟨0, zero_lt_iff.2 hN⟩ fun n (hn : _ < N) => ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
n : ℕ
hn : upperCrossingTime a b f N n ω < N
⊢ n ≤ N
have neg : ∀ (hnN : ¬n ≤ N), False
Tactic: by_contra hnN
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : lowerCrossingTime a b f N n ω < N
⊢ upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω ∧
    lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
have h' : upperCrossingTime a b f N n ω < N
Tactic: have h' : upperCrossingTime a b f N n ω < N :=
    lt_of_le_of_lt upperCrossingTime_le_lowerCrossingTime h
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
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 ω
have zero : hittingBtwn f (Set.Iic a) 0 N ω = hittingBtwn f (Set.Iic a) 0 M ω
Tactic: simp only [upperCrossingTime_zero, bot_eq_zero',
      lowerCrossingTime_zero, true_and, eq_comm]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : lowerCrossingTime a b f N 0 ω < N
h' : upperCrossingTime a b f N 0 ω < N
⊢ hittingBtwn f (Set.Iic a) 0 N ω = hittingBtwn f (Set.Iic a) 0 M ω
have zero : ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a
Tactic: refine hittingBtwn_eq_hittingBtwn_of_exists hNM ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : lowerCrossingTime a b f N 0 ω < N
h' : upperCrossingTime a b f N 0 ω < N
⊢ ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a
have zero : ∀ (h : ∃ j ∈ Set.Ico (upperCrossingTime a b f N 0 ω) N, f j ω ∈ Set.Iic a) (h' : upperCrossingTime a b f N 0 ω < N),
  ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a
Tactic: rw [lowerCrossingTime, hittingBtwn_lt_iff] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : lowerCrossingTime a b f N 0 ω < N
h' : upperCrossingTime a b f N 0 ω < N
zero :
  ∀ (h : ∃ j ∈ Set.Ico (upperCrossingTime a b f N 0 ω) N, f j ω ∈ Set.Iic a) (h' : upperCrossingTime a b f N 0 ω < N),
    ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a
⊢ ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a
have zero₁ : ∀ (h : hittingBtwn f (Set.Iic a) (upperCrossingTime a b f N 0 ω) N ω < N) (h' : upperCrossingTime a b f N 0 ω < N),
  N ≤ N
Tactic: rw [lowerCrossingTime, hittingBtwn_lt_iff] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : ∃ j ∈ Set.Ico (upperCrossingTime a b f N 0 ω) N, f j ω ∈ Set.Iic a
h' : upperCrossingTime a b f N 0 ω < N
⊢ ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a
have zero : ∀ (j : ℕ) (hj₁ : j ∈ Set.Ico (upperCrossingTime a b f N 0 ω) N) (hj₂ : f j ω ∈ Set.Iic a),
  ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a
Tactic: obtain ⟨j, hj₁, hj₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
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) ω
have 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 ω
Tactic: specialize ih (lt_of_le_of_lt (lowerCrossingTime_mono (Nat.le_succ _)) h)
      (lt_of_le_of_lt (upperCrossingTime_mono (Nat.le_succ _)) h')
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω
⊢ upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω
have rw : ∀ (h' : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b)
  (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 [upperCrossingTime_succ_eq, hittingBtwn_lt_iff] at h'
Cleared hypotheses: h', ih
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω
rw :
  ∀ (h' : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b)
    (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 ω
⊢ upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω
have hi : ∀ (h' : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω < 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 ω),
  N ≤ N
Tactic: rw [upperCrossingTime_succ_eq, hittingBtwn_lt_iff] at h'
Cleared hypotheses: h', ih
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
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 ω
⊢ hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f M k ω) M ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω
have obtain : ∀ (j : ℕ) (hj₁ : j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N) (hj₂ : f j ω ∈ Set.Ici b),
  hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f M k ω) M ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω
Tactic: obtain ⟨j, hj₁, hj₂⟩ := h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
h : lowerCrossingTime 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 ω
j : ℕ
hj₁ : j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N
hj₂ : f j ω ∈ Set.Ici b
⊢ hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f M k ω) M ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω
have rw : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω =
  hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) M ω
Tactic: rw [eq_comm, ih.2]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
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 ω
⊢ 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) ω
have this : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω
Tactic: 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
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω
⊢ 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) ω
have succ : lowerCrossingTime a b f M (k + 1) ω = lowerCrossingTime a b f N (k + 1) ω
Tactic: refine ⟨this, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω
⊢ lowerCrossingTime a b f M (k + 1) ω = lowerCrossingTime a b f N (k + 1) ω
have succ : hittingBtwn f (Set.Iic a) (upperCrossingTime a b f N (k + 1) ω) N ω =
  hittingBtwn f (Set.Iic a) (upperCrossingTime a b f N (k + 1) ω) M ω
Tactic: simp only [lowerCrossingTime, eq_comm, this, Nat.succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω
⊢ hittingBtwn f (Set.Iic a) (upperCrossingTime a b f N (k + 1) ω) N ω =
    hittingBtwn f (Set.Iic a) (upperCrossingTime a b f N (k + 1) ω) M ω
have succ : ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
Tactic: refine hittingBtwn_eq_hittingBtwn_of_exists hNM ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
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 ω
⊢ ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
have h₁ : ∃ j ∈ Set.Ico (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
Tactic: rw [lowerCrossingTime, hittingBtwn_lt_iff _ le_rfl] at h
Cleared hypotheses: h, h', ih, this
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω
⊢ ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
have 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: obtain ⟨j, hj₁, hj₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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
⊢ upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω ∧
    lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
have 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 ω
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₂⟩
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω
⊢ upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω ∧
    lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
have 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) ω
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₂⟩
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < 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 ω
have this : 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
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω
have refine : upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω
Tactic: refine ⟨?_, this⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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) ω
have 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 ω
Tactic: rw [upperCrossingTime_succ_eq, upperCrossingTime_succ_eq, eq_comm, this]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω
have refine : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
Tactic: refine hittingBtwn_eq_hittingBtwn_of_exists hNM ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω
⊢ ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
have 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
Tactic: rw [upperCrossingTime_succ_eq, hittingBtwn_lt_iff] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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
⊢ ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
have 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
Tactic: rw [upperCrossingTime_succ_eq, hittingBtwn_lt_iff] at h
Cleared hypotheses: h, this