mathlib-initiative/mathlib-tactics huggingface dataset:
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
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ ↑i ∧ ↑i < π ω}
i : ℕ
x✝ : i ∈ Finset.range (N + 1)
⊢ Integrable (f (i + 1)) (μ.restrict {ω | τ ω ≤ ↑i ∧ ↑i < π ω})

pp: case hg
Ω : 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
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ ↑i ∧ ↑i < π ω}
i : ℕ
x✝ : i ∈ Finset.range (N + 1)
⊢ Integrable (f i) (μ.restrict {ω | τ ω ≤ ↑i ∧ ↑i < π ω})

Tactic:
· exact (hf.integrable _).integrableOn

Goal state after:
case hg
Ω : 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
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ ↑i ∧ ↑i < π ω}
i : ℕ
x✝ : i ∈ Finset.range (N + 1)
⊢ Integrable (f i) (μ.restrict {ω | τ ω ≤ ↑i ∧ ↑i < π ω})
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: case hg
Ω : 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
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ ↑i ∧ ↑i < π ω}
i : ℕ
x✝ : i ∈ Finset.range (N + 1)
⊢ Integrable (f i) (μ.restrict {ω | τ ω ≤ ↑i ∧ ↑i < π ω})

Tactic:
· exact (hf.integrable _).integrableOn

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

Goal state before:
pp: Ω : 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)
⊢ Measurable fun p ↦ min (↑↑p.1) (τ p.2)

Tactic:
let m_set : ∀ t : Set (Set.Iic i × Ω), MeasurableSpace t := fun _ =>
    @Subtype.instMeasurableSpace (Set.Iic i × Ω) _ m_prod

Goal state after:
Ω : 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
⊢ Measurable fun p ↦ min (↑↑p.1) (τ p.2)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : 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
⊢ Measurable fun p ↦ min (↑↑p.1) (τ p.2)

Tactic:
let s := {p : Set.Iic i × Ω | τ p.2 ≤ i}

Goal state after:
Ω : 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}
⊢ Measurable fun p ↦ min (↑↑p.1) (τ p.2)
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x ↦ X x - integral μ X) μ
⊢ X = (fun x ↦ X x - integral μ X) + fun x ↦ integral μ X

Tactic:
ext1 x

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x ↦ X x - integral μ X) μ
x : Ω
⊢ X x = ((fun x ↦ X x - integral μ X) + fun x ↦ integral μ X) x
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) ∂μ
⊢ (Function.support fun x ↦ rexp (t * X x)) = Set.univ

Tactic:
ext1 x

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 : Ω
⊢ (x ∈ Function.support fun x ↦ rexp (t * X x)) ↔ x ∈ Set.univ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inr.h₀.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
b : ι
a✝ : b ∈ {i ∈ s | i < n}
hneq : b ≠ i
⊢ ω ∉ {ω | τ ω = ↑b}

Tactic:
Set.mem_ofPred,

Goal state after:
case inr.h₀.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
b : ι
a✝ : b ∈ {i ∈ s | i < n}
hneq : b ≠ i
⊢ ¬τ ω = ↑b
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : τ ω < ↑n
⊢ stoppedProcess u τ n ω = {a | ↑n ≤ τ a}.indicator (u n) ω + ∑ c ∈ s with c < n, {ω | τ ω = ↑c}.indicator (u c) ω

Tactic:
rw [stoppedProcess_eq_of_ge (le_of_lt h)]
    have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at h
    specialize hbdd ω h
    lift τ ω to ι using h_top with i hi
    rw [Finset.sum_eq_single_of_mem i]
    · simp only [untopD_coe]
      rw [Set.indicator_of_notMem, zero_add, Set.indicator_of_mem] <;> rw [Set.mem_ofPred]
      · exact hi.symm
      · rw [← hi]
        exact not_le.2 h
    · rw [Finset.mem_filter]
      simp only [Set.mem_image, Finset.mem_coe, coe_eq_coe, exists_eq_right] at hbdd
      exact ⟨hbdd, mod_cast h⟩
    · intro b _ hneq
      rw [Set.indicator_of_notMem]
      rw [Set.mem_ofPred, ← hi]
      exact mod_cast hneq.symm

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ μ.real {ω | X ω ≤ ε} ≤ rexp (-t * ε + cgf X μ t)

Tactic:
refine (measure_le_le_exp_mul_mgf ε ht h_int).trans ?_
  rw [exp_add]
  exact mul_le_mul le_rfl (le_exp_log _) mgf_nonneg (exp_pos _).le

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

Goal state before:
pp: m : ℝ
⊢ gaussianPDFReal m 0 = 0

Tactic:
ext1 x

Goal state after:
m x : ℝ
⊢ gaussianPDFReal m 0 x = 0 x
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ Integrable (fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ

Tactic:
by_cases hv : v = 0

Goal state after:
case pos
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ Integrable (fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ

case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ Integrable (fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case e_a
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))
⊢ max (rexp (t * p * p⁻¹ * x)) (rexp (-(t * p * p⁻¹ * x))) = max (rexp (t * x)) (rexp (-(t * x)))

Tactic:
congr <;> rw [mul_assoc, mul_inv_cancel₀ hp_zero, mul_one]

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ ∂gaussianReal μ v/∂ℙ =ᵐ[ℙ] gaussianPDF μ v

Tactic:
by_cases hv : v = 0

Goal state after:
case pos
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ ∂gaussianReal μ v/∂ℙ =ᵐ[ℙ] gaussianPDF μ v

case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ ∂gaussianReal μ v/∂ℙ =ᵐ[ℙ] gaussianPDF μ v
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
y : ℝ
⊢ Measure.map (fun x ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

Tactic:
by_cases hv : v = 0

Goal state after:
case pos
μ : ℝ
v : ℝ≥0
y : ℝ
hv : v = 0
⊢ Measure.map (fun x ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

case neg
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
⊢ Measure.map (fun x ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v
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
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ (∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ ∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v / mgf X μ v ^ 2 =
    deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v

Tactic:
rw [pow_two, div_mul_eq_div_div, mul_div_assoc, div_self, mul_one]
      exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
c : ℝ
⊢ Measure.map (fun x ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)

Tactic:
by_cases hv : v = 0

Goal state after:
case pos
μ : ℝ
v : ℝ≥0
c : ℝ
hv : v = 0
⊢ Measure.map (fun x ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)

case neg
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
⊢ Measure.map (fun x ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
z : ℂ
⊢ complexMGF id (gaussianReal μ v) z = cexp (z * ↑μ + ↑↑v * z ^ 2 / 2)

Tactic:
by_cases hv : v = 0

Goal state after:
case pos
μ : ℝ
v : ℝ≥0
z : ℂ
hv : v = 0
⊢ complexMGF id (gaussianReal μ v) z = cexp (z * ↑μ + ↑↑v * z ^ 2 / 2)

case neg
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ complexMGF id (gaussianReal μ v) z = cexp (z * ↑μ + ↑↑v * z ^ 2 / 2)
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x : ℝ
⊢ ((covarianceBilin μ) x) x = x ^ 2 * Var[id; μ]

Tactic:
covarianceBilin_real,

Goal state after:
μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x : ℝ
⊢ x * x * Var[id; μ] = x ^ 2 * Var[id; μ]
Module: Mathlib.Probability.Distributions.Gaussian.Real

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

Tactic:
rw [this, gaussianReal_map_const_mul]

Goal state after:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
this : ⇑L = fun x ↦ L 1 * x
⊢ gaussianReal (L 1 * μ) (NNReal.mk (L 1 ^ 2) ⋯ * v) =
    gaussianReal ((fun x ↦ L 1 * x) μ) (((fun x ↦ L 1 * x) 1 ^ 2).toNNReal * v)
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case neg
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✝¹ x✝ : E
⊢ ¬MemLp (id ∘ fun x ↦ c + x) 2 μ

Tactic:
contrapose h

Goal state after:
case neg
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c x✝¹ x✝ : E
h : MemLp (id ∘ fun x ↦ c + x) 2 μ
⊢ MemLp id 2 μ
Module: Mathlib.Probability.Moments.CovarianceBilin

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

Tactic:
by
  by_cases h : MemLp id 2 μ
  · ext x y
    have h_Lp : MemLp id 2 (μ.map (fun x ↦ c + x)) :=
      (measurableEmbedding_addLeft _).memLp_map_measure_iff.mpr <| (memLp_const c).add h
    rw [covarianceBilin_apply h_Lp,
      covarianceBilin_apply h, integral_map (by fun_prop) (by fun_prop)]
    congr with z
    rw [integral_map (by fun_prop) h_Lp.1]
    simp only [id_eq]
    rw [integral_add (integrable_const _)]
    · simp
    · exact h.integrable (by simp)
  · ext
    rw [covarianceBilin_of_not_memLp, covarianceBilin_of_not_memLp h]
    rw [(measurableEmbedding_addLeft _).memLp_map_measure_iff.not]
    contrapose h
    convert! (memLp_const (-c)).add h
    ext; simp

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
s : Set (StrongDual 𝕜 E)
r : ℝ
hxr : ∀ x ∈ s, ‖x‖ ≤ r
⊢ ∃ r, ∀ x ∈ s, ‖(toLpₗ μ p) x‖ ≤ r

Tactic:
refine ⟨r * (eLpNorm id p μ).toReal, fun L hLs ↦ ?_⟩

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
s : Set (StrongDual 𝕜 E)
r : ℝ
hxr : ∀ x ∈ s, ‖x‖ ≤ r
L : StrongDual 𝕜 E
hLs : L ∈ s
⊢ ‖(toLpₗ μ p) L‖ ≤ r * (eLpNorm id p μ).toReal
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: a : ℝ
n : ℕ
⊢ normThreshold a (n + 1) ^ 2 ≤ a ^ 2 * (1 + √2) ^ 2 * 2 ^ (n + 2)

Tactic:
by
  simp_rw [normThreshold_eq, mul_pow, mul_assoc]
  gcongr
  calc (√2 ^ (n + 2) - 1) ^ 2
  _ ≤ (√2 ^ (n + 2)) ^ 2 := by
    gcongr
    · calc 0 ≤ √2 ^ (0 + 2) - 1 := by simp
      _ ≤ √2 ^ (n + 2) - 1 := by gcongr <;> simp
    · exact sub_le_self _ (by simp)
  _ = 2 ^ (n + 2) := by rw [← pow_mul, mul_comm, pow_mul, Real.sq_sqrt (by positivity)]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
h : ¬MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ¬MemLp (fun x ↦ x - ∫ (y : E), y ∂μ) 2 μ

Tactic:
contrapose h

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp (fun x ↦ x - ∫ (y : E), y ∂μ) 2 μ
⊢ MemLp id 2 μ
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: case right
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
n : StrongDual ℝ E → ℤ
h :
  ∀ (L : StrongDual ℝ E),
    ↑(n L) =
      (↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2 - ↑(L m) * I + ↑((f L) L) / 2) /
        (2 * ↑π * I)
this✝¹ : Continuous n
this✝ : ∀ (x : StrongDual ℝ E), n = Function.const (StrongDual ℝ E) (n x)
this : ∀ (L : StrongDual ℝ E), n L = 0
hn : ∀ (L : StrongDual ℝ E), ((covarianceBilinDual μ) L) L = (f L) L ∧ L (∫ (x : E), x ∂μ) = L m
⊢ f = covarianceBilinDual μ

Tactic:
rw [← toBilinForm_inj]

Goal state after:
case right
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
n : StrongDual ℝ E → ℤ
h :
  ∀ (L : StrongDual ℝ E),
    ↑(n L) =
      (↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2 - ↑(L m) * I + ↑((f L) L) / 2) /
        (2 * ↑π * I)
this✝¹ : Continuous n
this✝ : ∀ (x : StrongDual ℝ E), n = Function.const (StrongDual ℝ E) (n x)
this : ∀ (L : StrongDual ℝ E), n L = 0
hn : ∀ (L : StrongDual ℝ E), ((covarianceBilinDual μ) L) L = (f L) L ∧ L (∫ (x : E), x ∂μ) = L m
⊢ f.toBilinForm = (covarianceBilinDual μ).toBilinForm
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I✝ J I : Finset ℝ≥0
⊢ IsGaussian (projectiveFamily I)

Tactic:
rw [projectiveFamily,
    show ⇑(MeasurableEquiv.toLp 2 (I → ℝ)).symm = ⇑(EuclideanSpace.equiv I ℝ) from rfl]

Goal state after:
I✝ J I : Finset ℝ≥0
⊢ IsGaussian (Measure.map (⇑(EuclideanSpace.equiv ↥I ℝ)) (multivariateGaussian 0 (covMatrix I)))
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : Fintype ι
E : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (fun ω x ↦ X x ω) P
⊢ HasGaussianLaw (fun ω ↦ ∑ i, X i ω) P

Tactic:
convert! hX.sum
  simp

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
h : ∀ (t : T), X t =ᵐ[P] Y t
I : Finset T
h' : ∀ᵐ (ω : Ω) ∂P, ∀ (i : ↥I), X (↑i) ω = Y (↑i) ω
⊢ Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P = Measure.map (fun ω ↦ I.restrict fun x ↦ Y x ω) P

Tactic:
refine Measure.map_congr ?_

Goal state after:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
h : ∀ (t : T), X t =ᵐ[P] Y t
I : Finset T
h' : ∀ᵐ (ω : Ω) ∂P, ∀ (i : ↥I), X (↑i) ω = Y (↑i) ω
⊢ (fun ω ↦ I.restrict fun x ↦ X x ω) =ᵐ[P] fun ω ↦ I.restrict fun x ↦ Y x ω
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
⊢ ∀ᵐ (b : β) ∂ν a, Tendsto (f (a, b)) atTop (𝓝 1)

Tactic:
by
  filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.tendsto_atTop_one

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : (ν a).restrict s = 0
q : ℚ
hq : x < ↑q
this : (κ a).real (s ×ˢ Iic ↑q) = 0
⊢ (κ a) (s ×ˢ Iic ↑q) = 0

Tactic:
rw [measureReal_eq_zero_iff] at this
      simpa [measure_ne_top] using this

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
⊢ ⋂ r, s ×ˢ Iic ↑(-r) = ⋂ r, s ×ˢ Iic ↑r

Tactic:
ext1 x

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
⊢ x ∈ ⋂ r, s ×ˢ Iic ↑(-r) ↔ x ∈ ⋂ r, s ×ˢ Iic ↑r
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
x✝ : MeasurableSpace β
f : α × β → StieltjesFunction ℝ
κ : Kernel α (β × ℝ)
ν : Kernel α β
hf : IsCondKernelCDF f κ ν
p : α × β
x : ℝ
⊢ ((toKernel f hf) p) (Iic x) = ENNReal.ofReal (↑(f p) x)

Tactic:
by
  rw [IsCondKernelCDF.toKernel_apply p, (f p).measure_Iic (hf.tendsto_atBot_zero p)]
  simp

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this✝ : IsProbabilityMeasure P
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
this : Fintype ι := Fintype.ofFinite ι
⊢ (ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω) ⟂ᵢ[P] ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω

Tactic:
let := Fintype.ofFinite κ

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this✝¹ : IsProbabilityMeasure P
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
this✝ : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
⊢ (ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω) ⟂ᵢ[P] ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun n ↦ Iic ↑(s n)
i j : ℕ
hij : i ≤ j
⊢ ↑(s i) ≤ ↑(s j)

Tactic:
by exact mod_cast hs_mono hij

Goal state after: