awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : 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
have neg : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
Tactic: refine False.elim (h₂ ?_)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : 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 ω})
have pos : ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
Tactic: refine False.elim (h₁ ?_)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : 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)
have this : upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
Tactic: have : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) =
        upperCrossingTime a b f N (k + 1) := by
      ext ω
      simp only [upperCrossingTime_succ_eq, ← ih.2, hittingBtwn, Set.mem_Ici, tsub_le_iff_right]
      split_ifs with h₁ h₂ h₂
      · simp_rw [← sub_le_iff_le_add, hf ω]
      · refine False.elim (h₂ ?_)
        simp_all only [Set.mem_Ici, not_true_eq_false]
      · refine False.elim (h₁ ?_)
        simp_all only [Set.mem_Ici]
      · rfl
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : 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)
⊢ 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)
have succ : lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) = lowerCrossingTime a b f N (k + 1)
Tactic: refine ⟨this, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : 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)
have succ : ∀ (ω : Ω),
  lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω = lowerCrossingTime a b f N (k + 1) ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : 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) ω
have succ : (if
      ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
        Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺ 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
Tactic: simp only [lowerCrossingTime, this, hittingBtwn, Set.mem_Iic]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : 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,
          Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺ 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
have pos : ∀
  (h₁ :
    ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
      Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺)
  (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: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : 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)
ω : Ω
pos :
  ∀
    (h₁ :
      ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
        Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺)
    (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})
⊢ (if
        ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
          Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺ 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
have neg : ∀
  (h₁ :
    ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
      Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺)
  (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: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : 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)
ω : Ω
pos :
  ∀
    (h₁ :
      ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
        Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺)
    (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})
neg :
  ∀
    (h₁ :
      ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
        Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺)
    (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
⊢ (if
        ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
          Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺ 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
have pos₁ : ∀
  (h₁ :
    ¬∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
        Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺)
  (h₂ : ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a),
  N = sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i : ℕ | f i ω ≤ a})
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : 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)
ω : Ω
pos :
  ∀
    (h₁ :
      ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
        Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺)
    (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})
neg :
  ∀
    (h₁ :
      ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
        Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺)
    (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
pos₁ :
  ∀
    (h₁ :
      ¬∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
          Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺)
    (h₂ : ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a),
    N = sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i : ℕ | f i ω ≤ a})
⊢ (if
        ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
          Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺ 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
have neg₁ : ∀
  (h₁ :
    ¬∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
        Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺)
  (h₂ : ¬∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a), N = N
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : 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,
    Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺
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
have neg : ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
Tactic: refine False.elim (h₂ ?_)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : 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,
      Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺
h₂ : ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ N = sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i : ℕ | f i ω ≤ a})
have pos : ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
  Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺
Tactic: refine False.elim (h₁ ?_)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : 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
have zero : 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
Tactic: induction n with
  | zero =>
    refine ⟨rfl, ?_⟩
    simp +unfoldPartialApp only [lowerCrossingTime_zero, hittingBtwn,
      Set.mem_Icc, Set.mem_Iic]
    simp_all
  | succ k ih =>
    have : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) =
        upperCrossingTime a b f N (k + 1) := by
      ext ω
      simp only [upperCrossingTime_succ_eq, ← ih.2, hittingBtwn, Set.mem_Ici, tsub_le_iff_right]
      split_ifs with h₁ h₂ h₂
      · simp_rw [← sub_le_iff_le_add, hf ω]
      · refine False.elim (h₂ ?_)
        simp_all only [Set.mem_Ici, not_true_eq_false]
      · refine False.elim (h₁ ?_)
        simp_all only [Set.mem_Ici]
      · rfl
    refine ⟨this, ?_⟩
    ext ω
    simp only [lowerCrossingTime, this, hittingBtwn, Set.mem_Iic]
    split_ifs with h₁ h₂ h₂
    · simp_rw [hf' ω]
    · refine False.elim (h₂ ?_)
      simp_all only [Set.mem_Iic, not_true_eq_false]
    · refine False.elim (h₁ ?_)
      simp_all only [Set.mem_Iic]
    · rfl
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : 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
zero :
  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
⊢ 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
have succ : ∀ (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)
Tactic: induction n with
  | zero =>
    refine ⟨rfl, ?_⟩
    simp +unfoldPartialApp only [lowerCrossingTime_zero, hittingBtwn,
      Set.mem_Icc, Set.mem_Iic]
    simp_all
  | succ k ih =>
    have : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) =
        upperCrossingTime a b f N (k + 1) := by
      ext ω
      simp only [upperCrossingTime_succ_eq, ← ih.2, hittingBtwn, Set.mem_Ici, tsub_le_iff_right]
      split_ifs with h₁ h₂ h₂
      · simp_rw [← sub_le_iff_le_add, hf ω]
      · refine False.elim (h₂ ?_)
        simp_all only [Set.mem_Ici, not_true_eq_false]
      · refine False.elim (h₁ ?_)
        simp_all only [Set.mem_Ici]
      · rfl
    refine ⟨this, ?_⟩
    ext ω
    simp only [lowerCrossingTime, this, hittingBtwn, Set.mem_Iic]
    split_ifs with h₁ h₂ h₂
    · simp_rw [hf' ω]
    · refine False.elim (h₂ ?_)
      simp_all only [Set.mem_Iic, not_true_eq_false]
    · refine False.elim (h₁ ?_)
      simp_all only [Set.mem_Iic]
    · rfl
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ (f N ω - a)⁺) x ∂μ
have refine : (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ =
  (b - a - 0) * ∫ (x : Ω), (↑(upcrossingsBefore 0 (b - a) (f - fun (x : ℕ) (x_1 : Ω) ↦ a)⁺ N x) : ℝ) ∂μ
Tactic: refine le_trans (le_of_eq ?_)
    (integral_mul_upcrossingsBefore_le_integral (hf.sub_martingale (martingale_const _ _ _)).pos
      (fun ω => posPart_nonneg _)
      (fun ω => posPart_nonneg _) (sub_pos.2 hab))
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ =
    (b - a - 0) * ∫ (x : Ω), (↑(upcrossingsBefore 0 (b - a) (f - fun (x : ℕ) (x_1 : Ω) ↦ a)⁺ N x) : ℝ) ∂μ
have simp_rw : (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N x) : ℝ) ∂μ =
  (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore 0 (b - a) (f - fun (x : ℕ) (x_1 : Ω) ↦ a)⁺ N x) : ℝ) ∂μ
Tactic: simp_rw [sub_zero, ← upcrossingsBefore_pos_eq hab]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
⊢ (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ (f N ω - a)⁺) x ∂μ
have pos : ∀ (hab : a < b),
  (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ (f N ω - a)⁺) x ∂μ
Tactic: by_cases! hab : a < b
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
pos :
  ∀ (hab : a < b),
    (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ (f N ω - a)⁺) x ∂μ
⊢ (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ (f N ω - a)⁺) x ∂μ
have neg : ∀ (hab : b ≤ a),
  (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ (f N ω - a)⁺) x ∂μ
Tactic: by_cases! hab : a < b
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : b ≤ a
⊢ (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ (f N ω - a)⁺) x ∂μ
have hab₁ : b - a ≤ 0
Tactic: rw [← sub_nonpos] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
⊢ upcrossingsBefore a b f N ω =
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i
have pos : ∀ (hN : N = 0),
  upcrossingsBefore a b f N ω =
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i
Tactic: by_cases hN : N = 0