mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ IsAtom (findAtom r)

Tactic:
constructor

Goal state after:
case left
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ findAtom r ≠ ⊥

case right
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ ∀ b < findAtom r, b = ⊥
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a : X
b : ↥S
⊢ S.restrictAux a ≤ b ↔ a ≤ ↑b

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a : X
b : ↥S
⊢ S.restrictAux a ≤ b → a ≤ ↑b

case mpr
X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a : X
b : ↥S
⊢ a ≤ ↑b → S.restrictAux a ≤ b
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: case inr
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
oh : t₁.root ≤ v₁ ∧ t₁.root ≤ v₂
⊢ t₁ = t₂

Tactic:
ext

Goal state after:
case inr
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
oh : t₁.root ≤ v₁ ∧ t₁.root ≤ v₂
⊢ t₁.root = t₂.root
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
x : X
⊢ x ∈ range ⇑S.toNucleus ↔ x ∈ ↑S

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
x : X
⊢ x ∈ range ⇑S.toNucleus → x ∈ ↑S

case mpr
X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
x : X
⊢ x ∈ ↑S → x ∈ range ⇑S.toNucleus
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
n : Nucleus X
x : X
⊢ n.toSublocale.restrict x = ⟨n x, ⋯⟩

Tactic:
ext

Goal state after:
X : Type u_1
inst✝ : Order.Frame X
n : Nucleus X
x : X
⊢ ↑(n.toSublocale.restrict x) = ↑⟨n x, ⋯⟩
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
⊢ upperClosure (s ×ˢ t) = upperClosure s ×ˢ upperClosure t

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
x✝ : α × β
⊢ x✝ ∈ ↑(upperClosure (s ×ˢ t)) ↔ x✝ ∈ ↑(upperClosure s ×ˢ upperClosure t)
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
⊢ lowerClosure (s ×ˢ t) = lowerClosure s ×ˢ lowerClosure t

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
x✝ : α × β
⊢ x✝ ∈ ↑(lowerClosure (s ×ˢ t)) ↔ x✝ ∈ ↑(lowerClosure s ×ˢ lowerClosure t)
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 : ι
a : Ω
⊢ τ a = ↑i ↔ τ a ≤ ↑i ∧ ∀ (x : Ω), τ x < ↑i → ¬τ a ≤ τ x

Tactic:
constructor

Goal state after:
case mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
a : Ω
⊢ τ a = ↑i → τ a ≤ ↑i ∧ ∀ (x : Ω), τ x < ↑i → ¬τ a ≤ τ x

case mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
a : Ω
⊢ (τ a ≤ ↑i ∧ ∀ (x : Ω), τ x < ↑i → ¬τ a ≤ τ x) → τ a = ↑i
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : InfSet ι
u : ι → Ω → β
n m : ι
⊢ hittingBtwn u ∅ n m = fun x ↦ m

Tactic:
ext

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : InfSet ι
u : ι → Ω → β
n m : ι
x✝ : Ω
⊢ hittingBtwn u ∅ n m x✝ = m
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : InfSet ι
u : ι → Ω → β
n : ι
⊢ hittingAfter u ∅ n = fun x ↦ ⊤

Tactic:
ext

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : InfSet ι
u : ι → Ω → β
n : ι
x✝ : Ω
⊢ hittingAfter u ∅ n x✝ = ⊤
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 ι
j : ι
hj₁ : n ≤ j
hj₂ : u j ω ∈ s
⊢ u (hittingAfter u s n ω).untopA ω ∈ s

Tactic:
exact hittingAfter_mem_set ⟨j, hj₁, hj₂⟩

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
h : lowerCrossingTime a b f N n ω ≠ N
⊢ stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N n ω)) ω ≤ a

Tactic:
obtain ⟨j, hj₁, hj₂⟩ :=
    (hittingBtwn_le_iff_of_lt _ (lt_of_le_of_ne lowerCrossingTime_le h)).1 le_rfl
  exact stoppedValue_hittingBtwn_mem ⟨j, ⟨hj₁.1, le_trans hj₁.2 lowerCrossingTime_le⟩, hj₂⟩

Goal state after:
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 : ι
ω : Ω
inst✝ : WellFoundedLT ι
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:
constructor

Goal state after:
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
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

case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ (∃ j ∈ Set.Icc n i, u j ω ∈ s) → hittingBtwn u s n m ω ≤ i
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 : ι
ω : Ω
inst✝ : WellFoundedLT ι
⊢ hittingAfter u s n ω ≤ ↑i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
constructor

Goal state after:
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
⊢ hittingAfter u s n ω ≤ ↑i → ∃ j ∈ Set.Icc n i, u j ω ∈ s

case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
⊢ (∃ j ∈ Set.Icc n i, u j ω ∈ s) → hittingAfter u s n ω ≤ ↑i
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
⊢ hittingBtwn u s n m ω < i ↔ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
constructor

Goal state after:
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
⊢ hittingBtwn u s n m ω < i → ∃ j ∈ Set.Ico n i, u j ω ∈ s

case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
⊢ (∃ j ∈ Set.Ico n i, u j ω ∈ s) → hittingBtwn u s n m ω < i
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 : ι
ω : Ω
⊢ hittingAfter u s n ω < ↑i ↔ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
constructor

Goal state after:
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
⊢ hittingAfter u s n ω < ↑i → ∃ j ∈ Set.Ico n i, u j ω ∈ s

case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
⊢ (∃ j ∈ Set.Ico n i, u j ω ∈ s) → hittingAfter u s n ω < ↑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₁ : 0 ≤ ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
⊢ (fun x ↦ ∑ x_1 ∈ Finset.range n, upcrossingStrat a b f N x_1 x * (f (x_1 + 1) x - f x_1 x)) =
    ∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)

Tactic:
ext

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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : ℕ → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted 𝒢 fun n ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ω ≤ μ[f i.succ - f i | ↑𝒢 i] ω
hω2 : μ[ξ i • (f (i + 1) - f i) | ↑𝒢 i] ω = (ξ i • μ[f (i + 1) - f i | ↑𝒢 i]) ω
⊢ 0 ω ≤ μ[ξ i • (f (i + 1) - f i) | ↑𝒢 i] ω

Tactic:
simp only [Pi.zero_apply, Nat.succ_eq_add_one, Pi.smul_apply'] at hω1 hω2 ⊢

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : ℕ → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted 𝒢 fun n ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ≤ μ[f (i + 1) - f i | ↑𝒢 i] ω
hω2 : μ[ξ i • (f (i + 1) - f i) | ↑𝒢 i] ω = ξ i ω • μ[f (i + 1) - f i | ↑𝒢 i] ω
⊢ 0 ≤ μ[ξ i • (f (i + 1) - f i) | ↑𝒢 i] ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}
i : ι
h_eq_iUnion : {ω | τ ω ≤ ↑i} = ⋃ k, ⋃ (_ : k ≤ i), {ω | τ ω = ↑k}
⊢ MeasurableSet {ω | τ ω ≤ ↑i}

Tactic:
rw [h_eq_iUnion]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}
i : ι
h_eq_iUnion : {ω | τ ω ≤ ↑i} = ⋃ k, ⋃ (_ : k ≤ i), {ω | τ ω = ↑k}
⊢ MeasurableSet (⋃ k, ⋃ (_ : k ≤ i), {ω | τ ω = ↑k})
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 = ⊥
⊢ {ω | τ ω ≤ ↑t} = {ω | τ ω < ↑t} ∪ {ω | τ ω = ↑t}

Tactic:
ext

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 = ⊥
x✝ : Ω
⊢ x✝ ∈ {ω | τ ω ≤ ↑t} ↔ x✝ ∈ {ω | τ ω < ↑t} ∪ {ω | τ ω = ↑t}
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ (upcrossingsBefore a b f N ω).succ ∈ {n | upperCrossingTime a b f (N₂ + 1) n ω < N₂ + 1}

Tactic:
rw [Set.mem_ofPred_eq, upperCrossingTime_succ_eq, hittingBtwn_lt_iff _ le_rfl]

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ ∃ j ∈ Set.Ico (lowerCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) (N₂ + 1), f j ω ∈ Set.Ici b
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : ConditionallyCompleteLinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : Countable ι
x✝ : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
hi : i < n'
⊢ {ω | hittingBtwn u s n n' ω ≤ i} = ⋃ j ∈ Set.Icc n i, u j ⁻¹' s

Tactic:
ext

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : ConditionallyCompleteLinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : Countable ι
x✝¹ : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
hi : i < n'
x✝ : Ω
⊢ x✝ ∈ {ω | hittingBtwn u s n n' ω ≤ i} ↔ x✝ ∈ ⋃ 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
m : MeasurableSpace Ω
inst✝² : ConditionallyCompleteLinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : Countable ι
x✝ : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
⊢ {ω | hittingAfter u s n ω ≤ ↑i} = ⋃ j ∈ Set.Icc n i, u j ⁻¹' s

Tactic:
ext

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : ConditionallyCompleteLinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : Countable ι
x✝¹ : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
x✝ : Ω
⊢ x✝ ∈ {ω | hittingAfter u s n ω ≤ ↑i} ↔ x✝ ∈ ⋃ 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
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
inst✝ : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ ↑N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
x : Ω
⊢ hittingBtwn u s (τ x).untopA N x ≤ n ↔
    (∃ i, τ x = ↑i ∧ i ≤ n ∧ hittingBtwn u s i N x ≤ n) ∨ ∃ i, τ x = ↑i ∧ n < i ∧ hittingBtwn u s i N x ≤ n

Tactic:
specialize hτbdd x

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
inst✝ : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
x : Ω
hτbdd : τ x ≤ ↑N
⊢ hittingBtwn u s (τ x).untopA N x ≤ n ↔
    (∃ i, τ x = ↑i ∧ i ≤ n ∧ hittingBtwn u s i N x ≤ n) ∨ ∃ i, τ x = ↑i ∧ n < i ∧ hittingBtwn u s i N x ≤ n
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
inst✝ : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
x : Ω
hτbdd : τ x ≤ ↑N
h_top : τ x ≠ ⊤
⊢ hittingBtwn u s (τ x).untopA N x ≤ n ↔
    (∃ i, τ x = ↑i ∧ i ≤ n ∧ hittingBtwn u s i N x ≤ n) ∨ ∃ i, τ x = ↑i ∧ n < i ∧ hittingBtwn u s i N x ≤ n

Tactic:
lift τ x to ι using h_top with t

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
inst✝ : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
x : Ω
t : ι
hτbdd : ↑t ≤ ↑N
⊢ hittingBtwn u s (↑t).untopA N x ≤ n ↔
    (∃ i, ↑t = ↑i ∧ i ≤ n ∧ hittingBtwn u s i N x ≤ n) ∨ ∃ i, ↑t = ↑i ∧ n < i ∧ hittingBtwn u s i N x ≤ n
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
inst✝ : MeasurableSpace β
f : Filtration ι m✝
u : ι → Ω → β
τ : Ω → WithTop ι
hτ✝ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ ↑N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hittingBtwn u s (τ x).untopA N x ≤ n} =
    (⋃ i, ⋃ (_ : i ≤ n), {x | τ x = ↑i} ∩ {x | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ i, ⋃ (_ : i > n), {x | τ x = ↑i} ∩ {x | hittingBtwn u s i N x ≤ n}
x : Ω
m : ι
hm : n < m
hτ : τ x = ↑m
⊢ m ≤ N

Tactic:
specialize hτbdd x

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
inst✝ : MeasurableSpace β
f : Filtration ι m✝
u : ι → Ω → β
τ : Ω → WithTop ι
hτ✝ : IsStoppingTime f τ
N : ι
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hittingBtwn u s (τ x).untopA N x ≤ n} =
    (⋃ i, ⋃ (_ : i ≤ n), {x | τ x = ↑i} ∩ {x | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ i, ⋃ (_ : i > n), {x | τ x = ↑i} ∩ {x | hittingBtwn u s i N x ≤ n}
x : Ω
hτbdd : τ x ≤ ↑N
m : ι
hm : n < m
hτ : τ x = ↑m
⊢ m ≤ N
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
inst✝ : MeasurableSpace β
f : Filtration ι m✝
u : ι → Ω → β
τ : Ω → WithTop ι
hτ✝ : IsStoppingTime f τ
N : ι
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hittingBtwn u s (τ x).untopA N x ≤ n} =
    (⋃ i, ⋃ (_ : i ≤ n), {x | τ x = ↑i} ∩ {x | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ i, ⋃ (_ : i > n), {x | τ x = ↑i} ∩ {x | hittingBtwn u s i N x ≤ n}
x : Ω
hτbdd : τ x ≤ ↑N
m : ι
hm : n < m
hτ : τ x = ↑m
h_top : τ x ≠ ⊤
⊢ m ≤ N

Tactic:
lift τ x to ι using h_top with t

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m✝ : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
inst✝ : MeasurableSpace β
f : Filtration ι m✝
u : ι → Ω → β
τ : Ω → WithTop ι
hτ✝ : IsStoppingTime f τ
N : ι
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hittingBtwn u s (τ x).untopA N x ≤ n} =
    (⋃ i, ⋃ (_ : i ≤ n), {x | τ x = ↑i} ∩ {x | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ i, ⋃ (_ : i > n), {x | τ x = ↑i} ∩ {x | hittingBtwn u s i N x ≤ n}
x : Ω
m : ι
hm : n < m
t : ι
hτ : ↑t = ↑m
hτbdd : ↑t ≤ ↑N
⊢ m ≤ N
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
⊢ s ∩ {ω | π ω ≤ ↑i} = s ∩ {ω | τ ω ≤ ↑i} ∩ {ω | π ω ≤ ↑i}

Tactic:
ext

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
x✝ : Ω
⊢ x✝ ∈ s ∩ {ω | π ω ≤ ↑i} ↔ x✝ ∈ s ∩ {ω | τ ω ≤ ↑i} ∩ {ω | π ω ≤ ↑i}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
⊢ (MeasurableSet s ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω | ↑i ≤ ↑i_1})) ↔ MeasurableSet s

Tactic:
constructor

Goal state after:
case mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
⊢ (MeasurableSet s ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω | ↑i ≤ ↑i_1})) → MeasurableSet s

case mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
⊢ MeasurableSet s → MeasurableSet s ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω | ↑i ≤ ↑i_1})
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : WithTop ι), {ω | τ ω = ↑i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = ↑i} ∩ {_ω | ↑i ≤ j}
⊢ MeasurableSet (s ∩ {ω | τ ω = ↑i}) ↔ MeasurableSet (s ∩ {ω | τ ω = ↑i})

Tactic:
constructor

Goal state after:
case mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : WithTop ι), {ω | τ ω = ↑i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = ↑i} ∩ {_ω | ↑i ≤ j}
⊢ MeasurableSet (s ∩ {ω | τ ω = ↑i}) → MeasurableSet (s ∩ {ω | τ ω = ↑i})

case mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : WithTop ι), {ω | τ ω = ↑i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = ↑i} ∩ {_ω | ↑i ≤ j}
⊢ MeasurableSet (s ∩ {ω | τ ω = ↑i}) → MeasurableSet (s ∩ {ω | τ ω = ↑i})
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ : ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) ω) N, (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ¬∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i | (f i ω - a)⁺ ≤ 0}) = N

Tactic:
refine False.elim (h₂ ?_)
      simp_all only [Set.mem_Iic, not_true_eq_false]

Goal state after: