mathlib-initiative/mathlib-tactics huggingface dataset:
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 τ
i : ι
⊢ MeasurableSet {ω | ↑i < τ ω}

Tactic:
have : {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ := by
    ext1 ω; simp only [Set.mem_ofPred_eq, Set.mem_compl_iff, not_le]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | ↑i < τ ω} = {ω | τ ω ≤ ↑i}ᶜ
⊢ MeasurableSet {ω | ↑i < τ ω}
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case h.inl
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝¹ : i ∈ ↑(Finset.range N)
j : ℕ
a✝ : j ∈ ↑(Finset.range N)
hij : i ≠ j
hij' : i < j
⊢ min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
    max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)

Tactic:
rw [min_eq_left (upperCrossingTime_mono (Nat.succ_le_succ hij'.le) :
      upperCrossingTime a b f N _ ω ≤ upperCrossingTime a b f N _ ω),
      max_eq_right (lowerCrossingTime_mono hij'.le :
        lowerCrossingTime a b f N _ _ ≤ lowerCrossingTime _ _ _ _ _ _)]
    refine le_trans upperCrossingTime_le_lowerCrossingTime
      (lowerCrossingTime_mono (Nat.succ_le_of_lt hij'))

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

Goal state before:
pp: case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : ∃ b ∈ Set.Icc n m ∩ {i | u i ω ∈ s}, b < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
simp only [Set.mem_inter_iff, Set.mem_Icc, Set.mem_ofPred_eq] at h'

Goal state after:
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
h' : ∃ b, ((n ≤ b ∧ b ≤ m) ∧ u b ω ∈ s) ∧ b < i
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ

Tactic:
have h₁ : (0 : ℝ) ≤
      μ[∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)] := by
    have := (hf.sum_sub_upcrossingStrat_mul a b N).setIntegral_le (zero_le (a := n)) .univ
    rw [setIntegral_univ, setIntegral_univ] at this
    refine le_trans ?_ this
    simp only [Finset.range_zero, Finset.sum_empty, integral_zero', le_refl]

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ : 0 ≤ ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}
i : ι
h_eq_iUnion : {ω | τ ω ≤ ↑i} = ⋃ k, ⋃ (_ : k ≤ i), {ω | τ ω = ↑k}
⊢ MeasurableSet (⋃ k, ⋃ (_ : k ≤ i), {ω | τ ω = ↑k})

Tactic:
refine MeasurableSet.biUnion (Set.to_countable _) fun k hk => ?_

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}
i : ι
h_eq_iUnion : {ω | τ ω ≤ ↑i} = ⋃ k, ⋃ (_ : k ≤ i), {ω | τ ω = ↑k}
k : ι
hk : k ∈ fun k ↦ inst✝¹.toLE.1 k i
⊢ MeasurableSet {ω | τ ω = ↑k}
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
h' : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s
⊢ hittingBtwn u s n m₁ ω = hittingBtwn u s n m₂ ω

Tactic:
simp only [hittingBtwn, if_pos h']
  obtain ⟨j, hj₁, hj₂⟩ := h'
  rw [if_pos]
  · refine le_antisymm ?_ (by gcongr; exacts [bddBelow_Icc.inter_of_left, ⟨j, hj₁, hj₂⟩])
    refine le_csInf ⟨j, Set.Icc_subset_Icc_right h hj₁, hj₂⟩ fun i hi => ?_
    by_cases hi' : i ≤ m₁
    · exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hi.1.1, hi'⟩, hi.2⟩
    · change j ∈ {i | u i ω ∈ s} at hj₂
      exact ((csInf_le bddBelow_Icc.inter_of_left ⟨hj₁, hj₂⟩).trans hj₁.2).trans (le_of_not_ge hi')
  exact ⟨j, ⟨hj₁.1, hj₁.2.trans h⟩, hj₂⟩

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 : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b

pp: case hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ N ≤ N

Tactic:
· obtain ⟨j, hj₁, hj₂⟩ := h
    exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩

Goal state after:
case hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ N ≤ N
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
h_exists_lt' : ∀ (u : WithTop ι), ↑t < u → ∃ i, ↑(s i) < u
h_eq_iInter : {ω | τ ω ≤ ↑t} = ⋂ m, {ω | τ ω < ↑(s m)}
⊢ ↑f t = ⨅ m_1, ↑f (s m_1)

Tactic:
nth_rw 1 [← hf.eq, Filtration.rightCont_eq_of_neBot_nhdsGT]

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
h_exists_lt' : ∀ (u : WithTop ι), ↑t < u → ∃ i, ↑(s i) < u
h_eq_iInter : {ω | τ ω ≤ ↑t} = ⋂ m, {ω | τ ω < ↑(s m)}
⊢ ⨅ j, ⨅ (_ : j > t), ↑f j = ⨅ m_1, ↑f (s m_1)
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
inst✝ : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ ↑N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
⊢ MeasurableSet {ω | (fun x ↦ ↑(hittingBtwn u s (τ x).untopA N x)) ω ≤ ↑n}

Tactic:
have h₁ : {x | hittingBtwn u s (τ x).untopA N x ≤ n} =
    (⋃ i ≤ n, {x | τ x = i} ∩ {x | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ i > n, {x | τ x = i} ∩ {x | hittingBtwn u s i N x ≤ n} := by
    ext x
    simp only [Set.mem_ofPred_eq, gt_iff_lt, Set.mem_union, Set.mem_iUnion, Set.mem_inter_iff,
      exists_and_left, exists_prop]
    specialize hτbdd x
    have h_top : τ x ≠ ⊤ := fun h => by simp [h] at hτbdd
    lift τ x to ι using h_top with t
    simp [← or_and_right, le_or_gt]

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
inst✝ : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ ↑N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hittingBtwn u s (τ x).untopA N x ≤ n} =
    (⋃ i, ⋃ (_ : i ≤ n), {x | τ x = ↑i} ∩ {x | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ i, ⋃ (_ : i > n), {x | τ x = ↑i} ∩ {x | hittingBtwn u s i N x ≤ n}
⊢ MeasurableSet {ω | (fun x ↦ ↑(hittingBtwn u s (τ x).untopA N x)) ω ≤ ↑n}
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case mpr
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℕ
hk : ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ ∃ k, ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k

Tactic:
· refine ⟨k, fun N => ?_⟩
    simp only [ENNReal.coe_natCast, Nat.cast_le, hk N]

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

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

Tactic:
rw [lintegral_iSup']

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

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

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} +
      ENNReal.ofReal (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)

Tactic:
calc
    _ ≤ ENNReal.ofReal
          (∫ ω in {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω},
            stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω ∂μ) +
        ENNReal.ofReal
          (∫ ω in {ω | ((range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) < ε},
            stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω ∂μ) := by
      gcongr with ω hω
      · exact smul_le_stoppedValue_hittingBtwn hsub n
      · exact (hsub.integrable n).integrableOn
      · refine Integrable.integrableOn ?_
        refine hsub.integrable_stoppedValue ?_ (fun ω ↦ mod_cast hittingBtwn_le ω)
        exact hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici
      · exact nullMeasurableSet_lt (measurable_range_sup'' fun n _ ↦
          (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)).aemeasurable aemeasurable_const
      rw [Set.mem_ofPred_eq] at hω
      have : hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω = n := by
        simp only [hittingBtwn, Set.mem_ofPred_eq, ite_eq_right_iff, forall_exists_index, and_imp]
        intro m hm hεm
        exact False.elim
          ((not_le.2 hω) ((le_sup'_iff _).2 ⟨m, mem_range.2 (Nat.lt_succ_of_le hm.2), hεm⟩))
      simp only [stoppedValue, this, ge_iff_le]
      refine le_of_eq ?_
      congr
    _ = ENNReal.ofReal
        (∫ ω, stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω ∂μ) := by
      rw [← ENNReal.ofReal_add, ← setIntegral_union]
      · rw [← setIntegral_univ (μ := μ)]
        convert! rfl
        ext ω
        change _ ↔ (ε : ℝ) ≤ _ ∨ _ < (ε : ℝ)
        simp only [le_or_gt, Set.mem_univ]
      · grind
      · exact measurableSet_lt (measurable_range_sup'' fun n _ =>
          (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)) measurable_const
      · exact Integrable.integrableOn (hsub.integrable_stoppedValue
          (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
          (fun ω ↦ mod_cast hittingBtwn_le ω))
      · exact Integrable.integrableOn (hsub.integrable_stoppedValue
          (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
          (fun ω ↦ mod_cast hittingBtwn_le ω))
      exacts [integral_nonneg fun x => hnonneg _ _, integral_nonneg fun x => hnonneg _ _]
    _ ≤ ENNReal.ofReal (μ[f n]) := by
      refine ENNReal.ofReal_le_ofReal ?_
      rw [← stoppedValue_const f n]
      refine hsub.expected_stoppedValue_mono
        (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
        (isStoppingTime_const _ _) (fun ω ↦ ?_) (fun _ => mod_cast le_rfl)
      simp [hittingBtwn_le]

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

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

Tactic:
simp only [cgf, mgf_undef hX, log_zero]

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

Goal state before:
pp: case e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ ∫ (ω : Ω), X ω ^ 2 * rexp (v * X ω) ∂μ - (2 * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      deriv (cgf X μ) v ^ 2 * mgf X μ v =
    ∫ (ω : Ω), (X ω ^ 2 - 2 * X ω * deriv (cgf X μ) v + deriv (cgf X μ) v ^ 2) * rexp (v * X ω) ∂μ

Tactic:
simp_rw [add_mul, sub_mul]

Goal state after:
case e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ ∫ (ω : Ω), X ω ^ 2 * rexp (v * X ω) ∂μ - (2 * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      deriv (cgf X μ) v ^ 2 * mgf X μ v =
    ∫ (ω : Ω),
      X ω ^ 2 * rexp (v * X ω) - 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω) +
        deriv (cgf X μ) v ^ 2 * rexp (v * X ω) ∂μ
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
this : (deriv fun t ↦ rexp (↑v * t ^ 2 / 2)) = fun t ↦ ↑v * t * rexp (↑v * t ^ 2 / 2)
⊢ deriv (deriv fun t ↦ rexp (↑v * t ^ 2 / 2)) 0 = ↑v

Tactic:
rw [this, deriv_fun_mul (by fun_prop) (by fun_prop), deriv_fun_mul (by fun_prop) (by fun_prop)]

Goal state after:
μ : ℝ
v : ℝ≥0
this : (deriv fun t ↦ rexp (↑v * t ^ 2 / 2)) = fun t ↦ ↑v * t * rexp (↑v * t ^ 2 / 2)
⊢ (deriv (fun y ↦ ↑v) 0 * 0 + ↑v * deriv (fun y ↦ y) 0) * rexp (↑v * 0 ^ 2 / 2) +
      ↑v * 0 * deriv (fun t ↦ rexp (↑v * t ^ 2 / 2)) 0 =
    ↑v
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
L : E ≃L[ℝ] F
⊢ IsGaussian (Measure.map (⇑L) μ) ↔ IsGaussian μ

Tactic:
by
  refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
  suffices μ = (μ.map L).map L.symm by rw [this]; infer_instance
  rw [Measure.map_map (by fun_prop) (by fun_prop)]
  simp

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[⇑L; μ] ≠ 0
⊢ (Measure.map (⇑L) μ) {L x} = 0

Tactic:
have : NullSingletonClass (μ.map L) := by
        rw [map_eq_gaussianReal L]
        refine nullSingletonClass_gaussianReal ?_
        simp only [ne_eq, Real.toNNReal_eq_zero, not_le]
        exact lt_of_le_of_ne (variance_nonneg _ _) hL.symm

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[⇑L; μ] ≠ 0
this : NullSingletonClass (Measure.map (⇑L) μ)
⊢ (Measure.map (⇑L) μ) {L x} = 0
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : Ω → E
inst✝ : InnerProductSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
⊢ charFun (Measure.map (X + Y) P) = charFun (Measure.map X P) * charFun (Measure.map Y P)

Tactic:
by
  ext t
  rw [hXY.map_add_eq_map_conv_map₀ mX mY, charFun_conv, Pi.mul_apply]

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : ι → Ω → E
inst✝ : NormedSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (s.restrict X) P
⊢ charFunDual (Measure.map (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)

Tactic:
have := hX.isProbabilityMeasure
  induction s using Finset.induction with
  | empty => ext; simp [show (0 : Ω → E) = fun _ ↦ 0 from rfl]
  | insert i s hi hs =>
    rw [Finset.sum_insert hi, IndepFun.charFunDual_map_add_eq_mul, Finset.prod_insert hi, hs]
    · exact fun i hi ↦ (mX i (mem_insert_of_mem hi))
    · exact hX.precomp (g := fun x : s ↦ ⟨x.1, mem_insert_of_mem x.2⟩) (fun _ ↦ by simp)
    · exact mX i (mem_insert_self i s)
    · exact Finset.aemeasurable_sum s (fun i hi ↦ (mX i (mem_insert_of_mem hi)))
    symm
    convert!
      iIndepFun.indepFun_finsetSum_of_notMem₀ (i := ⟨i, mem_insert_self i s⟩) (f :=
        fun (x : (insert i s : Finset ι)) ↦ X x.1) (s := {x | x.1 ∈ s}) hX (fun i ↦ (mX i.1 i.2))
        (by simpa)
    let e : ((insert i s) : Finset ι) → ι := Subtype.val
    convert! (Finset.sum_of_injOn Subtype.val ?_ ?_ ?_ ?_).symm
    · simp
    · intro _ _; grind
    · simp; grind
    · grind

Goal state after:
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: case inr
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : LinearOrder T
inst✝⁶ : OrderBot T
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
I : Finset T
this✝ : IsProbabilityMeasure P
hI : I.Nonempty
this :
  (fun ω ↦ I.restrict fun x ↦ X x ω) =ᵐ[P]
    ⇑(incrementsToRestrict ℝ I) ∘ fun ω i ↦
      X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω
i : Fin #I
⊢ HasGaussianLaw (fun ω ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω) P

Tactic:
refine IndepFun.hasGaussianLaw_sub_of_sub (law _) (law _) ?_

Goal state after:
case inr
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : LinearOrder T
inst✝⁶ : OrderBot T
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
I : Finset T
this✝ : IsProbabilityMeasure P
hI : I.Nonempty
this :
  (fun ω ↦ I.restrict fun x ↦ X x ω) =ᵐ[P]
    ⇑(incrementsToRestrict ℝ I) ∘ fun ω i ↦
      X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω
i : Fin #I
⊢ X (I.orderEmbOfFinWithBot i.castSucc) ⟂ᵢ[P] X (I.orderEmbOfFinWithBot i.succ) - X (I.orderEmbOfFinWithBot i.castSucc)
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
⊢ MeasurableSet {a | ∀ (q r : ℚ), q ≤ r → f a q ≤ f a r}

Tactic:
simp_rw [Set.ofPred_forall]

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
⊢ MeasurableSet (⋂ i, ⋂ i_1, ⋂ (_ : i ≤ i_1), {x | f x i ≤ f x i_1})
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
⊢ MeasurableSet {a | IsRatStieltjesPoint f a}

Tactic:
have h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)} :=
    measurableSet_tendsto _ (fun q ↦ hf.eval)

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
⊢ MeasurableSet {a | IsRatStieltjesPoint f a}
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
⊢ MeasurableSet {a | IsRatStieltjesPoint f a}

Tactic:
have h4 : MeasurableSet {a | ∀ t : ℚ, ⨅ r : Ioi t, f a r = f a t} := by
    rw [Set.ofPred_forall]
    refine MeasurableSet.iInter (fun q ↦ ?_)
    exact measurableSet_eq_fun (.iInf fun _ ↦ hf.eval) hf.eval

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
⊢ MeasurableSet {a | IsRatStieltjesPoint f a}
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: ⊢ Monotone defaultRatCDF

Tactic:
unfold defaultRatCDF
  intro x y hxy
  dsimp only
  split_ifs with h_1 h_2 h_2
  exacts [le_rfl, zero_le_one, absurd (hxy.trans_lt h_2) h_1, le_rfl]

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case pos.refine_1
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : t < 0
⊢ (⨅ r, if ↑r < 0 then 0 else 1) ≤ 0

pp: case pos.refine_2
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : t < 0
x : ↑(Ioi t)
⊢ 0 ≤ if ↑x < 0 then 0 else 1

Tactic:
· obtain ⟨q, htq, hq_neg⟩ : ∃ q, t < q ∧ q < 0 := ⟨t / 2, by linarith, by linarith⟩
      refine (ciInf_le h_bdd ⟨q, htq⟩).trans ?_
      rw [if_pos]
      rwa [Subtype.coe_mk]

Goal state after:
case pos.refine_2
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : t < 0
x : ↑(Ioi t)
⊢ 0 ≤ if ↑x < 0 then 0 else 1