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

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : orderOf a ^ 2 ∣ n
⊢ ⋃ i ∈ {y | orderOf y = n}, ball (a • i) δ = ⋃ x ∈ {y | orderOf y = n}, ball x δ

Tactic:
smul_eq_mul,

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : orderOf a ^ 2 ∣ n
⊢ ⋃ i ∈ {y | orderOf y = n}, ball (a * i) δ = ⋃ x ∈ {y | orderOf y = n}, ball x δ
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : ↑{b | orderOf b = n} → ↑{b | orderOf b = n} := fun b ↦ ⟨a * ↑b, ⋯⟩
b : A
hb : b ∈ {b | orderOf b = n}
⊢ f ⟨a⁻¹ * b, ⋯⟩ = ⟨b, hb⟩

Tactic:
simp only [f, mul_inv_cancel_left]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: 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)
⊢ (∀ᵐ (x : 𝕊) ∂μ, x ∉ addWellApproximable 𝕊 δ) ∨ ∀ᵐ (x : 𝕊) ∂μ, x ∈ addWellApproximable 𝕊 δ

Tactic:
have hu₀ : ∀ p : Nat.Primes, addOrderOf (u p) = (p : ℕ) := by
    rintro ⟨p, hp⟩; exact addOrderOf_div_of_gcd_eq_one hp.pos (gcd_one_left p)

Goal state after:
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
⊢ (∀ᵐ (x : 𝕊) ∂μ, x ∉ addWellApproximable 𝕊 δ) ∨ ∀ᵐ (x : 𝕊) ∂μ, x ∈ addWellApproximable 𝕊 δ
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
ha : a ∈ upperBounds s
b : α
t : Set α
hts : t ⊆ s
ht_ne : t.Nonempty
ht_c : t.Countable
ht_lub : IsLUB t b
hat : a ∈ upperBounds t
⊢ b ≤ a

Tactic:
exact (isLUB_le_iff ht_lub).mpr hat

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
a✝ : α
inst✝ : CompleteLattice α
h_csc : CountableSupClosed {a | ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨆ n, t n = a}
a : α
ha : a ∈ s
⊢ (∀ (n : ℕ), (fun x ↦ a) n ∈ s) ∧ ⨆ n, (fun x ↦ a) n = a

Tactic:
simp [ha]

Goal state after:
Module: Mathlib.Order.Extension.Linear

Goal state before:
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 (h.2 (_root_.trans yb bx)).elim

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

Goal state before:
pp: α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂, f.preimage s ∈ l₁) → ∀ s ∈ l₂, f.core s ∈ l₁

Tactic:
exact fun h s sl₂ => mem_of_superset (h s sl₂) (PFun.preimage_subset_core _ _)

Goal state after:
Module: Mathlib.Order.Interval.Set.SurjOn

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a < b
⊢ SurjOn f (Ico a b) (Ico (f a) (f b))

Tactic:
intro p hp
    rcases eq_left_or_mem_Ioo_of_mem_Ico hp with (rfl | hp')
    · exact mem_image_of_mem f (left_mem_Ico.mpr hab)
    · exact image_mono Ioo_subset_Ico_self <|
        surjOn_Ioo_of_monotone_surjective h_mono h_surj a b hp'

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : CompleteLattice X
x✝ : Set (Nucleus X)
⊢ sInf x✝ ∈ upperBounds (lowerBounds x✝)

Tactic:
simp +contextual [mem_lowerBounds, mem_upperBounds, ← coe_le_coe, Pi.le_def]

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : I.IsPrime
J : Ideal P
⊢ I < J → ∀ (x : P), x ∈ ↑J

Tactic:
hIJ

Goal state after:
P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : I.IsPrime
J : Ideal P
hIJ : I < J
⊢ ∀ (x : P), x ∈ ↑J
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ R.leftDual (R.rightDual (R.leftDual J)) ⊆ R.leftDual J

Tactic:
apply R.gc_leftDual_rightDual.monotone_l; exact R.gc_leftDual_rightDual.le_u_l J

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

Goal state before:
pp: case inl
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun f
ha : a ∈ u
⊢ P.Rel a (f a)

Tactic:
exact hf.rel_apply ha

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

Goal state before:
pp: case inr
α : Type u_1
u : Set α
P : Partition u
f g : α → α
hf : P.IsRepFun f
hg : P.IsRepFun g
x : α
hx : x ∉ u
⊢ f x = f x

Tactic:
hf.apply_of_notMem hx

Goal state after:
case inr
α : Type u_1
u : Set α
P : Partition u
f g : α → α
hf : P.IsRepFun f
hg : P.IsRepFun g
x : α
hx : x ∉ u
⊢ x = x
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case refine_2
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a b : α
hab : P.Rel a b
⊢ (if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯) =
    if ha : b ∈ u then if hb : ∃ b_1, P.Rel b ↑b_1 then f₀ hb.choose else P.rep ⋯ else b

Tactic:
dif_pos hab.right_mem

Goal state after:
case refine_2
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a b : α
hab : P.Rel a b
⊢ (if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯) = if hb : ∃ b_1, P.Rel b ↑b_1 then f₀ hb.choose else P.rep ⋯
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
⊢ MeasurableSet (Prod.mk ⟨n + 1, ⋯⟩ ⁻¹' (fun p ↦ (↑p.1, p.2)) ⁻¹' s)

Tactic:
refine measurableSet_preimage (mβ := Subtype.instMeasurableSpace.prod (𝓕 n))
    measurable_prodMk_left <| measurableSet_preimage ?_ hs

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
⊢ Measurable fun p ↦ (↑p.1, p.2)
Module: Mathlib.Probability.Process.HittingTime

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

Tactic:
if_pos ⟨n, le_rfl⟩

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLattice ι
u : ι → Ω → β
n : ι
ω : Ω
⊢ ↑(sInf {j | n ≤ j}) = ↑n
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : 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 + 1) ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ
⊢ Supermartingale f 𝒢 μ

Tactic:
rw [← neg_neg f]
  refine (submartingale_of_setIntegral_le_succ hadp.neg (fun i => (hint i).neg) ?_).neg
  simpa only [integral_neg, Pi.neg_apply, neg_le_neg_iff]

Goal state after:
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
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
hhpred : StronglyAdapted ℱ fun n ↦ h (n + 1)
this : IsStronglyPredictable ℱ g
⊢ martingalePart (f + g) ℱ μ n =ᵐ[μ] f n

Tactic:
have hhmgle : Martingale h ℱ μ := hf.sub (martingale_martingalePart
    (hf.stronglyAdapted.add this.stronglyAdapted) fun n => (hf.integrable n).add <| hgint n)

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✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
hhpred : StronglyAdapted ℱ fun n ↦ h (n + 1)
this : IsStronglyPredictable ℱ g
hhmgle : Martingale h ℱ μ
⊢ martingalePart (f + g) ℱ μ n =ᵐ[μ] f n
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
hmn : m ≤ n
h : m < n
⊢ hittingBtwn u s n m ω = m

Tactic:
exact hittingBtwn_of_lt h

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

Goal state before:
pp: case succ
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
ω : Ω
n✝ : ℕ
⊢ upperCrossingTime a b f N (n✝ + 1) ω ≤ N

Tactic:
· simp only [upperCrossingTime_succ, hittingBtwn_le]

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
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ sInf (Set.Icc n' m ∩ {i | u i ω ∈ s})

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

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

pp: case neg
Ω : 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 ≤ m

Tactic:
· gcongr
    exacts [⟨n, by simp [mem_lowerBounds]; grind⟩]

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

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

case neg
Ω : 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 ≤ m
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 β
n m : ι
hnm : n ≤ m
ω : Ω
h_n : ¬∃ j, n ≤ j ∧ u j ω ∈ s
h_m : ∃ j, m ≤ j ∧ u j ω ∈ s
⊢ ⊤ ≤ ↑(sInf {j | m ≤ j ∧ u j ω ∈ s})

pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h_n : ¬∃ j, n ≤ j ∧ u j ω ∈ s
h_m : ¬∃ j, m ≤ j ∧ u j ω ∈ s
⊢ ⊤ ≤ ⊤

Tactic:
· have ⟨t, ht⟩ := h_m
    exact absurd ⟨t, hnm.trans ht.1, ht.2⟩ h_n

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h_n : ¬∃ j, n ≤ j ∧ u j ω ∈ s
h_m : ¬∃ j, m ≤ j ∧ u j ω ∈ s
⊢ ⊤ ≤ ⊤
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (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 ω)) ω
i : ℕ
x✝ : i ∈ Finset.range N
hi : i ∉ Finset.range (upcrossingsBefore a b f N ω)
hi' : ¬i = upcrossingsBefore a b f N ω
⊢ 0 ≤
    stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (i + 1) ω)) ω -
      stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N i ω)) ω

Tactic:
· rw [sub_eq_zero_of_upcrossingsBefore_lt hab]
          rw [Finset.mem_range, not_lt] at hi
          exact lt_of_le_of_ne hi (Ne.symm hi')

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})
i : ι
⊢ MeasurableSet ((sᶜ ∪ {ω | τ ω ≤ ↑i}ᶜ) ∩ {ω | τ ω ≤ ↑i})

Tactic:
refine MeasurableSet.inter ?_ ?_
      · rw [← Set.compl_inter]
        exact (hs.2 i).compl
      · exact hτ i

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

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

Tactic:
· refine ⟨le_iSup f i s h, fun j ↦ ?_⟩
    by_cases hij : i ≤ j
    · norm_cast
      simp only [hij, Set.ofPred_true, Set.inter_univ]
      exact f.mono hij _ h
    · norm_cast
      simp only [hij, Set.ofPred_false, Set.inter_empty, @MeasurableSet.empty _ (f.1 j)]

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

Goal state before:
pp: case hf
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
⊢ Integrable (stoppedValue f π) μ

Tactic:
exact hf.integrable_stoppedValue hπ hbdd

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

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

Tactic:
smul_eq_mul,

Goal state after:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ : ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1
h₂ :
  ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 0
⊢ upcrossingsBefore a b f N ω =
    (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card * 1 +
      (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card • 0
Module: Mathlib.Probability.Martingale.Upcrossing

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

Tactic:
smul_eq_mul,

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

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

Tactic:
by_cases hN : N = 0
  · simp [hN]
  rw [← Finset.sum_Ico_consecutive _ (Nat.succ_le_succ zero_le)
    (Nat.succ_le_succ (upcrossingsBefore_le f ω hab))]
  have h₁ : ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
      {n : ℕ | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1 := by
    rintro k hk
    rw [Finset.mem_Ico] at hk
    rw [Set.indicator_of_mem]
    · rfl
    · exact upperCrossingTime_lt_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab
        (Nat.lt_succ_iff.1 hk.2)
  have h₂ : ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
      {n : ℕ | upperCrossingTime a b f N n ω < N}.indicator 1 k = 0 := by
    rintro k hk
    rw [Finset.mem_Ico, Nat.succ_le_iff] at hk
    rw [Set.indicator_of_notMem]
    simp only [Set.mem_ofPred_eq, not_lt]
    exact (upperCrossingTime_eq_of_upcrossingsBefore_lt hab hk.1).symm.le
  rw [Finset.sum_congr rfl h₁, Finset.sum_congr rfl h₂, Finset.sum_const, Finset.sum_const,
    smul_eq_mul, mul_one, smul_eq_mul, mul_zero, Nat.card_Ico, Nat.add_succ_sub_one,
    add_zero, add_zero]

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
h : ↑i ≤ τ ω
⊢ stoppedProcess u τ i ω = u i ω

Tactic:
by simp [stoppedProcess, min_eq_left h]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
hX : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ rexp (cgf X μ t) = mgf X μ t

Tactic:
rw [cgf, exp_log (mgf_pos' hμ.out hX)]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ ∫ (x : Ω), rexp (t * α • X x) ∂μ = ∫ (x : Ω), rexp (α * t * X x) ∂μ

Tactic:
smul_eq_mul,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ ∫ (x : Ω), rexp (t * (α * X x)) ∂μ = ∫ (x : Ω), rexp (α * t * X x) ∂μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_1
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ t₁ ≤ a • t₁ + b • t₂

Tactic:
simp only [smul_eq_mul]

Goal state after:
case refine_1
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ t₁ ≤ a * t₁ + b * t₂
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a • t₁ + b • t₂ ≤ t₂

Tactic:
simp only [smul_eq_mul]

Goal state after:
case refine_2
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a * t₁ + b * t₂ ≤ t₂
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
inst✝ : MeasurableSpace E
μ : Measure E
h : Integrable id μ
L : E →L[𝕜] F
⊢ ∫ (x : E), L x ∂μ = L (∫ (x : E), id x ∂μ)

Tactic:
change ∫ x, L (id x) ∂μ = _

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
inst✝ : MeasurableSpace E
μ : Measure E
h : Integrable id μ
L : E →L[𝕜] F
⊢ ∫ (x : E), L (id x) ∂μ = L (∫ (x : E), id x ∂μ)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
f : Ω → E
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
inst✝¹ : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
⊢ μ[f | hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = ↑i}] μ[f | ↑ℱ i]

Tactic:
refine condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le (ℱ.le i)
    (hτ.measurableSet_eq' i) fun t => ?_

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
f : Ω → E
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
inst✝¹ : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
t : Set Ω
⊢ MeasurableSet ({x | τ x = ↑i} ∩ t) ↔ MeasurableSet ({x | τ x = ↑i} ∩ t)
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ deriv (cgf X μ) v = (∫ (x : Ω), (fun ω ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v

Tactic:
have hv : Integrable (fun ω ↦ exp (v * X ω)) μ := interior_subset (s := integrableExpSet X μ) h

Goal state after:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
hv : Integrable (fun ω ↦ rexp (v * X ω)) μ
⊢ deriv (cgf X μ) v = (∫ (x : Ω), (fun ω ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v