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

Goal state before:
pp: case mp
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : f ≤ cardinalGenerate g hc
⊢ g ⊆ f.sets

pp: case mpr
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
⊢ f ≤ cardinalGenerate g hc

Tactic:
· exact subset_trans (fun s => CardinalGenerateSets.basic) h

Goal state after:
case mpr
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
⊢ f ≤ cardinalGenerate g hc
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
n : ℕ
hn : ↑n = s.chainHeight r
l : Set α
hl : l ⊆ s
he : l.encard = ↑(n + 1)
⊢ ↑n < ↑(n + 1)

Tactic:
exact_mod_cast lt_add_one _

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

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b : α
h : ∀ (a : α), IsRegular (a ⊔ aᶜ)
a : α
⊢ (aᶜ ⊓ aᶜᶜ)ᶜ = ⊤

Tactic:
inf_compl_eq_bot,

Goal state after:
α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b : α
h : ∀ (a : α), IsRegular (a ⊔ aᶜ)
a : α
⊢ ⊥ᶜ = ⊤
Module: Mathlib.Order.Heyting.Regular

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b : α
a : Regular α
⊢ ⊤ ≤ ((↑a)ᶜ ⊓ (↑a)ᶜᶜ)ᶜ

Tactic:
inf_compl_eq_bot,

Goal state after:
α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b : α
a : Regular α
⊢ ⊤ ≤ ⊥ᶜ
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
⊢ g i ≤ g j

Tactic:
obtain h | ⟨-, h⟩ := Prod.lex_iff.1 hij

Goal state after:
case refine_2.inl
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : (f i, g i, i).1 < (f j, g j, j).1
⊢ g i ≤ g j

case refine_2.inr
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : Prod.Lex (fun x1 x2 ↦ x1 < x2) WellOrderingRel (f i, g i, i).2 (f j, g j, j).2
⊢ g i ≤ g j
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
⊢ Antivary f g ↔ ∃ x, Monotone f ∧ Antitone g

Tactic:
by
  simp [← antivaryOn_univ, antivaryOn_iff_exists_monotoneOn_antitoneOn]

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ n (x ⇨ y) ⊓ x ≤ n (x ⇨ y) ⊓ n x

Tactic:
by gcongr; exact n.le_apply

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝ : SemilatticeInf P
I : Ideal P
hI : I.IsPrime
x y : P
F : PFilter P := ⋯.toPFilter
⊢ x ∈ F ∧ y ∈ F → x ⊓ y ∈ F

Tactic:
exact fun h => inf_mem h.1 h.2

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
⊢ sSup {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = s

Tactic:
suffices sSup {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = sSup P ⊓ sSup Q by simpa

Goal state after:
α✝ : 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
⊢ sSup {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = sSup ↑P ⊓ sSup ↑Q
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 R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
⊢ ∃ y ∈ removeBot {a | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y

Tactic:
by
    have ⟨q, hq⟩ := hQ ha
    have ⟨r, hr⟩ := hR ha
    refine ⟨q ⊓ r, ⟨?_, ?_⟩, ?_⟩ <;> grind [le_inf_iff, P.ne_bot_of_mem ha]

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

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
⊢ f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel a b

Tactic:
obtain h1 | h2 := hf.forall_apply_eq_apply_iff a
  · refine ⟨by grind, ?_⟩
    rintro (h | h)
    · exact congrArg _ h.1
    exact hf.apply_eq_apply h
  grind

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

Goal state before:
pp: o : OrderType.{u_1}
⊢ IsEmpty o.ToType ↔ o = 0

Tactic:
by
  rw [← @type_eq_zero o.ToType, type_toType]

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
x✝ : X
⊢ ↑(S.restrict ↑(S.restrict x✝)) ≤ ↑(S.restrict x✝)

Tactic:
rw [S.giRestrict.gc.l_u_l_eq_l]

Goal state after:
Module: Mathlib.Order.Sublocale

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

Tactic:
by
  ext x
  constructor
  · simp +contextual [eq_comm]
  · intro hx
    exact ⟨x, by simp_all⟩

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
⊢ (fun n ↦ (OrderDual.ofDual n).toSublocale) ((fun s ↦ OrderDual.toDual s.toNucleus) S) = S

Tactic:
by ext x; simpa using ⟨by simp +contextual [eq_comm], fun hx ↦ ⟨x, by simp [hx]⟩⟩

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

Goal state before:
pp: case refine_2.inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i j : ι
A : Set Ω
hA : MeasurableSet A
hij : i ≤ j
⊢ MeasurableSet ((fun x ↦ (↑x.1, x.2)) ⁻¹' Set.Ioi j ×ˢ A)

Tactic:
simp [(by grind : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' Set.Ioi j ×ˢ A = ∅)]

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

Goal state before:
pp: case refine_2.inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i j : ι
A : Set Ω
hA : MeasurableSet A
hij : i ≤ j
⊢ MeasurableSet ((fun x ↦ (↑x.1, x.2)) ⁻¹' Set.Ioi j ×ˢ A)

Tactic:
· simp [(by grind : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' Set.Ioi j ×ˢ A = ∅)]

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₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ sInf (Set.Icc n m₁ ∩ {i | u i ω ∈ s}) = sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s})

pp: case hc
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ ∃ j ∈ Set.Icc n m₂, u j ω ∈ s

Tactic:
· refine le_antisymm ?_ (by gcongr; exacts [bddBelow_Icc.inter_of_left, ⟨j, hj₁, hj₂⟩])
    refine le_csInf ⟨j, Set.Icc_subset_Icc_right h hj₁, hj₂⟩ fun i hi => ?_
    by_cases hi' : i ≤ m₁
    · exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hi.1.1, hi'⟩, hi.2⟩
    · change j ∈ {i | u i ω ∈ s} at hj₂
      exact ((csInf_le bddBelow_Icc.inter_of_left ⟨hj₁, hj₂⟩).trans hj₁.2).trans (le_of_not_ge hi')

Goal state after:
case hc
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ ∃ j ∈ Set.Icc n m₂, u j ω ∈ s
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case zero
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : hittingBtwn f (Set.Iic a) (upperCrossingTime a b f N 0 ω) N ω < N
h' : upperCrossingTime a b f N 0 ω < N
⊢ ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a

Tactic:
hittingBtwn_lt_iff

Goal state after:
case zero
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : ∃ j ∈ Set.Ico (upperCrossingTime a b f N 0 ω) N, f j ω ∈ Set.Iic a
h' : upperCrossingTime a b f N 0 ω < N
⊢ ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a

case zero.hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : hittingBtwn f (Set.Iic a) (upperCrossingTime a b f N 0 ω) N ω < N
h' : upperCrossingTime a b f N 0 ω < N
⊢ N ≤ N
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  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' : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω < N
⊢ upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω

Tactic:
hittingBtwn_lt_iff

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  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' : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω

case hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  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' : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω < N
⊢ N ≤ N
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b

Tactic:
hittingBtwn_lt_iff

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b

case hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ N ≤ N
Module: Mathlib.Probability.Process.Stopping

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

Tactic:
have h' := h.2 i

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

Goal state before:
pp: case pos
Ω : 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
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ N = sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ f i ω})

Tactic:
refine False.elim (h₁ ?_)
        simp_all only [Set.mem_Ici]

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 ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
h : MeasurableSet (s ∩ {ω | τ ω ≤ ↑i}) ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i} ∩ {ω | τ ω ≤ ↑i_1})
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})

Tactic:
have h' := h.2 i

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
h : MeasurableSet (s ∩ {ω | τ ω ≤ ↑i}) ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i} ∩ {ω | τ ω ≤ ↑i_1})
h' : MeasurableSet (s ∩ {ω | τ ω ≤ ↑i} ∩ {ω | τ ω ≤ ↑i})
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ

Tactic:
by
  by_cases! hab : a < b
  · simp_rw [upcrossings]
    have : ∀ N, ∫⁻ ω, ENNReal.ofReal ((f N ω - a)⁺) ∂μ = ENNReal.ofReal (∫ ω, (f N ω - a)⁺ ∂μ) := by
      intro N
      rw [ofReal_integral_eq_lintegral_ofReal]
      · exact (hf.sub_martingale (martingale_const _ _ _)).pos.integrable _
      · exact Eventually.of_forall fun ω => posPart_nonneg _
    rw [lintegral_iSup']
    · simp_rw [this, ENNReal.mul_iSup, iSup_le_iff]
      intro N
      rw [(by simp :
          ∫⁻ ω, upcrossingsBefore a b f N ω ∂μ = ∫⁻ ω, ↑(upcrossingsBefore a b f N ω : ℝ≥0) ∂μ),
        lintegral_coe_eq_integral, ← ENNReal.ofReal_mul (sub_pos.2 hab).le]
      · simp_rw [NNReal.coe_natCast]
        exact (ENNReal.ofReal_le_ofReal
          (hf.mul_integral_upcrossingsBefore_le_integral_pos_part a b N)).trans
            (le_iSup (α := ℝ≥0∞) _ N)
      · simp only [NNReal.coe_natCast, hf.stronglyAdapted.integrable_upcrossingsBefore hab]
    · exact fun n => measurable_from_top.comp_aemeasurable
        (hf.stronglyAdapted.measurable_upcrossingsBefore hab).aemeasurable
    · filter_upwards with ω N M hNM
      rw [Nat.cast_le]
      exact upcrossingsBefore_mono hab hNM ω
  · rw [← sub_nonpos] at hab
    rw [ENNReal.ofReal_of_nonpos hab, zero_mul]
    exact zero_le

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
inst✝ : Bot ι
⊢ (stoppedValue u fun x ↦ ⊥) = u ⊥

Tactic:
by
  ext; simp [stoppedValue, ← WithTop.coe_bot]

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

Goal state before:
pp: case refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
j : WithTop ι
⊢ MeasurableSet ((fun a ↦ τ (↑a).2) ⁻¹' Set.Iic j)

Tactic:
cases j with
    | top => simp
    | coe j =>
      have h_set_eq : (fun x : s => τ (x : Set.Iic i × Ω).snd) ⁻¹' Set.Iic j =
          (fun x : s => (x : Set.Iic i × Ω).snd) ⁻¹' {ω | τ ω ≤ min i j} := by
        ext1 ω
        simp only [Set.mem_preimage, Set.mem_Iic, coe_min, le_inf_iff,
          Set.preimage_ofPred_eq, Set.mem_ofPred_eq, iff_and_self]
        exact fun _ => ω.prop
      rw [h_set_eq]
      suffices h_meas : @Measurable _ _ (m_set s) (f i) fun x : s ↦ (x : Set.Iic i × Ω).snd from
        h_meas (f.mono (min_le_left _ _) _ (hτ.measurableSet_le (min i j)))
      exact measurable_snd.comp (@measurable_subtype_coe _ m_prod _)

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
t : ℝ
hX : AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) (Measure.map Y μ)
⊢ ∫ (x : Ω'), rexp (t * X (Y x)) ∂μ = ∫ (x : Ω'), rexp (t * (X ∘ Y) x) ∂μ

Tactic:
Function.comp_apply

Goal state after:
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
⊢ μ (limsup s atTop) = 1

Tactic:
have : IsProbabilityMeasure μ := hs.isProbabilityMeasure
  rw [measure_congr (eventuallyEq_set.2 (ae_mem_limsup_atTop_iff μ <|
    measurableSet_filtrationOfSet' hsm) : (limsup s atTop : Set Ω) =ᵐ[μ]
      {ω | Tendsto (fun n => ∑ k ∈ Finset.range n,
        (μ[(s (k + 1)).indicator (1 : Ω → ℝ)|filtrationOfSet hsm k]) ω) atTop atTop})]
  suffices {ω | Tendsto (fun n => ∑ k ∈ Finset.range n,
      (μ[(s (k + 1)).indicator (1 : Ω → ℝ)|filtrationOfSet hsm k]) ω) atTop atTop} =ᵐ[μ] Set.univ by
    rw [measure_congr this, measure_univ]
  have : ∀ᵐ ω ∂μ, ∀ n, (μ[(s (n + 1)).indicator (1 : Ω → ℝ) | filtrationOfSet hsm n]) ω = _ :=
    ae_all_iff.2 fun n => hs.condExp_indicator_filtrationOfSet_ae_eq hsm n.lt_succ_self
  filter_upwards [this] with ω hω
  refine eq_true (?_ : Tendsto _ _ _)
  simp_rw [hω]
  have htends : Tendsto (fun n => ∑ k ∈ Finset.range n, μ (s (k + 1))) atTop (𝓝 ∞) := by
    rw [← ENNReal.tsum_add_one_eq_top hs' (measure_ne_top _ _)]
    exact ENNReal.tendsto_nat_tsum _
  rw [ENNReal.tendsto_nhds_top_iff_nnreal] at htends
  refine tendsto_atTop_atTop_of_monotone' ?_ ?_
  · refine monotone_nat_of_le_succ fun n => ?_
    rw [← sub_nonneg, Finset.sum_range_succ_sub_sum]
    exact ENNReal.toReal_nonneg
  · rintro ⟨B, hB⟩
    refine not_eventually.2 (Frequently.of_forall fun n => ?_) (htends B.toNNReal)
    rw [mem_upperBounds] at hB
    specialize hB (∑ k ∈ Finset.range n, μ (s (k + 1))).toReal _
    · refine ⟨n, ?_⟩
      rw [ENNReal.toReal_sum (by finiteness)]
      rfl
    · rwa [not_lt, ENNReal.ofNNReal_toNNReal, ENNReal.le_ofReal_iff_toReal_le]
      · simp
      · exact le_trans (by positivity) hB

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

Goal state before:
pp: case empty
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_int : ∀ i ∈ ∅, AEStronglyMeasurable (fun ω ↦ rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (fun ω ↦ 1) μ

Tactic:
exact aestronglyMeasurable_const

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

Goal state before:
pp: case inl
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : ↑n ≤ τ ω
⊢ ∀ x ∈ {i ∈ s | i < n}, {ω | τ ω = ↑x}.indicator (u x) ω = 0

pp: case inl.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : ↑n ≤ τ ω
⊢ ω ∈ {a | ↑n ≤ τ a}

Tactic:
· intro m hm
      refine Set.indicator_of_notMem ?_ _
      rw [Finset.mem_filter] at hm
      simp only [Set.mem_ofPred_eq]
      refine (lt_of_lt_of_le ?_ h).ne'
      exact mod_cast hm.2

Goal state after:
case inl.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : ↑n ≤ τ ω
⊢ ω ∈ {a | ↑n ≤ τ a}
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω ↦ rexp (t * X i ω)) μ
⊢ cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, cgf (X i) μ t

Tactic:
by
  have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure
  simp_rw [cgf]
  rw [← log_prod fun j hj => ?_]
  · rw [h_indep.mgf_sum₀ h_meas]
  · exact (mgf_pos (h_int j hj)).ne'

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
⊢ MemLp (stoppedValue u τ) p μ

Tactic:
by
  refine memLp_stoppedValue_of_mem_finset hτ hu (s := Finset.Iic N) fun ω => ?_
  simp only [Finset.coe_Iic, Set.mem_image, Set.mem_Iic]
  specialize hbdd ω
  have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at hbdd
  lift τ ω to ι using h_top with i hi
  exact ⟨i, mod_cast hbdd, rfl⟩

Goal state after:
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
h_nonpos : X ω ≤ 0
⊢ rexp ((v - t) * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)

Tactic:
le_add_iff_nonneg_left

Goal state after:
case refine_2.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
h_nonpos : X ω ≤ 0
⊢ 0 ≤ rexp ((v + t) * X ω)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case e_a.e_s
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n i : ℕ
⊢ i ∈ Finset.Iio n ↔ i ∈ Finset.range n

Tactic:
Finset.mem_Iio,

Goal state after:
case e_a.e_s
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n i : ℕ
⊢ i < n ↔ i ∈ Finset.range n
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ (∑ k ∈ Finset.range n, (s (k + 1)).indicator 1) ω) atTop atTop ↔
      Tendsto (fun n ↦ predictablePart (process s) ℱ μ n ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔
      Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑ℱ k] ω) atTop atTop

Tactic:
predictablePart_process_ae_eq

Goal state after:
case refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ (∑ k ∈ Finset.range n, (s (k + 1)).indicator 1) ω) atTop atTop ↔
      Tendsto (fun n ↦ (∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑ℱ k]) ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔
      Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑ℱ k] ω) atTop atTop
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
⊢ HasFPowerSeriesAt (mgf X μ)
    (FormalMultilinearSeries.ofScalars ℝ fun n ↦ (∫ (x : Ω), (fun ω ↦ X ω ^ n * rexp (v * X ω)) x ∂μ) / ↑n !) v

Tactic:
convert! (analyticAt_mgf hv).hasFPowerSeriesAt
  rw [iteratedDeriv_mgf hv]

Goal state after: