mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : UpperSet α
t : UpperSet β
⊢ s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : UpperSet α
t : UpperSet β
⊢ s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : UpperSet α
t₁ t₂ : UpperSet β
⊢ Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Codisjoint s₁ s₂ ∨ Codisjoint t₁ t₂

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : UpperSet α
t₁ t₂ : UpperSet β
⊢ Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Codisjoint s₁ s₂ ∨ Codisjoint t₁ t₂
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : LowerSet α
t : LowerSet β
⊢ s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : LowerSet α
t : LowerSet β
⊢ s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : LowerSet α
t₁ t₂ : LowerSet β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : LowerSet α
t₁ t₂ : LowerSet β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
h : IsProgressive f u
i : ι
this : u i = (fun p ↦ u (↑p.1) p.2) ∘ fun x ↦ (⟨i, ⋯⟩, x)
⊢ Measurable (u i)

Tactic:
this

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
h : IsProgressive f u
i : ι
this : u i = (fun p ↦ u (↑p.1) p.2) ∘ fun x ↦ (⟨i, ⋯⟩, x)
⊢ Measurable ((fun p ↦ u (↑p.1) p.2) ∘ fun x ↦ (⟨i, ⋯⟩, x))
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
t : ι → Ω → ι
h : IsProgressive f u
ht : IsProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this : (fun p ↦ u (t (↑p.1) p.2) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨t (↑p.1) p.2, ⋯⟩, p.2)
⊢ Measurable fun p ↦ (fun i ω ↦ u (t i ω) ω) (↑p.1) p.2

Tactic:
this

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
t : ι → Ω → ι
h : IsProgressive f u
ht : IsProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this : (fun p ↦ u (t (↑p.1) p.2) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨t (↑p.1) p.2, ⋯⟩, p.2)
⊢ Measurable ((fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨t (↑p.1) p.2, ⋯⟩, p.2))
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝¹ : TopologicalSpace β
u : ι → Ω → β
inst✝ : MeasurableSpace ι
h : IsStronglyProgressive f u
i : ι
this : u i = (fun p ↦ u (↑p.1) p.2) ∘ fun x ↦ (⟨i, ⋯⟩, x)
⊢ StronglyMeasurable (u i)

Tactic:
this

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝¹ : TopologicalSpace β
u : ι → Ω → β
inst✝ : MeasurableSpace ι
h : IsStronglyProgressive f u
i : ι
this : u i = (fun p ↦ u (↑p.1) p.2) ∘ fun x ↦ (⟨i, ⋯⟩, x)
⊢ StronglyMeasurable ((fun p ↦ u (↑p.1) p.2) ∘ fun x ↦ (⟨i, ⋯⟩, x))
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝⁴ : TopologicalSpace β
u : ι → Ω → β
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
ht : IsStronglyProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this : (fun p ↦ u (t (↑p.1) p.2) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨t (↑p.1) p.2, ⋯⟩, p.2)
⊢ StronglyMeasurable fun p ↦ (fun i ω ↦ u (t i ω) ω) (↑p.1) p.2

Tactic:
this

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝⁴ : TopologicalSpace β
u : ι → Ω → β
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
ht : IsStronglyProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this : (fun p ↦ u (t (↑p.1) p.2) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨t (↑p.1) p.2, ⋯⟩, p.2)
⊢ StronglyMeasurable ((fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨t (↑p.1) p.2, ⋯⟩, p.2))
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
⊢ predictablePart f ℱ μ 0 = 0

Tactic:
[

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
⊢ predictablePart f ℱ μ 0 = 0
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
⊢ ∑ i ∈ ∅, μ[f (i + 1) - f i | ↑ℱ i] = 0

Tactic:
Finset.sum_empty

Goal state after:
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case refine_2.ht
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
e : E
he : e ∈ Set.range (Y m)
n : ℕ
ω : Ω
hnω : Y m (n, ω) = e
⊢ e ∈ ⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k)

Tactic:
[

Goal state after:
case refine_2.ht
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
e : E
he : e ∈ Set.range (Y m)
n : ℕ
ω : Ω
hnω : Y m (n, ω) = e
⊢ e ∈ ⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : IsMin i
this : {ω | τ ω < ↑i} = ∅
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
this

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : IsMin i
this : {ω | τ ω < ↑i} = ∅
⊢ MeasurableSet ∅
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
this : {ω | τ ω < ↑i} = τ ⁻¹' Set.Iic ↑(Order.pred i)
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
this

Goal state after:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
this : {ω | τ ω < ↑i} = τ ⁻¹' Set.Iic ↑(Order.pred i)
⊢ MeasurableSet (τ ⁻¹' Set.Iic ↑(Order.pred i))
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω = ↑i} = {ω | τ ω ≤ ↑i} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < ↑i), {ω | τ ω ≤ j}
⊢ MeasurableSet {ω | τ ω = ↑i}

Tactic:
this

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω = ↑i} = {ω | τ ω ≤ ↑i} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < ↑i), {ω | τ ω ≤ j}
⊢ MeasurableSet ({ω | τ ω ≤ ↑i} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < ↑i), {ω | τ ω ≤ j})
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hittingBtwn u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ hittingBtwn u s n m ω ≤ k

Tactic:
[

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hittingBtwn u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ hittingBtwn u s n m ω ≤ k
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω < ↑i} = {ω | τ ω ≤ ↑i} \ {ω | τ ω = ↑i}
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
this

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω < ↑i} = {ω | τ ω ≤ ↑i} \ {ω | τ ω = ↑i}
⊢ MeasurableSet ({ω | τ ω ≤ ↑i} \ {ω | τ ω = ↑i})
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst✝ : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | ↑i ≤ τ ω} = {ω | τ ω < ↑i}ᶜ
⊢ MeasurableSet {ω | ↑i ≤ τ ω}

Tactic:
this

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst✝ : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | ↑i ≤ τ ω} = {ω | τ ω < ↑i}ᶜ
⊢ MeasurableSet {ω | τ ω < ↑i}ᶜ
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
R : ℝ
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ‖f (i + 1) ω - f i ω‖ ≤ R
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ‖predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω‖ ≤ R

Tactic:
[

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
R : ℝ
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ‖f (i + 1) ω - f i ω‖ ≤ R
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ‖predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω‖ ≤ R
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | ↑i < τ ω} = {ω | τ ω ≤ ↑i}ᶜ
⊢ MeasurableSet {ω | ↑i < τ ω}

Tactic:
this

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | ↑i < τ ω} = {ω | τ ω ≤ ↑i}ᶜ
⊢ MeasurableSet {ω | τ ω ≤ ↑i}ᶜ
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
h : ∃ j, n ≤ j ∧ u j ω ∈ s
⊢ ↑n ≤ ↑(sInf {j | n ≤ j ∧ u j ω ∈ s})

pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
h : ¬∃ j, n ≤ j ∧ u j ω ∈ s
⊢ ↑n ≤ ⊤

Tactic:
· exact_mod_cast le_csInf h fun b hb => hb.1

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
h : ¬∃ j, n ≤ j ∧ u j ω ∈ s
⊢ ↑n ≤ ⊤
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s

Tactic:
[

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
this : {ω | τ ω < ↑i} = ∅
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
this

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
this : {ω | τ ω < ↑i} = ∅
⊢ MeasurableSet ∅
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
hl : hittingBtwn u s n m ω < m
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s

Tactic:
[

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
hl : hittingBtwn u s n m ω < m
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i

Tactic:
[

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
n : ℕ
hn : upperCrossingTime a b f N n ω < N
hn' : ¬n ≤ k
⊢ False

Tactic:
exact hn.ne (upperCrossingTime_stabilize (not_le.1 hn').le hk)

Goal state after:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : ∀ s ∈ 𝓝 i, ∃ a, ∀ (b : ℕ), a ≤ b → seq b ∈ s
h_bound : ∀ (j : ℕ), seq j < i
k : WithTop ι
hk_lt_i : k < ↑i
⊢ ∃ i, k ≤ ↑(seq i)

Tactic:
cases k with

Goal state after:
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun ω ↦ ↑(upperCrossingTime a b f N k ω)) ∧
    IsStoppingTime ℱ fun ω ↦ ↑(lowerCrossingTime a b f N k ω)
n : ℕ
⊢ MeasurableSet {ω | ↑(upperCrossingTime a b f N (k + 1) ω) ≤ ↑n}

Tactic:
[

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun ω ↦ ↑(upperCrossingTime a b f N k ω)) ∧
    IsStoppingTime ℱ fun ω ↦ ↑(lowerCrossingTime a b f N k ω)
n : ℕ
⊢ MeasurableSet {ω | ↑(upperCrossingTime a b f N (k + 1) ω) ≤ ↑n}
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
[

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ False

Tactic:
[

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ False
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
n i : ℕ
x✝ : i ∈ Finset.range N
hl : MeasurableSet {ω | lowerCrossingTime a b f N i ω ≤ n}
hu : MeasurableSet {ω | upperCrossingTime a b f N (i + 1) ω ≤ n}
⊢ MeasurableSet fun ω ↦ ({n | lowerCrossingTime a b f N i ω ≤ n} ∩ {n | n < upperCrossingTime a b f N (i + 1) ω}) n

Tactic:
[

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
n i : ℕ
x✝ : i ∈ Finset.range N
hl : MeasurableSet {ω | lowerCrossingTime a b f N i ω ≤ n}
hu : MeasurableSet {ω | upperCrossingTime a b f N (i + 1) ω ≤ n}
⊢ MeasurableSet fun ω ↦ ({n | lowerCrossingTime a b f N i ω ≤ n} ∩ {n | n < upperCrossingTime a b f N (i + 1) ω}) n
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
by
  obtain ⟨i', hi'_lub⟩ : ∃ i', IsLUB (Set.Iio i) i' := exists_lub_Iio i
  rcases lub_Iio_eq_self_or_Iio_eq_Iic i hi'_lub with hi'_eq_i | h_Iio_eq_Iic
  · rw [← hi'_eq_i] at hi'_lub ⊢
    exact hτ.measurableSet_lt_of_isLUB i' hi'_lub
  · have h_lt_eq_preimage : {ω : Ω | τ ω < i} = τ ⁻¹' Set.Iio i := rfl
    have h_Iio_eq_Iic' : Set.Iio (i : WithTop ι) = Set.Iic (i' : WithTop ι) := by
      rw [← image_coe_Iio, ← image_coe_Iic, h_Iio_eq_Iic]
    rw [h_lt_eq_preimage, h_Iio_eq_Iic']
    exact f.mono (le_of_isLUB_Iio i hi'_lub) _ (hτ.measurableSet_le i')

Goal state after:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | ↑i ≤ τ ω} = {ω | τ ω < ↑i}ᶜ
⊢ MeasurableSet {ω | ↑i ≤ τ ω}

Tactic:
this

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | ↑i ≤ τ ω} = {ω | τ ω < ↑i}ᶜ
⊢ MeasurableSet {ω | τ ω < ↑i}ᶜ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | τ ω = ↑i} = {ω | τ ω ≤ ↑i} ∩ {ω | τ ω ≥ ↑i}
⊢ MeasurableSet {ω | τ ω = ↑i}

Tactic:
this

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | τ ω = ↑i} = {ω | τ ω ≤ ↑i} ∩ {ω | τ ω ≥ ↑i}
⊢ MeasurableSet ({ω | τ ω ≤ ↑i} ∩ {ω | τ ω ≥ ↑i})
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ
h₂ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ -
      ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ ≤ ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ

Tactic:
[

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ
h₂ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ -
      ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ ≤ ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this✝ : (𝓝[>] t).NeBot
h_freq : ∃ᶠ (x : ι) in 𝓝[>] t, t < x
this : ∃ ns, Tendsto ns atTop (𝓝[>] t) ∧ ∀ (n : ℕ), t < ns n
⊢ ∃ s, (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)

Tactic:
[

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this✝ : (𝓝[>] t).NeBot
h_freq : ∃ᶠ (x : ι) in 𝓝[>] t, t < x
this : ∃ ns, Tendsto ns atTop (𝓝[>] t) ∧ ∀ (n : ℕ), t < ns n
⊢ ∃ s, (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)