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

Goal state before:
pp: case refine_2.a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨆ y ∈ Y, f a y ≤ f a b

Tactic:
exact le_trans h (iInf₂_le a ha)

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

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
⊢ sSup {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = sSup ↑P ⊓ sSup ↑Q

Tactic:
rw [sSup_inf_sSup]

Goal state after:
α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
⊢ sSup {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = ⨆ p ∈ ↑P ×ˢ ↑Q, p.1 ⊓ p.2
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
s u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun f
hs : u ⊆ s
⊢ f '' s ⊆ s

Tactic:
by
  rintro _ ⟨a, haS, rfl⟩
  by_cases ha : a ∈ u
  · exact hs <| hf.apply_mem ha
  exact (hf.apply_of_notMem ha).symm ▸ haS

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

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
⊢ f a = f b ↔ a = b ∨ P.Rel a b

Tactic:
simp only [or_iff_not_imp_left, ← ne_eq]

Goal state after:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
⊢ f a = f b ↔ a ≠ b → P.Rel a b
Module: Mathlib.Order.ScottContinuity.Complete

Goal state before:
pp: β : Type u_2
inst✝ : CompleteLinearOrder β
b : β
d : Set β
x✝¹ : d.Nonempty
x✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
⊢ min (sSup d) b = sSup ((fun a ↦ min a b) '' d)

Tactic:
by rw [sSup_inf_eq, sSup_image]

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a : X
b : ↥S
⊢ S.restrictAux a ≤ b ↔ a ≤ ↑b

Tactic:
by
    constructor <;> intro h
    · exact le_trans (by simp +contextual [restrictAux]) h
    · exact sInf_le (by simp [h])

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
ω : Ω
h₁ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ∞
⊢ liminf (fun n ↦ ‖f n ω‖ₑ) atTop < ∞ → ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)

Tactic:
h₂

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
ω : Ω
h₁ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ∞
h₂ : liminf (fun n ↦ ‖f n ω‖ₑ) atTop < ∞
⊢ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
⊢ u (min (↑(min (↑i) (σ ω)).untopA) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω

Tactic:
by_cases hτ : τ ω = ⊤

Goal state after:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : τ ω = ⊤
⊢ u (min (↑(min (↑i) (σ ω)).untopA) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω

case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
⊢ u (min (↑(min (↑i) (σ ω)).untopA) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ μ.real Set.univ ≠ 0

Tactic:
· rw [Ne, measureReal_eq_zero_iff, Measure.measure_univ_eq_zero]
    simp only [hμ, not_false_iff]

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

Goal state before:
pp: case mpr
Ω : 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 : c ∈ lowerBounds (Set.range fun n ↦ f n ω✝)
ω : ℝ
hω : ω ∈ Set.range fun n ↦ (-f) n ω✝
⊢ ω ≤ -c

Tactic:
mem_lowerBounds

Goal state after:
case mpr
Ω : 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 ω✝, c ≤ x
ω : ℝ
hω : ω ∈ Set.range fun n ↦ (-f) n ω✝
⊢ ω ≤ -c
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : v ≠ 0
h : ENNReal.ofReal (∫ (x : ℝ), gaussianPDFReal μ v x) = ENNReal.ofReal 1
⊢ ∫ (x : ℝ), gaussianPDFReal μ v x = 1

Tactic:
← ENNReal.ofReal_eq_ofReal_iff (integral_nonneg (gaussianPDFReal_nonneg _ _)) zero_le_one

Goal state after:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
h : ENNReal.ofReal (∫ (x : ℝ), gaussianPDFReal μ v x) = ENNReal.ofReal 1
⊢ ENNReal.ofReal (∫ (x : ℝ), gaussianPDFReal μ v x) = ENNReal.ofReal 1
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case refine_1
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√↑v)⁻¹ * (√(2 * π))⁻¹ = |c| * (√(2 * π * (c ^ 2 * ↑v)))⁻¹

Tactic:
simp (disch := positivity) only [Real.sqrt_mul, mul_inv_rev, field]

Goal state after:
case refine_1
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ √(c ^ 2) / √↑v = |c| / √↑v
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
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ ((covarianceBilin (Measure.map (⇑L) μ)) u) v =
    ((covarianceBilin μ) ((ContinuousLinearMap.adjoint L) u)) ((ContinuousLinearMap.adjoint L) v)

Tactic:
covarianceBilin_apply,

Goal state after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ ∫ (z : F),
      ⟪u, z - ∫ (x : F), id x ∂Measure.map (⇑L) μ⟫ * ⟪v, z - ∫ (x : F), id x ∂Measure.map (⇑L) μ⟫ ∂Measure.map (⇑L) μ =
    ((covarianceBilin μ) ((ContinuousLinearMap.adjoint L) u)) ((ContinuousLinearMap.adjoint L) v)

case h
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ MemLp id 2 (Measure.map (⇑L) μ)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂
⊢ μ₁ = μ₂ ∧ v₁ = v₂

Tactic:
rw [← integral_id_gaussianReal (μ := μ₁) (v := v₁),
    ← integral_id_gaussianReal (μ := μ₂) (v := v₂), h]

Goal state after:
μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂
⊢ ∫ (x : ℝ), x ∂gaussianReal μ₂ v₂ = ∫ (x : ℝ), x ∂gaussianReal μ₂ v₂ ∧ v₁ = v₂
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this✝ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
h✝ : ‖c‖ / 2 ≤ ‖y‖
⊢ 2 * ‖c‖ ^ (↑p - 1) * ‖y‖ + 0 ≤ 2 * ‖c‖ ^ (↑p - 1) * ‖y‖ + 2 ^ ↑p * ‖y - c‖ ^ ↑p

Tactic:
gcongr; positivity

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

Goal state before:
pp: case e_a
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 < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ n =
    ENNReal.ofReal (rexp (2 ^ n * Real.log (μ {x | ‖x‖ ≤ a} / (1 - μ {x | ‖x‖ ≤ a})).toReal⁻¹))

Tactic:
← Real.log_rpow (by positivity),

Goal state after:
case e_a
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 < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ n =
    ENNReal.ofReal (rexp (Real.log ((μ {x | ‖x‖ ≤ a} / (1 - μ {x | ‖x‖ ≤ a})).toReal⁻¹ ^ 2 ^ n)))
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
  f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
    (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
this : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((g L) L) / 2)
hg : g.toBilinForm.IsPosSemidef
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilin μ

Tactic:
have := gaussian_charFunDual_congr hg this

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
  f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
    (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
this✝ : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((g L) L) / 2)
hg : g.toBilinForm.IsPosSemidef
this : m = ∫ (x : E), x ∂μ ∧ g = covarianceBilinDual μ
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilin μ
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic

Goal state before:
pp: case inl
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
hX : HasIndepIncrements X P
t : ℕ → T
ht : Monotone t
this : IsProbabilityMeasure P
⊢ iIndepFun (∅.restrict fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P

Tactic:
exact iIndepFun.of_subsingleton

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
hX : HasIndepIncrements X P
r s t : T
hrs : r ≤ s
hst : s ≤ t
⊢ (X s - X r) ⟂ᵢ[P] X t - X s

Tactic:
let τ : ℕ → T
    | 0 => r
    | 1 => s
    | _ => t
  exact hX.nat (t := τ) (fun _ ↦ by grind) |>.indepFun (by grind : 0 ≠ 1)

Goal state after:
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✝ : NormedSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
⊢ charFunDual (Measure.map (X + Y) P) = charFunDual (Measure.map X P) * charFunDual (Measure.map Y P)

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

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

Goal state before:
pp: case hv
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
⊢ (covarianceBilin
        (Measure.map (⇑(PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm)
          (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P))).toBilinForm =
    (covarianceBilin (Measure.map (⇑(PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm) (projectiveFamily I))).toBilinForm

Tactic:
refine LinearMap.BilinForm.ext_of_isSymm isPosSemidef_covarianceBilin.isSymm
        isPosSemidef_covarianceBilin.isSymm fun x ↦ ?_

Goal state after:
case hv
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
⊢ ((covarianceBilin
            (Measure.map (⇑(PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm)
              (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P))).toBilinForm
        x)
      x =
    ((covarianceBilin (Measure.map (⇑(PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm) (projectiveFamily I))).toBilinForm
        x)
      x
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case pos
α : 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
⊢ 0 = (κ a) (s ×ˢ Iic x)

Tactic:
have ⟨q, hq⟩ := exists_rat_gt x

Goal state after:
case pos
α : 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
⊢ 0 = (κ a) (s ×ˢ Iic x)
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1
qs : ℝ → ℚ := fun x ↦ ⋯.choose
hqs_tendsto : Tendsto qs atBot atBot
x : ℝ
⊢ ↑(hf.stieltjesFunction a) x ≤ f a (qs x)

Tactic:
← stieltjesFunction_eq hf

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1
qs : ℝ → ℚ := fun x ↦ ⋯.choose
hqs_tendsto : Tendsto qs atBot atBot
x : ℝ
⊢ ↑(hf.stieltjesFunction a) x ≤ ↑(hf.stieltjesFunction a) ↑(qs x)
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x ↦ ⋯.choose
hqs_tendsto : Tendsto qs atTop atTop
x : ℝ
⊢ f a (qs x) ≤ ↑(hf.stieltjesFunction a) x

Tactic:
← stieltjesFunction_eq hf

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x ↦ ⋯.choose
hqs_tendsto : Tendsto qs atTop atTop
x : ℝ
⊢ ↑(hf.stieltjesFunction a) ↑(qs x) ≤ ↑(hf.stieltjesFunction a) x
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
t : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ ⨅ r, (ρ.IicSnd ↑↑r) s = (ρ.IicSnd ↑t) s

Tactic:
ρ.IicSnd_apply _ hs,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
t : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ ⨅ r, ρ (s ×ˢ Iic ↑↑r) = ρ (s ×ˢ Iic ↑t)
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun r ↦ (ρ.IicSnd ↑r) s) atTop (𝓝 (ρ.fst s))

Tactic:
ρ.IicSnd_apply _ hs,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑r)) atTop (𝓝 (ρ.fst s))
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
this : ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, (preCDF ρ r * 1) x ∂ρ.fst
⊢ Measurable 1

Tactic:
rw [Pi.one_def]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
this : ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, (preCDF ρ r * 1) x ∂ρ.fst
⊢ Measurable fun x ↦ 1
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a✝ : Unit
r r' : ℚ
hrr' : r ≤ r'
a : α
h₁ : Monotone fun r ↦ preCDF ρ r a
⊢ (∀ (r : ℚ), preCDF ρ r a ≤ 1) → (preCDF ρ r a).toReal ≤ (preCDF ρ r' a).toReal

Tactic:
h₂

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a✝ : Unit
r r' : ℚ
hrr' : r ≤ r'
a : α
h₁ : Monotone fun r ↦ preCDF ρ r a
h₂ : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ (preCDF ρ r a).toReal ≤ (preCDF ρ r' a).toReal
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case hsm
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ∀ (i : { r' // t < r' }), NullMeasurableSet (s ×ˢ Iic ↑↑i) ρ

pp: case hfin
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ∃ i, ρ (s ×ˢ Iic ↑↑i) ≠ ∞

Tactic:
· exact fun _ => (hs.prod measurableSet_Iic).nullMeasurableSet

Goal state after:
case hfin
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ∃ i, ρ (s ×ˢ Iic ↑↑i) ≠ ∞
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝² : SFinite μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
h1 : (⇑κ ∘ₘ μ).prod ν = map Prod.swap (ν.prod (⇑κ ∘ₘ μ))
⊢ ⇑(κ ∥ₖ Kernel.id) ∘ₘ map Prod.swap (ν.prod μ) = ⇑(κ ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.swap β α) ∘ₘ ν.prod μ

Tactic:
rw [Kernel.swap, Measure.deterministic_comp_eq_map]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝² : SFinite μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
h1 : (⇑κ ∘ₘ μ).prod ν = map Prod.swap (ν.prod (⇑κ ∘ₘ μ))
⊢ ⇑(Kernel.swap β γ) ∘ₘ ⇑(Kernel.id ∥ₖ κ) ∘ₘ ν.prod μ = map Prod.swap (⇑(Kernel.id ∥ₖ κ) ∘ₘ ν.prod μ)

Tactic:
rw [Kernel.swap, Measure.deterministic_comp_eq_map]

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
⊢ HasLaw (fun ω ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'

Tactic:
convert! gaussianReal_div_const hY _

Goal state after:
case e'_6.e'_1
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
⊢ 0 = 0 / √Var[X 0; P]

case e'_6.e'_2
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
⊢ 1 = Var[X 0; P].toNNReal / NNReal.mk (√Var[X 0; P] ^ 2) ⋯
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
⊢ μ ⊗ₘ κ.map f = map (Prod.map id f) (μ ⊗ₘ κ)

Tactic:
by
  calc μ ⊗ₘ (κ.map f)
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.id ×ₖ κ) ∘ₘ μ := by
    rw [comp_assoc, Kernel.parallelComp_comp_prod, compProd_eq_comp_prod,
      Kernel.id_comp, Kernel.deterministic_comp_eq_map]
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (μ ⊗ₘ κ) := by rw [compProd_eq_comp_prod]
  _ = (μ ⊗ₘ κ).map (Prod.map id f) := by
    rw [Kernel.id, Kernel.deterministic_parallelComp_deterministic, deterministic_comp_eq_map]

Goal state after: