Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
⊢ (if ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a) then
      sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ (f i ω - a)⁺ + a})
    else N) =
    if ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b then
      sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ f i ω})
    else N

Tactic:
split_ifs with h₁ h₂ h₂

Goal state after:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ (f i ω - a)⁺ + a}) =
    sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ f i ω})

case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ¬∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ (f i ω - a)⁺ + a}) = N

case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ N = sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ f i ω})

case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ¬∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ N = N