mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
this : r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z))
⊢ r (x ⊓ y ⊓ z) (y ⊓ z)

Tactic:
inf_comm x,

Goal state after:
α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
this : r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z))
⊢ r (y ⊓ x ⊓ z) (y ⊓ z)
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ n (x ⇨ y) ≤ x ⇨ n y

Tactic:
by
  rw [le_himp_iff]
  calc
    n (x ⇨ y) ⊓ x
    _ ≤ n (x ⇨ y) ⊓ n x := by gcongr; exact n.le_apply
    _ = n (y ⊓ x) := by rw [← map_inf, himp_inf_self]
    _ ≤ n y := by gcongr; exact inf_le_left

Goal state after:
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:
by
  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.Process.Stopping

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i i' : ι
hi'_lub : IsLUB (Set.Iio i) i'
h_Iio_eq_Iic : Set.Iio i = Set.Iic i'
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
have h_lt_eq_preimage : {ω : Ω | τ ω < i} = τ ⁻¹' Set.Iio i := rfl

Goal state after:
case inr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i i' : ι
hi'_lub : IsLUB (Set.Iio i) i'
h_Iio_eq_Iic : Set.Iio i = Set.Iic i'
h_lt_eq_preimage : {ω | τ ω < ↑i} = τ ⁻¹' Set.Iio ↑i
⊢ MeasurableSet {ω | τ ω < ↑i}
Module: Mathlib.Probability.Process.HittingTime

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

Tactic:
exact hm

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

Goal state before:
pp: case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : AddGroup ι
inst✝² : Preorder ι
inst✝¹ : AddRightMono ι
inst✝ : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
ω : Ω
a : ι
⊢ a + i ≤ j ↔ a ≤ j - i

Tactic:
← le_sub_iff_add_le

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
this : MeasurableSpace Ω := ⨆ n, ↑ℱ n
⊢ μ {a | ¬∃ c, Tendsto (fun n ↦ f n a) atTop (𝓝 c)} = 0

Tactic:
exact hf.exists_ae_tendsto_of_bdd hbdd

Goal state after:
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✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
have : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i} := by
    ext1 ω
    simp only [lt_iff_le_and_ne, Set.mem_ofPred_eq, Set.mem_sdiff]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | τ ω < ↑i} = {ω | τ ω ≤ ↑i} \ {ω | τ ω = ↑i}
⊢ MeasurableSet {ω | τ ω < ↑i}
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 τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
have : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i} := by
    ext1 ω
    simp only [lt_iff_le_and_ne, Set.mem_ofPred_eq, Set.mem_sdiff]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω < ↑i} = {ω | τ ω ≤ ↑i} \ {ω | τ ω = ↑i}
⊢ MeasurableSet {ω | τ ω < ↑i}
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
⊢ centralMoment X 1 μ = 0

Tactic:
by
  rcases eq_zero_or_isProbabilityMeasure μ with rfl | h
  · simp [centralMoment]
  by_cases h_int : Integrable X μ
  · rw [centralMoment_one' h_int]
    simp
  · simp only [centralMoment, Pi.sub_apply, pow_one]
    have : ¬Integrable (fun x => X x - integral μ X) μ := by
      refine fun h_sub => h_int ?_
      have h_add : X = (fun x => X x - integral μ X) + fun _ => integral μ X := by ext1 x; simp
      rw [h_add]
      fun_prop
    rw [integral_undef this]

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

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R

Tactic:
filter_upwards [hbdd] with ω hω i

Goal state after:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ω : Ω
hω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
ι : Type u_3
μ : ι → Measure Ω
hμ : Integrable (fun ω ↦ rexp (t * X ω)) (Measure.sum μ)
⊢ ∫ (x : Ω), rexp (t * X x) ∂Measure.sum μ = ∑' (i : ι), ∫ (x : Ω), rexp (t * X x) ∂μ i

Tactic:
integral_sum_measure hμ

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

Goal state before:
pp: case mp
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n ↦ f n ω✝) ↔ ∃ c, Tendsto (fun n ↦ f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n ↦ (-f) n ω✝) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n ↦ f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : ∀ x ∈ Set.range fun n ↦ (-f) n ω✝, x ≤ c
ω : ℝ
hω : ω ∈ Set.range fun n ↦ f n ω✝
⊢ -c ≤ ω

Tactic:
refine neg_le.2 (hc _ ?_)

Goal state after:
case mp
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n ↦ f n ω✝) ↔ ∃ c, Tendsto (fun n ↦ f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n ↦ (-f) n ω✝) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n ↦ f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : ∀ x ∈ Set.range fun n ↦ (-f) n ω✝, x ≤ c
ω : ℝ
hω : ω ∈ Set.range fun n ↦ f n ω✝
⊢ -ω ∈ Set.range fun n ↦ (-f) n ω✝
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω ↦ rexp (a * X ω)) μ
hb : Integrable (fun ω ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
ha_zero : a = 0
⊢ AEMeasurable X μ

Tactic:
refine aemeasurable_of_aemeasurable_exp_mul ?_ hb.1.aemeasurable
        rw [ha_zero] at hab
        exact Ne.symm hab

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), ↑i ≤ τ ω
hη : ∀ (ω : Ω), ↑i ≤ η ω
hs : MeasurableSet s
⊢ IsStoppingTime 𝒢 (s.piecewise τ η)

Tactic:
intro n
  have : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n} := by
    ext1 ω
    simp only [Set.piecewise, Set.mem_ofPred_eq]
    by_cases hx : ω ∈ s <;> simp [hx]
  rw [this]
  by_cases hin : i ≤ n
  · have hs_n : MeasurableSet[𝒢 n] s := 𝒢.mono hin _ hs
    exact (hs_n.inter (hτ_st n)).union (hs_n.compl.inter (hη_st n))
  · have hτn : ∀ ω, ¬τ ω ≤ n := fun ω hτn => hin (mod_cast (hτ ω).trans hτn)
    have hηn : ∀ ω, ¬η ω ≤ n := fun ω hηn => hin (mod_cast (hη ω).trans hηn)
    simp [hτn, hηn, @MeasurableSet.empty _ _]

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
x : ℝ
hv : v ≠ 0
⊢ 0 < gaussianPDFReal μ v x

Tactic:
by
  rw [gaussianPDFReal]
  positivity

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
x : ℝ
⊢ 0 ≤ gaussianPDFReal μ v x

Tactic:
by
  rw [gaussianPDFReal]
  positivity

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

Goal state before:
pp: ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ cov[fun ω ↦ ⟪∑ i, ⟪(basisFun ι ℝ) i, x⟫ • (basisFun ι ℝ) i, toLp 2 fun x ↦ X x ω⟫, fun ω ↦
      ⟪∑ i, ⟪(basisFun ι ℝ) i, y⟫ • (basisFun ι ℝ) i, toLp 2 fun x ↦ X x ω⟫; μ] =
    ∑ x_1, ∑ x_2, x.ofLp x_1 * y.ofLp x_2 * cov[X x_1, X x_2; μ]

Tactic:
sum_inner,

Goal state after:
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ cov[fun ω ↦ ∑ i, ⟪⟪(basisFun ι ℝ) i, x⟫ • (basisFun ι ℝ) i, toLp 2 fun x ↦ X x ω⟫, fun ω ↦
      ∑ i, ⟪⟪(basisFun ι ℝ) i, y⟫ • (basisFun ι ℝ) i, toLp 2 fun x ↦ X x ω⟫; μ] =
    ∑ x_1, ∑ x_2, x.ofLp x_1 * y.ofLp x_2 * cov[X x_1, X x_2; μ]
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
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ μ {x | ‖x‖ ≤ a} * μ {x | b < ‖x‖} ≤ μ {x | (b - a) / √2 < ‖x‖} ^ 2

Tactic:
calc μ {x | ‖x‖ ≤ a} * μ {x | b < ‖x‖}
  _ = (μ.prod μ) ({x | ‖x‖ ≤ a} ×ˢ {y | b < ‖y‖}) := by rw [Measure.prod_prod]
    -- This is the measure of two bands in the plane (draw a picture!)
  _ = (μ.prod μ) {p | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} := rfl
  _ = ((μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4)))) {p | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} := by
    -- We can rotate the bands since `μ.prod μ` is invariant under rotation
    rw [h]
  _ = (μ.prod μ) {p | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2} := by
    rw [Measure.map_apply (by fun_prop)]
    swap
    · refine MeasurableSet.inter ?_ ?_
      · change MeasurableSet {p : E × E | ‖p.1‖ ≤ a}
        exact measurableSet_le (by fun_prop) (by fun_prop)
      · change MeasurableSet {p : E × E | b < ‖p.2‖}
        exact measurableSet_lt (by fun_prop) (by fun_prop)
    congr 1
    simp only [Set.preimage_ofPred_eq, ContinuousLinearMap.rotation_apply, Real.cos_neg,
      Real.cos_pi_div_four, Real.sin_neg, Real.sin_pi_div_four, neg_smul, neg_neg]
    have h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹ := by
      simp only [norm_mul, norm_inv, Real.norm_ofNat, Real.norm_eq_abs]
      rw [abs_of_nonneg (by positivity)]
      nth_rw 1 [← Real.sq_sqrt (by simp : (0 : ℝ) ≤ 2)]
      rw [pow_two, mul_inv, mul_assoc, inv_mul_cancel₀ (by positivity), mul_one]
    congr! with p
    · rw [← sub_eq_add_neg, ← smul_sub, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]
    · rw [← smul_add, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]
  _ ≤ (μ.prod μ) {p | (b - a) / √2 < ‖p.1‖ ∧ (b - a) / √2 < ‖p.2‖} := by
    -- The rotated bands are contained in quadrants.
    refine measure_mono fun p ↦ ?_
    simp only [Set.mem_ofPred_eq, and_imp]
    intro hp1 hp2
    suffices (b - a) / √2 < min ‖p.1‖ ‖p.2‖ from lt_min_iff.mp this
    calc (b - a) / √2
    _ < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 := by
      suffices b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2 by
        calc (b - a) / √2 < (‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2) / √2 := by gcongr
        _ = (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 := by
          field_simp; rw [Real.sq_sqrt (by positivity)]; ring
      calc b - a < ‖p.1 + p.2‖ / √2 - a := by gcongr
      _ ≤ ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2 := by gcongr
    _ ≤ min ‖p.1‖ ‖p.2‖ := by
      have := norm_add_sub_norm_sub_le_two_mul_min p.1 p.2
      linarith
  _ = (μ.prod μ) ({x | (b - a) / √2 < ‖x‖} ×ˢ {y | (b - a) / √2 < ‖y‖}) := rfl
  _ ≤ μ {x | (b - a) / √2 < ‖x‖} ^ 2 := by rw [Measure.prod_prod, pow_two]

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

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
t : E
⊢ (∫ (x : Fin (finrank ℝ E) → ℝ),
      cexp (↑⟪∑ i, x i • (stdOrthonormalBasis ℝ E) i, t⟫ * I) ∂Measure.pi fun x ↦ gaussianReal 0 1) =
    cexp (-↑‖t‖ ^ 2 / 2)

Tactic:
sum_inner,

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
t : E
⊢ (∫ (x : Fin (finrank ℝ E) → ℝ),
      cexp (↑(∑ i, ⟪x i • (stdOrthonormalBasis ℝ E) i, t⟫) * I) ∂Measure.pi fun x ↦ gaussianReal 0 1) =
    cexp (-↑‖t‖ ^ 2 / 2)
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
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
μ : Measure E
inst✝ : IsGaussian μ
⊢ ∃ C, 0 < C ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ

Tactic:
obtain ⟨C, hC_pos, hC⟩ : ∃ C, 0 < C
      ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ μ.map (ContinuousLinearEquiv.neg ℝ)) :=
    exists_integrable_exp_sq_of_map_rotation_eq_self
      (map_rotation_eq_self_of_forall_strongDual_eq_zero
        (integral_dual_conv_map_neg_eq_zero (μ := μ)) _)
  -- We must now prove that the integrability with respect to
  -- `μ ∗ μ.map (ContinuousLinearEquiv.neg ℝ)` implies integrability with respect to `μ` for
  -- another constant `C' < C`.
  refine ⟨C / 2, by positivity, ?_⟩
  exact integrable_exp_sq_of_conv_neg μ hC (by positivity) (by simp [hC_pos])

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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
X : Ω → E
inst✝ : InnerProductSpace ℝ E
t : E
hX : HasGaussianLaw X P
⊢ charFun (Measure.map X P) t = cexp (↑(∫ (x : Ω), (fun ω ↦ ⟪t, X ω⟫) x ∂P) * I - ↑Var[fun ω ↦ ⟪t, X ω⟫; P] / 2)

Tactic:
by
  rw [hX.isGaussian_map.charFun_eq, integral_map hX.aemeasurable (by fun_prop),
    variance_map (by fun_prop) hX.aemeasurable, integral_complex_ofReal, Function.comp_def]

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

Goal state before:
pp: I : Finset ℝ≥0
s : ↥I
| ∫ (x : ↥I → ℝ), x s ∂projectiveFamily I

Tactic:
2

Goal state after:
I : Finset ℝ≥0
s : ↥I
| fun x ↦ x s
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t : ℝ≥0
⊢ ∫ (x : Ω), B t x ∂P = 0

Tactic:
by
  rw [(hB.hasLaw_eval t).integral_eq, integral_id_gaussianReal]

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

Goal state before:
pp: case refine_2
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
this : Nonempty { r' // y < ↑r' }
r : { q' // y < ↑q' }
⊢ { q' // x < ↑q' }

Tactic:
exact ⟨r.1, hxy.trans_lt r.prop⟩

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

Goal state before:
pp: case e_f.mk
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
a : α
x : ℝ
fst✝ : Unit
b : α
⊢ toRatCDF (fun p ↦ f p.2) (fst✝, b) = toRatCDF f (fst✝, b).2

Tactic:
| mk _ b =>

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 : ℝ
this :
  (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) = fun b ↦
    (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal
⊢ Integrable (fun b ↦ (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal) (ν a)

Tactic:
refine integrable_toReal_of_lintegral_ne_top ?_ ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) = fun b ↦
    (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal
⊢ AEMeasurable (fun b ↦ ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)) (ν a)

case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) = fun b ↦
    (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal
⊢ ∫⁻ (x_1 : β), ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, x_1)) x) ∂ν a ≠ ∞
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) = fun b ↦
    (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal
⊢ ∫⁻ (x_1 : β), ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, x_1)) x) ∂ν a ≠ ∞

Tactic:
rw [lintegral_stieltjesOfMeasurableRat hf]
    exact measure_ne_top _ _

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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
q : ℚ
⊢ Measurable fun t ↦ f (a, t) q

Tactic:
let h := hf.measurable
  rw [measurable_pi_iff] at h
  exact (h q).comp measurable_prodMk_left

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

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
t : Set α
x✝¹ : MeasurableSet t
x✝ : ρ.fst t ≠ ∞
⊢ ∫⁻ (x_1 : α) in t, ENNReal.ofReal (preCDF ρ x x_1).toReal ∂ρ.fst ≤ ρ.fst univ

Tactic:
rw [← lintegral_one]

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
t : Set α
x✝¹ : MeasurableSet t
x✝ : ρ.fst t ≠ ∞
⊢ ∫⁻ (x_1 : α) in t, ENNReal.ofReal (preCDF ρ x x_1).toReal ∂ρ.fst ≤ ∫⁻ (x : α), 1 ∂ρ.fst
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
⊢ ∀ᵐ (t : β) ∂ν a, ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)

Tactic:
filter_upwards [hf.nonneg a] with c hc
  refine fun q ↦ ⟨0, ?_⟩
  simp [mem_lowerBounds, hc]

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

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝¹ : Finite ι
κ : ι → Type u_4
inst✝ : ∀ (i : ι), Finite (κ i)
X : (i : ι) → κ i → Ω → ℝ
hX : HasGaussianLaw (fun ω i j ↦ X i j ω) P
h : ∀ (i j : ι), i ≠ j → ∀ (k : κ i) (l : κ j), cov[X i k, X j l; P] = 0
this✝² : IsProbabilityMeasure P
this✝¹ : (fun i ω j ↦ X i j ω) = fun i ↦ ofLp ∘ toLp 2 ∘ fun ω j ↦ X i j ω
this✝ : (i : ι) → Fintype (κ i) := fun i ↦ Fintype.ofFinite (κ i)
this : Fintype ι := Fintype.ofFinite ι
i j : ι
hij : i ≠ j
x : WithLp 2 (κ i → ℝ)
y : WithLp 2 (κ j → ℝ)
⊢ cov[fun ω ↦
      ⟪∑ x_1, ((EuclideanSpace.basisFun (κ i) ℝ).repr x).ofLp x_1 • (EuclideanSpace.basisFun (κ i) ℝ) x_1,
        (toLp 2 ∘ fun ω j ↦ X i j ω) ω⟫,
      fun ω ↦
      ⟪∑ x, ((EuclideanSpace.basisFun (κ j) ℝ).repr y).ofLp x • (EuclideanSpace.basisFun (κ j) ℝ) x,
        (toLp 2 ∘ fun ω j_1 ↦ X j j_1 ω) ω⟫;
      P] =
    0

Tactic:
sum_inner,

Goal state after:
case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝¹ : Finite ι
κ : ι → Type u_4
inst✝ : ∀ (i : ι), Finite (κ i)
X : (i : ι) → κ i → Ω → ℝ
hX : HasGaussianLaw (fun ω i j ↦ X i j ω) P
h : ∀ (i j : ι), i ≠ j → ∀ (k : κ i) (l : κ j), cov[X i k, X j l; P] = 0
this✝² : IsProbabilityMeasure P
this✝¹ : (fun i ω j ↦ X i j ω) = fun i ↦ ofLp ∘ toLp 2 ∘ fun ω j ↦ X i j ω
this✝ : (i : ι) → Fintype (κ i) := fun i ↦ Fintype.ofFinite (κ i)
this : Fintype ι := Fintype.ofFinite ι
i j : ι
hij : i ≠ j
x : WithLp 2 (κ i → ℝ)
y : WithLp 2 (κ j → ℝ)
⊢ cov[fun ω ↦
      ∑ i_1,
        ⟪((EuclideanSpace.basisFun (κ i) ℝ).repr x).ofLp i_1 • (EuclideanSpace.basisFun (κ i) ℝ) i_1,
          (toLp 2 ∘ fun ω j ↦ X i j ω) ω⟫,
      fun ω ↦
      ∑ i,
        ⟪((EuclideanSpace.basisFun (κ j) ℝ).repr y).ofLp i • (EuclideanSpace.basisFun (κ j) ℝ) i,
          (toLp 2 ∘ fun ω j_1 ↦ X j j_1 ω) ω⟫;
      P] =
    0
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝ : ρ.IsCondKernel ρCond
hρ : ρ ≠ 0
⊢ IsSFiniteKernel ρCond

Tactic:
contrapose hρ

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝ : ρ.IsCondKernel ρCond
hρ : ¬IsSFiniteKernel ρCond
⊢ ρ = 0