mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case e_p
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
p : ℕ
⊢ (fun n ↦ 0 < n) = fun x ↦ 0 < x ∧ ((¬p ∣ x ∨ p ∣ x ∧ ¬p * p ∣ x) ∨ p * p ∣ x)

Tactic:
ext n

Goal state after:
case e_p
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := ⋯
μ : Measure 𝕊 := ⋯
u : Nat.Primes → 𝕊 := ⋯
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := ⋯
X : ℕ → Set 𝕊 := ⋯
A : ℕ → Set 𝕊 := ⋯
B : ℕ → Set 𝕊 := ⋯
C : ℕ → Set 𝕊 := ⋯
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
p n : ℕ
⊢ 0 < n ↔ 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
Module: Mathlib.Order.Concept

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ (⨆ i, f i).extent = lowerPolar r (⋂ i, (f i).intent)

Tactic:
by
  simp_rw [iSup, extent_sSup, ← Set.iInf_eq_iInter, iInf_range]

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
s : Set α
y✝ y : α
x✝ : s.Countable
hy : IsLUB s y✝
hs_subset : ∀ y_1 ∈ s, y_1 = y
z : α
hzs : z ∈ s
⊢ y ∈ s

Tactic:
rwa [hs_subset z hzs] at hzs

Goal state after:
Module: Mathlib.Order.Filter.Cocardinal

Goal state before:
pp: α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
S : Set (Set α)
hS : #↑S < c
hSs : ∀ s ∈ S, s ∈ cocardinal α hreg
⊢ #↑(⋃₀ (compl '' S)) < c

Tactic:
mk_sUnion_le

Goal state after:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
S : Set (Set α)
hS : #↑S < c
hSs : ∀ s ∈ S, s ∈ cocardinal α hreg
⊢ #↑(compl '' S) * ⨆ s, #↑↑s < c
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
⊢ (univ.chainHeight fun x1 x2 ↦ r ↑x1 ↑x2) = s.chainHeight r

Tactic:
by
  have hc := Set.chainHeight_eq_of_relEmbedding univ <| Subtype.relEmbedding (r · ·) (· ∈ s)
  have hs : Subtype.val ⁻¹'o (r · ·) = (fun x y : s ↦ r x y) := by funext; simp
  simpa [hs] using hc.symm

Goal state after:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ y✝ z✝ : α
h1 : r w x✝
h2 : r y✝ z✝
compatible_left_sup : ∀ {x y t : α}, r x y → r (x ⊔ t) (y ⊔ t)
⊢ r (w ⊔ y✝) (x✝ ⊔ z✝)

Tactic:
exact transitive h₂ h₃ h₄ (by
      simpa [sup_comm w] using compatible_left_sup h2)
      (compatible_left_sup h1)

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f x y

Tactic:
exact iInf₂_le_of_le x hx (le_iSup₂_of_le y hy (le_refl _))

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet (Set.Ioc n (n + 1) ×ˢ s)

pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ {n + 1} = Set.Ioc n (n + 1)

Tactic:
· exact measurableSet_predictable_Ioc_prod _ _ hs

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ {n + 1} = Set.Ioc n (n + 1)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
p : ↑(Set.singleton (n + 1)) × Ω
⊢ ↑p.1 = 0 → p.2 ∉ A

Tactic:
exact fun hp1 ↦ False.elim <| Nat.succ_ne_zero n (hp1 ▸ p.1.2.symm)

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this✝ : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
this : MeasurableSpace Ω := ↑𝓕 n
⊢ StronglyMeasurable (u (n + 1))

Tactic:
let X m := (Function.curry (h𝓕.approx m) (n + 1))

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this✝ : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
this : MeasurableSpace Ω := ↑𝓕 n
X : ℕ → Ω → E := fun m_1 ↦ Function.curry (⇑(StronglyMeasurable.approx h𝓕 m_1)) (n + 1)
⊢ StronglyMeasurable (u (n + 1))
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: case refine_1
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁸ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
ℱ : Filtration ι m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : Lattice E
inst✝³ : ContinuousSup E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f g : ι → Ω → E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ f i ≤ᵐ[μ] μ[(f ⊔ g) j | ↑ℱ i]

Tactic:
exact EventuallyLE.trans (hf.2.1 i j hij)
      (condExp_mono (hf.integrable _) (Integrable.sup (hf.integrable j) (hg.integrable j))
        (Eventually.of_forall fun x => le_sup_left))

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

Goal state before:
pp: case refine_1
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
k : ℕ
hk : k < i
⊢ μ[f (k + 1) - f k | ↑ℱ i] =ᵐ[μ] f (k + 1) - f k

Tactic:
condExp_of_stronglyMeasurable

Goal state after:
case refine_1
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
k : ℕ
hk : k < i
⊢ f (k + 1) - f k =ᵐ[μ] f (k + 1) - f k

case refine_1.hf
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
k : ℕ
hk : k < i
⊢ StronglyMeasurable (f (k + 1) - f k)

case refine_1.hfi
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
k : ℕ
hk : k < i
⊢ Integrable (f (k + 1) - f k) μ
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: case refine_2
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
k : ℕ
hk : k < i
⊢ μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] μ[f (k + 1) - f k | ↑ℱ k]

Tactic:
condExp_of_stronglyMeasurable

Goal state after:
case refine_2
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
k : ℕ
hk : k < i
⊢ μ[f (k + 1) - f k | ↑ℱ k] =ᵐ[μ] μ[f (k + 1) - f k | ↑ℱ k]

case refine_2.hf
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
k : ℕ
hk : k < i
⊢ StronglyMeasurable μ[f (k + 1) - f k | ↑ℱ k]

case refine_2.hfi
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
k : ℕ
hk : k < i
⊢ Integrable μ[f (k + 1) - f k | ↑ℱ k] μ
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✝¹ : Preorder E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Submartingale f 𝒢 μ
hfadp : StronglyAdapted 𝒢 fun n ↦ f (n + 1)
n : ℕ
⊢ f 0 ≤ᵐ[μ] f n

Tactic:
induction n with

Goal state after:
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✝¹ : Preorder E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Supermartingale f 𝒢 μ
hfadp : StronglyAdapted 𝒢 fun n ↦ f (n + 1)
n : ℕ
⊢ f n ≤ᵐ[μ] f 0

Tactic:
induction n with

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

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

Tactic:
induction n with

Goal state after:
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✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Martingale f 𝒢 μ
hfadp : StronglyAdapted 𝒢 fun n ↦ f (n + 1)
n : ℕ
⊢ f n =ᵐ[μ] f 0

Tactic:
induction n with

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : lowerCrossingTime a b f N n ω < N
h' : upperCrossingTime a b f N n ω < N
⊢ upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω ∧
    lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω

Tactic:
induction n with

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι), t < u → ∃ i, s i < u
u : WithTop ι
hu : ↑t < u
⊢ ∀ᶠ (x : ℕ) in atTop, ↑(s x) < u

Tactic:
have hs_tendsto' : Tendsto (fun n ↦ (s n : WithTop ι)) atTop (𝓝 (t : WithTop ι)) :=
      WithTop.continuous_coe.continuousAt.tendsto.comp hs_tendsto

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι), t < u → ∃ i, s i < u
u : WithTop ι
hu : ↑t < u
hs_tendsto' : Tendsto (fun n ↦ ↑(s n)) atTop (𝓝 ↑t)
⊢ ∀ᶠ (x : ℕ) in atTop, ↑(s x) < u
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
⊢ IsStoppingTime f τ

Tactic:
intro t
  by_cases ht : 𝓝[>] t = ⊥
  · have h_eq : {ω | τ ω ≤ t} = {ω | τ ω < t} ∪ {ω | τ ω = t} := by ext; grind
    rw [h_eq]
    exact (hτ1 t).union (hτ2 t ht)
  have : (𝓝[>] t).NeBot := ⟨ht⟩
  -- now `t` is a limit point on the right
  obtain ⟨s, hs_gt, hs_tendsto⟩ : ∃ s : ℕ → ι, (∀ n, t < s n) ∧ Tendsto s atTop (𝓝 t) := by
    have h_freq : ∃ᶠ x in 𝓝[>] t, t < x :=
      Eventually.frequently <| eventually_nhdsWithin_of_forall fun _ hx ↦ hx
    have := exists_seq_forall_of_frequently h_freq
    simp_rw [tendsto_nhdsWithin_iff] at this
    obtain ⟨s, ⟨hs_tendsto, _⟩, hs_gt⟩ := this
    exact ⟨s, hs_gt, hs_tendsto⟩
  have h_exists_lt (u : ι) (hu : t < u) : ∃ i, s i < u :=
    Eventually.exists (f := atTop) (hs_tendsto.eventually_lt_const hu)
  have h_exists_lt' (u : WithTop ι) (hu : t < u) : ∃ i, s i < u := by
    refine Eventually.exists (f := atTop) ?_
    have hs_tendsto' : Tendsto (fun n ↦ (s n : WithTop ι)) atTop (𝓝 (t : WithTop ι)) :=
      WithTop.continuous_coe.continuousAt.tendsto.comp hs_tendsto
    exact hs_tendsto'.eventually_lt_const hu
  -- we write `{τ ≤ t}` as a countable intersection of `{τ < s n}`
  have h_eq_iInter : {ω | τ ω ≤ t} = ⋂ m, {ω | τ ω < s m} := by
    ext ω
    simp only [Set.mem_ofPred_eq, Set.mem_iInter]
    refine ⟨fun h_le m ↦ h_le.trans_lt (mod_cast (hs_gt m)), fun h_lt ↦ ?_⟩
    refine le_of_forall_gt fun u hu ↦ ?_
    obtain ⟨i, hi⟩ : ∃ i, s i < u := h_exists_lt' u hu
    exact (h_lt i).trans hi
  rw [h_eq_iInter]
  have h𝓕_eq_iInf : f t = ⨅ m, f (s m) := by
    nth_rw 1 [← hf.eq, Filtration.rightCont_eq_of_neBot_nhdsGT]
    refine le_antisymm ?_ ?_
    · simp only [gt_iff_lt, le_iInf_iff]
      exact fun i ↦ iInf₂_le (s i) (hs_gt i)
    · simp only [gt_iff_lt, le_iInf_iff]
      intro i hti
      obtain ⟨m, hm⟩ := h_exists_lt i hti
      exact (iInf_le _ m).trans (f.mono hm.le)
  rw [h𝓕_eq_iInf]
  simp only [MeasurableSpace.measurableSet_sInf, Set.mem_range, forall_exists_index,
    forall_apply_eq_imp_iff]
  intro k
  have h_eq_k : ⋂ m, {ω | τ ω < s m} = ⋂ (m) (hm : s m ≤ s k), {ω | τ ω < s m} := by
    ext x
    simp only [Set.mem_iInter, Set.mem_ofPred_eq]
    refine ⟨fun h m _ ↦ h m, fun h m ↦ ?_⟩
    rcases le_total (s m) (s k) with hmk | hkm
    · exact h m hmk
    · exact (h k le_rfl).trans_le (mod_cast hkm)
  rw [h_eq_k]
  exact MeasurableSet.iInter fun m ↦ MeasurableSet.iInter fun hm ↦ f.mono hm _ (hτ1 (s m))

Goal state after:
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 ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
⊢ upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N n = upperCrossingTime a b f N n ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N n = lowerCrossingTime a b f N n

Tactic:
induction n with

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

Goal state before:
pp: case compl
Ω : 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 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n ↦ μ[g | ↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
s : Set Ω
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
t : Set Ω
htmeas : MeasurableSet t
ht : μ t < ∞ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
x✝ : μ tᶜ < ∞
hgeq : ∫ (x : Ω) in tᶜ, g x ∂μ.trim hle = ∫ (x : Ω), g x ∂μ.trim hle - ∫ (x : Ω) in t, g x ∂μ.trim hle
hheq :
  ∫ (x : Ω) in tᶜ, limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle =
    ∫ (x : Ω), limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle -
      ∫ (x : Ω) in t, limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle
⊢ ∫ (x : Ω), g x ∂μ.trim hle - ∫ (x : Ω) in t, g x ∂μ =
    ∫ (x : Ω), limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle -
      ∫ (x : Ω) in t, limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle

Tactic:
←
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas,

Goal state after:
case compl
Ω : 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 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n ↦ μ[g | ↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
s : Set Ω
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
t : Set Ω
htmeas : MeasurableSet t
ht : μ t < ∞ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
x✝ : μ tᶜ < ∞
hgeq : ∫ (x : Ω) in tᶜ, g x ∂μ.trim hle = ∫ (x : Ω), g x ∂μ.trim hle - ∫ (x : Ω) in t, g x ∂μ.trim hle
hheq :
  ∫ (x : Ω) in tᶜ, limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle =
    ∫ (x : Ω), limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle -
      ∫ (x : Ω) in t, limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle
⊢ ∫ (x : Ω), g x ∂μ.trim hle - ∫ (x : Ω) in t, g x ∂μ =
    ∫ (x : Ω), limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ.trim hle -
      ∫ (x : Ω) in t, limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ x ∂μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

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

Tactic:
calc exp (t * X ω)
      _ ≤ exp (b * X ω) := exp_le_exp.mpr (mul_le_mul_of_nonneg_right htb h)
      _ ≤ exp (a * X ω) + exp (b * X ω) := le_add_of_nonneg_left (exp_nonneg _)

Goal state after:
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 ω)) μ
this : IsProbabilityMeasure μ
j : ι
hj : j ∈ s
⊢ mgf (X j) μ t ≠ 0

Tactic:
exact (mgf_pos (h_int j hj)).ne'

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

Goal state before:
pp: Ω : 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
⊢ Integrable (fun a ↦ |X a| ^ p * rexp (v * X a + x * |X a|)) μ

Tactic:
have ht : t ≠ 0 := by
    suffices |t| ≠ 0 by simpa
    exact (h_nonneg.trans_lt hx).ne'

Goal state after:
Ω : 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
⊢ Integrable (fun a ↦ |X a| ^ p * rexp (v * X a + x * |X a|)) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
n : ℕ
⊢ Integrable (fun ω ↦ |X ω| ^ n) μ

Tactic:
convert!
    integrable_rpow_abs_of_integrable_exp_mul ht ht_int_pos ht_int_neg
      (by positivity : 0 ≤ (n : ℝ)) with
    ω
  simp

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp id p (gaussianReal μ v)

Tactic:
lift p to ℝ≥0 using hp
  exact memLp_id_gaussianReal p

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ Measure.map (⇑L) (gaussianReal μ v) = gaussianReal (L μ) ((L 1 ^ 2).toNNReal * v)

Tactic:
by
  have : (L : ℝ → ℝ) = fun x ↦ L 1 * x := by simp
  rw [this, gaussianReal_map_const_mul]
  congr
  simp only [mul_one, left_eq_sup]
  positivity

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
μ : Measure E
inst✝ : CompleteSpace E
hμ : MemLp id 2 μ
x y : E
⊢ ⟪(covarianceOperator μ) x, y⟫ = ∫ (z : E), ⟪x, z⟫ * ⟪y, z⟫ ∂μ

Tactic:
by
  simp [covarianceOperator, uncenteredCovarianceBilinDual_apply hμ]

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ x - c) μ)

Tactic:
simp_rw [sub_eq_add_neg]; infer_instance

Goal state after: