-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem leastGE_eq_min (π : Ω → ℕ) (r : ℝ) (ω : Ω) {n : ℕ} (hπn : ∀ ω, π ω ≤ n) :
    leastGE f r (π ω) ω = min (π ω) (leastGE f r n ω)

Proof state:
case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : π ω ≤ leastGE f r n ω
h : ∃ j ∈ Set.Icc 0 (π ω), f j ω ∈ Set.Ici r
⊢ π ω ≤ hitting f (Set.Ici r) 0 (π ω) ω

Tactic:
refine hle.trans (Eq.le ?_)

Result:
case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : π ω ≤ leastGE f r n ω
h : ∃ j ∈ Set.Icc 0 (π ω), f j ω ∈ Set.Ici r
⊢ leastGE f r n ω = hitting f (Set.Ici r) 0 (π ω) ω

Proof state:
case neg
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : ¬π ω ≤ leastGE f r n ω
⊢ π ω ⊓ leastGE f r n ω ≤ leastGE f r (π ω) ω

Tactic:
rw [min_eq_right (not_le.1 hle).le, leastGE, leastGE, ←
  hitting_eq_hitting_of_exists (hπn ω) _]

Result:
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : ¬π ω ≤ leastGE f r n ω
⊢ ∃ j ∈ Set.Icc 0 (π ω), f j ω ∈ Set.Ici r

Proof state:
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : ¬π ω ≤ leastGE f r n ω
⊢ ∃ j ∈ Set.Icc 0 (π ω), f j ω ∈ Set.Ici r

Tactic:
rw [not_le, leastGE, hitting_lt_iff _ (hπn ω)] at hle

Result:
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : ∃ j ∈ Set.Ico 0 (π ω), f j ω ∈ Set.Ici r
⊢ ∃ j ∈ Set.Icc 0 (π ω), f j ω ∈ Set.Ici r

Proof state:
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : ∃ j ∈ Set.Ico 0 (π ω), f j ω ∈ Set.Ici r
⊢ ∃ j ∈ Set.Icc 0 (π ω), f j ω ∈ Set.Ici r

Tactic:
exact
  let ⟨j, hj₁, hj₂⟩ := hle
  ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩

Result:
no goals

Proof state:
case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : π ω ≤ leastGE f r n ω
h : ∃ j ∈ Set.Icc 0 (π ω), f j ω ∈ Set.Ici r
⊢ leastGE f r n ω = hitting f (Set.Ici r) 0 (π ω) ω

Tactic:
rw [leastGE, ← hitting_eq_hitting_of_exists (hπn ω) h]

Result:
no goals

Proof state:
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
⊢ leastGE f r (π ω) ω = π ω ⊓ leastGE f r n ω

Tactic:
refine le_antisymm (le_min (leastGE_le _) (leastGE_mono (hπn ω) r ω)) ?_

Result:
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
⊢ π ω ⊓ leastGE f r n ω ≤ leastGE f r (π ω) ω

Proof state:
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
⊢ π ω ⊓ leastGE f r n ω ≤ leastGE f r (π ω) ω

Tactic:
by_cases hle : π ω ≤ leastGE f r n ω

Result:
case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : π ω ≤ leastGE f r n ω
⊢ π ω ⊓ leastGE f r n ω ≤ leastGE f r (π ω) ω

case neg
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : ¬π ω ≤ leastGE f r n ω
⊢ π ω ⊓ leastGE f r n ω ≤ leastGE f r (π ω) ω

Proof state:
case neg
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : π ω ≤ leastGE f r n ω
h : ¬∃ j ∈ Set.Icc 0 (π ω), f j ω ∈ Set.Ici r
⊢ π ω ≤ hitting f (Set.Ici r) 0 (π ω) ω

Tactic:
simp only [hitting, if_neg h, le_rfl]

Result:
no goals

Proof state:
case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : π ω ≤ leastGE f r n ω
⊢ π ω ≤ hitting f (Set.Ici r) 0 (π ω) ω

Tactic:
by_cases h : ∃ j ∈ Set.Icc 0 (π ω), f j ω ∈ Set.Ici r

Result:
case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : π ω ≤ leastGE f r n ω
h : ∃ j ∈ Set.Icc 0 (π ω), f j ω ∈ Set.Ici r
⊢ π ω ≤ hitting f (Set.Ici r) 0 (π ω) ω

case neg
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : π ω ≤ leastGE f r n ω
h : ¬∃ j ∈ Set.Icc 0 (π ω), f j ω ∈ Set.Ici r
⊢ π ω ≤ hitting f (Set.Ici r) 0 (π ω) ω

Proof state:
case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : π ω ≤ leastGE f r n ω
⊢ π ω ⊓ leastGE f r n ω ≤ leastGE f r (π ω) ω

Tactic:
rw [min_eq_left hle, leastGE]

Result:
case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
ω : Ω
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
hle : π ω ≤ leastGE f r n ω
⊢ π ω ≤ hitting f (Set.Ici r) 0 (π ω) ω