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

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

Tactic:
simp_rw [measure_iUnion h (fun _ ↦ measurableSet_closedBall), tsum_fintype,
      B, μ.addHaar_closedBall_center, Finset.sum_const, Finset.card_univ, Fintype.card_Icc,
      Nat.card_Icc, tsub_zero]

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

Tactic:
← map_inf,

Goal state after:
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ n ((x ⇨ y) ⊓ x) = n (y ⊓ x)
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
⊢ ∀ i ≥ x ⊓ y, ∀ (b : X), (∀ x_1 ≥ x, b ⊓ m x_1 ≤ n x_1) → (∀ i ≥ y, b ⊓ m i ≤ n i) → b ≤ m i → b ≤ n i

Tactic:
intro k

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
⊢ k ≥ x ⊓ y → ∀ (b : X), (∀ x_1 ≥ x, b ⊓ m x_1 ≤ n x_1) → (∀ i ≥ y, b ⊓ m i ≤ n i) → b ≤ m k → b ≤ n k
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1
hly : ∀ i ≥ y, l ⊓ m i ≤ n i
hlk : l ≤ m k
⊢ l = l ⊓ (m (x ⊔ k) ⊓ m (y ⊔ k))

Tactic:
← map_inf,

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1
hly : ∀ i ≥ y, l ⊓ m i ≤ n i
hlk : l ≤ m k
⊢ l = l ⊓ m ((x ⊔ k) ⊓ (y ⊔ k))
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1
hly : ∀ i ≥ y, l ⊓ m i ≤ n i
hlk : l ≤ m k
⊢ n (x ⊔ k) ⊓ n (y ⊔ k) = n k

Tactic:
← map_inf,

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1
hly : ∀ i ≥ y, l ⊓ m i ≤ n i
hlk : l ≤ m k
⊢ n ((x ⊔ k) ⊓ (y ⊔ k)) = n k
Module: Mathlib.Order.Nucleus

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

Tactic:
← map_inf,

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
hy : y ≥ x
⊢ m ((m y ⇨ n y) ⊓ y) ⇨ n y = m y ⇨ n y
Module: Mathlib.Order.PrimeSeparator

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

Tactic:
exact ⟨J₁.isIdeal, le_trans IJ' le_sup_left, hdis⟩

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 β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b

Tactic:
rw [isSaddlePointOn_iff ha hb] at h

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ 1 * type α = type α

Tactic:
simp only [show 1 = type PUnit by rfl, ← type_lex_prod]

Goal state after:
o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ type (Lex (α × PUnit.{u + 1})) = type α
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ type α * 1 = type α

Tactic:
simp only [show 1 = type PUnit by rfl, ← type_lex_prod]

Goal state after:
o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ type (Lex (PUnit.{u + 1} × α)) = type α
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : UpperSet α
t : UpperSet β
⊢ s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤

Tactic:
by
  simp_rw [SetLike.ext'_iff]
  exact prod_eq_empty_iff

Goal state after:
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : LowerSet α
t : LowerSet β
⊢ s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥

Tactic:
by
  simp_rw [SetLike.ext'_iff]
  exact prod_eq_empty_iff

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝⁴ : TopologicalSpace β
u : ι → Ω → β
γ : Type u_4
inst✝³ : MeasurableSpace ι
inst✝² : PseudoMetrizableSpace β
fltr : Filter γ
inst✝¹ : fltr.NeBot
inst✝ : fltr.IsCountablyGenerated
U : γ → ι → Ω → β
h : ∀ (l : γ), IsStronglyProgressive f (U l)
h_tendsto : Tendsto U fltr (𝓝 u)
i : ι
⊢ Tendsto (fun l p ↦ U l (↑p.1) p.2) fltr (𝓝 fun p ↦ u (↑p.1) p.2)

Tactic:
tendsto_pi_nhds

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝⁴ : TopologicalSpace β
u : ι → Ω → β
γ : Type u_4
inst✝³ : MeasurableSpace ι
inst✝² : PseudoMetrizableSpace β
fltr : Filter γ
inst✝¹ : fltr.NeBot
inst✝ : fltr.IsCountablyGenerated
U : γ → ι → Ω → β
h : ∀ (l : γ), IsStronglyProgressive f (U l)
h_tendsto : ∀ (x : ι), Tendsto (fun i ↦ U i x) fltr (𝓝 (u x))
i : ι
⊢ ∀ (x : ↑(Set.Iic i) × Ω), Tendsto (fun i_1 ↦ U i_1 (↑x.1) x.2) fltr (𝓝 (u (↑x.1) x.2))
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✝¹ : 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])
⊢ ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0

Tactic:
intro k

Goal state after:
Ω : 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])
k : ℕ
⊢ i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
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✝¹ : 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
⊢ f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i]) =ᵐ[μ]
    martingalePart f ℱ μ i

Tactic:
have h_lt : ∀ k, k < i → μ[f (k + 1) - f k | ℱ i] - μ[μ[f (k + 1) - f k | ℱ k] | ℱ i] =ᵐ[μ]
      f (k + 1) - f k - μ[f (k + 1) - f k | ℱ k] := by
    refine fun k hk => EventuallyEq.sub ?_ ?_
    · rw [condExp_of_stronglyMeasurable]
      · exact ((hf (k + 1)).mono (ℱ.mono (Nat.succ_le_of_lt hk))).sub ((hf k).mono (ℱ.mono hk.le))
      · exact (hf_int _).sub (hf_int _)
    · rw [condExp_of_stronglyMeasurable]
      · exact stronglyMeasurable_condExp.mono (ℱ.mono hk.le)
      · exact integrable_condExp

Goal state after:
Ω : 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
h_lt :
  ∀ k < i,
    μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] f (k + 1) - f k - μ[f (k + 1) - f k | ↑ℱ k]
⊢ f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i]) =ᵐ[μ]
    martingalePart f ℱ μ i
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m_1 x ↦
    match x.1 with
    | 0 => (h₀.approx m_1) x.2
    | n.succ => (⋯.approx m_1) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
n : ℕ
ω : Ω
⊢ Tendsto (fun m ↦ X m (n, ω)) atTop (𝓝 (Function.uncurry u (n, ω)))

pp: case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m_1 x ↦
    match x.1 with
    | 0 => (h₀.approx m_1) x.2
    | n.succ => (⋯.approx m_1) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
n : ℕ
ω : Ω
⊢ (fun n_1 ↦ ((fun m_1 ↦ { toFun := Y m_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ }) n_1) (n, ω)) =ᶠ[atTop]
    fun m ↦ X m (n, ω)

Tactic:
· rcases n with rfl | n
      · exact h₀.tendsto_approx ω
      · exact (h n).tendsto_approx ω

Goal state after:
case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m_1 x ↦
    match x.1 with
    | 0 => (h₀.approx m_1) x.2
    | n.succ => (⋯.approx m_1) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
n : ℕ
ω : Ω
⊢ (fun n_1 ↦ ((fun m_1 ↦ { toFun := Y m_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ }) n_1) (n, ω)) =ᶠ[atTop]
    fun m ↦ X m (n, ω)
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLattice ι
u : ι → Ω → β
n : ι
ω : Ω
⊢ ↑(sInf {j | n ≤ j}) = ↑n

Tactic:
exact_mod_cast csInf_Ici

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
n i : ℕ
x✝ : i ∈ Finset.range N
hl : MeasurableSet {ω | lowerCrossingTime a b f N i ω ≤ n}
hu : MeasurableSet {ω | upperCrossingTime a b f N (i + 1) ω ≤ n}
⊢ MeasurableSet fun ω ↦ ({n | lowerCrossingTime a b f N i ω ≤ n} ∩ {n | ¬upperCrossingTime a b f N (i + 1) ω ≤ n}) n

Tactic:
exact hl.inter hu.compl

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✝⁴ : PartialOrder E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : ℕ → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted 𝒢 fun n ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ≤ μ[f (i + 1) - f i | ↑𝒢 i] ω
hω2 : μ[ξ i • (f (i + 1) - f i) | ↑𝒢 i] ω = ξ i ω • μ[f (i + 1) - f i | ↑𝒢 i] ω
⊢ 0 • 0 ≤ μ[ξ i • (f (i + 1) - f i) | ↑𝒢 i] ω

Tactic:
hnonneg i ω,

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : ℕ → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted 𝒢 fun n ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ≤ μ[f (i + 1) - f i | ↑𝒢 i] ω
hω2 : μ[ξ i • (f (i + 1) - f i) | ↑𝒢 i] ω = ξ i ω • μ[f (i + 1) - f i | ↑𝒢 i] ω
⊢ ξ i ω • 0 ≤ μ[ξ i • (f (i + 1) - f i) | ↑𝒢 i] ω

case hb
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : ℕ → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted 𝒢 fun n ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ≤ μ[f (i + 1) - f i | ↑𝒢 i] ω
hω2 : μ[ξ i • (f (i + 1) - f i) | ↑𝒢 i] ω = ξ i ω • μ[f (i + 1) - f i | ↑𝒢 i] ω
⊢ 0 ≤ 0
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b, a_1 ≤ b ∧ f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1, a ≤ b_1 ∧ b < f b_1 ω
⊢ ∀ (k : ℕ), ∃ N, k ≤ upcrossingsBefore a b f N ω

Tactic:
intro k

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b, a_1 ≤ b ∧ f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1, a ≤ b_1 ∧ b < f b_1 ω
k : ℕ
⊢ ∃ N, k ≤ upcrossingsBefore a b f N ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case neg
Ω : 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
h_exists_lt' : ∀ (u : WithTop ι), ↑t < u → ∃ i, ↑(s i) < u
h_eq_iInter : {ω | τ ω ≤ ↑t} = ⋂ m, {ω | τ ω < ↑(s m)}
h𝓕_eq_iInf : ↑f t = ⨅ m_1, ↑f (s m_1)
⊢ ∀ (a : ℕ), MeasurableSet (⋂ m, {ω | τ ω < ↑(s m)})

Tactic:
intro k

Goal state after:
case neg
Ω : 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
h_exists_lt' : ∀ (u : WithTop ι), ↑t < u → ∃ i, ↑(s i) < u
h_eq_iInter : {ω | τ ω ≤ ↑t} = ⋂ m, {ω | τ ω < ↑(s m)}
h𝓕_eq_iInf : ↑f t = ⨅ m_1, ↑f (s m_1)
k : ℕ
⊢ MeasurableSet (⋂ m, {ω | τ ω < ↑(s m)})
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
⊢ ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω

Tactic:
intro k

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k : ℕ
⊢ ∑ n ∈ Finset.range N,
      (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
        (fun m ↦ f (m + 1) ω - f m ω) n =
    stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
      stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
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
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 : g =ᵐ[μ] limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n ↦ μ[g | ↑ℱ n] x) atTop (𝓝 (g x))

Tactic:
by
    filter_upwards [this, (martingale_condExp g ℱ μ).submartingale.ae_tendsto_limitProcess hR] with
      x heq ht
    rwa [heq]

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

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

Tactic:
have ht : ∀ᵐ x ∂μ, Tendsto (fun n => (μ[μ[g | ⨆ n, ℱ n] | ℱ n]) x)
      atTop (𝓝 ((μ[g | ⨆ n, ℱ n]) x)) :=
    integrable_condExp.tendsto_ae_condExp stronglyMeasurable_condExp
  have heq : ∀ n, ∀ᵐ x ∂μ, (μ[μ[g | ⨆ n, ℱ n] | ℱ n]) x = (μ[g | ℱ n]) x := fun n =>
    condExp_condExp_of_le (le_iSup _ n) (iSup_le fun n => ℱ.le n)
  rw [← ae_all_iff] at heq
  filter_upwards [heq, ht] with x hxeq hxt
  exact hxt.congr hxeq

Goal state after:
Module: Mathlib.Probability.ConditionalExpectation

Goal state before:
pp: case pos.refine_5
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
u v : Ω → E
⊢ u =ᵐ[μ] v →
    MemLp u 1 μ →
      μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ → μ.real s • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ

Tactic:
huv

Goal state after:
case pos.refine_5
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
u v : Ω → E
huv : u =ᵐ[μ] v
⊢ MemLp u 1 μ →
    μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ → μ.real s • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), ‖f (n + 1) ω - f n ω‖ ≤ ↑R
h₀ : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop atTop ↔ Tendsto (fun n ↦ predictablePart f ℱ μ n ω) atTop atTop

Tactic:
have h₂ := (martingale_martingalePart hf hint).ae_not_tendsto_atTop_atBot h₀

Goal state after:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), ‖f (n + 1) ω - f n ω‖ ≤ ↑R
h₀ : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop atTop ↔ Tendsto (fun n ↦ predictablePart f ℱ μ n ω) atTop atTop
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
ht_nonneg : 0 ≤ t
⊢ Integrable (fun ω ↦ rexp (|t| * |X ω|)) μ

Tactic:
simp_rw [abs_of_nonneg ht_nonneg]
    exact integrable_exp_mul_abs ht_int_pos ht_int_neg

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

Goal state before:
pp: l u v : ℝ
hv : v ∈ Set.Ioo l u
⊢ v - min (v - l) (u - v) / 2 ∈ Set.Ioo l u

Tactic:
have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hv.1, hv.2]
  constructor
  · calc l = v - (v - l) := by abel
    _ ≤ v - ((v - l) ⊓ (u - v)) := by gcongr; exact inf_le_left
    _ < v - ((v - l) ⊓ (u - v)) / 2 := by gcongr; exact half_lt_self (by positivity)
  · calc v - ((v - l) ⊓ (u - v)) / 2
    _ ≤ v := by
      rw [sub_le_iff_le_add]
      exact le_add_of_nonneg_right (by positivity)
    _ < u := hv.2

Goal state after: