mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
b c : ℕ
hcb : c ≤ b
⊢ partialTraj κ b c ∘ₖ partialTraj κ a b = partialTraj κ a c

Tactic:
partialTraj_le hcb,

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
b c : ℕ
hcb : c ≤ b
⊢ deterministic (frestrictLe₂ hcb) ⋯ ∘ₖ partialTraj κ a b = partialTraj κ a c
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)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
⊢ ν = infinitePi μ

Tactic:
by
  refine (isProjectiveLimit_infinitePi μ).unique ?_ |>.symm
  refine fun s ↦ (pi_eq fun t ht ↦ ?_).symm
  classical
  rw [Measure.map_apply, restrict_preimage_univ, hν, ← prod_attach, univ_eq_attach]
  · congr with i
    rw [dif_pos i.2]
  any_goals fun_prop
  · rintro i
    split_ifs with hi
    · exact ht ⟨i, hi⟩
    · exact .univ
  · exact .univ_pi ht

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

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)) ∘ₘ
      ⇑(Kernel.copy 𝓧) ∘ₘ ⇑(Kernel.deterministic f hf) ∘ₘ μ =
    ⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ
      ⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) ∘ₘ ⇑(Kernel.copy 𝓧) ∘ₘ ⇑(Kernel.deterministic f hf) ∘ₘ μ

Tactic:
← Kernel.parallelComp_id_left_comp_parallelComp,

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.id ∥ₖ Kernel.deterministic f hf ∘ₖ (Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ)) ∘ₘ
      ⇑(Kernel.copy 𝓧) ∘ₘ ⇑(Kernel.deterministic f hf) ∘ₘ μ =
    ⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ
      ⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) ∘ₘ ⇑(Kernel.copy 𝓧) ∘ₘ ⇑(Kernel.deterministic f hf) ∘ₘ μ
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ
      ⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) ∘ₘ ⇑(Kernel.copy 𝓧) ∘ₘ ⇑(Kernel.deterministic f hf) ∘ₘ μ =
    ⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ ⇑(Kernel.deterministic f hf ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ

Tactic:
by rw [parallelProd_posterior_comp_copy_comp]

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
⊢ ((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

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 : ℕ
hf : (fun x ↦ x (a + 1)) = (fun x ↦ x ⟨a + 1, ⋯⟩) ∘ frestrictLe (a + 1)
⊢ ((traj κ a).map fun x ↦ x (a + 1)) = κ a
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ =
    ⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) ∘ₘ μ

Tactic:
by -- `deterministic` is used here
    rw [Measure.comp_assoc, Kernel.parallelComp_self_comp_copy]

Goal state after:
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

Tactic:
simpa [Set.countable_univ_iff]

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

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

Tactic:
← Kernel.parallelComp_id_left_comp_parallelComp,

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 η
⊢ ⇑(Kernel.id ∥ₖ κ†μ ∘ₖ (Kernel.id ∥ₖ η†(⇑κ ∘ₘ μ)) ∘ₖ Kernel.copy 𝓨) ∘ₘ ⇑(η ∘ₖ κ) ∘ₘ μ =
    ⇑(Kernel.swap Ω 𝓨) ∘ₘ ⇑(Kernel.id ∥ₖ η ∘ₖ (Kernel.id ∥ₖ κ) ∘ₖ Kernel.copy Ω) ∘ₘ μ
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]
  refine (ae_eq_posterior_of_compProd_eq_swap_comp ((κ†μ) ∘ₖ η†(κ ∘ₘ μ)) ?_).symm
  simp_rw [Measure.compProd_eq_comp_prod, ← Kernel.parallelComp_comp_copy,
    ← Kernel.parallelComp_id_left_comp_parallelComp, ← Measure.comp_assoc]
  calc (Kernel.id ∥ₖ κ†μ) ∘ₘ (Kernel.id ∥ₖ η†(κ ∘ₘ μ)) ∘ₘ (Kernel.copy 𝓨) ∘ₘ η ∘ₘ κ ∘ₘ μ
  _ = (Kernel.id ∥ₖ κ†μ) ∘ₘ (η ∥ₖ Kernel.id) ∘ₘ Kernel.copy 𝓧 ∘ₘ κ ∘ₘ μ := by
    rw [parallelProd_posterior_comp_copy_comp]
  _ = (η ∥ₖ Kernel.id) ∘ₘ (Kernel.id ∥ₖ κ†μ) ∘ₘ Kernel.copy 𝓧 ∘ₘ κ ∘ₘ μ := by
    rw [Measure.comp_assoc, Kernel.parallelComp_comm, ← Measure.comp_assoc]
  _ = (η ∥ₖ Kernel.id) ∘ₘ (κ ∥ₖ Kernel.id) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    rw [parallelProd_posterior_comp_copy_comp]
  _ = (Kernel.swap _ _) ∘ₘ (Kernel.id ∥ₖ η) ∘ₘ (Kernel.id ∥ₖ κ) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    simp_rw [Measure.comp_assoc]
    conv_rhs => rw [← Kernel.comp_assoc]
    rw [Kernel.swap_parallelComp, Kernel.comp_assoc, ← Kernel.comp_assoc (Kernel.swap Ω 𝓧),
      Kernel.swap_parallelComp, Kernel.comp_assoc, Kernel.swap_copy]

Goal state after:
Module: Mathlib.Probability.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]
  intro κ hκ
  rw [← κ.comp_assoc η]
  exact iInf_le_of_le (κ ∘ₖ η) (iInf_le_of_le inferInstance le_rfl)

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

Goal state before:
pp: case h₁
n : ℕ
p : ↑I
k : ℕ
⊢ k ∉ Finset.Iic n → (ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • dirac k) {k} = 0

Tactic:
· simp_all [Nat.choose_eq_zero_of_lt]

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)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ ∫ (x : (n : ℕ) → X n), A.indicator (fun x_1 ↦ f x_1 x) (frestrictLe b x) ∂(traj κ a) u =
    ∫ (y : (n : ℕ) → X n) in frestrictLe b ⁻¹' A, f (frestrictLe b y) y ∂(traj κ a) u

pp: X : ℕ → Type u_1
inst✝³ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝² : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ Integrable (uncurry fun x y ↦ A.indicator (fun x ↦ f x y) x) ((partialTraj κ a b) u ⊗ₘ traj κ b)

Tactic:
· simp_rw [← Set.indicator_comp_right, ← integral_indicator (measurable_frestrictLe b hA)]
    rfl

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)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ Integrable (uncurry fun x y ↦ A.indicator (fun x ↦ f x y) x) ((partialTraj κ a b) u ⊗ₘ traj κ b)
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
b : β
this : ∀ (a : α), (if p a = 0 then 0 else p a * (f a) b) = p a * (f a) b
⊢ (p.bindOnSupport fun a x ↦ f a) b = (p.bind f) b

Tactic:
simp only [bindOnSupport_apply fun a _ => f a, p.bind_apply f, dite_eq_ite, mul_ite,
    mul_zero, this]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
b : β
⊢ map (Function.const α b) p = pure b

Tactic:
simp only [map, Function.comp_def, bind_const, Function.const]

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

Goal state before:
pp: E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ∞
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
⊢ μ[|s] = (μ t)⁻¹ • (μ.restrict (toMeasurable μ s)).withDensity 1

Tactic:
withDensity_one,

Goal state after:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ∞
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
⊢ μ[|s] = (μ t)⁻¹ • μ.restrict (toMeasurable μ s)
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: case neg
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
hns : ¬μ s = 0
this✝ : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ μ[|s] = (μ s)⁻¹ • (μ.restrict s).withDensity 1

Tactic:
withDensity_one,

Goal state after:
case neg
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
hns : ¬μ s = 0
this✝ : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ μ[|s] = (μ s)⁻¹ • μ.restrict s
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
hX : ¬AEMeasurable X ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂Measure.map X ℙ

Tactic:
rw [map_of_not_aemeasurable hX, integral_zero_measure, integral_non_aestronglyMeasurable]

Goal state after:
case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
hX : ¬AEMeasurable X ℙ
⊢ ¬AEStronglyMeasurable X ℙ
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: ι : Type u_1
α : Type u_4
Ω : ι → Type u_5
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
f : α → ι
hf : Function.Injective f
⊢ map (fun ω i ↦ ω (f i)) (infinitePi P) = infinitePi fun i ↦ P (f i)

Tactic:
(iIndepFun_iff_map_fun_eq_infinitePi_map <| by fun_prop).mp ?_

Goal state after:
ι : Type u_1
α : Type u_4
Ω : ι → Type u_5
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
f : α → ι
hf : Function.Injective f
⊢ (infinitePi fun i ↦ map (fun ω ↦ ω (f i)) (infinitePi P)) = infinitePi fun i ↦ P (f i)

ι : Type u_1
α : Type u_4
Ω : ι → Type u_5
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
f : α → ι
hf : Function.Injective f
⊢ iIndepFun (fun i ω ↦ ω (f i)) (infinitePi P)
Module: Mathlib.Probability.Kernel.Invariance

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
⊢ κ ∘ₖ const α μ = const α μ

Tactic:
rw [comp_const κ μ, hκ.def]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
inst✝ : IsMarkovKernel κ
π : Measure α
h_rev : κ.IsReversible π
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α), (κ x) s ∂π = ∫⁻ (x : α) in s, (κ x) Set.univ ∂π

Tactic:
simpa [restrict_univ] using (h_rev hs .univ).symm

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

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
a✝ : PUnit.{u + 1} × X✝.carrier
s✝ : Set Y✝.carrier
hs : MeasurableSet s✝
this : IsSFiniteKernel κ.hom
⊢ ∫⁻ (b : PUnit.{u + 1}), (κ.hom a✝.2) (Prod.mk b ⁻¹' Prod.snd ⁻¹' s✝) ∂Kernel.id a✝.1 = (κ.hom a✝.2) s✝

Tactic:
simp only [Kernel.id_apply, lintegral_dirac]

Goal state after:
X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
a✝ : PUnit.{u + 1} × X✝.carrier
s✝ : Set Y✝.carrier
hs : MeasurableSet s✝
this : IsSFiniteKernel κ.hom
⊢ (κ.hom a✝.2) (Prod.mk a✝.1 ⁻¹' Prod.snd ⁻¹' s✝) = (κ.hom a✝.2) s✝
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ IsSFiniteKernel (Kernel.swap X.carrier Y.carrier)

Tactic:
rw [Kernel.swap]

Goal state after:
X Y : SFinKer
⊢ IsSFiniteKernel (Kernel.deterministic Prod.swap ⋯)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ IsSFiniteKernel (Kernel.swap Y.carrier X.carrier)

Tactic:
rw [Kernel.swap]

Goal state after:
X Y : SFinKer
⊢ IsSFiniteKernel (Kernel.deterministic Prod.swap ⋯)
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
⊢ ∫⁻ (x : X), g x * f x ∂π x₀ = g x₀ * ∫⁻ (x : X), f x ∂π x₀

Tactic:
by
  refine hg.ennreal_induction ?_ ?_ ?_
  · rintro c A hA
    simp_rw [← smul_indicator_one_apply, smul_mul_assoc, smul_eq_mul]
    rw [lintegral_const_mul, hπ.lintegral_indicator_mul h𝓑𝓧 hf hA]
    · measurability
  · rintro g₁ g₂ - _ hg₂_meas hg₁ hg₂
    simp only [Pi.add_apply, add_mul]
    rw [lintegral_add_right, hg₁, hg₂]
    · exact (hg₂_meas.mono h𝓑𝓧 le_rfl).mul hf
  · rintro g' hg'_meas hg'_mono hg'
    simp_rw [ENNReal.iSup_mul]
    rw [lintegral_iSup (fun n ↦ ((hg'_meas _).mono h𝓑𝓧 le_rfl).fun_mul hf)
      (hg'_mono.mul_const zero_le)]
    simp_rw [hg']

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

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ}, MeasurableSet s → MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
            (Measure.map (fun ω ↦ (ω, f ω, g ω)) μ) ((k ⁻¹' s) ×ˢ t ×ˢ u)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ) (s ×ˢ t ×ˢ u) =
    (⇑(Kernel.id ×ₖ
            ((condExpKernel μ (MeasurableSpace.comap k mγ)).map f ×ₖ
              (condExpKernel μ (MeasurableSpace.comap k mγ)).map g)) ∘ₘ
        μ.trim ⋯)
      ((k ⁻¹' s) ×ˢ t ×ˢ u)

Tactic:
Measure.bind_apply ((hk_meas hs).prod (ht.prod hu)) (by fun_prop),

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ}, MeasurableSet s → MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
            (Measure.map (fun ω ↦ (ω, f ω, g ω)) μ) ((k ⁻¹' s) ×ˢ t ×ˢ u)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ) (s ×ˢ t ×ˢ u) =
    ∫⁻ (a : Ω),
      ((Kernel.id ×ₖ
            ((condExpKernel μ (MeasurableSpace.comap k mγ)).map f ×ₖ
              (condExpKernel μ (MeasurableSpace.comap k mγ)).map g))
          a)
        ((k ⁻¹' s) ×ˢ t ×ˢ u) ∂μ.trim ⋯
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
ι : Type u_3
inst✝⁶ : LinearOrder ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝² : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst✝¹ : Nonempty ι
h✝ : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_countable_range : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i}
i : WithTop ι
hi : i ∈ Set.range τ
h : i = ⊤
⊢ False

Tactic:
simp only [h, Set.mem_range] at hi

Goal state after:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
ι : Type u_3
inst✝⁶ : LinearOrder ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝² : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst✝¹ : Nonempty ι
h✝ : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_countable_range : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i}
i : WithTop ι
h : i = ⊤
hi : ∃ y, τ y = ⊤
⊢ False
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: case refine_1
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
⊢ ∀ᵐ (x : Ω) ∂μ.restrict {x | σ x ≤ τ x},
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x

pp: case refine_2
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
⊢ ∀ᵐ (x : Ω) ∂μ.restrict {x | σ x ≤ τ x}ᶜ,
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x

Tactic:
· exact condExp_min_stopping_time_ae_eq_restrict_le hσ hτ

Goal state after:
case refine_2
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
⊢ ∀ᵐ (x : Ω) ∂μ.restrict {x | σ x ≤ τ x}ᶜ,
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
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 Y : T → Ω → E
hX✝ : IsAEKolmogorovProcess X P p q M
h : ∀ (t : T), X t =ᵐ[P] Y t
t : T
ω : Ω
hX : X t ω = IsAEKolmogorovProcess.mk X hX✝ t ω
⊢ X t ω = Y t ω → Y t ω = IsAEKolmogorovProcess.mk X hX✝ t ω

Tactic:
hY

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 Y : T → Ω → E
hX✝ : IsAEKolmogorovProcess X P p q M
h : ∀ (t : T), X t =ᵐ[P] Y t
t : T
ω : Ω
hX : X t ω = IsAEKolmogorovProcess.mk X hX✝ t ω
hY : X t ω = Y t ω
⊢ Y t ω = IsAEKolmogorovProcess.mk X hX✝ t ω
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case hg
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ IntervalIntegrable (fun x ↦ 1) ρ 0 ↑N

Tactic:
· exact continuous_const.intervalIntegrable _ _

Goal state after: