mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case e_f.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun X P
this✝ : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
i : ι
⊢ MemLp id 2 (Measure.map (X i) P)

pp: case e_f.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun X P
this✝ : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
i : ι
⊢ Integrable id (Measure.map (X i) P)

Tactic:
· exact (hX1 i).isGaussian_map.memLp_two_id

Goal state after:
case e_f.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun X P
this✝ : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
i : ι
⊢ Integrable id (Measure.map (X i) P)
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
t : ℝ≥0
⊢ ∫ (x : Ω), X t x ∂P = 0

pp: case refine_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
⊢ cov[X s, X t; P] = ↑s

Tactic:
· rw [(law t).integral_eq, integral_id_gaussianReal]

Goal state after:
case refine_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
⊢ cov[X s, X t; P] = ↑s
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case refine_2.hY
Ω : 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 → ℝ)
⊢ ∀ (i : κ j),
    MemLp
      (fun ω ↦
        (starRingEnd ℝ) (((EuclideanSpace.basisFun (κ j) ℝ).repr y).ofLp i) *
          ⟪(EuclideanSpace.basisFun (κ j) ℝ) i, (toLp 2 ∘ fun ω j_1 ↦ X j j_1 ω) ω⟫)
      2 P

Tactic:
simpa using fun i ↦ ((hX.eval j).eval i).memLp_two.const_mul _

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : ↑(Ioi q)
⊢ (fun t ↦ ⨅ r', f (a, t) ↑r') ≤ᵐ[ν a] fun c ↦ f (a, c) ↑r

Tactic:
· filter_upwards [hf.bddBelow_range a] with t ht using ciInf_le (ht _) r

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

Goal state before:
pp: case hXY
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
⊢ IsGaussianProcess (Sum.elim (fun s ω ↦ B (t₀ + s) ω - B t₀ ω) fun t ↦ B ↑t) P

Tactic:
apply hB.isGaussianProcess.of_isGaussianProcess
    rintro (t | ⟨t, ht⟩)
    · exact ⟨{t₀, t₀ + t},
        { toFun x := x ⟨t₀ + t, by simp⟩ - x ⟨t₀, by simp⟩
          map_add' x y := by simp; abel
          map_smul' c x := by simp; ring }, by simp⟩
    · exact ⟨{t},
        { toFun x := x ⟨t, by simp⟩
          map_add' x y := by simp
          map_smul' c x := by simp }, by simp⟩

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 : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ r, Iic ↑r) ∂ν a = (κ a) (s ×ˢ ⋃ r, Iic ↑r)

Tactic:
prod_iUnion

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ r, Iic ↑r) ∂ν a = (κ a) (⋃ 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) ∘ₘ ⇑(Kernel.swap β α) ∘ₘ ν.prod μ = ⇑(Kernel.swap β γ) ∘ₘ ⇑(Kernel.id ∥ₖ κ) ∘ₘ ν.prod μ

Tactic:
by
      rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ✝ : Kernel α (β × Ω)
κCond✝ : Kernel (α × β) Ω
inst✝³ : Countable α
κCond : α → Kernel β Ω
inst✝² : ∀ (a : α), IsMarkovKernel (κCond a)
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
inst✝ : ∀ (a : α), (κ a).IsCondKernel (κCond a)
a : α
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), ((condKernelCountable κCond h_atom) (a, b)) (Prod.mk b ⁻¹' s) ∂κ.fst a = ((κ a).fst ⊗ₘ κCond a) s

Tactic:
condKernelCountable_apply,

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ✝ : Kernel α (β × Ω)
κCond✝ : Kernel (α × β) Ω
inst✝³ : Countable α
κCond : α → Kernel β Ω
inst✝² : ∀ (a : α), IsMarkovKernel (κCond a)
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
inst✝ : ∀ (a : α), (κ a).IsCondKernel (κCond a)
a : α
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), ((κCond a) b) (Prod.mk b ⁻¹' s) ∂κ.fst a = ((κ a).fst ⊗ₘ κCond a) s
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
⊢ ENNReal.ofReal (∫ (x : γ) in A, κ.density ν a x s ∂ν a) = (κ a) (A ×ˢ s)

Tactic:
rw [setIntegral_density hκν a hs hA, measureReal_def,
      ENNReal.ofReal_toReal (measure_ne_top _ _)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ Tendsto (fun m ↦ (κ a) (univ ×ˢ seq m)) atTop (𝓝 0)

Tactic:
have h : Tendsto (fun m ↦ κ a (univ ×ˢ seq m)) atTop
      (𝓝 ((κ a) (⋂ n, (fun m ↦ univ ×ˢ seq m) n))) := by
    apply tendsto_measure_iInter_atTop
    · measurability
    · exact antitone_const.set_prod hseq
    · exact ⟨0, measure_ne_top _ _⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
h : Tendsto (fun m ↦ (κ a) (univ ×ˢ seq m)) atTop (𝓝 ((κ a) (⋂ n, (fun m ↦ univ ×ˢ seq m) n)))
⊢ Tendsto (fun m ↦ (κ a) (univ ×ˢ seq m)) atTop (𝓝 0)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ∞
⊢ ∫ (x : α) in (fun a ↦ (X a, Y a)) ⁻¹' t ×ˢ univ, f (X x, Y x) ∂μ = ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ

Tactic:
mk_preimage_prod,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ∞
⊢ ∫ (x : α) in X ⁻¹' t ∩ Y ⁻¹' univ, f (X x, Y x) ∂μ = ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case pos
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ μ ((fun ω ↦ (X ω, ω)) ⁻¹' univ ×ˢ s) = 0

Tactic:
mk_preimage_prod,

Goal state after:
case pos
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ μ (X ⁻¹' univ ∩ (fun ω ↦ ω) ⁻¹' s) = 0
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case pos.hf
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ AEMeasurable (fun ω ↦ (X ω, ω)) μ

Tactic:
exact hX.prodMk aemeasurable_id

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
⊢ ∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x univ = 1

Tactic:
by
  have h := fun n ↦ densityProcess_fst_univ_ae κ n a
  rw [← ae_all_iff] at h
  filter_upwards [h] with x hx
  simp [density, hx]

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

Goal state before:
pp: ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ ∏' (i : ι), ((if i ∈ u ↔ i ∈ s then ↑(toNNReal p) else 0) + if i ∈ s then 0 else ↑(toNNReal (σ p))) =
    ∏ i ∈ u, if i ∈ s then ↑(toNNReal p) else ↑(toNNReal (σ p))

Tactic:
tprod_eq_prod,

Goal state after:
ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ ∏ b ∈ ?m.145, ((if b ∈ u ↔ b ∈ s then ↑(toNNReal p) else 0) + if b ∈ s then 0 else ↑(toNNReal (σ p))) =
    ∏ i ∈ u, if i ∈ s then ↑(toNNReal p) else ↑(toNNReal (σ p))

ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ ∀ b ∉ ?m.145, ((if b ∈ u ↔ b ∈ s then ↑(toNNReal p) else 0) + if b ∈ s then 0 else ↑(toNNReal (σ p))) = 1

ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ Finset ι
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᵐ[μ] Y
ω : Ω
hω : X ω = Y ω
⊢ μ[X | ?m.39] ω = μ[Y | ?m.39] ω → ((X - μ[X | m]) ^ 2) ω = ((Y - μ[Y | m]) ^ 2) ω

Tactic:
hω'

Goal state after:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᵐ[μ] Y
ω : Ω
hω : X ω = Y ω
hω' : μ[X | ?m.39] ω = μ[Y | ?m.39] ω
⊢ ((X - μ[X | m]) ^ 2) ω = ((Y - μ[Y | m]) ^ 2) ω
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᵐ[μ] Y
ω : Ω
hω : X ω = Y ω
hω' : μ[X | ?m.39] ω = μ[Y | ?m.39] ω
⊢ (Y ω - μ[X | m] ω) ^ 2 = (Y ω - μ[Y | m] ω) ^ 2

Tactic:
hω'

Goal state after:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᵐ[μ] Y
ω : Ω
hω : X ω = Y ω
hω' : μ[X | m] ω = μ[Y | m] ω
⊢ (Y ω - μ[Y | m] ω) ^ 2 = (Y ω - μ[Y | m] ω) ^ 2
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), Var[X; μ | m] x ∂μ + Var[μ[X | m]; μ] =
    ∫ (x : Ω), (μ[X ^ 2 | m] - μ[X | m] ^ 2) x ∂μ + (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), μ[X | m] x ∂μ) ^ 2)

Tactic:
congr 1
      · exact integral_congr_ae <| condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX
      · exact variance_eq_sub (hX.condExp one_le_two)

Goal state after:
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
⊢ 0 = Kernel.sum fun i ↦ 0

Tactic:
exact sum_zero.symm

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
inst✝ : ∀ (n : ℕ), SigmaFinite (μ n)
n : ℕ
s : (i : ↥(Ioc n (n + 1))) → Set (X ↑i)
hs : ∀ (i : ↥(Ioc n (n + 1))), MeasurableSet (s i)
this : Subsingleton ↥(Ioc n (n + 1))
⊢ (map (⇑(piSingleton n)) (μ (n + 1))) (Set.univ.pi s) = ∏ i, (μ ↑i) (s i)

Tactic:
rw [Fintype.prod_subsingleton _ ⟨n + 1, mem_Ioc.2 (by lia)⟩,
    Measure.map_apply (by fun_prop) (.univ_pi hs)]

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
inst✝ : ∀ (n : ℕ), SigmaFinite (μ n)
n : ℕ
s : (i : ↥(Ioc n (n + 1))) → Set (X ↑i)
hs : ∀ (i : ↥(Ioc n (n + 1))), MeasurableSet (s i)
this : Subsingleton ↥(Ioc n (n + 1))
⊢ (μ (n + 1)) (⇑(piSingleton n) ⁻¹' Set.univ.pi s) = (μ ↑⟨n + 1, ⋯⟩) (s ⟨n + 1, ⋯⟩)
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n ↦ fs n a
a : α
b : β
h_finsetSum : ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) ↑n
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → f a b = min (f a b) ↑b_1

Tactic:
exact ⟨⌈(f a b).toReal⌉₊, fun n hn => (min_eq_left (h_le a b n hn)).symm⟩

Goal state after:
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
n : ℕ
⊢ IsFiniteKernel (κ.withDensity (fs n))

Tactic:
refine isFiniteKernel_withDensity_of_bounded _ (ENNReal.coe_ne_top : ↑n + 1 ≠ ∞) fun a b => ?_

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
n : ℕ
a : α
b : β
⊢ fs n a b ≤ ↑((fun x1 x2 ↦ x1 + x2) (↑n) 1)
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
hm : MeasurableSet (κ.mutuallySingularSetSlice η a)
⊢ ((η.withDensity (κ.rnDeriv η)) a) (s \ κ.mutuallySingularSetSlice η a) + (κ a) (s ∩ κ.mutuallySingularSetSlice η a) =
    (κ a) (s ∩ κ.mutuallySingularSetSlice η a) + (κ a) (s \ κ.mutuallySingularSetSlice η a)

Tactic:
withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice (hs.diff hm)
      (sdiff_subset_iff.mpr (by simp)),

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
hm : MeasurableSet (κ.mutuallySingularSetSlice η a)
⊢ (κ a) (s \ κ.mutuallySingularSetSlice η a) + (κ a) (s ∩ κ.mutuallySingularSetSlice η a) =
    (κ a) (s ∩ κ.mutuallySingularSetSlice η a) + (κ a) (s \ κ.mutuallySingularSetSlice η a)
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this : (κ a) s * (κ a) s = (κ a) s
hκ : (κ a) s = 0
⊢ (κ a) s = 0 ∨ (κ a) s = 1

Tactic:
simp [hκ]

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a n : ℕ
η : Kernel ((i : ↥(Iic a)) → X ↑i) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe b) = partialTraj κ a b
⊢ η = traj κ a

Tactic:
by
  ext x : 1
  refine ((isProjectiveLimit_trajFun _ _ _).unique ?_).symm
  rw [isProjectiveLimit_nat_iff' _ _ n]
  · intro k hk
    rw [inducedFamily_Iic, ← map_apply _ (measurable_frestrictLe k), hη k hk]
  · exact isProjectiveMeasureFamily_partialTraj κ x

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst✝ : IsFiniteKernel η
⊢ ⇑(η ∥ₖ Kernel.id) ∘ₘ ⇑(κ ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ =
    ⇑(Kernel.swap Ω 𝓨) ∘ₘ ⇑(Kernel.id ∥ₖ η) ∘ₘ ⇑(Kernel.id ∥ₖ κ) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ

Tactic:
simp_rw [Measure.comp_assoc]
    conv_rhs => rw [← Kernel.comp_assoc]
    rw [Kernel.swap_parallelComp, Kernel.comp_assoc, ← Kernel.comp_assoc (Kernel.swap Ω 𝓧),
      Kernel.swap_parallelComp, Kernel.comp_assoc, Kernel.swap_copy]

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
| (fun x i ↦ x ⟨↑i, ⋯⟩) ∘ (Set.Ioi a).domRestrict

Tactic:
change (Ioc a b).restrict

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
| (Ioc a b).restrict
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝² : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝¹ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝ : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
hf : AEStronglyMeasurable f ((traj κ a) x₀)
⊢ ∀ᵐ (x : (i : ↥(Iic b)) → X ↑i) ∂(partialTraj κ a b) x₀, AEStronglyMeasurable f ((traj κ b) x)

Tactic:
rw [← traj_comp_partialTraj hab] at hf
  exact hf.comp

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
⊢ (partialTraj κ a b) u ⊗ₘ traj κ b = Measure.map (fun x ↦ (frestrictLe b x, x)) ((traj κ a) u)

Tactic:
ext s ms
  rw [Measure.map_apply, Measure.compProd_apply, ← traj_comp_partialTraj hab, comp_apply']
  · congr 1 with x
    rw [← traj_map_updateFinset, Measure.map_apply, Measure.map_apply]
    · congr 1 with y
      simp only [Set.mem_preimage]
      congrm (fun i ↦ ?_, fun i ↦ ?_) ∈ s <;> simp [updateFinset]
    any_goals fun_prop
    all_goals exact ms.preimage (by fun_prop)
  any_goals exact ms.preimage (by fun_prop)
  fun_prop

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

Goal state before:
pp: n : ℕ
p : ↑I
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℕ → E
⊢ ∫ (x : ℕ), f x ∂Bin(n, p) = ∑ k ≤ n, (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • f k

Tactic:
by
  rw [binomial_eq_sum_dirac, integral_finsetSum_measure]
  · simp
  exact fun _ _ ↦ (integrable_dirac (by simp)).smul_measure (by simp)

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

Goal state before:
pp: E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
hμs : μ s = 0 ∨ μ s = ∞
⊢ pdf X ℙ μ =ᵐ[μ] 0

Tactic:
rcases hμs with H | H
  · simp only [IsUniform, ProbabilityTheory.cond, H, ENNReal.inv_zero, restrict_eq_zero.mpr H,
    smul_zero] at hu
    simp [pdf, hu]
  · simp only [IsUniform, ProbabilityTheory.cond, H, ENNReal.inv_top, zero_smul] at hu
    simp [pdf, hu]

Goal state after: