mathlib-initiative/mathlib-tactics huggingface dataset:
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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X ↑i)
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
⊢ ∫⁻ (a : (i : ↥(Iic b)) → X ↑i), S.indicator 1 a ∂(partialTraj κ a b) (frestrictLe a x₀) =
    ∫⁻ (z : (i : ↥(Iic b)) → X ↑i),
      (cylinder (Iic b) S).indicator 1 (updateFinset x₀ (Iic b) z) ∂(partialTraj κ a b) (frestrictLe a x₀)

Tactic:
]

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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X ↑i)
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
⊢ ∫⁻ (a : (i : ↥(Iic b)) → X ↑i), S.indicator 1 a ∂(partialTraj κ a b) (frestrictLe a x₀) =
    ∫⁻ (z : (i : ↥(Iic b)) → X ↑i),
      (cylinder (Iic b) S).indicator 1 (updateFinset x₀ (Iic b) z) ∂(partialTraj κ a b) (frestrictLe a x₀)
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
⊢ ENNReal.ofReal (↑(u.ncard.choose k) * ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)) =
    ENNReal.ofReal (↑(u.ncard.choose k) * ↑p ^ k * (1 - ↑p) ^ (u.ncard - k))

Tactic:
]

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

Goal state before:
pp: case e_f
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
b : ℕ
S : Set ((i : ↥(Iic b)) → X ↑i)
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
x : (i : ↥(Iic b)) → X ↑i
⊢ x ∈ S ↔ (Iic b).restrict (updateFinset x₀ (Iic b) x) ∈ S

Tactic:
]

Goal state after:
case e_f
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
b : ℕ
S : Set ((i : ↥(Iic b)) → X ↑i)
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
x : (i : ↥(Iic b)) → X ↑i
⊢ x ∈ S ↔ (Iic b).restrict (updateFinset x₀ (Iic b) x) ∈ S
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
p : ↑I
inst✝ : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
⊢ setBer(∅, p) {s_1 | s_1 ∈ s ∧ s_1 ⊆ ∅} = (dirac ∅) s

Tactic:
]

Goal state after:
ι : Type u_1
p : ↑I
inst✝ : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
⊢ setBer(∅, p) {s_1 | s_1 ∈ s ∧ s_1 ⊆ ∅} = (dirac ∅) s
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: case neg
ι : Type u_1
p : ↑I
inst✝ : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
h : ∅ ∉ s
this : {t | t ∈ s ∧ t ⊆ ∅} = ∅
⊢ setBer(∅, p) ∅ = (dirac ∅) s

Tactic:
]

Goal state after:
case neg
ι : Type u_1
p : ↑I
inst✝ : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
h : ∅ ∉ s
this : {t | t ∈ s ∧ t ⊆ ∅} = ∅
⊢ setBer(∅, p) ∅ = (dirac ∅) s
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case refine_1
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X ↑i)
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ I \ J
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case refine_2
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X ↑i)
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ J
⊢ (μ ↑⟨x, hx⟩) (s ⟨x, hx⟩) = (μ ↑⟨x, ⋯⟩) (s ⟨↑⟨x, ⋯⟩, hx⟩)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs

Goal state before:
pp: V : Type u_1
p : ↑I
inst✝ : Countable V
S : Set (SimpleGraph V)
⊢ setBer(Sym2.diagSetᶜ, p) (edgeSet '' S) = setBer(Sym2.diagSetᶜ, p) (edgeSet '' S)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs

Goal state before:
pp: case intro
V : Type u_1
p : ↑I
inst✝ : Finite V
G : SimpleGraph V
val✝ : Fintype V
⊢ ↑(toNNReal p) ^ G.edgeSet.ncard * ↑(toNNReal (σ p)) ^ (Sym2.diagSetᶜ.ncard - G.edgeSet.ncard) =
    ↑(toNNReal p) ^ G.edgeSet.ncard * ↑(toNNReal (σ p)) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)

Tactic:
]

Goal state after:
case intro
V : Type u_1
p : ↑I
inst✝ : Finite V
G : SimpleGraph V
val✝ : Fintype V
⊢ ↑(toNNReal p) ^ G.edgeSet.ncard * ↑(toNNReal (σ p)) ^ (Sym2.diagSetᶜ.ncard - G.edgeSet.ncard) =
    ↑(toNNReal p) ^ G.edgeSet.ncard * ↑(toNNReal (σ p)) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι := { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
this : s = cylinder univ (⇑(piCongrLeft X e) ⁻¹' s)
⊢ (piContent μ) (cylinder univ (⇑(piCongrLeft X e) ⁻¹' s)) = (Measure.pi μ) s

Tactic:
]

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι := { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
this : s = cylinder univ (⇑(piCongrLeft X e) ⁻¹' s)
⊢ (piContent μ) (cylinder univ (⇑(piCongrLeft X e) ⁻¹' s)) = (Measure.pi μ) s
Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs

Goal state before:
pp: case intro
V : Type u_1
p : ↑I
inst✝ : Finite V
G : SimpleGraph V
val✝ : Fintype V
⊢ Nat.card ↑Sym2.diagSetᶜ = Nat.card ↑Sym2.diagSetᶜ

Tactic:
]

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : ¬m ≤ m₀
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
hm : m ≤ m₀
X : Ω → ℝ
μ : Measure Ω
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 = 0

Tactic:
]

Goal state after:
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] ω = μ[Y | m] ω
⊢ (Y ω - μ[Y | m] ω) ^ 2 = (Y ω - μ[Y | m] ω) ^ 2

Tactic:
]

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] = μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m]

Tactic:
]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι := { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
this : s = cylinder univ (⇑(piCongrLeft X e) ⁻¹' s)
⊢ (Measure.map (⇑(piCongrLeft X { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }))
        (Measure.pi fun i ↦ μ ↑i))
      s =
    (Measure.map (⇑(piCongrLeft (fun i ↦ X i) e)) (Measure.pi fun i ↦ μ (e i))) s

Tactic:
]

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι := { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
this : s = cylinder univ (⇑(piCongrLeft X e) ⁻¹' s)
⊢ (Measure.map (⇑(piCongrLeft X { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }))
        (Measure.pi fun i ↦ μ ↑i))
      s =
    (Measure.map (⇑(piCongrLeft (fun i ↦ X i) e)) (Measure.pi fun i ↦ μ (e i))) s
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case inl
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (f n) ↑(Iic (a n))
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto : ∀ (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X ↑i
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (f n) (updateFinset x (Iic k) y)
x✝ : ∀ (n : ℕ), Nonempty (X n)
F : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (l x))
x : (n : ℕ) → X n
n : ℕ
h : k + 1 < a n
⊢ lmarginalPartialTraj κ k k.succ (lmarginalPartialTraj κ k.succ (a n) (f n)) x =
    lmarginalPartialTraj κ k (k + 1) (lmarginalPartialTraj κ (k + 1) (a n) (f n)) x

Tactic:
]

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
⊢ Integrable (2 * (X * μ[X | m])) μ

Tactic:
]

Goal state after:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
⊢ Integrable (2 * (X * μ[X | m])) μ
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
⊢ IsProbabilityMeasure (⇑(traj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) 0) ∘ₘ Measure.pi fun i ↦ μ ↑i)

Tactic:
]

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
⊢ IsProbabilityMeasure (⇑(traj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) 0) ∘ₘ Measure.pi fun i ↦ μ ↑i)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
⊢ (∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x) *
      ∏ x ∈ Ioc b c, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    (∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x) *
      ∏ x ∈ Ioc b c, Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x

Tactic:
]

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
⊢ (∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x) *
      ∏ x ∈ Ioc b c, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    (∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x) *
      ∏ x ∈ Ioc b c, Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2 = μ[X ^ 2 | m] - μ[X | m] ^ 2

Tactic:
by ring

Goal state after:
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 : Ω), (X ^ 2) x ∂μ - ∫ (a : Ω), (μ[X | m] ^ 2) a ∂μ +
      (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2) =
    ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ +
      (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2)

pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ Integrable (μ[X | m] ^ 2) μ

Tactic:
]

Goal state after:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ Integrable (μ[X | m] ^ 2) μ
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case inr.inl
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (f n) ↑(Iic (a n))
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto : ∀ (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X ↑i
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (f n) (updateFinset x (Iic k) y)
x✝ : ∀ (n : ℕ), Nonempty (X n)
F : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (l x))
x : (n : ℕ) → X n
n : ℕ
h : k + 1 = a n
⊢ lmarginalPartialTraj κ k (k + 1) (f n) x = lmarginalPartialTraj κ k (k + 1) (f n) x

Tactic:
]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc a b
⊢ (μ ↑⟨x, ⋯⟩) (s ⟨x, ⋯⟩) = (μ ↑⟨x, hx⟩) (s ⟨↑⟨x, hx⟩, ⋯⟩)

Tactic:
]

Goal state after:
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 : Ω), (X ^ 2) x ∂μ - ∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ +
      (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2) =
    ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2

Tactic:
]

Goal state after:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ +
      (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2) =
    ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc b c
⊢ (μ ↑⟨x, ⋯⟩) (s ⟨x, ⋯⟩) = (μ ↑⟨x, hx⟩) (s ⟨↑⟨x, hx⟩, ⋯⟩)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:
pp: case inl
Ω : Type u_1
m₀ : MeasurableSpace Ω
X : Ω → ℝ
⊢ Var[X; 0 | ⊥] =ᶠ[⊥] fun x ↦ ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂0) ^ 2 ∂0

Tactic:
]

Goal state after:
case inl
Ω : Type u_1
m₀ : MeasurableSpace Ω
X : Ω → ℝ
⊢ Var[X; 0 | ⊥] =ᶠ[⊥] fun x ↦ ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂0) ^ 2 ∂0
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
⊢ μ[(c • X - μ[c • X | m]) ^ 2 | m] =ᵐ[μ] μ[c ^ 2 • (X - μ[X | m]) ^ 2 | m]

Tactic:
]

Goal state after:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
⊢ μ[(c • X - μ[c • X | m]) ^ 2 | m] =ᵐ[μ] μ[c ^ 2 • (X - μ[X | m]) ^ 2 | m]
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
⊢ (∏ x ≤ a, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x) *
      ∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    (∏ x ≤ a, Function.extend Subtype.val (fun i ↦ (μ ↑i) (frestrictLe₂ hab s i)) 1 x) *
      ∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x

Tactic:
]

Goal state after:
case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
⊢ (∏ x ≤ a, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x) *
      ∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    (∏ x ≤ a, Function.extend Subtype.val (fun i ↦ (μ ↑i) (frestrictLe₂ hab s i)) 1 x) *
      ∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
⊢ { toFun := fun a ↦ (κ a).withDensity (f a), measurable' := ⋯ } a = (κ a).withDensity (f a)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
⊢ { toFun := fun a ↦ (κ a).withDensity (f a), measurable' := ⋯ } a = (κ a).withDensity (f a)
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
s : Set β
⊢ ∫⁻ (a_1 : β) in s, f a a_1 ∂κ a = ∫⁻ (b : β) in s, f a b ∂κ a

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), f a =ᵐ[κ a] g a
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ a).withDensity (g a)) s✝ = ((κ a).withDensity (g a)) s✝

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : Measurable (Function.uncurry f)
⊢ (κ a).withDensity (f a) ≪ κ a

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : Measurable (Function.uncurry f)
⊢ (κ a).withDensity (f a) ≪ κ a
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Iic a
⊢ (μ ↑⟨x, ⋯⟩) (s ⟨x, ⋯⟩) = (μ ↑⟨x, hx⟩) (s ⟨↑⟨x, hx⟩, ⋯⟩)

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : ¬Measurable (Function.uncurry f)
⊢ 0 a ≪ κ a

Tactic:
]

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : ¬Measurable (Function.uncurry f)
⊢ 0 a ≪ κ a
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ a✝¹).withDensity (1 a✝¹)) s✝ = (κ a✝¹) s✝

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ a✝¹).withDensity (1 a✝¹)) s✝ = (κ a✝¹) s✝
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ a✝¹).withDensity (0 a✝¹)) s✝ = (0 a✝¹) s✝

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ a✝¹).withDensity (0 a✝¹)) s✝ = (0 a✝¹) s✝
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc a b
⊢ (μ ↑⟨x, ⋯⟩) (s ⟨x, ⋯⟩) = (μ ↑⟨x, hx⟩) (s ⟨↑⟨x, hx⟩, ⋯⟩)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
g : β → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (a_1 : β), (f a * g) a_1 ∂κ a = ∫⁻ (b : β), f a b * g b ∂κ a

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
g : β → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (a_1 : β), (f a * g) a_1 ∂κ a = ∫⁻ (b : β), f a b * g b ∂κ a
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : β → E
inst✝ : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ ∫ (x : β), g a x • f x ∂κ a = ∫ (b : β), g a b • f b ∂κ a

pp: case f_meas
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : β → E
inst✝ : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ Measurable (g a)

pp: case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : β → E
inst✝ : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ Measurable (Function.uncurry fun a b ↦ ↑(g a b))

Tactic:
]

Goal state after:
case f_meas
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : β → E
inst✝ : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ Measurable (g a)

case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : β → E
inst✝ : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ Measurable (Function.uncurry fun a b ↦ ↑(g a b))