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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s : Set α
x : α
hxs : x ∈ s
⊢ IsLUB {x} x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
⊢ countableSupClosure Set.univ = Set.univ

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
⊢ countableSupClosure ∅ = ∅

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
x : α
⊢ countableSupClosure {x} = {x}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
⊢ ⋂₀ ∅ ⊆ Set.univ

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : SetRel α β
l : Filter α
⊢ Set.univ ∈ {s | r.core s ∈ l}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
⊢ ∅ ⊆ s ∧ IsChain r ∅

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
⊢ 1 ≤ ↑(n + 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝¹ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
i j : ℕ
b : α j
h : i ≤ j
x✝ :
  ¬⟨i, π h b⟩ = ⟨j, b⟩ ∧
    ∀ (a : ℕ) (b_1 : α a), ⟨i, π h b⟩ ≤ ⟨a, b_1⟩ → ⟨a, b_1⟩ ≤ ⟨j, b⟩ → ¬⟨a, b_1⟩ = ⟨i, π h b⟩ → ⟨a, b_1⟩ = ⟨j, b⟩
hne : ¬⟨i, π h b⟩ = ⟨j, b⟩
h' : ∀ (a : ℕ) (b_1 : α a), ⟨i, π h b⟩ ≤ ⟨a, b_1⟩ → ⟨a, b_1⟩ ≤ ⟨j, b⟩ → ¬⟨a, b_1⟩ = ⟨i, π h b⟩ → ⟨a, b_1⟩ = ⟨j, b⟩
hle' : i + 1 ≤ j
⊢ ⟨i, π h b⟩.fst ≤ ⟨i + 1, π hle' b⟩.fst

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝¹ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
i j : ℕ
b : α j
h : i ≤ j
x✝ :
  ¬⟨i, π h b⟩ = ⟨j, b⟩ ∧
    ∀ (a : ℕ) (b_1 : α a), ⟨i, π h b⟩ ≤ ⟨a, b_1⟩ → ⟨a, b_1⟩ ≤ ⟨j, b⟩ → ¬⟨a, b_1⟩ = ⟨i, π h b⟩ → ⟨a, b_1⟩ = ⟨j, b⟩
hne : ¬⟨i, π h b⟩ = ⟨j, b⟩
h' : ∀ (a : ℕ) (b_1 : α a), ⟨i, π h b⟩ ≤ ⟨a, b_1⟩ → ⟨a, b_1⟩ ≤ ⟨j, b⟩ → ¬⟨a, b_1⟩ = ⟨i, π h b⟩ → ⟨a, b_1⟩ = ⟨j, b⟩
hle' : i + 1 ≤ j
⊢ π hle' ⟨j, b⟩.snd = ⟨i + 1, π hle' b⟩.snd

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.PFilter

Goal state before:
pp: P : Type u_1
inst✝ : Preorder P
p q : P
⊢ principal q ≤ principal p ↔ p ≤ q

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : SemilatticeInf X
n m : Nucleus X
x y : X
⊢ ∀ (a b : X), a ⊓ b = a ⊓ b

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : SemilatticeInf X
n m : Nucleus X
x y : X
⊢ ∀ (x : X), x ≤ x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝¹ : SemilatticeInf X
n m : Nucleus X
x y : X
inst✝ : OrderTop X
⊢ ∀ (a b : X), ⊤ (a ⊓ b) = ⊤ a ⊓ ⊤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝¹ : SemilatticeInf X
n m : Nucleus X
x y : X
inst✝ : OrderTop X
⊢ ∀ (x : X), ⊤ (⊤ x) ≤ ⊤ x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝¹ : SemilatticeInf X
n m : Nucleus X
x y : X
inst✝ : OrderTop X
⊢ ∀ (x : X), x ≤ ⊤ x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝¹ : SemilatticeInf X
n m : Nucleus X
x y : X
inst✝ : OrderTop X
x✝¹ : Nucleus X
x✝ : X
⊢ x✝¹ x✝ ≤ ⊤ x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
i : ℕ
a : α i
j : ℕ
b : α j
hne : ⟨i, a⟩ ≠ ⟨j, b⟩
hij : i ≤ j
h2 : π hij b = a
hle : i + 1 ≤ j
⊢ ⟨i, a⟩.fst ≤ ⟨i + 1, π hle b⟩.fst

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
⊢ ∀ (b : X), (∀ x_1 ≥ x, b ⊓ m x_1 ≤ n x_1) → (∀ i ≥ y, b ⊓ m i ≤ n i) → b ≤ m k → b ≤ n k

Tactic:
l

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
⊢ (∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1) → (∀ i ≥ y, l ⊓ m i ≤ n i) → l ≤ m k → l ≤ n k
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
i : ℕ
a : α i
j : ℕ
b : α j
hne : ⟨i, a⟩ ≠ ⟨j, b⟩
hij : i ≤ j
h2 : π hij b = a
hle : i + 1 ≤ j
⊢ ⟨i, a⟩.fst + 1 = ⟨i + 1, π hle b⟩.fst

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
i : ℕ
a : α i
j : ℕ
b : α j
hne : ⟨i, a⟩ ≠ ⟨j, b⟩
hij : i ≤ j
h2 : π hij b = a
hle : i + 1 ≤ j
⊢ π hle ⟨j, b⟩.snd = ⟨i + 1, π hle b⟩.snd

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
⊢ R.rightDual I ⊆ R.rightDual (R.leftDual (R.rightDual I))

Tactic:
· exact R.gc_leftDual_rightDual.le_u_l (R.rightDual I)

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
s t x y z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q : Partition s
P : Set α
indep : _root_.sSupIndep P
hsSup : sSup P = s
⊢ ⊥ ∉ P \ {⊥}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
s : α
inst✝ : CompleteLattice α
⊢ ↑⊤ ⊆ {s}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
x✝¹ : α × α
p q : α
x✝ : (p, q) ∈ ↑P ×ˢ ↑Q
hp : (p, q).1 ∈ ↑P
hq : (p, q).2 ∈ ↑Q
⊢ (p, q).1 ⊓ (p, q).2 ≤ p ⊓ q

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
t u : Set α
P : Partition u
h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P.Rel x y → x = y
⊢ ∀ (x : ↑t), ↑x ∉ u → ↑x = ↑x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
t u : Set α
P : Partition u
h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P.Rel x y → x = y
⊢ ∀ (x : ↑t), ↑x ∈ u → P.Rel ↑x ↑x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
⊢ ∀ ⦃x y : α⦄, x ∈ ∅ → y ∈ ∅ → P.Rel x y → x = y

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
⊢ t₁.root ≤ v₁ ⊓ v₂

Tactic:
simp only [le_inf_iff]

Goal state after:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
⊢ t₁.root ≤ v₁ ∧ t₁.root ≤ v₂
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: 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₂
⊢ v₁ ⊓ v₂ ≤ v₁

Tactic:
by simp

Goal state after:
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 b : X
s : ↥S
⊢ Sublocale.restrictAux✝ S a ⊓ Sublocale.restrictAux✝ S b ≤ s ↔
    Sublocale.restrictAux✝ S a ≤ Sublocale.restrictAux✝ S b ⇨ s

Tactic:
by simp

Goal state after:
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 b : X
s : ↥S
c : ↥S := ⟨a ⇨ ↑s, ⋯⟩
⊢ ↑(Sublocale.restrictAux✝ S b) ≤ ↑c ↔ b ≤ ↑c

Tactic:
S.giAux.u_le_u_iff,

Goal state after:
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 b : X
s : ↥S
c : ↥S := ⟨a ⇨ ↑s, ⋯⟩
⊢ Sublocale.restrictAux✝ S b ≤ c ↔ b ≤ ↑c
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
⊢ ∀ {a b : (Nucleus X)ᵒᵈ},
    { toFun := fun n ↦ (OrderDual.ofDual n).toSublocale, invFun := fun s ↦ OrderDual.toDual s.toNucleus, left_inv := ⋯,
            right_inv := ⋯ }
          a ≤
        { toFun := fun n ↦ (OrderDual.ofDual n).toSublocale, invFun := fun s ↦ OrderDual.toDual s.toNucleus,
            left_inv := ⋯, right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
by simp

Goal state after:
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 β
⊢ ↑s₂ ⊆ ↑s₁ ∧ ↑t₂ ⊆ ↑t₁ ∨ ↑s₂ = ∅ ∨ ↑t₂ = ∅ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₂ = ⊤ ∨ t₂ = ⊤

Tactic:
by simp

Goal state after:
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 β
⊢ ↑s₁ ⊆ ↑s₂ ∧ ↑t₁ ⊆ ↑t₂ ∨ ↑s₁ = ∅ ∨ ↑t₁ = ∅ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₁ = ⊥ ∨ t₁ = ⊥

Tactic:
by simp

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : i ≤ j
⊢ (Set.Ioi i \ Set.Ioi j) ×ˢ s = Set.Ioi i ×ˢ (s \ s) ∪ (Set.Ioi i \ Set.Ioi j) ×ˢ s

Tactic:
by simp

Goal state after:
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
inst✝ : CompleteSpace E
hf : Martingale f ℱ μ
n i : ℕ
hi : i ∈ Finset.range n
⊢ f i - f i =ᵐ[μ] 0

Tactic:
by simp

Goal state after:
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
inst✝² : CompleteSpace E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
⊢ ∀ᵐ (ω : Ω) ∂μ, Monotone fun x ↦ predictablePart f ℱ μ x ω

Tactic:
by
  have := ae_all_iff.2 <| fun n : ℕ ↦ hf.condExp_sub_nonneg n.le_succ
  filter_upwards [this] with ω h
  simp only [Pi.zero_apply, Nat.succ_eq_add_one, ← ge_iff_le] at h
  refine monotone_nat_of_le_succ fun n ↦ (?_ : _ ≥ _)
  grw [predictablePart_add_one, Pi.add_apply, h n, add_zero]

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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : Preorder ι
m0 : MeasurableSpace Ω
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
ℱ : Filtration ι m0
μ : Measure Ω
i j : ι
x✝ : i ≤ j
⊢ μ[0 j | ↑ℱ i] =ᵐ[μ] 0 i

Tactic:
by simp

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

Goal state before:
pp: Ω : 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 : ℕ
s : E
n : ℕ
hmk : m < n + 1
⊢ 0 ≤ n

Tactic:
by simp

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLattice ι
u : ι → Ω → β
n : ι
⊢ hittingAfter u Set.univ n = fun x ↦ ↑n

Tactic:
by
  ext ω
  classical
  simp only [hittingAfter_def, Set.mem_univ, and_true]
  rw [if_pos ⟨n, le_rfl⟩]
  exact_mod_cast csInf_Ici

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

Goal state before:
pp: case succ
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝¹ : Preorder E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Submartingale f 𝒢 μ
hfadp : StronglyAdapted 𝒢 fun n ↦ f (n + 1)
k : ℕ
ih : f 0 ≤ᵐ[μ] f k
⊢ f 0 ≤ᵐ[μ] f (k + 1)

Tactic:
| succ k ih =>

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

Goal state before:
pp: case succ
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝¹ : Preorder E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Supermartingale f 𝒢 μ
hfadp : StronglyAdapted 𝒢 fun n ↦ f (n + 1)
k : ℕ
ih : f k ≤ᵐ[μ] f 0
⊢ f (k + 1) ≤ᵐ[μ] f 0

Tactic:
| succ k ih =>

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ lowerCrossingTime a b f N n ω ≤ N

Tactic:
by
  simp only [lowerCrossingTime, hittingBtwn_le ω]

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 : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i

Tactic:
have h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s := ⟨i, ⟨hin, him⟩, his⟩

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 n : ℕ
ω : Ω
h : lowerCrossingTime a b f N n ω ≠ N
⊢ stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N n ω)) ω ≤ a

Tactic:
by
  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.Martingale.Upcrossing

Goal state before:
pp: case succ
Ω : 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 ω)
⊢ (IsStoppingTime ℱ fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ∧
    IsStoppingTime ℱ fun ω ↦ ↑(lowerCrossingTime a b f N (k + 1) ω)

Tactic:
| succ k ih =>

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

Goal state before:
pp: case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
h' : hittingAfter u s n ω ≤ ↑i
h_top : hittingAfter u s n ω ≠ ⊤
h_le : ↑n ≤ hittingAfter u s n ω
⊢ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
refine ⟨(hittingAfter u s n ω).untopA, ?_, hittingAfter_mem_set_of_ne_top h_top⟩

Goal state after:
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
h' : hittingAfter u s n ω ≤ ↑i
h_top : hittingAfter u s n ω ≠ ⊤
h_le : ↑n ≤ hittingAfter u s n ω
⊢ (hittingAfter u s n ω).untopA ∈ Set.Icc n i
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: case succ
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Martingale f 𝒢 μ
hfadp : StronglyAdapted 𝒢 fun n ↦ f (n + 1)
k : ℕ
ih : f k =ᵐ[μ] f 0
⊢ f (k + 1) =ᵐ[μ] f 0

Tactic:
| succ k ih =>

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

Goal state before:
pp: case pos
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : N = 0
⊢ upcrossingsBefore a b f N ω ≤ N

pp: case neg
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
⊢ upcrossingsBefore a b f N ω ≤ N

Tactic:
· subst hN
    rw [upcrossingsBefore_zero]

Goal state after:
case neg
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
⊢ upcrossingsBefore a b f N ω ≤ N
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  lowerCrossingTime a b f N k ω < N →
    upperCrossingTime a b f N k ω < N →
      upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
        lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : upperCrossingTime a b f N (k + 1) ω < N
⊢ upperCrossingTime a b f M (k + 1) ω = upperCrossingTime a b f N (k + 1) ω ∧
    lowerCrossingTime a b f M (k + 1) ω = lowerCrossingTime a b f N (k + 1) ω

Tactic:
| succ k ih =>

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

Goal state before:
pp: case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b, a_1 ≤ b ∧ f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1, a ≤ b_1 ∧ b < f b_1 ω
k : ℕ
ih : ∃ N, k ≤ upcrossingsBefore a b f N ω
⊢ ∃ N, k + 1 ≤ upcrossingsBefore a b f N ω

Tactic:
| succ k ih =>

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

Goal state before:
pp: case neg
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n ↦ ↑‖f n ω‖₊) atTop < ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ∞
h : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ |f n ω|
a b : ℚ
hab : a < b
h₁ : ∃ᶠ (i : ℕ) in atTop, f i ω < ↑a
h₂ : ∃ᶠ (i : ℕ) in atTop, ↑b < f i ω
⊢ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)

Tactic:
exact
      False.elim ((hf₂ a b hab).ne (upcrossings_eq_top_of_frequently_lt (Rat.cast_lt.2 hab) h₁ h₂))

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

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
h₂ :
  ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
    ∑ k ∈ Finset.range N,
      (stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω)
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤
    ∑ x ∈ Finset.range N,
      (stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (x + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N x ω)) ω)

Tactic:
refine le_trans ?_ h₂

Goal state after:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
h₂ :
  ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
    ∑ k ∈ Finset.range N,
      (stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω)
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤ ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
⊢ MeasurableSet ∅ ∧ ∀ (i : ι), MeasurableSet (∅ ∩ {ω | τ ω ≤ ↑i})

Tactic:
by simp

Goal state after:
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 : ι
⊢ MeasurableSet (s ∩ {ω | τ ω = ↑i}) ↔ MeasurableSet (s ∩ {ω | τ ω = ↑i})

Tactic:
have : ∀ j, {ω : Ω | τ ω = i} ∩ {ω : Ω | τ ω ≤ j} = {ω : Ω | τ ω = i} ∩ {_ω | i ≤ j} := by
    intro j
    ext1 ω
    simp only [Set.mem_inter_iff, Set.mem_ofPred_eq, and_congr_right_iff]
    intro hxi
    rw [hxi]

Goal state after:
Ω : 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.OptionalStopping

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst✝ : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ ↑n
ω : Ω
⊢ ↑n ≠ ⊤

Tactic:
by simp

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 : ι
⊢ MeasurableSet {ω | τ ω = ↑i}

Tactic:
exact hτ.measurableSet_eq i

Goal state after: