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 ∘ₖ partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n ×ₖ
                const ((i : ↥(Iic a)) → X ↑i) (Measure.map (⇑(piSingleton n)) (μ (n + 1)))).map
            (_root_.IicProdIoc n (n + 1))).map
        (restrict₂ ⋯))
      x₀ =
    Measure.pi fun i ↦ μ ↑i

pp: 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)

Tactic:
id_comp,

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
⊢ (((partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n ×ₖ
                const ((i : ↥(Iic a)) → X ↑i) (Measure.map (⇑(piSingleton n)) (μ (n + 1)))).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.RadonNikodym

Goal state before:
pp: case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝ : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : (∂κ a/∂η a) x ≤ 1 x
hα : Countable α
⊢ (∂κ a/∂η a) x ≤ ENNReal.ofReal (1 x)

Tactic:
simp only [Pi.one_apply, ENNReal.ofReal_one]

Goal state after:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝ : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : (∂κ a/∂η a) x ≤ 1 x
hα : Countable α
⊢ (∂κ a/∂η a) x ≤ 1
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)
s : Finset ℕ
S : Set ((i : ↥s) → X ↑i)
mS : MeasurableSet S
hA : cylinder s S ∈ measurableCylinders X
⊢ (piContent μ) (cylinder s S) = (infinitePiNat μ) (cylinder s S)

Tactic:
rw [piContent_cylinder _ mS, cylinder, ← map_apply (measurable_restrict _) mS,
    infinitePiNat_map_restrict]

Goal state after:
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
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
h_le : κ ≤ κ + η
x : γ
hx : κ.rnDerivAux (κ + η) a x ≤ 1 x
⊢ x ∈ s → ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x = 1

Tactic:
hxs

Goal state after:
α : 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
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
h_le : κ ≤ κ + η
x : γ
hx : κ.rnDerivAux (κ + η) a x ≤ 1 x
hxs : x ∈ s
⊢ ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x = 1
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 : α
h : κ a ≪ η a
⊢ ∀ᵐ (x : γ) ∂κ a, 0 < (κ.rnDeriv η a x).toReal

Tactic:
filter_upwards [rnDeriv_pos h, h.ae_le (rnDeriv_ne_top κ _)] with x h0 htop
  simp_all only [pos_iff_ne_zero, ne_eq, ENNReal.toReal_pos, not_false_eq_true]

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

Goal state before:
pp: case refine_2
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn f ↑(Iic a)
hab : a ≤ b
x : (n : ℕ) → X n
y : (i : ↥(Ioc b c)) → X ↑i
i : ℕ
hi : i ∈ ↑(Iic a)
⊢ Function.updateFinset x (Ioc b c) y i = x i

Tactic:
simp_all only [coe_Iic, Set.mem_Iic, Function.updateFinset, mem_Ioc, dite_eq_right_iff]
    lia

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

Goal state before:
pp: case hg
α : 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
⊢ Measurable fun b ↦ (η b) s

pp: case hg_fin
α : 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 : β) in t, (η a) s ∂κ a ≠ ⊤

pp: case h_le
α : 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
⊢ (fun b ↦ (η b) s) ≤ᵐ[(κ a).restrict t] fun b ↦ 1

Tactic:
· exact η.measurable_coe hs

Goal state after:
case hg_fin
α : 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 : β) in t, (η a) s ∂κ a ≠ ⊤

case h_le
α : 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
⊢ (fun b ↦ (η b) s) ≤ᵐ[(κ a).restrict t] fun b ↦ 1
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Countable ι
t : (i : ι) → Set (X i)
mt : ∀ (i : ι), MeasurableSet (t i)
⊢ Countable ↑Set.univ

pp: case mt
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Countable ι
t : (i : ι) → Set (X i)
mt : ∀ (i : ι), MeasurableSet (t i)
⊢ ∀ i ∈ Set.univ, MeasurableSet (t i)

Tactic:
· simpa [Set.countable_univ_iff]

Goal state after:
case mt
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Countable ι
t : (i : ι) → Set (X i)
mt : ∀ (i : ι), MeasurableSet (t i)
⊢ ∀ i ∈ Set.univ, MeasurableSet (t i)
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✝¹ : IsMarkovKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
⊢ ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂⇑P ∘ₘ π ≤ avgRisk ℓ P κ π

Tactic:
avgRisk_eq_lintegral_lintegral_lintegral hl

Goal state after:
Θ : 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✝¹ : IsMarkovKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
⊢ ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂⇑P ∘ₘ π ≤
    ∫⁻ (x : 𝓧), ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂κ x ∂⇑P ∘ₘ π
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∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝³ : StandardBorelSpace Θ
inst✝² : Nonempty Θ
f : 𝓧 → 𝓨
inst✝¹ : IsFiniteKernel P
inst✝ : IsFiniteMeasure π
hf : IsArgminEstimator ℓ P π f
hl : Measurable (Function.uncurry ℓ)
⊢ avgRisk ℓ P hf.kernel π = ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂⇑P ∘ₘ π

Tactic:
avgRisk_eq_lintegral_lintegral_lintegral hl

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝³ : StandardBorelSpace Θ
inst✝² : Nonempty Θ
f : 𝓧 → 𝓨
inst✝¹ : IsFiniteKernel P
inst✝ : IsFiniteMeasure π
hf : IsArgminEstimator ℓ P π f
hl : Measurable (Function.uncurry ℓ)
⊢ ∫⁻ (x : 𝓧), ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂hf.kernel x ∂⇑P ∘ₘ π =
    ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂⇑P ∘ₘ π
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫ (a : ℝ) in Icc 0 x, r * rexp (-(r * a)) ∂volume = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal

Tactic:
have : ∫ a in uIoc 0 x, r * rexp (-(r * a)) = ∫ a in 0..x, r * rexp (-(r * a)) := by
        rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_eq_mul, if_pos h, one_mul]

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0..x, r * rexp (-(r * a))
⊢ ∫ (a : ℝ) in Icc 0 x, r * rexp (-(r * a)) ∂volume = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r : ℝ≥0
t : ℝ
⊢ ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • cexp (↑(inner ℝ (↑n) t) * I) = cexp (↑↑r * (cexp (↑t * I) - 1))

Tactic:
Real.inner_apply

Goal state after:
r : ℝ≥0
t : ℝ
⊢ ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • cexp (↑(↑n * t) * I) = cexp (↑↑r * (cexp (↑t * I) - 1))
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
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
⊢ map (fun ω i ↦ s.restrict X i ω) P = Measure.pi fun i ↦ map (s.restrict X i) P

pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
⊢ ∀ (i : ↥s), AEMeasurable (s.restrict X i) P

Tactic:
· have : s.restrict ∘ (fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω := by ext; simp
      rw [← this, ← AEMeasurable.map_map_of_aemeasurable, h, infinitePi_map_restrict]
      · simp
      · fun_prop
      exact mX

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
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
⊢ ∀ (i : ↥s), AEMeasurable (s.restrict X i) P
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
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✝⁶ : (t : T) → TopologicalSpace (F t)
inst✝⁵ : (t : T) → MeasurableSpace (F t)
inst✝⁴ : ∀ (t : T), BorelSpace (F t)
inst✝³ : ∀ (t : T), HasOuterApproxClosed (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst✝² : IsFiniteMeasure P
inst✝¹ : Finite S
inst✝ : Finite T
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : ((t : T) → F t) →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ (f fun x ↦ X x ω) * g fun x ↦ Y x ω) x ∂P =
      (∫ (x : Ω), (fun ω ↦ f fun x ↦ X x ω) x ∂P) * ∫ (x : Ω), (fun ω ↦ g fun x ↦ Y x ω) x ∂P
⊢ (fun ω s ↦ X s ω) ⟂ᵢ[P] fun ω t ↦ Y t ω

Tactic:
have := Fintype.ofFinite S; have := Fintype.ofFinite T
  refine pi_indepFun_pi_of_prod_bcf mX mY fun f g ↦ ?_
  convert!
    h (∏ s, (f s).compContinuous ⟨Function.eval s, by fun_prop⟩)
      (∏ t, (g t).compContinuous ⟨Function.eval t, by fun_prop⟩) <;> simp

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

Goal state before:
pp: Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst✝⁹ : (t : T) → TopologicalSpace (F t)
inst✝⁸ : (t : T) → MeasurableSpace (F t)
inst✝⁷ : ∀ (t : T), BorelSpace (F t)
inst✝⁶ : ∀ (t : T), HasOuterApproxClosed (F t)
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst✝¹ : Fintype T
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω), (⇑f ∘ Z * ∏ t, ⇑(g t) ∘ Y t) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P
⊢ Z ⟂ᵢ[P] fun ω t ↦ Y t ω

Tactic:
rw [indepFun_iff_map_prod_eq_prod_map_map mZ (aemeasurable_pi_lambda _ mY)]
  refine eq_prod_of_integral_mul_prod_boundedContinuousFunction fun f g ↦ ?_
  rw [integral_map, integral_map, integral_map]
  · convert! h f g <;> simp
  any_goals fun_prop
  all_goals exact Measurable.aestronglyMeasurable (by fun_prop)

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndepSets m' hm' (fun i ↦ {s i}) μ ↔
    ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω ↦ 1 | m']

Tactic:
by
  rw [iCondIndepSets_iff]
  · simp_all only [Set.mem_singleton_iff]
    constructor
    · intros
      simp [*]
    · grind
  · simpa

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

Goal state before:
pp: case h
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := ⋯
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hξ : f a ξ ≤ x
hx : ¬x = 1
g : ↑I → ℝ := ⋯
⊢ x < 1

Tactic:
exact lt_of_le_of_ne x.2.2 hx

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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hξ : f a ξ ≤ x
hx : ¬x = 1
g : ↑I → ℝ := fun y ↦ (κ a).real (Icc 0 y)
⊢ (𝓝[>] x).NeBot

Tactic:
by
      refine nhdsGT_neBot_of_exists_gt ?_
      use 1
      exact lt_of_le_of_ne x.2.2 hx

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

Goal state before:
pp: k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
⊢ ENNReal.ofReal (↑(b.choose k) * ↑x ^ k * (1 - ↑x) ^ (b - k)) = (binomial x h b) (Fin.ofNat (b + 1) k)

Tactic:
have eq1 : 1 - (x : ℝ≥0∞) = ENNReal.ofReal (1 - x : ℝ) := by norm_cast

Goal state after:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - ↑x = ENNReal.ofReal (1 - ↑x)
⊢ ENNReal.ofReal (↑(b.choose k) * ↑x ^ k * (1 - ↑x) ^ (b - k)) = (binomial x h b) (Fin.ofNat (b + 1) k)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : c = 0
ω' : Ω'
h : (κ ω') Set.univ ≤ 1
⊢ (κ ω') {ω | ε ≤ X ω} ≤ ENNReal.ofReal 1

Tactic:
simp only [ENNReal.ofReal_one]

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : c = 0
ω' : Ω'
h : (κ ω') Set.univ ≤ 1
⊢ (κ ω') {ω | ε ≤ X ω} ≤ 1
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:

Tactic:
(κ ω').real {ω | ε ≤ X ω}
  -- choose the minimizer of the r.h.s. of `h` for `t ≥ 0`. That is, `t = ε / c`.
  _ ≤ exp (-(ε / c) * ε + c * (ε / c) ^ 2 / 2) := h (ε / c) (by positivity)
  _ = exp (- ε ^ 2 / (2 * c)) := by congr; field

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : {ω | 0 < X ω} = ⋃ ε, {ω | ↑↑ε ≤ X ω}
ε : ℚ
ω' : Ω'
hm : ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ↑ε ≤ X ω} ≤ rexp (-t * ↑ε + ↑0 * t ^ 2 / 2)
a✝ : IsFiniteMeasure (κ ω')
hε : 0 < ε
⊢ (κ ω') {ω | ↑ε ≤ X ω} = 0

Tactic:
simp only [neg_mul, NNReal.coe_zero, zero_mul, zero_div, add_zero] at hm

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : {ω | 0 < X ω} = ⋃ ε, {ω | ↑↑ε ≤ X ω}
ε : ℚ
ω' : Ω'
a✝ : IsFiniteMeasure (κ ω')
hε : 0 < ε
hm : ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ↑ε ≤ X ω} ≤ rexp (-(t * ↑ε))
⊢ (κ ω') {ω | ↑ε ≤ X ω} = 0
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p✝ q✝ : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp✝ : IsStable 𝓕 p✝
hq✝ : IsStable 𝓕 q✝
x✝ : Locally p✝ 𝓕 X P ∧ Locally q✝ 𝓕 X P
hpX✝ : Locally p✝ 𝓕 X P
hqX✝ : Locally q✝ 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
⊢ p
    (stoppedProcess (fun i ↦ {ω | ⊥ < (hpX.localSeq ⊓ hqX.localSeq) n ω}.indicator (X i))
      ((hpX.localSeq ⊓ hqX.localSeq) n))

Tactic:
convert!
    hp _ (hpX.stoppedProcess_localSeq n) _ <|
      hqX.isLocalizingSequence_localSeq.isStoppingTime n using 1

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p✝ q✝ : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp✝ : IsStable 𝓕 p✝
hq✝ : IsStable 𝓕 q✝
x✝ : Locally p✝ 𝓕 X P ∧ Locally q✝ 𝓕 X P
hpX✝ : Locally p✝ 𝓕 X P
hqX✝ : Locally q✝ 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
⊢ stoppedProcess (fun i ↦ {ω | ⊥ < (hpX.localSeq ⊓ hqX.localSeq) n ω}.indicator (X i))
      ((hpX.localSeq ⊓ hqX.localSeq) n) =
    stoppedProcess
      (fun i ↦
        {ω | ⊥ < hqX.localSeq n ω}.indicator
          (stoppedProcess (fun i ↦ {ω | ⊥ < hpX.localSeq n ω}.indicator (X i)) (hpX.localSeq n) i))
      (hqX.localSeq n)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case neg
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : f x ∉ Set.Ioc (-A) A
⊢ |0| ≤ |A|

Tactic:
simp [abs_nonneg]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case neg
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h✝ : f x ∉ Set.Ioc (-A) A
⊢ |0| ≤ |f x|

Tactic:
simp [abs_nonneg]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
hX : HasSubgaussianMGF X c μ
hXY : IdentDistrib X Y μ μ'
⊢ HasSubgaussianMGF Y c μ'

Tactic:
by
  rw [← id_map_iff hXY.aemeasurable_fst] at hX
  rwa [← id_map_iff hXY.aemeasurable_snd, ← hXY.map_eq]

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : Semiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
φ✝ φ : ρ.Equiv σ
g : G
⊢ LinearMap.id ∘ₗ σ g = σ g ∘ₗ LinearMap.id

Tactic:
id_comp,

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : Semiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
φ✝ φ : ρ.Equiv σ
g : G
⊢ σ g = σ g ∘ₗ LinearMap.id