mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∃ x, (⟨i, a⟩ ≤ x ∧ ⟨i, a⟩.fst + 1 = x.fst) ∧ x ≤ ⟨j, b⟩

Tactic:
have hle : i + 1 ≤ j := hij.lt_of_ne (by rintro rfl; simp [← h2, π_refl] at hne)

Goal state after:
α : ℕ → 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
⊢ ∃ x, (⟨i, a⟩ ≤ x ∧ ⟨i, a⟩.fst + 1 = x.fst) ∧ x ≤ ⟨j, b⟩
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:
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 + 1 = ⟨i + 1, π hle b⟩.fst

Tactic:
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:
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
P : Set α
indep : _root_.sSupIndep P
hsSup : sSup P = s
⊢ ⊥ ∉ P \ {⊥}

Tactic:
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
P : Partition ⊥
x✝ : α
⊢ x✝ ∈ P ↔ x✝ ∈ removeBot ∅ ⋯ ⋯

Tactic:
simp

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

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

Tactic:
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:
simp

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

Goal state before:
pp: case refine_1
α✝ : 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 R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
q : α
hq : q ∈ Q ∧ a ≤ q
r : α
hr : r ∈ R ∧ a ≤ r
⊢ q ⊓ r ∈ {a | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q}

Tactic:
grind [le_inf_iff, P.ne_bot_of_mem ha]

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

Goal state before:
pp: case refine_2
α✝ : 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 R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
q : α
hq : q ∈ Q ∧ a ≤ q
r : α
hr : r ∈ R ∧ a ≤ r
⊢ q ⊓ r ∉ {⊥}

Tactic:
grind [le_inf_iff, P.ne_bot_of_mem ha]

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

Goal state before:
pp: case refine_3
α✝ : 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 R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
q : α
hq : q ∈ Q ∧ a ≤ q
r : α
hr : r ∈ R ∧ a ≤ r
⊢ a ≤ q ⊓ r

Tactic:
grind [le_inf_iff, P.ne_bot_of_mem ha]

Goal state after:
Module: Mathlib.Order.ScottContinuity.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder α'
inst✝ : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
⊢ ScottContinuous (Prod.map f g)

Tactic:
by
  refine .fromProd (fun a d hd₁ hd₂ c hdc ↦ ?_) (fun b d hd₁ hd₂ c hdc ↦ ?_)
  · have e1 : (fun b ↦ (f a, g b)) '' d = {f a} ×ˢ (g '' d) := by aesop
    simp_rw [Prod.map_apply, e1]
    exact .prod (singleton_nonempty _) (hd₁.image _) isLUB_singleton (hg hd₁ hd₂ hdc)
  · have e2 : ((fun a ↦ (f a, g b)) '' d) = (f '' d) ×ˢ {g b} := by aesop
    simp_rw [Prod.map_apply, e2]
    exact .prod (hd₁.image _) (singleton_nonempty _) (hf hd₁ hd₂ hdc) isLUB_singleton

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:
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:
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:
simp

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
⊢ Order.pred ⊥ = ⊥

Tactic:
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
x : Set ↥S
⊢ ∀ x_1 ∈ x, x_1 ∈ Subtype.val ⁻¹' S.carrier

Tactic:
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₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
⊢ v₁ ⊓ v₂ ≤ v₁

Tactic:
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:
simp

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ 0 + type α = type α

Tactic:
simp only [show 0 = type PEmpty by rfl, ← type_lex_sum]
      exact (OrderIso.emptySumLex (β := PEmpty) (α := α)).type_congr

Goal state after:
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:
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:
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:
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 g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n i : ℕ
hi : i ∈ Finset.range n
⊢ μ[(f + g) (i + 1) - (f + g) i | ↑ℱ i] =ᵐ[μ] μ[f (i + 1) - f i + (g (i + 1) - g i) | ↑ℱ i]

Tactic:
simp

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n i : ℕ
hi : i ∈ Finset.range n
⊢ μ[f (i + 1) + g (i + 1) - (f i + g i) | ↑ℱ i] =ᵐ[μ] μ[f (i + 1) - f i + (g (i + 1) - g i) | ↑ℱ i]
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:
simp

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

Goal state before:
pp: case inl
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet ∅

Tactic:
simp

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

Goal state before:
pp: case inr.inl
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
⊢ MeasurableSet ∅

Tactic:
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:
simp

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:
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:
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)
n : ℕ
ω : Ω
m : ℕ
hm : n ≤ m
⊢ { toFun := Y m, measurableSet_fiber' := ⋯, finite_range' := ⋯ } (n, ω) = X m (n, ω)

Tactic:
simp

Goal state after:
Ω : 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)
n : ℕ
ω : Ω
m : ℕ
hm : n ≤ m
⊢ Y m (n, ω) = X 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 ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
by_cases hi_min : IsMin i

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

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
⊢ MeasurableSet {ω | τ ω < ↑i}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos.top
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ∀ (b : ι), ¬b < i
ω : Ω
⊢ ¬⊤ < ↑i

Tactic:
simp

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

Goal state before:
pp: case top
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
ω : Ω
⊢ ⊤ < ↑i ↔ ⊤ ≤ ↑(Order.pred i)

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ

Tactic:
induction hij with

Goal state after:
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 : ι
ω : Ω
h : ¬∃ j, n ≤ j ∧ u j ω ∈ s
⊢ ↑n ≤ ⊤

Tactic:
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 : ι
h_lub : IsLUB (Set.Iio i) i
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
by_cases hi_min : IsMin i

Goal state after:
case pos
Ω : 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
⊢ MeasurableSet {ω | τ ω < ↑i}

case neg
Ω : 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
⊢ MeasurableSet {ω | τ ω < ↑i}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos.top
Ω : 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
ω : Ω
⊢ ¬⊤ < ↑i

Tactic:
simp

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

Goal state before:
pp: case refine_2
Ω : 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 : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
k : WithTop ι
j : ℕ
hk_seq_j : k ≤ ↑(seq j)
⊢ k < ↑i

Tactic:
exact hk_seq_j.trans_lt (mod_cast h_bound j)

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:
by
  constructor <;> intro h'
  · exact ⟨hittingBtwn u s n m ω, ⟨le_hittingBtwn_of_exists h_exists, h'⟩,
      hittingBtwn_mem_set h_exists⟩
  · have h'' : ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s := by
      obtain ⟨k₁, hk₁_mem, hk₁_s⟩ := h_exists
      obtain ⟨k₂, hk₂_mem, hk₂_s⟩ := h'
      refine ⟨min k₁ k₂, ⟨le_min hk₁_mem.1 hk₂_mem.1, min_le_min hk₁_mem.2 hk₂_mem.2⟩, ?_⟩
      exact min_rec' (fun j => u j ω ∈ s) hk₁_s hk₂_s
    obtain ⟨k, hk₁, hk₂⟩ := h''
    refine le_trans ?_ (hk₁.2.trans (min_le_right _ _))
    exact hittingBtwn_le_of_mem hk₁.1 (hk₁.2.trans (min_le_left _ _)) hk₂

Goal state after:
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 ∂μ
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✝

Tactic:
simp

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

Goal state before:
pp: case top
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}
i : ι
ω : Ω
⊢ ⊤ ≤ ↑i ↔ ∃ i_1 ≤ i, ⊤ = ↑i_1

Tactic:
simp

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

Goal state before:
pp: case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}
i : ι
ω : Ω
a : ι
⊢ a ≤ i ↔ ∃ i_1 ≤ i, a = i_1

Tactic:
simp

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

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ¬∃ j ∈ Set.Icc n m, u j ω ∈ F
hE : ¬∃ j ∈ Set.Icc n m, u j ω ∈ E
⊢ m ≤ m

Tactic:
simp

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

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ∃ j, n ≤ j ∧ u j ω ∈ F
hE : ¬∃ j, n ≤ j ∧ u j ω ∈ E
⊢ ↑(sInf {j | n ≤ j ∧ u j ω ∈ F}) ≤ ⊤

Tactic:
simp

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

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ¬∃ j, n ≤ j ∧ u j ω ∈ F
hE : ¬∃ j, n ≤ j ∧ u j ω ∈ E
⊢ ⊤ ≤ ⊤

Tactic:
simp

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

Goal state before:
pp: case hb
Ω : 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 ≤ 0

Tactic:
simp

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

Goal state before:
pp: case zero
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N 0 ω < N
⊢ upperCrossingTime a b f M 0 ω = upperCrossingTime a b f N 0 ω

Tactic:
simp

Goal state after:
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 β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ¬∃ j ∈ Set.Icc n' m, u j ω ∈ s
⊢ m ≤ m

Tactic:
simp

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 m : ι
hnm : n ≤ m
ω : Ω
⊢ (if ∃ j, n ≤ j ∧ u j ω ∈ s then ↑(sInf {i | n ≤ i ∧ u i ω ∈ s}) else ⊤) ≤
    if ∃ j, m ≤ j ∧ u j ω ∈ s then ↑(sInf {i | m ≤ i ∧ u i ω ∈ s}) else ⊤

Tactic:
split_ifs with h_n h_m h_m

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

case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h_n : ∃ j, n ≤ j ∧ u j ω ∈ s
h_m : ¬∃ j, m ≤ j ∧ u j ω ∈ s
⊢ ↑(sInf {j | n ≤ j ∧ u j ω ∈ s}) ≤ ⊤

case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h_n : ¬∃ j, n ≤ j ∧ u j ω ∈ s
h_m : ∃ j, m ≤ j ∧ u j ω ∈ s
⊢ ⊤ ≤ ↑(sInf {j | m ≤ j ∧ u j ω ∈ s})

case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h_n : ¬∃ j, n ≤ j ∧ u j ω ∈ s
h_m : ¬∃ j, m ≤ j ∧ u j ω ∈ s
⊢ ⊤ ≤ ⊤
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 m : ι
hnm : n ≤ m
ω : Ω
h_n : ∃ j, n ≤ j ∧ u j ω ∈ s
h_m : ¬∃ j, m ≤ j ∧ u j ω ∈ s
⊢ ↑(sInf {j | n ≤ j ∧ u j ω ∈ s}) ≤ ⊤

Tactic:
simp

Goal state after: