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 ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})
h_eq :
  ∀ (i : WithTop ι),
    s ∩ {ω | τ ω ≤ π ω} ∩ {ω | min (τ ω) (π ω) ≤ i} =
      s ∩ {ω | τ ω ≤ i} ∩ {ω | min (τ ω) (π ω) ≤ i} ∩ {ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
i : ι
⊢ Measurable fun a ↦ min (min (τ a) (π a)) ↑i

Tactic:
exact ((hτ.min hπ).min_const i).measurable_of_le fun _ => min_le_right _ _

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

Goal state before:
pp: case mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
h : MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})

Tactic:
measurableSet_min_iff hτ hπ

Goal state after:
case mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
h : MeasurableSet (s ∩ {ω | τ ω ≤ π ω}) ∧ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
Module: Mathlib.Probability.Martingale.Upcrossing

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

Tactic:
NNReal.coe_natCast

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ MeasurableSet (Set.univ ∩ {ω | τ ω ≤ π ω})

Tactic:
Set.univ_inter

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ MeasurableSet {ω | τ ω ≤ π ω}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
this : MeasurableSet {ω | τ ω ≤ π ω}
⊢ MeasurableSet {ω | τ ω ≤ π ω}

Tactic:
measurableSet_min_iff hτ hπ

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
this : MeasurableSet {ω | τ ω ≤ π ω} ∧ MeasurableSet {ω | τ ω ≤ π ω}
⊢ MeasurableSet {ω | τ ω ≤ π ω}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
h : MeasurableSet {ω | τ ω = π ω}
⊢ MeasurableSet {ω | τ ω = π ω}

Tactic:
measurableSet_min_iff hτ hπ

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
h : MeasurableSet {ω | τ ω = π ω} ∧ MeasurableSet {ω | τ ω = π ω}
⊢ MeasurableSet {ω | τ ω = π ω}
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: case hfs
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω))
    {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} μ

pp: case hft
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω))
    {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε} μ

pp: case hp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ 0 ≤
    ∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ

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

Tactic:
· exact Integrable.integrableOn (hsub.integrable_stoppedValue
          (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
          (fun ω ↦ mod_cast hittingBtwn_le ω))

Goal state after:
case hft
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω))
    {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε} μ

case hp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ 0 ≤
    ∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ

case hq
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ 0 ≤
    ∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
hωb : (upperBounds (Set.range fun n ↦ f n ω)).Nonempty
i : ℕ
hi : hωb.some < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
n : ℕ
⊢ f (min ↑n ⊤).untopA ω = f n ω

Tactic:
simp only [le_top, inf_of_le_left]
      congr

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

Goal state before:
pp: case hft
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω))
    {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε} μ

pp: case hp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ 0 ≤
    ∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ

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

Tactic:
· exact Integrable.integrableOn (hsub.integrable_stoppedValue
          (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
          (fun ω ↦ mod_cast hittingBtwn_le ω))

Goal state after:
case hp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ 0 ≤
    ∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ

case hq
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ 0 ≤
    ∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  {ω |
      Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑(filtrationOfSet hsm) k] ω) atTop atTop} =ᵐ[μ]
    Set.univ
⊢ μ {ω | Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑(filtrationOfSet hsm) k] ω) atTop atTop} =
    1

Tactic:
by
    rw [measure_congr this, measure_univ]

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

Goal state before:
pp: case e'_1.refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
h : BddAbove (Set.range fun n ↦ f n ω)
⊢ BddAbove (Set.range fun n ↦ g n ω)

Tactic:
obtain ⟨b, hb⟩ := h

Goal state after:
case e'_1.refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
b : ℝ
hb : b ∈ upperBounds (Set.range fun n ↦ f n ω)
⊢ BddAbove (Set.range fun n ↦ g n ω)
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case e'_1.refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
h : BddAbove (Set.range fun n ↦ g n ω)
⊢ BddAbove (Set.range fun n ↦ f n ω)

Tactic:
obtain ⟨b, hb⟩ := h

Goal state after:
case e'_1.refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
b : ℝ
hb : b ∈ upperBounds (Set.range fun n ↦ g n ω)
⊢ BddAbove (Set.range fun n ↦ f n ω)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
⊢ Measurable (sᶜ.domRestrict fun p ↦ min (↑↑p.1) (τ p.2))

Tactic:
let sc := sᶜ
    suffices h_min_eq_left :
      (fun x : sc => min (↑(x : Set.Iic i × Ω).fst) (τ (x : Set.Iic i × Ω).snd)) = fun x : sc =>
        ↑(x : Set.Iic i × Ω).fst by
      simp +unfoldPartialApp only [sc, Set.domRestrict, h_min_eq_left]
      exact (h_meas_fst _).withTop_coe
    ext1 ω
    rw [min_eq_left]
    have hx_fst_le : ↑(ω : Set.Iic i × Ω).fst ≤ i := (ω : Set.Iic i × Ω).fst.prop
    by_cases h : τ (ω : Set.Iic i × Ω).2 = ⊤
    · simp [h]
    · lift τ (ω : Set.Iic i × Ω).2 to ι using h with t ht
      norm_cast
      refine hx_fst_le.trans (le_of_lt ?_)
      convert! ω.prop
      simp only [sc, s, not_le, Set.mem_compl_iff, Set.mem_ofPred_eq, ← ht]
      norm_cast

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
x : Ω
⊢ 0 x ≤ rexp (t * X x)

Tactic:
Pi.zero_apply

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
x : Ω
⊢ 0 ≤ rexp (t * X x)
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 ι
this : IsProbabilityMeasure μ
⊢ mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi_notin_s h_rec =>
    have h_int' : ∀ i : ι, AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i =>
      ((h_meas i).const_mul t).exp.aestronglyMeasurable
    rw [sum_insert hi_notin_s,
      IndepFun.mgf_add (h_indep.indepFun_finsetSum_of_notMem₀ h_meas hi_notin_s).symm (h_int' i)
        (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),
      h_rec, prod_insert hi_notin_s]

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 μ
⊢ cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, cgf (X i) μ t

Tactic:
cgf

Goal state after:
Ω : 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 μ
⊢ log (mgf (∑ i ∈ s, X i) μ t) = ∑ i ∈ s, log (mgf (X i) μ t)
Module: Mathlib.Probability.Moments.IntegrableExpMul

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

Tactic:
by
    rw [mul_rpow (by positivity) (by positivity)]
    congr
    · simp
    · rw [rpow_max (by positivity) (by positivity) hp, ← exp_mul, ← exp_mul]
      ring_nf
      congr <;> rw [mul_assoc, mul_inv_cancel₀ hp_zero, mul_one]

Goal state after:
Module: Mathlib.Probability.Moments.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]

Goal state after:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v + min (v - l) (u - v) / 2 ∈ Set.Ioo l u
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]

Goal state after:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v - min (v - l) (u - v) / 2 ∈ Set.Ioo l u
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module ℝ E
mE : MeasurableSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
mF : MeasurableSpace F
inst✝¹ : OpensMeasurableSpace F
μ : Measure E
L : E →L[ℝ] F
inst✝ : IsGaussian μ
hL : Measurable ⇑L
L' : F →L[ℝ] ℝ
⊢ Measure.map (⇑(L' ∘SL L)) μ = gaussianReal (∫ (x : E), (L' ∘SL L) x ∂μ) Var[⇑(L' ∘SL L); μ].toNNReal

Tactic:
IsGaussian.map_eq_gaussianReal

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module ℝ E
mE : MeasurableSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
mF : MeasurableSpace F
inst✝¹ : OpensMeasurableSpace F
μ : Measure E
L : E →L[ℝ] F
inst✝ : IsGaussian μ
hL : Measurable ⇑L
L' : F →L[ℝ] ℝ
⊢ gaussianReal (∫ (x : E), (L' ∘SL L) x ∂μ) Var[⇑(L' ∘SL L); μ].toNNReal =
    gaussianReal (∫ (x : E), (L' ∘SL L) x ∂μ) Var[⇑(L' ∘SL L); μ].toNNReal
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case pos
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
⊢ ((covarianceBilin (Measure.map (fun x ↦ c + x) μ)) x) y = ((covarianceBilin μ) x) y

Tactic:
covarianceBilin_apply h_Lp,

Goal state after:
case pos
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
⊢ ∫ (z : E),
      ⟪x, z - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫ *
        ⟪y, z - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫ ∂Measure.map (fun x ↦ c + x) μ =
    ((covarianceBilin μ) x) y
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ (eLpNormEssSup (⇑L) μ).toReal ≤ ‖L‖ * (eLpNormEssSup id μ).toReal

Tactic:
simp only [eLpNormEssSup, id_eq]

Goal state after:
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ (essSup (fun x ↦ ‖L x‖ₑ) μ).toReal ≤ ‖L‖ * (essSup (fun x ↦ ‖x‖ₑ) μ).toReal
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case hb
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ essSup (fun x ↦ ‖L‖ₑ * ‖x‖ₑ) μ ≠ ∞

Tactic:
rw [ENNReal.essSup_const_mul]
      exact ENNReal.mul_ne_top (by simp) h_Lp.eLpNorm_ne_top

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
⊢ 0 < (1 - c).toReal

Tactic:
· simp [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hc_lt, hc_one_sub_lt_top]

Goal state after:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: ⊢ IsProjectiveMeasureFamily projectiveFamily

Tactic:
intro I J hJI
  nth_rw 2 [projectiveFamily]
  rw [Measure.map_map]
  · have : (Finset.restrict₂ (π := fun _ ↦ ℝ) hJI ∘ (MeasurableEquiv.toLp 2 (I → ℝ)).symm) =
        ofLp ∘ (EuclideanSpace.restrict₂ hJI) := by ext; simp
    rw [this, ((measurePreserving_ofLp_multivariateGaussian J).comp
        (measurePreserving_restrict₂_multivariateGaussian (posSemidef_covMatrix I) hJI)).map_eq]
  · exact Finset.measurable_restrict₂ _ -- fun_prop fails
  · fun_prop

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

Goal state before:
pp: case insert.hX
Ω : 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
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  (∀ i ∈ s, AEMeasurable (X i) P) →
    iIndepFun (s.restrict X) P → charFunDual (Measure.map (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun ((insert i s).restrict X) P
⊢ iIndepFun (s.restrict X) P

Tactic:
exact hX.precomp (g := fun x : s ↦ ⟨x.1, mem_insert_of_mem x.2⟩) (fun _ ↦ by simp)

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

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
⊢ HasGaussianLaw (fun ω i ↦ X (t i.succ) ω - X (t i.castSucc) ω) P

Tactic:
let L : ((univ.image t) → E) →L[ℝ] Fin n → E :=
    { toFun x i := x ⟨t i.succ, by simp⟩ - x ⟨t i.castSucc, by simp⟩
      map_add' x y := by ext; simp; abel
      map_smul' m x := by ext; simp; module }
  exact (hX.hasGaussianLaw _).map L

Goal state after: