mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case compl
α : 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 γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : ∫ (x : γ) in A, κ.density ν a x s ∂ν a + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = ∫ (x : γ), κ.density ν a x s ∂ν a
⊢ ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (Aᶜ ×ˢ s)

Tactic:
hA_eq,

Goal state after:
case compl
α : 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 γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = ∫ (x : γ), κ.density ν a x s ∂ν a
⊢ ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (Aᶜ ×ˢ s)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: case pos
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a b : ι
hab : a ≤ b
x : ↥(Iic b)
h : ↑x ≤ a
⊢ Measurable fun c ↦
    { toFun := fun x i ↦ if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩,
        invFun := fun x ↦ (fun i ↦ x ⟨↑i, ⋯⟩, fun i ↦ x ⟨↑i, ⋯⟩), left_inv := ⋯, right_inv := ⋯ }
      c x

pp: case neg
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a b : ι
hab : a ≤ b
x : ↥(Iic b)
h : ¬↑x ≤ a
⊢ Measurable fun c ↦
    { toFun := fun x i ↦ if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩,
        invFun := fun x ↦ (fun i ↦ x ⟨↑i, ⋯⟩, fun i ↦ x ⟨↑i, ⋯⟩), left_inv := ⋯, right_inv := ⋯ }
      c x

Tactic:
· simpa [h] using measurable_fst.eval

Goal state after:
case neg
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a b : ι
hab : a ≤ b
x : ↥(Iic b)
h : ¬↑x ≤ a
⊢ Measurable fun c ↦
    { toFun := fun x i ↦ if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩,
        invFun := fun x ↦ (fun i ↦ x ⟨↑i, ⋯⟩, fun i ↦ x ⟨↑i, ⋯⟩), left_inv := ⋯, right_inv := ⋯ }
      c x
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
⊢ ⇑(condDistrib (fun ω ↦ Y ω.2) (fun ω ↦ X ω.2) (ν.prod μ)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)

Tactic:
by
  by_cases hX : AEMeasurable X μ
  swap; · simp [Measure.map_of_not_aemeasurable hX, Filter.EventuallyEq]
  have h_map := condDistrib_map (X := X) (Y := Y) (f := Prod.snd (β := α) (α := γ))
      (ν := ν.prod μ) (mα := inferInstance) (mβ := inferInstance)
      (by simpa) (by simpa) (by fun_prop)
  rw [← AEMeasurable.map_map_of_aemeasurable (by simpa) (by fun_prop)] at h_map
  simp only [Measure.map_snd_prod, measure_univ, one_smul] at h_map
  exact h_map.symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : CountableOrCountablyGenerated α β
ρ : Kernel α (β × Ω)
inst✝¹ : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst✝ : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
⊢ ∀ᵐ (x : β) ∂ρ.fst a, κ (a, x) = ρ.condKernel (a, x)

Tactic:
filter_upwards [Kernel.condKernel_apply_eq_condKernel ρ a,
    Kernel.apply_eq_measure_condKernel_of_compProd_eq hκ a] with a h1 h2
  rw [h1, h2]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case neg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
this : IsEmpty ↥(Ioc a b)
x : (i : ↥(Iic a)) → X ↑i
s : Set ((i : ↥(Ioc a b)) → X ↑i)
ms : MeasurableSet s
hs : ¬s.Nonempty
⊢ (((partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a b).map (restrict₂ ⋯)) x) s =
    ((const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)) x) s

Tactic:
rw [Set.not_nonempty_iff_eq_empty.1 hs]

Goal state after:
case neg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
this : IsEmpty ↥(Ioc a b)
x : (i : ↥(Iic a)) → X ↑i
s : Set ((i : ↥(Ioc a b)) → X ↑i)
ms : MeasurableSet s
hs : ¬s.Nonempty
⊢ (((partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a b).map (restrict₂ ⋯)) x) ∅ =
    ((const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)) x) ∅
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: case neg
α : 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 α
this : MeasurableSpace.CountablyGenerated γ
⊢ (κ.map fun a ↦ (a, ())).density η a x univ ≤ 1 x

Tactic:
exact density_le_one ((fst_map_id_prod _ measurable_const).trans_le hκη) _ _ _

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: 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⟩)

Tactic:
exact ht ⟨i, hi⟩

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

Goal state before:
pp: case refine_2
α : 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)
⊢ κ = deterministic f ⋯

Tactic:
· ext a : 1
    exact hf a

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case ha
ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
⊢ Tendsto (fun s' ↦ ∏ i ∈ s', (μ ↑i) (t ↑i)) atTop (𝓝 ((infinitePi μ) (s.pi t)))

Tactic:
conv in ∏ _ ∈ _, _ =>
      rw [← infinitePi_pi _ (by measurability), ← infinitePi_map_restrict', map_apply
        (by fun_prop) (by apply MeasurableSet.pi (countable_toSet _) (by measurability)),
        domRestrict_preimage]
      simp only [coe_image, dite_eq_ite]

Goal state after:
case ha
ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
⊢ Tendsto (fun s' ↦ (infinitePi μ) ((Subtype.val '' ↑s').pi fun i ↦ if i ∈ s then t i else Set.univ)) atTop
    (𝓝 ((infinitePi μ) (s.pi t)))
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) sᶜ = 0

Tactic:
rw [measure_compl hs (by simp), measure_univ h₁, h₁, tsub_self]

Goal state after:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
η : Kernel 𝓧 𝓧'
inst✝ : IsMarkovKernel η
⊢ bayesRisk ℓ P π ≤ bayesRisk ℓ (η ∘ₖ P) π

Tactic:
simp only [bayesRisk, avgRisk, le_iInf_iff]

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
η : Kernel 𝓧 𝓧'
inst✝ : IsMarkovKernel η
⊢ ∀ (i : Kernel 𝓧' 𝓨),
    IsMarkovKernel i →
      ⨅ κ, ⨅ (_ : IsMarkovKernel κ), ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ P) θ ∂π ≤
        ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(i ∘ₖ (η ∘ₖ P)) θ ∂π
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: x a r : ℝ
ha : 0 < a
hr : 0 < r
hx : 0 < x
⊢ 0 < gammaPDFReal a r x

Tactic:
simp only [gammaPDFReal, if_pos hx.le]
  positivity

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

Goal state before:
pp: R : Type u_1
inst✝³ : MeasurableSpace R
inst✝² : AddMonoidWithOne R
inst✝¹ : MeasurableSingletonClass R
inst✝ : CharZero R
n : ℕ
p : ↑I
⊢ Bin(R, n, p).real {0} = (1 - ↑p) ^ n

Tactic:
rw [← Nat.cast_zero, map_cast_binomial_real_singleton]

Goal state after:
R : Type u_1
inst✝³ : MeasurableSpace R
inst✝² : AddMonoidWithOne R
inst✝¹ : MeasurableSingletonClass R
inst✝ : CharZero R
n : ℕ
p : ↑I
⊢ ↑(n.choose 0) * ↑p ^ 0 * (1 - ↑p) ^ (n - 0) = (1 - ↑p) ^ n
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)
μ₀ : Measure (X 0)
inst✝ : IsProbabilityMeasure μ₀
a : ℕ
⊢ Measure.map (frestrictLe a) (trajMeasure μ₀ κ) ⊗ₘ κ a =
    Measure.map (fun x ↦ (frestrictLe a x, x (a + 1))) (trajMeasure μ₀ κ)

Tactic:
by
  rw [Measure.compProd_eq_comp_prod, trajMeasure, Measure.map_comp _ _ (by fun_prop),
    traj_map_frestrictLe, Measure.comp_assoc, Measure.map_comp _ _ (by fun_prop)]
  congr with x₀ : 1
  rw [comp_apply, ← Measure.compProd_eq_comp_prod, map_apply _ (by fun_prop),
    partialTraj_compProd_eq_map_traj zero_le]

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

Goal state before:
pp: α : Type u_1
p : PMF α
x y : α
hy : y ≠ x
⊢ p y * (pure y) x = 0

Tactic:
pure_apply_of_ne _ _ hy.symm,

Goal state after:
α : Type u_1
p : PMF α
x y : α
hy : y ≠ x
⊢ p y * 0 = 0
Module: Mathlib.Probability.Distributions.TwoValued

Goal state before:
pp: Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
⊢ μ[1 | m] - μ[X | m] =ᵐ[μ] μ[1 - X | m]

Tactic:
refine (condExp_sub (integrable_const _)
            (.of_bound (C := 1) hXmeas.aestronglyMeasurable ?_) _).symm

Goal state after:
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
⊢ ∀ᵐ (x : Ω) ∂μ, ‖X x‖ ≤ 1
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)
⊢ iIndepFun (fun i ↦ Function.eval i) (infinitePi μ)

Tactic:
iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop),

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

Goal state before:
pp: ι : Type u_1
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), Measurable (X i)
⊢ iIndepFun (fun i ω ↦ X i (ω i)) (infinitePi P)

Tactic:
iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop),

Goal state after:
ι : Type u_1
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), Measurable (X i)
⊢ map (fun ω i ↦ X i (ω i)) (infinitePi P) = infinitePi fun i ↦ map (fun ω ↦ X i (ω i)) (infinitePi P)
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (fun i ω x ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (X i) P
this✝² : IsProbabilityMeasure P
this✝¹ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (map (X i j) P)
this✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun ω x ↦ X i x ω) P)
this : (⇑(MeasurableEquiv.piCurry 𝓧) ∘ fun ω p ↦ X p.fst p.snd ω) = fun ω i j ↦ X i j ω
⊢ iIndepFun (fun p ω ↦ X p.fst p.snd ω) P

Tactic:
iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop),

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (fun i ω x ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (X i) P
this✝² : IsProbabilityMeasure P
this✝¹ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (map (X i j) P)
this✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun ω x ↦ X i x ω) P)
this : (⇑(MeasurableEquiv.piCurry 𝓧) ∘ fun ω p ↦ X p.fst p.snd ω) = fun ω i j ↦ X i j ω
⊢ map (fun ω i ↦ X i.fst i.snd ω) P = infinitePi fun i ↦ map (fun ω ↦ X i.fst i.snd ω) P
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
s t : Set Ω
inst✝ : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (fun ω ↦ ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω).real t) =ᵐ[μ.restrict s]
    μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}]
ω : Ω
hω₁ : μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}] ω = μ[|s].real t
hω₂ :
  ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω).real t =
    μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}] ω
⊢ ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]

Tactic:
hω₁,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
s t : Set Ω
inst✝ : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (fun ω ↦ ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω).real t) =ᵐ[μ.restrict s]
    μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}]
ω : Ω
hω₁ : μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}] ω = μ[|s].real t
hω₂ : ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω).real t = μ[|s].real t
⊢ ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : Measure Ω
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s μ
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
⊢ μ t = 0 ∨ μ t = 1

Tactic:
by
  simpa only [ae_dirac_eq, Filter.eventually_pure]
    using! Kernel.measure_zero_or_one_of_measurableSet_limsup h_le h_indep hf hns hnsp hns_univ
      ht_tail

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
f₁ : X.carrier → PUnit.{?u.96 + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
⊢ { carrier := { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier × X.carrier,
      str := Prod.instMeasurableSpace } ≅
    X

Tactic:
have hf₁ : Measurable f₁ := by fun_prop

Goal state after:
X : SFinKer
f₁ : X.carrier → PUnit.{?u.96 + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
⊢ { carrier := { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier × X.carrier,
      str := Prod.instMeasurableSpace } ≅
    X
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_2
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ { hom := Kernel.id.map f₁, property := ⋯ } ≫ { hom := Kernel.id.map Prod.snd, property := ⋯ } = 𝟙 X

Tactic:
· ext : 1; dsimp
      rw [Kernel.id_map hf₂, Kernel.deterministic_comp_eq_map hf₂, Kernel.id_map hf₁,
        Kernel.deterministic_map hf₁ hf₂]
      ext : 1
      simp [Kernel.deterministic_apply, Kernel.id_apply, f₁]

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{?u.182 + 1} := fun x ↦ (x, PUnit.unit)
⊢ { carrier := X.carrier × { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier,
      str := Prod.instMeasurableSpace } ≅
    X

Tactic:
have hf₁ : Measurable f₁ := by fun_prop

Goal state after:
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{?u.182 + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
⊢ { carrier := X.carrier × { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier,
      str := Prod.instMeasurableSpace } ≅
    X
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✝¹ : IsFiniteMeasure P
inst✝ : Finite T
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : ((t : T) → F t) →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ f (Z ω) * g fun x ↦ Y x ω) x ∂P =
      (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (fun ω ↦ g fun x ↦ Y x ω) x ∂P
⊢ Z ⟂ᵢ[P] fun ω t ↦ Y t ω

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

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_2
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ { hom := Kernel.id.map f₁, property := ⋯ } ≫ { hom := Kernel.id.map Prod.fst, property := ⋯ } = 𝟙 X

Tactic:
· ext : 1; dsimp
      rw [Kernel.id_map hf₂, Kernel.deterministic_comp_eq_map hf₂, Kernel.id_map hf₁,
        Kernel.deterministic_map hf₁ hf₂]
      ext : 1
      simp [Kernel.deterministic_apply, Kernel.id_apply, f₁]

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
⊢ ((κ₁.hom ∥ₖ κ₂.hom ∥ₖ η.hom) a✝) (⇑prodAssoc ⁻¹' s✝) = ((κ₁.hom ∥ₖ (κ₂.hom ∥ₖ η.hom)) (prodAssoc a✝)) s✝

Tactic:
repeat rw [Kernel.parallelComp_apply]

Goal state after:
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
⊢ (((κ₁.hom a✝.1.1).prod (κ₂.hom a✝.1.2)).prod (η.hom a✝.2)) (⇑prodAssoc ⁻¹' s✝) =
    ((κ₁.hom (prodAssoc a✝).1).prod ((κ₂.hom (prodAssoc a✝).2.1).prod (η.hom (prodAssoc a✝).2.2))) s✝
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ CondIndepFun m' hm' f g μ ↔
    ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → CondIndepSet m' hm' (f ⁻¹' s) (g ⁻¹' t) μ

Tactic:
simp only [CondIndepFun, CondIndepSet, Kernel.indepFun_iff_indepSet_preimage hf hg]

Goal state after:
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
ω : Ω
hω₁ : X s ω = IsAEKolmogorovProcess.mk X hX s ω
hω₂ : X t ω = IsAEKolmogorovProcess.mk X hX t ω
⊢ edist (X s ω) (X t ω) ^ p = edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω) ^ p

Tactic:
hω₁,

Goal state after:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
ω : Ω
hω₁ : X s ω = IsAEKolmogorovProcess.mk X hX s ω
hω₂ : X t ω = IsAEKolmogorovProcess.mk X hX t ω
⊢ edist (IsAEKolmogorovProcess.mk X hX s ω) (X t ω) ^ p =
    edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω) ^ p
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
t : ℝ
p : ℝ≥0
⊢ MemLp (fun ω ↦ rexp (t * X ω)) (↑p) μ

Tactic:
by
  rw [HasSubgaussianMGF_iff_kernel] at h
  simpa using h.memLp_exp_mul t p

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ ρ.invariants.carrier = ⋂ g, Function.fixedPoints ⇑(ρ g)

Tactic:
by
  ext; simp [Function.IsFixedPt]

Goal state after:
Module: Mathlib.RepresentationTheory.Irreducible

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
inst✝⁶ : Monoid G
inst✝⁵ : Field k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
ρ : Representation k G V
inst✝² : ρ.IsIrreducible
inst✝¹ : FiniteDimensional k V
inst✝ : IsAlgClosed k
⊢ Bijective ⇑(algebraMap k (ρ.IntertwiningMap ρ))

Tactic:
have : Bijective (algebraMap k (Module.End k[G] ρ.asModule)) :=
    IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed k
  exact (Bijective.of_comp_iff' (IntertwiningMap.equivAlgEnd (ρ := ρ)).bijective _).1 this

Goal state after: