-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem crossing_pos_eq (hab : a < b) :
    upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = upperCrossingTime a b f N n ∧
      lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = lowerCrossingTime a b f N n

Proof state:
case zero.h
Ω : 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
ω : Ω
⊢ (if ∃ j ∈ Set.Icc ⊥ N, (f j ω - a)⁺ ∈ Set.Iic 0 then sInf (Set.Icc ⊥ N ∩ {i | (f i ω - a)⁺ ≤ 0}) else N) =
    if ∃ j ∈ Set.Icc ⊥ N, f j ω ∈ Set.Iic a then sInf (Set.Icc ⊥ N ∩ {i | f i ω ≤ a}) else N

Tactic:
split_ifs with h₁ h₂ h₂

Result:
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
ω : Ω
h₁ : ∃ j ∈ Set.Icc ⊥ N, (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ∃ j ∈ Set.Icc ⊥ N, f j ω ∈ Set.Iic a
⊢ sInf (Set.Icc ⊥ N ∩ {i | (f i ω - a)⁺ ≤ 0}) = sInf (Set.Icc ⊥ N ∩ {i | f i ω ≤ a})

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
ω : Ω
h₁ : ∃ j ∈ Set.Icc ⊥ N, (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ¬∃ j ∈ Set.Icc ⊥ N, f j ω ∈ Set.Iic a
⊢ sInf (Set.Icc ⊥ N ∩ {i | (f i ω - a)⁺ ≤ 0}) = 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
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc ⊥ N, (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ∃ j ∈ Set.Icc ⊥ N, f j ω ∈ Set.Iic a
⊢ N = sInf (Set.Icc ⊥ N ∩ {i | f i ω ≤ a})

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
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc ⊥ N, (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ¬∃ j ∈ Set.Icc ⊥ N, f j ω ∈ Set.Iic a
⊢ N = N

Proof state:
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
ω : Ω
h₁ : ∃ j ∈ Set.Icc ⊥ N, (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ¬∃ j ∈ Set.Icc ⊥ N, (f j ω - a)⁺ ≤ 0
⊢ sInf (Set.Icc ⊥ N ∩ {i | (f i ω - a)⁺ ≤ 0}) = N

Tactic:
exact False.elim (h₂ h₁)

Result:
no goals

Proof state:
case h
Ω : 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
ω : Ω
⊢ upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) ω = upperCrossingTime a b f N (k + 1) ω

Tactic:
simp only [upperCrossingTime_succ_eq, ← ih.2, hitting, Set.mem_Ici, tsub_le_iff_right]

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

Proof state:
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
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc ⊥ N, (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ∃ j ∈ Set.Icc ⊥ N, f j ω ∈ Set.Iic a
⊢ N = sInf (Set.Icc ⊥ N ∩ {i | f i ω ≤ a})

Tactic:
simp_rw [Set.mem_Iic, hf' _ _] at h₁

Result:
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
ω : Ω
h₂ : ∃ j ∈ Set.Icc ⊥ N, f j ω ∈ Set.Iic a
h₁ : ¬∃ j ∈ Set.Icc ⊥ N, f j ω ≤ a
⊢ N = sInf (Set.Icc ⊥ N ∩ {i | f i ω ≤ a})

Proof state:
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
ω : Ω
h₂ : ∃ j ∈ Set.Icc ⊥ N, f j ω ∈ Set.Iic a
h₁ : ¬∃ j ∈ Set.Icc ⊥ N, f j ω ≤ a
⊢ N = sInf (Set.Icc ⊥ N ∩ {i | f i ω ≤ a})

Tactic:
exact False.elim (h₁ h₂)

Result:
no goals

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
⊢ b - a ≤ (f ω i - a)⁺ ↔ b ≤ f ω i

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
h : b - a ≤ (f ω i - a)⁺
⊢ b ≤ f ω i

case refine_2
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
h : b ≤ f ω i
⊢ b - a ≤ (f ω i - a)⁺

Proof state:
Ω : 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 ω
⊢ upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = upperCrossingTime a b f N n ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = lowerCrossingTime a b f N n

Tactic:
have hf' (ω i) : (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a := by rw [posPart_nonpos, sub_nonpos]

Result:
Ω : 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
⊢ upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = upperCrossingTime a b f N n ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = lowerCrossingTime a b f N n

Proof state:
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
this : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) ω) N, (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) ω) N, (f j ω - a)⁺ ∈ Set.Iic 0

Tactic:
simp_all only [Set.mem_Iic]

Result:
no goals