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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ a < b ∨ a = b ∨ b < a ∨ IncompRel (fun x1 x2 ↦ x1 ≤ x2) a b

Tactic:
simpa using lt_or_antisymmRel_or_gt_or_incompRel a b

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ a ⊓ b = ⊥ ↔ ↑(a ⊓ b) = ↑⊥

Tactic:
Subtype.coe_injective.eq_iff

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ a ⊓ b = ⊥ ↔ a ⊓ b = ⊥
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ a ⊔ b = ⊤ ↔ ↑(a ⊔ b) = ↑⊤

Tactic:
Subtype.coe_injective.eq_iff

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ a ⊔ b = ⊤ ↔ a ⊔ b = ⊤
Module: Mathlib.Order.Concept

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.intent ⊆ d.intent
⊢ d.extent ⊆ c.extent

Tactic:
← c.lowerPolar_intent,

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.intent ⊆ d.intent
⊢ d.extent ⊆ lowerPolar r c.intent
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
a : α
b : β
ha : (a, b).1 ∈ countableSupClosure s
hb : (a, b).2 ∈ countableSupClosure t
⊢ (a, b) ∈ countableSupClosure (s ×ˢ t)

Tactic:
simp only [mem_countableSupClosure_iff] at ha hb ⊢

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
a : α
b : β
ha : ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a
hb : ∃ A, ∃ (_ : A ⊆ t) (_ : A.Nonempty) (_ : A.Countable), IsLUB A b
⊢ ∃ A, ∃ (_ : A ⊆ s ×ˢ t) (_ : A.Nonempty) (_ : A.Countable), IsLUB A (a, b)
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : SetRel α β
l : Filter α
x✝ y✝ : Set β
hs : x✝ ∈ {s | r.core s ∈ l}
ht : y✝ ∈ {s | r.core s ∈ l}
⊢ x✝ ∩ y✝ ∈ {s | r.core s ∈ l}

Tactic:
by
    simp only [Set.mem_ofPred_eq]
    convert! inter_mem hs ht
    rw [← SetRel.core_inter]

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

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

Tactic:
ha.eq

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Ici a) (Ici (f a))

Tactic:
rw [← Ioi_union_left, ← Ioi_union_left]
  exact
    (surjOn_Ioi_of_monotone_surjective h_mono h_surj a).union_union
      (@image_singleton _ _ f a ▸ surjOn_image _ _)

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
⊢ IF.I.IsProper

Tactic:
obtain ⟨w, h⟩ := IF.F.nonempty
  apply isProper_of_notMem (_ : w ∉ IF.I)
  rwa [← IF.compl_I_eq_F] at h

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
a : X
ha : a ∈ ↑S
b : X
hb : b ∈ ↑S
⊢ a ⊓ b ∈ ↑S

Tactic:
rw [← sInf_pair]

Goal state after:
X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
a : X
ha : a ∈ ↑S
b : X
hb : b ∈ ↑S
⊢ sInf {a, b} ∈ ↑S
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case refine_2
Ω : Type u_1
ι : Type u_2
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m✝
u : ι → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
i : ι
this✝ : MeasurableSpace (ι × Ω) := 𝓕.predictable
this : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑𝓕 i)
X : ℕ → ↑(Set.Iic i) × Ω → E := fun m x ↦ (StronglyMeasurable.approx h𝓕 m) (↑x.1, x.2)
m : ℕ
⊢ (Set.range (X m)).Finite

Tactic:
exact Set.Finite.subset (h𝓕.approx m).finite_range (by grind)

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

Goal state before:
pp: case refine_3
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
E : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
u : ι → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
i : ι
this✝ : MeasurableSpace (ι × Ω) := 𝓕.predictable
this : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑𝓕 i)
X : ℕ → ↑(Set.Iic i) × Ω → E := fun m_1 x ↦ (StronglyMeasurable.approx h𝓕 m_1) (↑x.1, x.2)
⊢ ∀ (x : { x // x ∈ Set.Iic i } × Ω),
    Tendsto (fun n ↦ ((fun m_1 ↦ { toFun := X m_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ }) n) x) atTop
      (𝓝 ((fun p ↦ u (↑p.1) p.2) x))

Tactic:
· exact fun n ↦ by apply h𝓕.tendsto_approx

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

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

Tactic:
simp only [coe_lt_coe, coe_le_coe]
      rw [le_pred_iff_of_not_isMin hi_min]

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

Goal state before:
pp: case step
Ω : 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 : ℕ
s : Set Ω
hs : MeasurableSet s
m✝ : ℕ
hk₁ : i.le m✝
hk₂ : ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f m✝ ω ∂μ
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f m✝.succ ω ∂μ

Tactic:
exact hk₂.trans (hf _ s (𝒢.mono hk₁ _ hs))

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

Goal state before:
pp: case pos.refine_2
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
b : ι
hb : b ∈ Set.Icc n m ∩ {i | u i ω ∈ s}
⊢ n ≤ b

Tactic:
rw [Set.mem_inter_iff] at hb

Goal state after:
case pos.refine_2
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
b : ι
hb : b ∈ Set.Icc n m ∧ b ∈ {i | u i ω ∈ s}
⊢ n ≤ b
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✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i =ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]
i j k : ℕ
hik : i ≤ k
hk : μ[f k | ↑𝒢 i] =ᵐ[μ] f i
ω : Ω
hω1 : μ[f k | ↑𝒢 i] ω = f i ω
hω2 : μ[f k | ?m.127] ω = μ[μ[f (k + 1) | ↑𝒢 k] | ?m.127] ω
hω3 : μ[μ[f (k + 1) | ↑𝒢 k] | ↑𝒢 i] ω = μ[f (k + 1) | ↑𝒢 i] ω
⊢ μ[f (k + 1) | ↑𝒢 i] ω = f i ω

Tactic:
rw [← hω1, hω2, hω3]

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

Goal state before:
pp: case zero
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
⊢ (IsStoppingTime ℱ fun ω ↦ ↑(upperCrossingTime a b f N 0 ω)) ∧
    IsStoppingTime ℱ fun ω ↦ ↑(lowerCrossingTime a b f N 0 ω)

Tactic:
refine ⟨isStoppingTime_const _ 0, ?_⟩
    simp only [lowerCrossingTime_zero, Nat.bot_eq_zero]
    exact hf.adapted.isStoppingTime_hittingBtwn measurableSet_Iic

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})

Tactic:
by gcongr; exacts [bddBelow_Icc.inter_of_left, ⟨j, hj₁, hj₂⟩]

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

Goal state before:
pp: case pos
Ω : 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 ≤ sInf (Set.Icc n' m ∩ {i | u i ω ∈ s})

Tactic:
have ⟨t, ht⟩ := h_n'

Goal state after:
case pos
Ω : 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
t : ι
ht : t ∈ Set.Icc n' m ∧ u t ω ∈ s
⊢ m ≤ sInf (Set.Icc n' m ∩ {i | u i ω ∈ s})
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case refine_1
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
h : b - a ≤ (f ω i - a)⁺
⊢ b ≤ f ω i

Tactic:
← sub_le_sub_iff_right a,

Goal state after:
case refine_1
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
h : b - a ≤ (f ω i - a)⁺
⊢ b - a ≤ f ω i - a
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : 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 ω
ω : Ω
i : ℕ
⊢ (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a

Tactic:
posPart_nonpos,

Goal state after:
Ω : 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 ω
ω : Ω
i : ℕ
⊢ f i ω - a ≤ 0 ↔ f i ω ≤ a
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
⊢ upcrossingsBefore a b f N ω = ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i

Tactic:
rw [← Finset.sum_Ico_consecutive _ (Nat.succ_le_succ zero_le)
    (Nat.succ_le_succ (upcrossingsBefore_le f ω hab))]

Goal state after:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
⊢ upcrossingsBefore a b f N ω =
    ∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ,
        {n | upperCrossingTime a b f N n ω < N}.indicator 1 i +
      ∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ, {n | upperCrossingTime a b f N n ω < N}.indicator 1 i
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ENNReal.ofReal (b - a) * ⨆ n, ∫⁻ (a_1 : Ω), ↑(upcrossingsBefore a b f n a_1) ∂μ ≤
    ⨆ N, ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)

Tactic:
ENNReal.mul_iSup,

Goal state after:
case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ⨆ i, ENNReal.ofReal (b - a) * ∫⁻ (a_1 : Ω), ↑(upcrossingsBefore a b f i a_1) ∂μ ≤
    ⨆ N, ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ENNReal.ofReal (b - a) * ⨆ n, ∫⁻ (a_1 : Ω), ↑(upcrossingsBefore a b f n a_1) ∂μ ≤
    ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ

pp: case pos.hf
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ∀ (n : ℕ), AEMeasurable (fun ω ↦ ↑(upcrossingsBefore a b f n ω)) μ

pp: case pos.h_mono
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ∀ᵐ (x : Ω) ∂μ, Monotone fun n ↦ ↑(upcrossingsBefore a b f n x)

Tactic:
· 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]

Goal state after:
case pos.hf
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ∀ (n : ℕ), AEMeasurable (fun ω ↦ ↑(upcrossingsBefore a b f n ω)) μ

case pos.h_mono
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ∀ᵐ (x : Ω) ∂μ, Monotone fun n ↦ ↑(upcrossingsBefore a b f n x)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : 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
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
h_min_eq_left : (fun x ↦ min (↑↑(↑x).1) (τ (↑x).2)) = fun x ↦ ↑↑(↑x).1
⊢ Measurable (sᶜ.domRestrict fun p ↦ min (↑↑p.1) (τ p.2))

Tactic:
simp +unfoldPartialApp only [sc, Set.domRestrict, h_min_eq_left]

Goal state after:
Ω : 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
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
h_min_eq_left : (fun x ↦ min (↑↑(↑x).1) (τ (↑x).2)) = fun x ↦ ↑↑(↑x).1
⊢ Measurable fun x ↦ ↑↑(↑x).1
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 μ)
⊢ mgf X (Measure.map Y μ) t = mgf (X ∘ Y) μ t

Tactic:
simp_rw [mgf, integral_map hY hX, Function.comp_apply]

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

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω ↦ rexp (a * X ω)) μ
hb : Integrable (fun ω ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) μ

Tactic:
refine AEMeasurable.aestronglyMeasurable ?_
      refine measurable_exp.comp_aemeasurable (AEMeasurable.const_mul ?_ _)
      by_cases ha_zero : a = 0
      · refine aemeasurable_of_aemeasurable_exp_mul ?_ hb.1.aemeasurable
        rw [ha_zero] at hab
        exact Ne.symm hab
      · exact aemeasurable_of_aemeasurable_exp_mul ha_zero ha.1.aemeasurable

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

Goal state before:
pp: case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), Measurable (X i)
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : Integrable (fun ω ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
h_int : ∀ i_1 ∈ insert i s, Integrable (fun ω ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, Integrable (fun ω ↦ rexp (t * X i ω)) μ
⊢ X i ⟂ᵢ[μ] ∑ x ∈ s, X x

Tactic:
exact (h_indep.indepFun_finsetSum_of_notMem h_meas hi_notin_s).symm

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

Goal state before:
pp: Ω : Type u_2
s : ℕ → Set Ω
ω : Ω
n : ℕ
⊢ |process s (n + 1) ω - process s n ω| ≤ ↑1

Tactic:
norm_cast
  rw [process, process, Finset.sum_apply, Finset.sum_apply,
    Finset.sum_range_succ_sub_sum, ← Real.norm_eq_abs, norm_indicator_eq_indicator_norm]
  refine Set.indicator_le' (fun _ _ => ?_) (fun _ _ => zero_le_one) _
  rw [Pi.one_apply, norm_one]

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
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
⊢ MemLp (stoppedValue u τ) p μ

Tactic:
stoppedValue_eq_of_mem_finset hbdd

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
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
⊢ MemLp (∑ i ∈ s, {ω | τ ω = ↑i}.indicator (u i)) p μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ μ.real {ω | X ω ≤ ε} ≤ rexp (-t * ε + cgf X μ t)

Tactic:
refine (measure_le_le_exp_mul_mgf ε ht h_int).trans ?_

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε + cgf X μ t)
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2.inl
Ω : 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_nonneg : 0 ≤ X ω
⊢ rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)

Tactic:
rw [abs_of_nonneg h_nonneg, ← add_mul, add_comm, le_add_iff_nonneg_right]

Goal state after:
case refine_2.inl
Ω : 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_nonneg : 0 ≤ X ω
⊢ 0 ≤ rexp ((v - t) * X ω)
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
⊢ 0 ≤ (s (n + 1)).indicator 1 ω

Tactic:
exact Set.indicator_nonneg (fun _ _ => zero_le_one) _

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
hz' : z.re ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (fun z ↦ ∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ n * cexp (z * ↑(X ω))) x ∂μ)
    (∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hz'

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
hz' : ∃ l u, z.re ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ
⊢ HasDerivAt (fun z ↦ ∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ n * cexp (z * ↑(X ω))) x ∂μ)
    (∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2.refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
h_le : ∀ (a : Ω), |X a| ^ p * rexp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)
ω : Ω
⊢ |(||X ω| ^ p|)| * rexp (v * X ω + x * |X ω|) ≤ |(p / (|t| - x)) ^ p| * rexp (v * X ω + |t| * |X ω|)

Tactic:
simp_rw [abs_rpow_of_nonneg (abs_nonneg _), abs_abs]

Goal state after:
case refine_2.refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
h_le : ∀ (a : Ω), |X a| ^ p * rexp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)
ω : Ω
⊢ |X ω| ^ p * rexp (v * X ω + x * |X ω|) ≤ |(p / (|t| - x)) ^ p| * rexp (v * X ω + |t| * |X ω|)
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : μ = 0
⊢ Integrable (fun ω ↦ rexp (t * X ω)) μ ↔ Integrable (fun ω ↦ rexp (t * Y ω)) μ'

Tactic:
simp [hμ, hμμ'.mp hμ]

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

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ covarianceBilin 0 = 0

Tactic:
rw [covarianceBilin]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ (covarianceBilinDual 0).bilinearComp (toDualMap ℝ E).toContinuousLinearMap (toDualMap ℝ E).toContinuousLinearMap = 0
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case h₁
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
x : E
⊢ ‖L x‖ₑ ≤ ‖L‖ₑ * ‖x‖ₑ

Tactic:
exact L.le_opENorm x

Goal state after: