-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem crossing_eq_crossing_of_lowerCrossingTime_lt {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 ω

Proof state:
case zero
Ω : 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 ω

Tactic:
simp only [upperCrossingTime_zero, bot_eq_zero', eq_self_iff_true,
  lowerCrossingTime_zero, true_and, eq_comm]

Result:
case zero
Ω : 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
⊢ hitting f (Set.Iic a) 0 N ω = hitting f (Set.Iic a) 0 M ω

Proof state:
Ω : 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 ω

Tactic:
induction' n with k ih

Result:
case zero
Ω : 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 ω

case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  lowerCrossingTime a b f N k ω < N →
    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) ω

Proof state:
case succ
Ω : 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

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

Result:
case succ
Ω : 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

Proof state:
Ω : 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 ω
⊢ upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω

Tactic:
simp only [upperCrossingTime_succ_eq]

Result:
Ω : 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 ω
⊢ hitting f (Set.Ici b) (lowerCrossingTime a b f M k ω) M ω = hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω

Proof state:
case hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : hitting 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

Result:
no goals

Proof state:
case intro.intro
Ω : 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
⊢ hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω = hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) M ω

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

Result:
no goals

Proof state:
case succ.intro.intro
Ω : 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₂⟩

Result:
no goals

Proof state:
Ω : 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 ω
⊢ hitting f (Set.Ici b) (lowerCrossingTime a b f M k ω) M ω = hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := h'

Result:
case intro.intro
Ω : 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
⊢ hitting f (Set.Ici b) (lowerCrossingTime a b f M k ω) M ω = hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω

Proof state:
case succ
Ω : 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) ω

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

Result:
case succ
Ω : 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 ω
⊢ hitting f (Set.Iic a) (upperCrossingTime a b f N (k + 1) ω) N ω =
    hitting f (Set.Iic a) (upperCrossingTime a b f N (k + 1) ω) M ω