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 ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
i : ℕ
hi : hωb.some (s := upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) < (↑i : ℝ)
⊢ ∀ (n : ℕ), f n ω < (↑i : ℝ)

Tactic:
have hib : ∀ n, f n ω < i := by
    intro n
    exact lt_of_le_of_lt ((mem_upperBounds.1 hωb.some_mem) _ ⟨n, rfl⟩) hi
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
i : ℕ
hi : hωb.some (s := upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) < (↑i : ℝ)
hib : ∀ (n : ℕ), f n ω < (↑i : ℝ)
n : ℕ
rw : f (min (↑n : WithTop ℕ) ⊤).untopA ω = f n ω
rw₁ : ∀ (j : ℕ), ⊥ ≤ j → f j ω ∉ Set.Ici (↑i : ℝ)
⊢ stoppedAbove f (↑i : ℝ) n ω = f n ω

Tactic:
rw [stoppedAbove, stoppedProcess, leastGE, hittingAfter_eq_top_iff.mpr]

Premises used: Iff.mpr, MeasureTheory.stoppedAbove, MeasureTheory.stoppedProcess, MeasureTheory.hittingAfter_eq_top_iff, MeasureTheory.leastGE
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
i : ℕ
hi : hωb.some (s := upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) < (↑i : ℝ)
hib : ∀ (n : ℕ), f n ω < (↑i : ℝ)
n : ℕ
simp : f (↑n : WithTop ℕ).untopA ω = f n ω
⊢ f (min (↑n : WithTop ℕ) ⊤).untopA ω = f n ω

Tactic:
simp only [le_top, inf_of_le_left]

Premises used: inf_of_le_left, le_top
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
i : ℕ
hi : hωb.some (s := upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) < (↑i : ℝ)
hib : ∀ (n : ℕ), f n ω < (↑i : ℝ)
n : ℕ
⊢ f (↑n : WithTop ℕ).untopA ω = f n ω

Tactic:
congr
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
i : ℕ
hi : hωb.some (s := upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) < (↑i : ℝ)
hib : ∀ (n : ℕ), f n ω < (↑i : ℝ)
n : ℕ
⊢ ∀ (j : ℕ), ⊥ ≤ j → f j ω ∉ Set.Ici (↑i : ℝ)

Tactic:
simp [hib]
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
i : ℕ
hi : hωb.some (s := upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) < (↑i : ℝ)
hib : ∀ (n : ℕ), f n ω < (↑i : ℝ)
⊢ ∀ (n : ℕ), stoppedAbove f (↑i : ℝ) n ω = f n ω

Tactic:
have heq : ∀ n, stoppedAbove f i n ω = f n ω := by
    intro n
    rw [stoppedAbove, stoppedProcess, leastGE, hittingAfter_eq_top_iff.mpr]
    · simp only [le_top, inf_of_le_left]
      congr
    · simp [hib]
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
i : ℕ
hi : hωb.some (s := upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) < (↑i : ℝ)
hib : ∀ (n : ℕ), f n ω < (↑i : ℝ)
heq : ∀ (n : ℕ), stoppedAbove f (↑i : ℝ) n ω = f n ω
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
simp only [← heq, hω i]
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ω : Ω
hω : 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:
⟨hω, fun ⟨c, hc⟩ => hc.bddAbove_range⟩

Premises used: Filter.Tendsto.bddAbove_range, BddAbove, Iff.intro, Set.range, _private.0.MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto_aux.match_1
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (ω : Ω) ↦
                  BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) →
                    ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
                x}
            x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (ω : Ω) ↦
                  BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔
                    ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
                x}
            x}
      a
h₁ h₂ :
  ∀ (ω : Ω)
    (hω : 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)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
filter_upwards [hf.exists_tendsto_of_abs_bddAbove_aux hf0 hbdd] with ω hω using
    ⟨hω, fun ⟨c, hc⟩ => hc.bddAbove_range⟩

Premises used: MeasureTheory.Submartingale.exists_tendsto_of_abs_bddAbove_aux
-- 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 ω
⊢ Submartingale g ℱ μ

Tactic:
have hg : Submartingale g ℱ μ :=
    hf.sub_martingale (martingale_const_fun _ _ (hf.stronglyAdapted 0) (hf.integrable 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 ℱ μ
h : ∀ (ω : Ω), g 0 ω = 0 ω
⊢ g 0 = 0

Tactic:
ext ω
-- 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 ℱ μ
ω : Ω
⊢ g 0 ω = 0 ω

Tactic:
simp only [g, sub_self, Pi.zero_apply]

Premises used: sub_self, Pi.zero_apply
-- 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 ℱ μ
⊢ g 0 = 0

Tactic:
have hg0 : g 0 = 0 := by
    ext ω
    simp only [g, sub_self, Pi.zero_apply]
-- 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
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)

Tactic:
simpa only [g, sub_sub_sub_cancel_right]

Premises used: sub_sub_sub_cancel_right
-- 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
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)

Tactic:
have hgbdd : ∀ᵐ ω ∂μ, ∀ i : ℕ, |g (i + 1) ω - g i ω| ≤ ↑R := by
    simpa only [g, sub_sub_sub_cancel_right]
-- 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 :
  ∀ (ω : Ω)
    (hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)),
    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:
filter_upwards [hg.bddAbove_iff_exists_tendsto_aux hg0 hgbdd] with ω hω

Premises used: MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto_aux
-- 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)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)

Tactic:
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 : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)
h₁ : (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
convert! hω using 1
-- 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)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)

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 : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)), BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)
h₁ : ∀ (h : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)), BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)

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 : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
h₁ :
  ∀ (b : ℝ) (hb : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) b),
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)

Tactic:
obtain ⟨b, hb⟩ := 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 : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)
h₁ :
  ∀ (b : ℝ) (hb : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ g n ω)) b),
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)

Tactic:
obtain ⟨b, hb⟩ := 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)
b : ℝ
hb : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) b
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)

Tactic:
⟨b + |f 0 ω|, fun y hy => ?_⟩

Premises used: abs, BddAbove, Set.Nonempty, 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)
b : ℝ
hb : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) b
h : ∀ (y : ℝ) (hy : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ g n ω) y), y ≤ b + |f 0 ω|
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)

Tactic:
refine ⟨b + |f 0 ω|, fun y hy => ?_⟩
-- 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
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)

Tactic:
⟨b + |f 0 ω|, fun y hy => ?_⟩

Premises used: abs, BddAbove, Set.Nonempty, 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)
b : ℝ
hb : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ g n ω)) b
h : ∀ (y : ℝ) (hy : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ f n ω) y), y ≤ b + |f 0 ω|
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)

Tactic:
refine ⟨b + |f 0 ω|, fun y hy => ?_⟩
-- 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 : ℕ) ↦ f n ω)) b
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ g n ω) y
h : ∀ (n : ℕ), (fun (n : ℕ) ↦ g n ω) n ≤ b + |f 0 ω|
⊢ y ≤ b + |f 0 ω|

Tactic:
obtain ⟨n, rfl⟩ := hy

Premises used: rfl
-- 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
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ f n ω) y
h : ∀ (n : ℕ), (fun (n : ℕ) ↦ f n ω) n ≤ b + |f 0 ω|
⊢ y ≤ b + |f 0 ω|

Tactic:
obtain ⟨n, rfl⟩ := hy

Premises used: rfl
-- 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 : ℕ) ↦ f n ω)) b
n : ℕ
h : f n ω + -f 0 ω ≤ b + |f 0 ω|
⊢ (fun (n : ℕ) ↦ g n ω) n ≤ b + |f 0 ω|

Tactic:
simp_rw [g, sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- 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 : ℕ) ↦ f n ω)) b
n : ℕ
⊢ f n ω + -f 0 ω ≤ b + |f 0 ω|

Tactic:
add_le_add (hb ⟨n, rfl⟩) (neg_le_abs _)

Premises used: add_le_add, neg_le_abs, Exists.intro, rfl
-- 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 : ℕ) ↦ f n ω)) b
n : ℕ
⊢ f n ω + -f 0 ω ≤ b + |f 0 ω|

Tactic:
exact add_le_add (hb ⟨n, rfl⟩) (neg_le_abs _)

Premises used: add_le_add, neg_le_abs, Exists.intro, rfl