-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem Adapted.isStoppingTime_crossing (hf : Adapted ℱ f) :
    IsStoppingTime ℱ (upperCrossingTime a b f N n) ∧
      IsStoppingTime ℱ (lowerCrossingTime a b f N n)

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
⊢ IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1))

Tactic:
intro n

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
n : ℕ
⊢ MeasurableSet {ω | upperCrossingTime a b f N (k + 1) ω ≤ n}

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
n : ℕ
⊢ MeasurableSet {ω | upperCrossingTime a b f N (k + 1) ω ≤ n}

Tactic:
simp_rw [upperCrossingTime_succ_eq]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
n : ℕ
⊢ MeasurableSet {ω | hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω ≤ n}

Proof state:
case succ
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
ih : IsStoppingTime ℱ (upperCrossingTime a b f N k) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N k)
⊢ IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1)) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N (k + 1))

Tactic:
obtain ⟨_, ih₂⟩ := ih

Result:
case succ.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
⊢ IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1)) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N (k + 1))

Proof state:
case zero
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
⊢ IsStoppingTime ℱ (lowerCrossingTime a b f N 0)

Tactic:
simp [hitting_isStoppingTime hf measurableSet_Iic]

Result:
no goals

Proof state:
case succ.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
⊢ IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1)) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N (k + 1))

Tactic:
have : IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1)) := by
  intro n
  simp_rw [upperCrossingTime_succ_eq]
  exact isStoppingTime_hitting_isStoppingTime ih₂ (fun _ => lowerCrossingTime_le)
    measurableSet_Ici hf _

Result:
case succ.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
this : IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1))
⊢ IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1)) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N (k + 1))

Proof state:
case succ.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
this : IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1))
n : ℕ
⊢ MeasurableSet {ω | lowerCrossingTime a b f N (k + 1) ω ≤ n}

Tactic:
exact isStoppingTime_hitting_isStoppingTime this (fun _ => upperCrossingTime_le)
  measurableSet_Iic hf _

Result:
no goals

Proof state:
case succ.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
this : IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1))
⊢ IsStoppingTime ℱ (lowerCrossingTime a b f N (k + 1))

Tactic:
intro n

Result:
case succ.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
this : IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1))
n : ℕ
⊢ MeasurableSet {ω | lowerCrossingTime a b f N (k + 1) ω ≤ n}

Proof state:
case succ.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
this : IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1))
⊢ IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1)) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N (k + 1))

Tactic:
refine ⟨this, ?_⟩

Result:
case succ.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
this : IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1))
⊢ IsStoppingTime ℱ (lowerCrossingTime a b f N (k + 1))

Proof state:
case zero
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
⊢ IsStoppingTime ℱ (upperCrossingTime a b f N 0) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N 0)

Tactic:
refine ⟨isStoppingTime_const _ 0, ?_⟩

Result:
case zero
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
⊢ IsStoppingTime ℱ (lowerCrossingTime a b f N 0)

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
n : ℕ
⊢ MeasurableSet {ω | hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω ≤ n}

Tactic:
exact isStoppingTime_hitting_isStoppingTime ih₂ (fun _ => lowerCrossingTime_le)
  measurableSet_Ici hf _

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
⊢ IsStoppingTime ℱ (upperCrossingTime a b f N n) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N n)

Tactic:
induction' n with k ih

Result:
case zero
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
⊢ IsStoppingTime ℱ (upperCrossingTime a b f N 0) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N 0)

case succ
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
ih : IsStoppingTime ℱ (upperCrossingTime a b f N k) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N k)
⊢ IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1)) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N (k + 1))