-- 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 h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ω : Ω
hω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R

Tactic:
erw [← abs_neg, neg_sub, sub_neg_eq_add, neg_add_eq_sub]

Result:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ω : Ω
hω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ |f (i + 1) ω - f i ω| ≤ ↑R

Proof state:
case 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)
c : ℝ
hc : Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)

Tactic:
refine ⟨-c, ?_⟩

Result:
case 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)
c : ℝ
hc : Tendsto (fun n => (-f) n ω) atTop (𝓝 c)
⊢ Tendsto (fun n => f n ω) atTop (𝓝 (-c))

Proof state:
case h.e'_3.h
Ω : 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)
x✝ : ℕ
⊢ f x✝ ω = -(-f) x✝ ω

Tactic:
simp only [neg_neg, Pi.neg_apply]

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

Tactic:
filter_upwards [hup, hdown] with ω hω₁ hω₂

Result:
case h
Ω : 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)
⊢ BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)

Proof state:
case h
Ω : 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)
⊢ BddAbove (Set.range fun n => (-f) n ω) ↔ BddBelow (Set.range fun n => f n ω)

Tactic:
constructor <;> rintro ⟨c, hc⟩ <;> refine ⟨-c, fun ω hω => ?_⟩

Result:
case h.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)
this : (∃ c, Tendsto (fun n => f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : c ∈ upperBounds (Set.range fun n => (-f) n ω✝)
ω : ℝ
hω : ω ∈ Set.range fun n => f n ω✝
⊢ -c ≤ ω

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