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

Goal state before:
pp: case refine_2.inl.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
a b : α
ab : s a b
ba : s b a
⊢ a = b

pp: case refine_2.inl.inr
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
a b : α
ab : s a b
bx : s b x
ya : s y a
⊢ a = b

pp: case refine_2.inr.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
a b : α
ax : s a x
yb : s y b
ba : s b a
⊢ a = b

pp: case refine_2.inr.inr
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
a b : α
ax : s a x
yb : s y b
bx : s b x
ya : s y a
⊢ a = b

Tactic:
· exact antisymm ab ba

Goal state after:
case refine_2.inl.inr
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
a b : α
ab : s a b
bx : s b x
ya : s y a
⊢ a = b

case refine_2.inr.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
a b : α
ax : s a x
yb : s y b
ba : s b a
⊢ a = b

case refine_2.inr.inr
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
a b : α
ax : s a x
yb : s y b
bx : s b x
ya : s y a
⊢ a = b
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
p : α → ι → Prop
hic : #ι < c
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i

Tactic:
simp only [Filter.Eventually, ofPred_forall]

Goal state after:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
p : α → ι → Prop
hic : #ι < c
⊢ ⋂ i, {x | p x i} ∈ l ↔ ∀ (i : ι), {x | p x i} ∈ l
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
p : α → (i : ι) → i ∈ S → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi

Tactic:
simp only [Filter.Eventually, ofPred_forall]

Goal state after:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
p : α → (i : ι) → i ∈ S → Prop
⊢ ⋂ i, ⋂ (i_1 : i ∈ S), {x | p x i i_1} ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), {x | p x i hi} ∈ l
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:
have : CardinalInterFilter l₁ (c₁ ⊓ c₂) :=
    CardinalInterFilter.of_cardinalInterFilter_of_le l₁ inf_le_left

Goal state after:
ι α β : 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₂
this : CardinalInterFilter l₁ (min c₁ c₂)
⊢ CardinalInterFilter (l₁ ⊓ l₂) (min c₁ c₂)
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:
have : CardinalInterFilter l₁ (c₁ ⊓ c₂) :=
    CardinalInterFilter.of_cardinalInterFilter_of_le l₁ inf_le_left

Goal state after:
ι α β : 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₂
this : CardinalInterFilter l₁ (min c₁ c₂)
⊢ CardinalInterFilter (l₁ ⊔ l₂) (min c₁ c₂)
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
x : α
hx : x ≤ f 0
⊢ Monotone (insertNth 0 x f)

Tactic:
Fin.monotone_iff_le_succ

Goal state after:
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
x : α
hx : x ≤ f 0
⊢ ∀ (i : Fin (n + 1)), insertNth 0 x f i.castSucc ≤ insertNth 0 x f i.succ
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
⊢ Monotone (i.castSucc.succ.insertNth x f)

Tactic:
Fin.monotone_iff_le_succ

Goal state after:
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
⊢ ∀ (i_1 : Fin (n + 1)), i.castSucc.succ.insertNth x f i_1.castSucc ≤ i.castSucc.succ.insertNth x f i_1.succ
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
j : Fin (n + 1)
hj : j < i.castSucc
⊢ i.castSucc.succ.insertNth x f j.castSucc < i.castSucc.succ.insertNth x f j.succ

pp: case inr.inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
⊢ i.castSucc.succ.insertNth x f i.castSucc.castSucc < i.castSucc.succ.insertNth x f i.castSucc.succ

pp: case inr.inr
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
j : Fin (n + 1)
hj : i.castSucc < j
⊢ i.castSucc.succ.insertNth x f j.castSucc < i.castSucc.succ.insertNth x f j.succ

Tactic:
· obtain ⟨j, rfl⟩ := j.eq_castSucc_of_ne_last (Fin.ne_last_of_lt hj)
    grind [insertNth_apply_below, castPred_castSucc]

Goal state after:
case inr.inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
⊢ i.castSucc.succ.insertNth x f i.castSucc.castSucc < i.castSucc.succ.insertNth x f i.castSucc.succ

case inr.inr
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
j : Fin (n + 1)
hj : i.castSucc < j
⊢ i.castSucc.succ.insertNth x f j.castSucc < i.castSucc.succ.insertNth x f j.succ
Module: Mathlib.Order.Height

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r = 0
⊢ s = ∅

Tactic:
(Tactic.tacticSeq
 (Tactic.tacticSeq1Indented
  [(Tactic.simp
    "simp"
    (Tactic.optConfig [])
    []
    ["only"]
    ["["
     [(Tactic.simpLemma [] [] `chainHeight)
      ","
      (Tactic.simpLemma [] [] `iSup_eq_zero)
      ","
      (Tactic.simpLemma [] [] `encard_eq_zero)
      ","
      (Tactic.simpLemma [] [] `Subtype.forall)
      ","
      (Tactic.simpLemma [] [] `and_imp)]
     "]"]
    [(Tactic.location "at" (Tactic.locationHyp [`h]))])
   []
   (Lean.Elab.Tactic.Ext.ext "ext" [(Tactic.rintroPat.one (Tactic.rcasesPat.one `x))] [])
   []
   (Tactic.simpa
    "simpa"
    []
    []
    (Tactic.simpaArgsRest
     (Tactic.optConfig [])
     []
     []
     []
     ["using"
      (Term.app
       `h
       [(choice
         («term{_}» "{" [`x] "}")
         (Term.structInst
          "{"
          []
          (Term.structInstFields [(Term.structInstField (Term.structInstLVal `x []) [])])
          (Term.optEllipsis [])
          []
          "}"))])]))]))

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
x : α
hx : f (last n) ≤ x
⊢ Monotone ((last (n + 1)).insertNth x f)

Tactic:
Fin.monotone_iff_le_succ

Goal state after:
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
x : α
hx : f (last n) ≤ x
⊢ ∀ (i : Fin (n + 1)), (last (n + 1)).insertNth x f i.castSucc ≤ (last (n + 1)).insertNth x f i.succ
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝ : SemilatticeInf P
I : Ideal P
hI : I.IsPrime
x y : P
⊢ x ⊓ y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
by
  contrapose!
  let F := hI.compl_filter.toPFilter
  change x ∈ F ∧ y ∈ F → x ⊓ y ∈ F
  exact fun h => inf_mem h.1 h.2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α → β
h : ScottContinuous f
x✝ : Set α
d₁ : x✝.Nonempty
d₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) x✝
⊢ f (sSup x✝) = sSup (f '' x✝)

Tactic:
by rw [IsLUB.sSup_eq (h d₁ d₂ (isLUB_iff_sSup_eq.mpr rfl))]

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

Goal state before:
pp: α β : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
⊢ lift.{u_1, u} (type α) = lift.{u_1, u} (type β) ↔ Nonempty (α ≃o β)

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨h⟩ ↦ congrArg lift <| type_congr h⟩
  rw [← type_ulift, ← type_ulift, type_eq_type] at h
  exact ⟨(ULift.orderIso.symm.trans h.some).trans ULift.orderIso⟩

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

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

Tactic:
obtain hij | hij := le_total j i

Goal state after:
case inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : j ≤ i
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)

case inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : i ≤ j
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)
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✝ : SigmaFiniteFiltration μ ℱ
hf : IsStronglyPredictable ℱ f
hfint : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
⊢ predictablePart f ℱ μ n =ᵐ[μ] f n - f 0

Tactic:
by
  simp only [predictablePart, ← Finset.sum_range_sub]
  exact eventuallyEq_sum fun i hi => (condExp_of_stronglyMeasurable (ℱ.le i)
    ((hf.measurable_add_one i).sub (hf.stronglyAdapted i))
    ((hfint (i + 1)).sub (hfint i))).eventuallyEq

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
inst✝¹ : OrderBot ι
ℱ : Filtration ι m0
μ : Measure Ω
inst✝ : SigmaFiniteFiltration μ ℱ
f : Ω → E
hf : StronglyMeasurable f
hfint : Integrable f μ
⊢ Martingale (fun x ↦ f) ℱ μ

Tactic:
refine ⟨fun i => hf.mono <| ℱ.mono bot_le, fun i j _ => ?_⟩

Goal state after:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : OrderBot ι
ℱ : Filtration ι m0
μ : Measure Ω
inst✝ : SigmaFiniteFiltration μ ℱ
f : Ω → E
hf : StronglyMeasurable f
hfint : Integrable f μ
i j : ι
x✝ : i ≤ j
⊢ μ[(fun x ↦ f) j | ↑ℱ i] =ᵐ[μ] (fun x ↦ f) i
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
| ∀ (x : ι), x ∈ Set.Icc m m ∧ u x ω ∈ s → sInf (Set.Icc m m ∩ {i | u i ω ∈ s}) = m

Tactic:
intro; rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
x✝ : ι
| m ≤ x✝ → x✝ ≤ m → u x✝ ω ∈ s → sInf ({m} ∩ {i | u i ω ∈ s}) = m
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
⊢ Antitone fun x ↦ hittingBtwn u x n m

Tactic:
intro E F hEF ω

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
⊢ (fun x ↦ hittingBtwn u x n m) F ω ≤ (fun x ↦ hittingBtwn u x n m) E ω
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
⊢ Antitone fun x ↦ hittingAfter u x n

Tactic:
intro E F hEF ω

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
⊢ (fun x ↦ hittingAfter u x n) F ω ≤ (fun x ↦ hittingAfter u x n) E ω
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω ↦ if h : ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c) then h.choose else 0
⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω))

Tactic:
have hle : ⨆ n, ℱ n ≤ m0 := sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω ↦ if h : ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c) then h.choose else 0
hle : ⨆ n, ↑ℱ n ≤ m0
⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω))
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n ↦ μ[g | ↑ℱ n] x) atTop (𝓝 (g x))

Tactic:
have hle : ⨆ n, ℱ n ≤ m0 := sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n ↦ μ[g | ↑ℱ n] x) atTop (𝓝 (g x))
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n ↦ μ[g | ↑ℱ n] x) atTop (𝓝 (g x))

Tactic:
have hunif : UniformIntegrable (fun n => μ[g | ℱ n]) 1 μ :=
    hg.uniformIntegrable_condExp_filtration

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n ↦ μ[g | ↑ℱ n]) 1 μ
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n ↦ μ[g | ↑ℱ n] x) atTop (𝓝 (g x))
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:
rw [← Set.univ_inter {ω | τ ω = i}, measurableSet_inter_eq_iff, Set.univ_inter]

Goal state after:
Ω : 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}
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 τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet {ω | τ ω = ↑i}

Tactic:
rw [← Set.univ_inter {ω | τ ω = i}, measurableSet_inter_eq_iff, Set.univ_inter]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet {ω | τ ω = ↑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)⁺ ∂μ)
N : ℕ
⊢ ENNReal.ofReal (b - a) * ENNReal.ofReal (∫ (a_1 : Ω), ↑↑(upcrossingsBefore a b f N a_1) ∂μ) ≤
    ⨆ N, ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)

pp: case pos.hfi
Ω : 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 : ℕ
⊢ Integrable (fun x ↦ ↑↑(upcrossingsBefore a b f N x)) μ

Tactic:
← ENNReal.ofReal_mul (sub_pos.2 hab).le

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)⁺ ∂μ)
N : ℕ
⊢ ENNReal.ofReal ((b - a) * ∫ (a_1 : Ω), ↑↑(upcrossingsBefore a b f N a_1) ∂μ) ≤
    ⨆ N, ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)

case pos.hfi
Ω : 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 : ℕ
⊢ Integrable (fun x ↦ ↑↑(upcrossingsBefore a b f N x)) μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
inst✝ : MeasurableSingletonClass Ω
ω : Ω
⊢ mgf X (Measure.dirac ω) t = rexp (t * X ω)

Tactic:
by
  rw [mgf, integral_dirac]

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

Goal state before:
pp: case e_a.e_a.e_a
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ t * p * p⁻¹ = t

Tactic:
mul_assoc,

Goal state after:
case e_a.e_a.e_a
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ t * (p * p⁻¹) = t
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case e_a.e_a
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ t * p * p⁻¹ = t

Tactic:
mul_assoc,

Goal state after:
case e_a.e_a
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ t * (p * p⁻¹) = t
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case neg
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
calc |x| ^ p
  _ ≤ ((t / p)⁻¹ * max (exp (t / p * x)) (exp (-t / p * x))) ^ p := by
    gcongr
    convert! h_abs_le (t / p) (div_pos ht (hp.lt_of_ne' hp_zero)) using 5
    rw [neg_div]
  _ = (p / t) ^ p * max (exp (t * x)) (exp (-t * x)) := by
    rw [mul_rpow (by positivity) (by positivity)]
    congr
    · simp
    · rw [rpow_max (by positivity) (by positivity) hp, ← exp_mul, ← exp_mul]
      ring_nf
      congr <;> rw [mul_assoc, mul_inv_cancel₀ hp_zero, mul_one]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
⊢ AnalyticOnNhd ℝ (deriv^[n] (mgf X μ)) (interior (integrableExpSet X μ))

Tactic:
exact analyticOnNhd_mgf.iterated_deriv n

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ ∫ (x : ℝ), (↑√(2 * π * ↑v))⁻¹ * cexp (-(↑x - ↑μ) ^ 2 / (2 * ↑↑v)) * cexp (z * ↑x) =
    (↑√(2 * π * ↑v))⁻¹ * ∫ (x : ℝ), cexp (-(2 * ↑↑v)⁻¹ * ↑x ^ 2 + (z + ↑μ / ↑↑v) * ↑x + -↑μ ^ 2 / (2 * ↑↑v))

Tactic:
mul_assoc,

Goal state after:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ ∫ (x : ℝ), (↑√(2 * (π * ↑v)))⁻¹ * (cexp (-(↑x - ↑μ) ^ 2 / (2 * ↑↑v)) * cexp (z * ↑x)) =
    (↑√(2 * (π * ↑v)))⁻¹ * ∫ (x : ℝ), cexp (-(2 * ↑↑v)⁻¹ * ↑x ^ 2 + (z + ↑μ / ↑↑v) * ↑x + -↑μ ^ 2 / (2 * ↑↑v))
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ

Tactic:
mul_assoc,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ Integrable (fun ω ↦ 2 * (X ω * (deriv (cgf X μ) v * rexp (v * X ω)))) μ