mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_2
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ (((Kernel.id ×ₖ (const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))).map ⇑(piSingleton n) ∘ₖ
                partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map
            (_root_.IicProdIoc n (n + 1))).map
        (restrict₂ ⋯))
      x₀ =
    Measure.pi fun i ↦ μ ↑i

Tactic:
map_const,

Goal state after:
case inl.refine_2
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ (((Kernel.id ×ₖ const ((i : ↥(Iic n)) → X ↑i) (Measure.map (⇑(piSingleton n)) (μ (n + 1))) ∘ₖ
                partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map
            (_root_.IicProdIoc n (n + 1))).map
        (restrict₂ ⋯))
      x₀ =
    Measure.pi fun i ↦ μ ↑i

case inl.refine_2.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ Measurable ⇑(piSingleton n)
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
⊢ IsFiniteKernel (κ.withDensity f)

Tactic:
by_cases hf : Measurable (Function.uncurry f)

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : Measurable (Function.uncurry f)
⊢ IsFiniteKernel (κ.withDensity f)

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : ¬Measurable (Function.uncurry f)
⊢ IsFiniteKernel (κ.withDensity f)
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 ≠ ∞
⊢ IsSFiniteKernel (κ.withDensity f)

Tactic:
by_cases hf : Measurable (Function.uncurry f)

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)
⊢ IsSFiniteKernel (κ.withDensity f)

case neg
α : 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)
⊢ IsSFiniteKernel (κ.withDensity f)
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_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
⊢ κ.withDensity f = (Kernel.sum κ.seq).withDensity f

Tactic:
congr

Goal state after:
case e_κ
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
⊢ κ = Kernel.sum κ.seq
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
⊢ (η.withDensity fun a x ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) =
    ((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity fun a x ↦
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)

Tactic:
congr

Goal state after:
case e_κ
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
⊢ η = (κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal
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
⊢ ∫⁻ (c : γ) in s, κ.rnDeriv η a c ∂η a ≤ (κ a) s

Tactic:
by
  rw [setLIntegral_congr_fun_ae hs ((κ.rnDeriv_eq_rnDeriv_measure).mono (fun x hx _ ↦ hx)),
    ← withDensity_apply' _ s]
  exact (κ a).withDensity_rnDeriv_le _ _

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)
⊢ (piContent μ).IsSigmaSubadditive

Tactic:
refine isSigmaSubadditive_of_addContent_iUnion_eq_tsum
    isSetRing_measurableCylinders (fun f hf hf_Union hf' ↦ ?_)

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
f : ℕ → Set ((i : ι) → X i)
hf : ∀ (i : ℕ), f i ∈ measurableCylinders X
hf_Union : ⋃ i, f i ∈ measurableCylinders X
hf' : Pairwise (Function.onFun Disjoint f)
⊢ (piContent μ) (⋃ i, f i) = ∑' (i : ℕ), (piContent μ) (f i)
Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ⟂ₘ η a
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
have hs : MeasurableSet s := Kernel.measurableSet_mutuallySingularSet κ η

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ⟂ₘ η a
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : DependsOn f ↑(Iic b)
mf : Measurable f
x : (i : ℕ) → X i
⊢ ∀ ⦃y : (i : ℕ) → X i⦄, (∀ i ∈ ↑(Iic a), x i = y i) → lmarginalPartialTraj κ a b f x = lmarginalPartialTraj κ a b f y

Tactic:
y

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : DependsOn f ↑(Iic b)
mf : Measurable f
x y : (i : ℕ) → X i
⊢ (∀ i ∈ ↑(Iic a), x i = y i) → lmarginalPartialTraj κ a b f x = lmarginalPartialTraj κ a b f y
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case a
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
i : ι
⊢ MeasurableSet (if h : i ∈ s then t ⟨i, h⟩ else Set.univ)

Tactic:
split_ifs with hi

Goal state after:
case pos
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
i : ι
hi : i ∈ s
⊢ MeasurableSet (t ⟨i, hi⟩)

case neg
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
i : ι
hi : i ∉ s
⊢ MeasurableSet Set.univ
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 : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ (trajContent κ x₀).IsSigmaSubadditive

Tactic:
refine isSigmaSubadditive_of_addContent_iUnion_eq_tsum
    isSetRing_measurableCylinders (fun f hf hf_Union hf' ↦ ?_)

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 : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ℕ → Set ((i : ℕ) → X i)
hf : ∀ (i : ℕ), f i ∈ measurableCylinders X
hf_Union : ⋃ i, f i ∈ measurableCylinders X
hf' : Pairwise (Disjoint on f)
⊢ (trajContent κ x₀) (⋃ i, f i) = ∑' (i : ℕ), (trajContent κ x₀) (f i)
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : StandardBorelSpace β
κ : Kernel α β
inst✝¹ : IsMarkovKernel κ
inst✝ : IsDeterministic κ
f : α → β
hf : ∀ (a : α), κ a = Measure.dirac (f a)
s : Set β
hs : MeasurableSet s
x : α
⊢ x ∈ {x | f x ∈ s} ↔ x ∈ {x | s.indicator 1 (f x) = 1}

Tactic:
exact (indicator_eq_one_iff_mem ENNReal).symm

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₀ : ((η ∘ₖ κ) a) s = 0
⊢ ∫⁻ (a : β) in t, (η a) s ∂κ a = ((η ∘ₖ κ) a) s * (κ a) t

Tactic:
rw [h₀, zero_mul, setLIntegral_eq_zero_iff ht <| η.measurable_coe hs]
    rw [comp_apply' _ _ _ hs, lintegral_eq_zero_iff <| η.measurable_coe hs] at h₀
    filter_upwards [h₀] with x hx _ using hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
⊢ ∫⁻ (a : β) in t, 1 ∂κ a = (κ a) t

Tactic:
rw [setLIntegral_one]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
integral_le_kernel : ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ (κ a) t
⊢ (κ a) t - ∫⁻ (a : β) in t, (η a) s ∂κ a = ∫⁻ (b : β) in t, 1 ∂κ a - ∫⁻ (b : β) in t, (η b) s ∂κ a

Tactic:
rw [setLIntegral_one]

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 : ℕ
⊢ ((traj κ a).map fun x ↦ x (a + 1)) = κ a

Tactic:
have hf : (fun x : Π n, X n ↦ x (a + 1)) =
      (fun x ↦ x ⟨a + 1, mem_Iic.2 le_rfl⟩) ∘ frestrictLe (a + 1) := rfl
  rw [hf, map_comp_right _ (by fun_prop) (by fun_prop), traj_map_frestrictLe,
    map_partialTraj_succ_self]

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 η
⊢ ⇑((η ∘ₖ κ)†μ) =ᵐ[⇑η ∘ₘ ⇑κ ∘ₘ μ] ⇑(κ†μ ∘ₖ η†(⇑κ ∘ₘ μ))

Tactic:
rw [Measure.comp_assoc]

Goal state after:
Ω : 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 η
⊢ ⇑((η ∘ₖ κ)†μ) =ᵐ[⇑(η ∘ₖ κ) ∘ₘ μ] ⇑(κ†μ ∘ₖ η†(⇑κ ∘ₘ μ))
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: case hfg
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
θ : Θ
y : 𝓨
⊢ ℓ θ y ≤ ↑C

Tactic:
exact hℓC θ y

Goal state after:
Module: Mathlib.Probability.Decision.BayesEstimator

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝⁴ : StandardBorelSpace Θ
inst✝³ : Nonempty Θ
hl : Measurable (Function.uncurry ℓ)
P : Kernel Θ 𝓧
inst✝² : IsFiniteKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsSFiniteKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
⊢ ∫⁻ (x : Θ × 𝓨), ℓ x.1 x.2 ∂π ⊗ₘ (κ ∘ₖ P) = ∫⁻ (θy : Θ × 𝓨), ℓ θy.1 θy.2 ∂⇑(P†π ×ₖ κ) ∘ₘ ⇑P ∘ₘ π

Tactic:
congr

Goal state after:
case e_μ
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝⁴ : StandardBorelSpace Θ
inst✝³ : Nonempty Θ
hl : Measurable (Function.uncurry ℓ)
P : Kernel Θ 𝓧
inst✝² : IsFiniteKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsSFiniteKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
⊢ π ⊗ₘ (κ ∘ₖ P) = ⇑(P†π ×ₖ κ) ∘ₘ ⇑P ∘ₘ π
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 : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : AEMeasurable f ((traj κ a) x₀)
⊢ ∫⁻ (x : (n : ℕ) → X n), f x ∂Measure.map (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀) =
    ∫⁻ (x : (n : ℕ) → X n), f (updateFinset x (Iic a) x₀) ∂(traj κ a) x₀

Tactic:
MeasureTheory.lintegral_map'

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 : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : AEMeasurable f ((traj κ a) x₀)
⊢ ∫⁻ (a_1 : (i : ℕ) → X i), f (updateFinset a_1 (Iic a) x₀) ∂(traj κ a) x₀ =
    ∫⁻ (x : (n : ℕ) → X n), f (updateFinset x (Iic a) x₀) ∂(traj κ a) x₀

case hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : AEMeasurable f ((traj κ a) x₀)
⊢ AEMeasurable f (Measure.map (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀))

case hg
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : AEMeasurable f ((traj κ a) x₀)
⊢ AEMeasurable (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀)
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : 0 < ∑' (b : α), if b = a then 0 else p b
⊢ ((if a = a then p a else 0) + ∑' (b : α), if b = a then 0 else p b) =
    (∑' (b : α), if b = a then p b else 0) + ∑' (b : α), if b = a then 0 else p b

Tactic:
congr

Goal state after:
case e_a
α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : 0 < ∑' (b : α), if b = a then 0 else p b
⊢ (if a = a then p a else 0) = ∑' (b : α), if b = a then p b else 0
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0..x, r * rexp (-(r * a))

Tactic:
intervalIntegral.intervalIntegral_eq_integral_uIoc,

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) =
    (if 0 ≤ x then 1 else -1) • ∫ (x : ℝ) in uIoc 0 x, r * rexp (-(r * x)) ∂volume
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α✝ : Type u
β✝ : Type v
e : α✝ ≃ β✝
a : PMF α✝
⊢ map (⇑e.symm) (map (⇑e) a) = a

Tactic:
simp [map_comp, map_id]

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α✝ : Type u
β✝ : Type v
e : α✝ ≃ β✝
a : PMF β✝
⊢ map (⇑e) (map (⇑e.symm) a) = a

Tactic:
simp [map_comp, map_id]

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r₁ r₂ : ℝ≥0
t : ℝ
⊢ Complex.exp (↑↑r₁ * (Complex.exp (↑t * Complex.I) - 1) + ↑↑r₂ * (Complex.exp (↑t * Complex.I) - 1)) =
    Complex.exp (↑↑(r₁ + r₂) * (Complex.exp (↑t * Complex.I) - 1))

Tactic:
congr

Goal state after:
r₁ r₂ : ℝ≥0
t : ℝ
⊢ ↑↑r₁ * (Complex.exp (↑t * Complex.I) - 1) + ↑↑r₂ * (Complex.exp (↑t * Complex.I) - 1) =
    ↑↑(r₁ + r₂) * (Complex.exp (↑t * Complex.I) - 1)
Module: Mathlib.Probability.HasCondDistrib

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
P : Measure Ω
X : Ω → 𝓧
Y : Ω → 𝓨
κ : Kernel 𝓧 𝓨
inst✝¹ : SFinite P
inst✝ : IsSFiniteKernel κ
h : HasCondDistrib Y X κ P
f : 𝓨 → 𝓩
hf : Measurable f
⊢ Measure.map (fun ω ↦ (X ω, f (Y ω))) P = Measure.map (Prod.map id f ∘ fun ω ↦ (X ω, Y ω)) P

Tactic:
congr

Goal state after:
Module: Mathlib.Probability.HasLawExists

Goal state before:
pp: case h
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ infinitePi μ = infinitePi fun i ↦ map (Function.eval i) (infinitePi μ)

Tactic:
congr

Goal state after:
case h
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ μ = fun i ↦ map (Function.eval i) (infinitePi μ)
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
μ : (i : ι) → Measure (𝓧 i)
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
hm : AEMeasurable (fun ω i ↦ X i ω) P
h : HasLaw (fun ω i ↦ X i ω) (infinitePi μ) P
⊢ iIndepFun X P

Tactic:
rw [iIndepFun_iff_map_fun_eq_infinitePi_map₀ hm, h.map_eq]

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
μ : (i : ι) → Measure (𝓧 i)
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
hm : AEMeasurable (fun ω i ↦ X i ω) P
h : HasLaw (fun ω i ↦ X i ω) (infinitePi μ) P
⊢ infinitePi μ = infinitePi fun i ↦ map (X i) P
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : Nonempty α
s : Set α
inst✝ : Fintype ↑s
⊢ (uniformOfFintype α).toOuterMeasure s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)

Tactic:
by
  classical
  rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply, Fintype.card_subtype,
    Finset.card_univ]

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

Goal state before:
pp: case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : Nonempty Ω
this : m ⊓ mΩ = m
a : Ω
s : Set Ω
hs : MeasurableSet s
⊢ ((condDistrib id id μ) a) s = ((condDistrib (fun a ↦ a) id μ) a) s

Tactic:
congr

Goal state after:
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
p : Set ι → Prop
f : Filter ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ ∀ᶠ (a : ι) in f, s a ≤ ⨆ n, ⨆ (_ : n ∉ t), s n

Tactic:
exact eventually_of_mem (hf t ht) le_iSup₂

Goal state after:
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : Fintype S
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
⊢ (fun ω s ↦ X s ω) ⟂ᵢ[P] U

Tactic:
indepFun_iff_map_prod_eq_prod_map_map (aemeasurable_pi_lambda _ mX) mU

Goal state after:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : Fintype S
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
⊢ map (fun ω ↦ (fun a ↦ X a ω, U ω)) P = (map (fun c a ↦ X a c) P).prod (map U P)