awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
h : b - a ≤ (f ω i - a)⁺
refine_1 : b - a ≤ f ω i - a
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : b - a ≤ (f ω i - a)⁺
⊢ b ≤ f ω i

Tactic:
rwa [← sub_le_sub_iff_right a, ←
        posPart_eq_of_posPart_pos (lt_of_lt_of_le hab' h)]

Premises used: sub_le_sub_iff_right, posPart_eq_of_posPart_pos, lt_of_lt_of_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : 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

Tactic:
rw [← sub_le_sub_iff_right a] at h

Premises used: sub_le_sub_iff_right
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
h : b - a ≤ f ω i - a
refine_2 refine_2₁ refine_2₂ refine_2₃ : b - a ≤ f ω i - a
⊢ b - a ≤ (f ω i - a)⁺

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

Premises used: Iff.mpr, posPart_eq_self, LT.lt.le, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : 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:
have hf : ∀ ω i, b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω := by
    intro i ω
    refine ⟨fun h => ?_, fun h => ?_⟩
    · rwa [← sub_le_sub_iff_right a, ←
        posPart_eq_of_posPart_pos (lt_of_lt_of_le hab' h)]
    · rw [← sub_le_sub_iff_right a] at h
      rwa [posPart_eq_self.2 (le_trans hab'.le h)]
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 ω
ω : Ω
i : ℕ
rw : f i ω - a ≤ 0 ↔ f i ω ≤ a
rw₁ rw₂ : f i ω ≤ a ↔ f i ω ≤ a
⊢ (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a

Tactic:
rw [posPart_nonpos, sub_nonpos]

Premises used: posPart_nonpos, sub_nonpos
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 ω
⊢ ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a

Tactic:
have hf' (ω i) : (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a := by rw [posPart_nonpos, sub_nonpos]
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 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:
⟨rfl, ?_⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 : 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 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:
refine ⟨rfl, ?_⟩
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
⊢ Eq.{u_1 + 1} (α := Ω → ℕ)
    (fun (x : Ω) ↦
      if ∃ j ∈ Set.Icc ⊥ N, Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j x - a)⁺ then
        sInf (Set.Icc ⊥ N ∩ {i : ℕ | (f i x - a)⁺ ≤ 0})
      else N)
    fun (x : Ω) ↦ if ∃ j ∈ Set.Icc ⊥ N, f j x ∈ Set.Iic a then sInf (Set.Icc ⊥ N ∩ {i : ℕ | f i x ≤ a}) else N

Tactic:
simp_all
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 :
  ∀ (ω : Ω),
    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)

Tactic:
ext ω
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 :
  (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
⊢ 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, hittingBtwn, Set.mem_Ici, tsub_le_iff_right]

Premises used: MeasureTheory.upperCrossingTime_succ_eq, MeasureTheory.hittingBtwn, tsub_le_iff_right, And.right, Set.mem_Ici
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
ω : Ω
pos :
  ∀
    (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 ω})
neg :
  ∀
    (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
pos₁ :
  ∀
    (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 ω})
neg₁ :
  ∀
    (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
⊢ (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₂
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
pos :
  sInf
      (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩
        {i : ℕ | b - a ≤ (f i ω - a)⁺}) =
    sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩ {i : ℕ | b ≤ f i ω})
⊢ 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 ω})

Tactic:
simp_rw [← sub_le_iff_le_add, hf ω]

Premises used: sub_le_iff_le_add
-- Module: Mathlib.Probability.Martingale.Upcrossing
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

Tactic:
False.elim (h₂ ?_)

Premises used: False.elim
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
neg : ∃ 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

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

Premises used: False.elim
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
⊢ ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b

Tactic:
simp_all only [Set.mem_Ici, not_true_eq_false]

Premises used: not_true_eq_false, Set.mem_Ici
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 ω})

Tactic:
False.elim (h₁ ?_)

Premises used: False.elim
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
pos :
  ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
    (f j ω - a)⁺ ∈ Set.Ici (b - a)
⊢ N = sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩ {i : ℕ | b ≤ f i ω})

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

Premises used: False.elim
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
⊢ ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
    (f j ω - a)⁺ ∈ Set.Ici (b - a)

Tactic:
simp_all only [Set.mem_Ici]

Premises used: Set.mem_Ici
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 = N

Tactic:
rfl
-- Module: Mathlib.Probability.Martingale.Upcrossing
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)

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
-- Module: Mathlib.Probability.Martingale.Upcrossing
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)

Tactic:
⟨this, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Probability.Martingale.Upcrossing
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)
succ : lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) = lowerCrossingTime 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)

Tactic:
refine ⟨this, ?_⟩
-- Module: Mathlib.Probability.Martingale.Upcrossing
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)
succ :
  ∀ (ω : Ω),
    lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω = lowerCrossingTime 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:
ext ω
-- Module: Mathlib.Probability.Martingale.Upcrossing
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)
ω : Ω
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
⊢ lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω = lowerCrossingTime a b f N (k + 1) ω

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

Premises used: MeasureTheory.lowerCrossingTime, MeasureTheory.hittingBtwn, Set.mem_Iic
-- Module: Mathlib.Probability.Martingale.Upcrossing
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})
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
⊢ (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:
split_ifs with h₁ h₂ h₂
-- Module: Mathlib.Probability.Martingale.Upcrossing
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}) =
    sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i : ℕ | f i ω ≤ a})

Tactic:
simp_rw [hf' ω]