awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
b : ℝ
hb : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ g n ω)) b
n : ℕ
⊢ (fun (n : ℕ) ↦ f n ω) n ≤ b + |f 0 ω|

Tactic:
sub_le_iff_le_add.1 (le_trans (sub_le_sub_left (le_abs_self _) _) (hb ⟨n, rfl⟩))

Premises used: le_abs_self, sub_le_iff_le_add, Exists.intro, Iff.mp, sub_le_sub_left, rfl, le_trans
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
b : ℝ
hb : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ g n ω)) b
n : ℕ
⊢ (fun (n : ℕ) ↦ f n ω) n ≤ b + |f 0 ω|

Tactic:
exact sub_le_iff_le_add.1 (le_trans (sub_le_sub_left (le_abs_self _) _) (hb ⟨n, rfl⟩))

Premises used: le_abs_self, sub_le_iff_le_add, Exists.intro, Iff.mp, sub_le_sub_left, rfl, le_trans
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
⊢ (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
h : ∀ (h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
h₁ : ∀ (h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
⊢ (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
h₁ : ∀ (c : ℝ) (hc : Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)

Tactic:
obtain ⟨c, hc⟩ := h
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
h₁ : ∀ (c : ℝ) (hc : Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
obtain ⟨c, hc⟩ := h
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)

Tactic:
⟨c - f 0 ω, hc.sub_const _⟩

Premises used: HSub.hSub, Filter.Tendsto.sub_const, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)

Tactic:
exact ⟨c - f 0 ω, hc.sub_const _⟩
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
⟨c + f 0 ω, ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
h : Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (c + f 0 ω))
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
refine ⟨c + f 0 ω, ?_⟩
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
⊢ Tendsto (fun (x : ℕ) ↦ g x ω + f 0 ω) atTop (𝓝 (c + f 0 ω))

Tactic:
have := hc.add_const (f 0 ω)
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
this : Tendsto (fun (x : ℕ) ↦ g x ω + f 0 ω) atTop (𝓝 (c + f 0 ω))
⊢ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (c + f 0 ω))

Tactic:
simpa only [g, sub_add_cancel]

Premises used: sub_add_cancel
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h : ∀ (ω : Ω) (hω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)) (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)

Tactic:
filter_upwards [hbdd] with ω hω i
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
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:
grind
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)

Tactic:
have hbdd' : ∀ᵐ ω ∂μ, ∀ i, |(-f) (i + 1) ω - (-f) i ω| ≤ R := by
    filter_upwards [hbdd] with ω hω i
    simp only [Pi.neg_apply]
    grind
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
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 : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
have hup := hf.submartingale.bddAbove_iff_exists_tendsto hbdd
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
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 ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)

Tactic:
have hdown := hf.neg.submartingale.bddAbove_iff_exists_tendsto hbdd'
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
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 :
  ∀ (ω : Ω)
    (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 ω)
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)

Tactic:
filter_upwards [hup, hdown] with ω hω₁ hω₂
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
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)
mp : (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) → ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
mpr : (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)) → ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
⊢ (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)

Tactic:
constructor
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
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:
⟨-c, hc.neg⟩

Premises used: Filter.Tendsto.neg, Exists.intro, Neg.neg
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
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⟩
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
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:
⟨-c, ?_⟩

Premises used: Exists.intro, Neg.neg
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
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)
mpr : Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (-c))
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
refine ⟨-c, ?_⟩
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
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 (x : ℕ) ↦ -(-f) x ω) atTop (𝓝 (-c))

Tactic:
hc.neg

Premises used: Filter.Tendsto.neg
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
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)
h : ∀ (x : ℕ), f x ω = -(-f) x ω
⊢ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (-c))

Tactic:
convert! hc.neg

Premises used: Filter.Tendsto.neg
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
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]

Premises used: neg_neg, Pi.neg_apply
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
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 : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)

Tactic:
have : (∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)) ↔
      ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c) := by
    constructor <;> rintro ⟨c, hc⟩
    · exact ⟨-c, hc.neg⟩
    · refine ⟨-c, ?_⟩
      convert! hc.neg
      simp only [neg_neg, Pi.neg_apply]
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
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)
h : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)

Tactic:
rw [hω₁, this, ← hω₂]