awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Upcrossing
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, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    HSub.hSub (α := ℝ) (∫ (x : Ω), f n x ∂μ) (∫ (x : Ω), f 0 x ∂μ)

Tactic:
le_trans h₁ ?_

Premises used: le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 ∂μ)
refine :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ ≤
    HSub.hSub (α := ℝ) (∫ (x : Ω), f n x ∂μ) (∫ (x : Ω), f 0 x ∂μ)
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    HSub.hSub (α := ℝ) (∫ (x : Ω), f n x ∂μ) (∫ (x : Ω), f 0 x ∂μ)

Tactic:
refine le_trans h₁ ?_

Premises used: le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 ∂μ)
simp_rw₁ :
  HSub.hSub (α := ℝ) (∫ (a : Ω), f n a ∂μ) (∫ (a : Ω), f 0 a ∂μ) ≤
    HSub.hSub (α := ℝ) (∫ (a : Ω), f n a ∂μ) (∫ (a : Ω), f 0 a ∂μ)
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) 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]

Premises used: le_refl, MeasureTheory.Submartingale.integrable, MeasureTheory.integral_sub', Finset.sum_range_sub
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : Preorder ι
inst_1 : OrderBot ι
inst_2 : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
ω : Ω
⊢ upcrossingsBefore a b f ⊥ ω = ⊥

Tactic:
simp [upcrossingsBefore]

Premises used: MeasureTheory.upcrossingsBefore
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossingsBefore a b f 0 ω = 0

Tactic:
simp [upcrossingsBefore]

Premises used: MeasureTheory.upcrossingsBefore
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
h : ∀ (ω : Ω), upcrossingsBefore a b f 0 ω = 0 ω
⊢ upcrossingsBefore a b f 0 = 0

Tactic:
ext ω
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossingsBefore a b f 0 ω = 0 ω

Tactic:
upcrossingsBefore_zero

Premises used: MeasureTheory.upcrossingsBefore_zero
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossingsBefore a b f 0 ω = 0 ω

Tactic:
exact upcrossingsBefore_zero

Premises used: MeasureTheory.upcrossingsBefore_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 ω
⊢ upperCrossingTime a b f N n ω < N

Tactic:
haveI : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N :=
    (upperCrossingTime_lt_nonempty hN).csSup_mem
      ((OrderBot.bddBelow _).finite_of_bddAbove (upperCrossingTime_lt_bddAbove hab))
  lt_of_le_of_lt (upperCrossingTime_mono hn) this

Premises used: lt_of_le_of_lt, MeasureTheory.upperCrossingTime_mono, Set.Nonempty.csSup_mem, MeasureTheory.upperCrossingTime_lt_bddAbove, MeasureTheory.upperCrossingTime_lt_nonempty, OrderBot.bddBelow, BddBelow.finite_of_bddAbove
-- Module: Mathlib.Probability.Martingale.Upcrossing
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

Tactic:
le_antisymm upperCrossingTime_le (not_lt.1 ?_)

Premises used: le_antisymm, not_lt, Iff.mp, MeasureTheory.upperCrossingTime_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
refine : ¬upperCrossingTime a b f N n ω < N
⊢ upperCrossingTime a b f N n ω = N

Tactic:
refine le_antisymm upperCrossingTime_le (not_lt.1 ?_)

Premises used: le_antisymm, MeasureTheory.upperCrossingTime_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ n ∉ {n : ℕ | upperCrossingTime a b f N n ω < N}

Tactic:
notMem_of_csSup_lt hn (upperCrossingTime_lt_bddAbove hab)

Premises used: notMem_of_csSup_lt, MeasureTheory.upperCrossingTime_lt_bddAbove
-- Module: Mathlib.Probability.Martingale.Upcrossing
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

Tactic:
convert! notMem_of_csSup_lt hn (upperCrossingTime_lt_bddAbove hab) using 1

Premises used: notMem_of_csSup_lt, MeasureTheory.upperCrossingTime_lt_bddAbove
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
pos : ∀ (hN : N = 0), upcrossingsBefore a b f N ω ≤ N
neg : ∀ (hN : ¬N = 0), upcrossingsBefore a b f N ω ≤ N
⊢ upcrossingsBefore a b f N ω ≤ N

Tactic:
by_cases hN : N = 0
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : N = 0
pos : upcrossingsBefore a b f 0 ω ≤ 0
⊢ upcrossingsBefore a b f N ω ≤ N

Tactic:
subst hN
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
pos pos₁ : LE.le (α := ℕ) 0 0
⊢ upcrossingsBefore a b f 0 ω ≤ 0

Tactic:
rw [upcrossingsBefore_zero]

Premises used: MeasureTheory.upcrossingsBefore_zero
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
⊢ upcrossingsBefore a b f N ω ≤ N

Tactic:
csSup_le ⟨0, zero_lt_iff.2 hN⟩ fun n (hn : _ < N) => ?_

Premises used: Iff.mpr, Exists.intro, zero_lt_iff, OfNat.ofNat, MeasureTheory.upcrossingsBefore, csSup_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
neg : ∀ (n : ℕ) (hn : upperCrossingTime a b f N n ω < N), n ≤ N
⊢ upcrossingsBefore a b f N ω ≤ N

Tactic:
refine csSup_le ⟨0, zero_lt_iff.2 hN⟩ fun n (hn : _ < N) => ?_

Premises used: Iff.mpr, Exists.intro, zero_lt_iff, OfNat.ofNat, csSup_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
n : ℕ
hn : upperCrossingTime a b f N n ω < N
neg : ∀ (hnN : ¬n ≤ N), False
⊢ n ≤ N

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

Tactic:
hn.ne (upperCrossingTime_eq_of_bound_le hab (not_le.1 hnN).le)

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

Tactic:
exact hn.ne (upperCrossingTime_eq_of_bound_le hab (not_le.1 hnN).le)

Premises used: not_le, LT.lt.le, MeasureTheory.upperCrossingTime_eq_of_bound_le, Iff.mp, LT.lt.ne
-- 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
⊢ 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
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 : hittingBtwn f (Set.Iic a) 0 N ω = hittingBtwn f (Set.Iic a) 0 M ω
⊢ 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:
simp only [upperCrossingTime_zero, bot_eq_zero',
      lowerCrossingTime_zero, true_and, eq_comm]

Premises used: MeasureTheory.lowerCrossingTime_zero, eq_comm, MeasureTheory.upperCrossingTime_zero, true_and, bot_eq_zero'
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 ω

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 : lowerCrossingTime a b f N 0 ω < N
h' : upperCrossingTime a b f N 0 ω < N
zero : ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a
⊢ hittingBtwn f (Set.Iic a) 0 N ω = hittingBtwn f (Set.Iic a) 0 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 : 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
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
⊢ ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a

Tactic:
rw [lowerCrossingTime, hittingBtwn_lt_iff] at h

Premises used: MeasureTheory.lowerCrossingTime, 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 (upperCrossingTime a b f N 0 ω) N, f j ω ∈ Set.Iic a
h' : upperCrossingTime a b f N 0 ω < N
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
⊢ ∃ j ∈ Set.Icc 0 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
h' : upperCrossingTime a b f N 0 ω < N
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:
⟨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
h' : upperCrossingTime a b f N 0 ω < N
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:
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.Iic a) (upperCrossingTime a b f N 0 ω) N ω < N
h' : upperCrossingTime a b f N 0 ω < 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.Iic a) (upperCrossingTime a b f N 0 ω) N ω < N
h' : upperCrossingTime a b f N 0 ω < 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
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 ω = 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')

Premises used: lt_of_le_of_lt, MeasureTheory.upperCrossingTime_mono, Nat.le_succ, MeasureTheory.lowerCrossingTime_mono
-- 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 ω
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 ω
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
⊢ upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω

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
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 ω
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 ω
⊢ 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'
-- 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
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
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 ω
⊢ 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:
rw [eq_comm, ih.2]

Premises used: eq_comm, And.right
-- 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
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 N k ω) N ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) M ω

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

Premises used: LT.lt.le, And.right, And.left, And.intro, Exists.intro, MeasureTheory.hittingBtwn_eq_hittingBtwn_of_exists
-- 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
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 N k ω) N ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) M ω

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

Premises used: LT.lt.le, And.right, And.left, And.intro, Exists.intro, MeasureTheory.hittingBtwn_eq_hittingBtwn_of_exists
-- 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' : 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:
le_rfl

Premises used: le_rfl
-- 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' : 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:
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
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 ω

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
-- 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 ω
⊢ 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:
⟨this, ?_⟩

Premises used: And.intro
-- 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 ω
succ : lowerCrossingTime a b f M (k + 1) ω = lowerCrossingTime a b f N (k + 1) ω
⊢ 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:
refine ⟨this, ?_⟩
-- 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 ω
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 ω
⊢ lowerCrossingTime a b f M (k + 1) ω = lowerCrossingTime a b f N (k + 1) ω

Tactic:
simp only [lowerCrossingTime, eq_comm, this, Nat.succ_eq_add_one]

Premises used: Nat.succ_eq_add_one, MeasureTheory.lowerCrossingTime, eq_comm
-- 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 ω
⊢ 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:
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
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 ω
succ : ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ 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:
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
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.Ico (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a

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

Premises used: le_rfl, MeasureTheory.lowerCrossingTime, MeasureTheory.hittingBtwn_lt_iff