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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun i ↦ α i) i)
he : e ∈ s
h : ∀ j < i, e j = sInf s j
⊢ sInf s i ≤ e i

Tactic:
rw [sInf_apply]

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun i ↦ α i) i)
he : e ∈ s
h : ∀ j < i, e j = sInf s j
⊢ ⨅ e, ↑e i ≤ e i
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun i ↦ α i) i)
h : ∀ f ∈ s, (∀ j < i, f j = sInf s j) → e i ≤ f i
⊢ e i ≤ sInf s i

Tactic:
rw [sInf_apply]

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun i ↦ α i) i)
h : ∀ f ∈ s, (∀ j < i, f j = sInf s j) → e i ≤ f i
⊢ e i ≤ ⨅ e, ↑e i
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
⊢ IsLUB s (sSup s)

Tactic:
refine ⟨fun e he ↦ ?_, fun e h ↦ ?_⟩
  · by_contra! hs
    obtain ⟨a, ha⟩ := hs
    exact ha.2.not_ge (le_sSup_apply he fun j hj ↦ (ha.1 j hj).symm)
  · by_contra! hs
    obtain ⟨a, ha⟩ := hs
    refine ha.2.not_ge <| sSup_apply_le fun f hf hf' ↦ apply_le_of_toLex (h hf) ?_
    simp_all

Goal state after:
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: case refine_2
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
⊢ ∃ r ∈ c, r x z

Tactic:
have : IsPartialOrder _ _ := hc₁ h₁s₁

Goal state after:
case refine_2
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this✝ : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this : IsPartialOrder α s₁
⊢ ∃ r ∈ c, r x z
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: case refine_3
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
⊢ x = y

Tactic:
have : IsPartialOrder _ _ := hc₁ h₁s₁

Goal state after:
case refine_3
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this✝ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this : IsPartialOrder α s₁
⊢ x = y
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst✝² : CardinalInterFilter l c
l₁ l₂ : Filter α
c₁ c₂ : Cardinal.{u}
inst✝¹ : CardinalInterFilter l₁ c₁
inst✝ : CardinalInterFilter l₂ c₂
⊢ CardinalInterFilter (l₁ ⊔ l₂) (min c₁ c₂)

Tactic:
by
  have : CardinalInterFilter l₁ (c₁ ⊓ c₂) :=
    CardinalInterFilter.of_cardinalInterFilter_of_le l₁ inf_le_left
  have : CardinalInterFilter l₂ (c₁ ⊓ c₂) :=
    CardinalInterFilter.of_cardinalInterFilter_of_le l₂ inf_le_right
  exact cardinalInterFilter_sup_eq _ _

Goal state after:
Module: Mathlib.Order.Heyting.Regular

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
ha : IsRegular a
⊢ Disjoint aᶜ b ↔ b ≤ a

Tactic:
← le_compl_iff_disjoint_left,

Goal state after:
α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
ha : IsRegular a
⊢ b ≤ aᶜᶜ ↔ b ≤ a
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
a b : α
n : ℕ
hb : 0 ≤ b
⊢ ↑n ∈ Set.Icc a b ↔ n ∈ Finset.Icc ⌈a⌉₊ ⌊b⌋₊

Tactic:
by
  simp [ceil_le, le_floor_iff hb]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
⊢ False

Tactic:
apply hn.ne'

Goal state after:
A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := ⋯
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
⊢ n = 0
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
⊢ ENNReal.ofReal T ≤ (n + 1) • volume (closedBall 0 (T / ↑(n + 1) / 2))

Tactic:
volume_closedBall,

Goal state after:
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
⊢ ENNReal.ofReal T ≤ (n + 1) • ENNReal.ofReal (min T (2 * (T / ↑(n + 1) / 2)))
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
⊢ a₁ ⊓ a₂ ∉ J

Tactic:
have a₂J₂ : a₂ ∈ J₂ := mem_of_subset_of_mem (le_sup_right : _ ≤ J ⊔ _) mem_principal_self

Goal state after:
case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
⊢ a₁ ⊓ a₂ ∉ J
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
x : α
u : Set α
P : Partition u
⊢ x ∈ u ↔ x ∈ P.partOf x ∧ P.partOf x ∈ P

Tactic:
refine ⟨fun hx ↦ ?_, fun ⟨hx, hP⟩ ↦ subset_of_mem hP hx⟩

Goal state after:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : x ∈ u
⊢ x ∈ P.partOf x ∧ P.partOf x ∈ P
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case refine_2.mp
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun f
b : α
ha : f b ∉ u
⊢ f b = b

Tactic:
exact hf.apply_of_notMem <| hf.apply_mem_iff le_rfl |>.not.mp ha

Goal state after:
Module: Mathlib.Order.Std

Goal state before:
pp: case isTrue
α : Type u_1
args : OfStdArgs α
this✝⁵ : LE α := args.le
this✝⁴ : LT α := args.lt
this✝³ :
  let this := args.le;
  let this_1 := args.lt;
  Std.LawfulOrderLT α
this✝² :
  let this := args.le;
  Std.IsLinearOrder α
this✝¹ : DecidableLE α := args.decidableLE
this✝ : Std.LawfulOrderLeftLeaningMin α
this : Std.LawfulOrderLeftLeaningMax α
a b : α
h✝ : b ≤ a
⊢ a = if a ≤ b then b else a

Tactic:
split
        · exact Std.le_antisymm ‹_› ‹_›
        · rfl

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 α
⊢ findAtom ⊥ = ⊥

Tactic:
by
  apply Function.iterate_fixed
  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 ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i : ι
⊢ Measurable fun x ↦ (↑x.1, x.2)

Tactic:
rw [measurable_iff_comap_le]
  refine MeasurableSpace.comap_le_iff_le_map.2 <|
    measurableSpace_le_predictable_of_measurableSet ?_ ?_
  · intros A hA
    simp only [MeasurableSpace.map_def,
      (by aesop : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' ({⊥} ×ˢ A) = {⊥} ×ˢ A)]
    exact (measurableSet_singleton _).prod <| 𝓕.mono bot_le _ hA
  · intros j A hA
    simp only [MeasurableSpace.map_def]
    obtain hji | hij := le_total j i
    · rw [(by grind : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' Set.Ioi j ×ˢ A
        = (Subtype.val ⁻¹' (Set.Ioc j i)) ×ˢ A)]
      exact (measurable_subtype_coe measurableSet_Ioc).prod (𝓕.mono hji _ hA)
    · simp [(by grind : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' Set.Ioi j ×ˢ A = ∅)]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf : ∀ (i j : ι), i ≤ j → ∀ (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
i j : ι
hij : i ≤ j
this : f i ≤ᵐ[μ.trim ⋯] μ[f j | ↑ℱ i]
⊢ f i ≤ᵐ[μ] μ[f j | ↑ℱ i]

Tactic:
exact ae_le_of_ae_le_trim this

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
⊢ ∃ j ∈ Set.Icc n i, u j ω ∈ s

pp: case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
⊢ hittingAfter u s n ω ≤ ↑i

Tactic:
· have h_top : hittingAfter u s n ω ≠ ⊤ := fun h ↦ by simp [h] at h'
    have h_le := le_hittingAfter (u := u) (s := s) (n := n) ω
    refine ⟨(hittingAfter u s n ω).untopA, ?_, hittingAfter_mem_set_of_ne_top h_top⟩
    lift (hittingAfter u s n ω) to ι using h_top with i'
    norm_cast at h' h_le

Goal state after:
case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
⊢ hittingAfter u s n ω ≤ ↑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 i' : ι
hi'_lub : IsLUB (Set.Iio i) i'
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
rcases lub_Iio_eq_self_or_Iio_eq_Iic i hi'_lub with hi'_eq_i | h_Iio_eq_Iic

Goal state after:
case inl
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i i' : ι
hi'_lub : IsLUB (Set.Iio i) i'
hi'_eq_i : i' = i
⊢ MeasurableSet {ω | τ ω < ↑i}

case inr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i i' : ι
hi'_lub : IsLUB (Set.Iio i) i'
h_Iio_eq_Iic : Set.Iio i = Set.Iic i'
⊢ MeasurableSet {ω | τ ω < ↑i}
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:
simp_rw [← not_le]

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 | ¬upperCrossingTime a b f N (i + 1) ω ≤ n}) n
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)) μ
m i : ℕ
hi : i ∈ Finset.range m
⊢ StronglyMeasurable (ξ i • (f (i + 1) - f i))

Tactic:
rw [Finset.mem_range] at hi

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)) μ
m i : ℕ
hi : i < m
⊢ StronglyMeasurable (ξ i • (f (i + 1) - f i))
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
hab : a < b
this : ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
⊢ ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * μ Set.univ

Tactic:
simp_rw [eLpNorm_one_eq_lintegral_enorm] at hbdd

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this : ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ‖f n x‖ₑ ∂μ ≤ ↑R
⊢ ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * μ Set.univ
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case h
Ω : 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 ω)) ω
i : ℕ
hi : i ∈ Finset.range (upcrossingsBefore a b f N ω)
⊢ i < upcrossingsBefore a b f N ω

Tactic:
rwa [Finset.mem_range] at hi

Goal state after:
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 τ
s : ℕ → Set Ω
i : ι
hs : ∀ (i : ℕ) (i_1 : ι), MeasurableSet (s i ∩ {ω | τ ω ≤ ↑i_1})
⊢ MeasurableSet ((⋃ i, s i) ∩ {ω | τ ω ≤ ↑i})

Tactic:
forall_comm

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
i : ι
hs : ∀ (b : ι) (a : ℕ), MeasurableSet (s a ∩ {ω | τ ω ≤ ↑b})
⊢ MeasurableSet ((⋃ i, s i) ∩ {ω | τ ω ≤ ↑i})
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ ↑N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
ω : Ω
hω : ω ∈ s
⊢ ↑i ≤ ↑j

Tactic:
exact mod_cast hij

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:
by
  rw [← Set.univ_inter {ω | τ ω = i}, measurableSet_inter_eq_iff, Set.univ_inter]
  exact hτ.measurableSet_eq 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✝ : SecondCountableTopology ι
hτ : IsStoppingTime f τ
⊢ Measurable τ

Tactic:
by
  refine measurable_of_Iic fun i ↦ ?_
  cases i with
  | top => simp
  | coe i => exact hτ.measurableSet_le' i

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

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)

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

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

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)

Tactic:
have hg : Submartingale g ℱ μ :=
    hf.sub_martingale (martingale_const_fun _ _ (hf.stronglyAdapted 0) (hf.integrable 0))

Goal state after:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case mp
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n ↦ f n ω✝) ↔ ∃ c, Tendsto (fun n ↦ f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n ↦ (-f) n ω✝) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n ↦ f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : c ∈ upperBounds (Set.range fun n ↦ (-f) n ω✝)
ω : ℝ
hω : ω ∈ Set.range fun n ↦ f n ω✝
⊢ -c ≤ ω

Tactic:
rw [mem_upperBounds] at hc
    refine neg_le.2 (hc _ ?_)
    simpa only [Pi.neg_apply, Set.mem_range, neg_inj]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝² : PartialOrder ι
ℱ : Filtration ι m
inst✝¹ : NormedAddCommGroup E
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ ↑N
ω : Ω
⊢ τ ω ∈ WithTop.some '' ↑(Finset.Iic N)

Tactic:
simp only [Finset.coe_Iic, Set.mem_image, Set.mem_Iic]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝² : PartialOrder ι
ℱ : Filtration ι m
inst✝¹ : NormedAddCommGroup E
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ ↑N
ω : Ω
⊢ ∃ x ≤ N, ↑x = τ ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝² : PartialOrder ι
ℱ : Filtration ι m
inst✝¹ : NormedAddCommGroup E
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ ↑N
ω : Ω
⊢ τ ω ∈ WithTop.some '' ↑(Finset.Iic N)

Tactic:
simp only [Finset.coe_Iic, Set.mem_image, Set.mem_Iic]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝² : PartialOrder ι
ℱ : Filtration ι m
inst✝¹ : NormedAddCommGroup E
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ ↑N
ω : Ω
⊢ ∃ x ≤ N, ↑x = τ ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : NormedAddCommGroup E
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
ω : Ω
h : τ ω < ↑n
⊢ τ ω ∈ WithTop.some '' ↑(Finset.Iic n)

Tactic:
simp only [Finset.coe_Iic, Set.mem_image, Set.mem_Iic]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : NormedAddCommGroup E
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
ω : Ω
h : τ ω < ↑n
⊢ ∃ x ≤ n, ↑x = τ ω