-- 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 succ.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
this : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
⊢ lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) ω = lowerCrossingTime a b f N (k + 1) ω

Tactic:
simp only [lowerCrossingTime, this, hitting, Set.mem_Iic]

Result:
case succ.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
this : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
⊢ (if ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) ω) N, (f j ω - a)⁺ ∈ Set.Iic 0 then
      sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i | (f i ω - a)⁺ ≤ 0})
    else N) =
    if ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a then
      sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i | f i ω ≤ a})
    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
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
⊢ sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i | (f i ω - a)⁺ ≤ 0}) =
    sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i | f i ω ≤ a})

Tactic:
simp_rw [hf' ω]

Result:
no goals

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
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
⊢ sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i | (f i ω - a)⁺ ≤ 0}) = N

Tactic:
refine False.elim (h₂ ?_)

Result:
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
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 a b f N (k + 1) ω) N, f j ω ∈ Set.Iic 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 ω
ω : Ω
i : ℕ
⊢ (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a

Tactic:
rw [posPart_nonpos, sub_nonpos]

Result:
no goals

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

Tactic:
rwa [posPart_eq_self.2 (le_trans hab'.le h)]

Result:
no goals

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 ω
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

Tactic:
induction' n with k ih

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

case succ
Ω : 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) ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = lowerCrossingTime a b f N (k + 1)

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
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 a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a

Tactic:
simp_all only [Set.mem_Iic, not_true_eq_false]

Result:
no goals

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 ω ∈ Set.Iic a
⊢ N = N

Tactic:
rfl

Result:
no goals