-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem Martingale.bddAbove_range_iff_bddBelow_range [IsFiniteMeasure μ] (hf : Martingale f ℱ μ)
    (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) :
    ∀ᵐ ω ∂μ, BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)

Proof state:
case mp.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun n => f n ω) atTop (𝓝 c)
⊢ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)

Tactic:
exact ⟨-c, hc.neg⟩

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)

Tactic:
have hdown := hf.neg.submartingale.bddAbove_iff_exists_tendsto hbdd'

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)

Proof state:
case h.mpr.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n => f n ω✝) ↔ ∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω✝) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : c ∈ lowerBounds (Set.range fun n => f n ω✝)
ω : ℝ
hω : ω ∈ Set.range fun n => (-f) n ω✝
⊢ ω ≤ -c

Tactic:
rw [mem_lowerBounds] at hc

Result:
case h.mpr.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n => f n ω✝) ↔ ∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω✝) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : ∀ x ∈ Set.range fun n => f n ω✝, c ≤ x
ω : ℝ
hω : ω ∈ Set.range fun n => (-f) n ω✝
⊢ ω ≤ -c

Proof state:
case h.mpr.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n => f n ω✝) ↔ ∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω✝) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : ∀ x ∈ Set.range fun n => f n ω✝, c ≤ x
ω : ℝ
hω : ∃ y, f y ω✝ = -ω
⊢ ω ≤ -c

Tactic:
refine le_neg.1 (hc _ ?_)

Result:
case h.mpr.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n => f n ω✝) ↔ ∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω✝) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : ∀ x ∈ Set.range fun n => f n ω✝, c ≤ x
ω : ℝ
hω : ∃ y, f y ω✝ = -ω
⊢ -ω ∈ Set.range fun n => f n ω✝

Proof state:
case h.mpr.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n => f n ω✝) ↔ ∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω✝) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : ∀ x ∈ Set.range fun n => f n ω✝, c ≤ x
ω : ℝ
hω : ω ∈ Set.range fun n => (-f) n ω✝
⊢ ω ≤ -c

Tactic:
simp_rw [Set.mem_range, Pi.neg_apply, neg_eq_iff_eq_neg] at hω

Result:
case h.mpr.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n => f n ω✝) ↔ ∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n => (-f) n ω✝) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : ∀ x ∈ Set.range fun n => f n ω✝, c ≤ x
ω : ℝ
hω : ∃ y, f y ω✝ = -ω
⊢ ω ≤ -c