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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : (ν a) (countablePartitionSet n x) = 0
⊢ Tendsto (fun m ↦ ((κ a) (countablePartitionSet n x ×ˢ seq m) / (ν a) (countablePartitionSet n x)).toReal) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ ∅) / (ν a) (countablePartitionSet n x)).toReal)

Tactic:
simp_rw [h0, ENNReal.toReal_div]
    simp

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

Goal state before:
pp: β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ

Tactic:
conv_rhs => rw [← ρ.disintegrate ρ.condKernel]

Goal state after:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : Integrable f ρ
⊢ ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω), f x ∂ρ

Tactic:
conv_rhs => rw [← ρ.disintegrate ρ.condKernel]

Goal state after:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : Integrable f ρ
⊢ ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ρ
⊢ ∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ

Tactic:
conv_rhs => rw [← ρ.disintegrate ρ.condKernel]

Goal state after:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ρ
⊢ ∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω ↦ f (a, ω)) (ρ.condKernel a)) ∧
      Integrable (fun a ↦ ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔
    Integrable f ρ

Tactic:
conv_rhs => rw [← ρ.disintegrate ρ.condKernel]

Goal state after:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω ↦ f (a, ω)) (ρ.condKernel a)) ∧
      Integrable (fun a ↦ ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔
    Integrable f (ρ.fst ⊗ₘ ρ.condKernel)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ((condDistrib Y X μ) (X x)) s ∂μ ≠ ∞

Tactic:
refine ne_of_lt ?_
    calc
      ∫⁻ a, condDistrib Y X μ (X a) s ∂μ ≤ ∫⁻ _, 1 ∂μ := lintegral_mono fun a => prob_le_one
      _ = μ univ := lintegral_one
      _ < ∞ := measure_lt_top _ _

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

Goal state before:
pp: case refine_1.left
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
⊢ (κ a) (countablePartitionSet n x ×ˢ univ) ≠ 0 → (κ a) {p | p.1 ∈ countablePartitionSet n x} ≠ 0

Tactic:
refine fun h h0 ↦ h (measure_mono_null (fun x ↦ ?_) h0)
      simp only [mem_prod, mem_ofPred_eq, and_imp]
      exact fun h _ ↦ h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ᵐ (x : γ) ∂κ.fst a, Tendsto (fun m ↦ κ.density κ.fst a x (seq m)) atTop (𝓝 1)

Tactic:
refine tendsto_of_integral_tendsto_of_monotone ?_ (integrable_const _) ?_ ?_ ?_
  · exact fun m ↦ integrable_density le_rfl _ (hseq_meas m)
  · rw [MeasureTheory.integral_const, smul_eq_mul, mul_one]
    convert! tendsto_integral_density_of_monotone (κ := κ) le_rfl a seq hseq hseq_iUnion hseq_meas
    simp only [measureReal_def]
    rw [fst_apply' _ _ MeasurableSet.univ]
    simp only [mem_univ, ofPred_true]
  · exact ae_of_all _ (fun c n m hnm ↦ density_mono_set le_rfl a c (hseq hnm))
  · exact ae_of_all _ (fun x m ↦ density_le_one le_rfl a x (seq m))

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

Goal state before:
pp: ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
⊢ ∀ᵐ (s : Set ι) ∂setBer(u, p), s ⊆ u

Tactic:
simp only [Filter.Eventually, mem_ae_iff, Set.compl_ofPred, Set.not_subset_iff_exists_mem_notMem,
    Set.ofPred_exists, Set.ofPred_and, measure_iUnion_null_iff]
  rintro i
  by_cases hi : i ∈ u
  · simp [*]
  calc
    setBer(u, p) ({s | i ∈ s} ∩ {s | i ∉ u})
    _ = setBer(u, p) {s | i ∈ s} := by simp [hi]
    _ = infinitePi (fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False)
          (cylinder {i} {fun _ ↦ True}) := by
      rw [setBernoulli_apply']; congr!; ext; simp [funext_iff]
    _ = 0 := by simp [infinitePi_cylinder, hi]

Goal state after:
Module: Mathlib.Probability.CondVar

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

Tactic:
rw [ae_zero]
    exact eventually_bot

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case pos
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

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 [Subsingleton.eq_univ_of_nonempty hs, @measure_univ .., measure_univ]
      exact (IsMarkovKernel.map _ (measurable_restrict₂ _)) |>.isProbabilityMeasure x

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) s =
    ((const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)) x) s
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 : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
n : ℕ
⊢ DependsOn ((cylinder (Iic (a n)) (S n)).indicator 1) ↑(Iic (a n))

Tactic:
exact dependsOn_cylinder_indicator_const ..

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
⊢ partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a b =
    (Kernel.id ×ₖ const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)).map (_root_.IicProdIoc a b)

Tactic:
partialTraj_eq_prod,

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
⊢ (Kernel.id ×ₖ (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a b).map (restrict₂ ⋯)).map
      (_root_.IicProdIoc a b) =
    (Kernel.id ×ₖ const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)).map (_root_.IicProdIoc a b)
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
⊢ κ.rnDeriv η a x = ∞ ↔ (a, x) ∈ κ.mutuallySingularSet η

Tactic:
by
  simp only [rnDeriv, ENNReal.div_eq_top, ne_eq, ENNReal.ofReal_eq_zero, not_le,
    tsub_le_iff_right, zero_add, ENNReal.ofReal_ne_top, not_false_eq_true, and_true, or_false,
    mutuallySingularSet, mem_ofPred_eq, and_iff_right_iff_imp]
  exact fun h ↦ zero_lt_one.trans_le h

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

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
⊢ (partialTraj κ a (b + 1)).map (frestrictLe₂ ⋯) = partialTraj κ a b

Tactic:
obtain hab | hba := le_or_gt a b

Goal state after:
case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ (partialTraj κ a (b + 1)).map (frestrictLe₂ ⋯) = partialTraj κ a b

case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hba : b < a
⊢ (partialTraj κ a (b + 1)).map (frestrictLe₂ ⋯) = partialTraj κ a b
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)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)
⊢ ∀ x ∈ s, x ∉ κ.mutuallySingularSetSlice η a

Tactic:
exact fun x hx hx_mem ↦ hs hx hx_mem

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

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
⊢ lmarginalPartialTraj κ a b f = f

Tactic:
by
  ext x₀
  rw [lmarginalPartialTraj, partialTraj_le hba, Kernel.lintegral_deterministic']
  · congr with i
    simp [updateFinset]
  · exact mf.comp measurable_updateFinset

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

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ ∫⁻ (z : (i : ↥(Iic b)) → X ↑i), f (updateFinset x₀ (Iic b) z) ∂(partialTraj κ a b) (frestrictLe a x₀) =
    ∫⁻ (x : (i : ↥(Ioc a b)) → X ↑i),
      f (updateFinset x₀ (Ioc a b) x) ∂((partialTraj κ a b).map (restrict₂ ⋯)) (frestrictLe a x₀)

Tactic:
partialTraj_eq_prod,

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ ∫⁻ (z : (i : ↥(Iic b)) → X ↑i),
      f
        (updateFinset x₀ (Iic b)
          z) ∂((Kernel.id ×ₖ (partialTraj κ a b).map (restrict₂ ⋯)).map (_root_.IicProdIoc a b)) (frestrictLe a x₀) =
    ∫⁻ (x : (i : ↥(Ioc a b)) → X ↑i),
      f (updateFinset x₀ (Ioc a b) x) ∂((partialTraj κ a b).map (restrict₂ ⋯)) (frestrictLe a x₀)
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
n : ℕ
s : Set ((i : ↥(Iic n)) → X ↑i)
ms : MeasurableSet s
⊢ (projectiveFamilyContent ⋯) (frestrictLe n ⁻¹' s) = (inducedFamily (fun b ↦ (partialTraj κ a b) x₀) (Iic n)) s

pp: case hC_gen
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
n : ℕ
s : Set ((i : ↥(Iic n)) → X ↑i)
ms : MeasurableSet s
⊢ MeasurableSpace.pi = generateFrom (measurableCylinders X)

pp: case hs
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
n : ℕ
s : Set ((i : ↥(Iic n)) → X ↑i)
ms : MeasurableSet s
⊢ frestrictLe n ⁻¹' s ∈ measurableCylinders X

Tactic:
projectiveFamilyContent_congr _ (frestrictLe n ⁻¹' s) rfl ms

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
n : ℕ
s : Set ((i : ↥(Iic n)) → X ↑i)
ms : MeasurableSet s
⊢ (inducedFamily (fun b ↦ (partialTraj κ a b) x₀) (Iic n)) s =
    (inducedFamily (fun b ↦ (partialTraj κ a b) x₀) (Iic n)) s

case hC_gen
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
n : ℕ
s : Set ((i : ↥(Iic n)) → X ↑i)
ms : MeasurableSet s
⊢ MeasurableSpace.pi = generateFrom (measurableCylinders X)

case hs
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
n : ℕ
s : Set ((i : ↥(Iic n)) → X ↑i)
ms : MeasurableSet s
⊢ frestrictLe n ⁻¹' s ∈ measurableCylinders X
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: case pos
α : 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
b : β
h✝ : b ∈ t
⊢ (η b) s * 1 b = (η b) s

pp: case neg
α : 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
b : β
h✝ : b ∉ t
⊢ (η b) s * 0 = 0

Tactic:
all_goals simp_all

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

Goal state before:
pp: case cylinder
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
ht : t ∈ measurableCylinders X
N : ℕ
S : Set ((i : ↥(Iic N)) → X ↑i)
mS : MeasurableSet S
t_eq : t = cylinder (Iic N) S
⊢ Measurable fun x₀ ↦ (projectiveFamilyContent ⋯) t

Tactic:
projectiveFamilyContent_congr _ t t_eq mS,

Goal state after:
case cylinder
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
ht : t ∈ measurableCylinders X
N : ℕ
S : Set ((i : ↥(Iic N)) → X ↑i)
mS : MeasurableSet S
t_eq : t = cylinder (Iic N) S
⊢ Measurable fun x₀ ↦ (inducedFamily (fun b ↦ (partialTraj κ a b) x₀) (Iic N)) S
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
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 ≠ ⊤

Tactic:
exact ne_top_of_le_ne_top (by simp) integral_le_kernel

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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ (infinitePi fun i ↦ μ (e i)) (⇑(Equiv.piCongrLeft X e) ⁻¹' (⇑e '' ↑(s.preimage ⇑e ⋯)).pi t) = ∏ i ∈ s, (μ i) (t i)

pp: case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Measurable ⇑(piCongrLeft X e)

pp: case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ MeasurableSet ((⇑e '' ↑(s.preimage ⇑e ⋯)).pi t)

Tactic:
Equiv.piCongrLeft_preimage_pi,

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ (infinitePi fun i ↦ μ (e i)) ((↑(s.preimage ⇑e ⋯)).pi fun i ↦ t (e i)) = ∏ i ∈ s, (μ i) (t i)

case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Measurable ⇑(piCongrLeft X e)

case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ MeasurableSet ((⇑e '' ↑(s.preimage ⇑e ⋯)).pi t)
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 b : ℕ
hb : b ≥ a + 1
| (Kernel.id.map id ×ₖ (traj κ a).map ((fun x i ↦ x ⟨↑i, ⋯⟩) ∘ (Set.Ioi a).domRestrict)).map (_root_.IicProdIoc a b)

Tactic:
enter [1, 2, 2]

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 b : ℕ
hb : b ≥ a + 1
| (fun x i ↦ x ⟨↑i, ⋯⟩) ∘ (Set.Ioi a).domRestrict
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : MeasurableSpace R
inst✝² : AddMonoidWithOne R
n : ℕ
p : ↑I
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSingletonClass R
f : R → E
⊢ Integrable f Bin(R, n, p)

Tactic:
simp [map_cast_binomial_eq_sum_dirac, integrable_finsetSum_measure, integrable_dirac,
    Integrable.smul_measure]

Goal state after:
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
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (s.restrict X) P
this✝¹ : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this✝ : (↑s).pi t = s.restrict ⁻¹' Set.univ.pi fun i ↦ t ↑i
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ ∏ i, (map (X ↑i) P) (t ↑i) = ∏ i ∈ s, (map (X i) P) (t i)

Tactic:
s.prod_coe_sort fun i ↦ P.map (X i) (t i)

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (s.restrict X) P
this✝¹ : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this✝ : (↑s).pi t = s.restrict ⁻¹' Set.univ.pi fun i ↦ t ↑i
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ ∏ i ∈ s, (map (X i) P) (t i) = ∏ i ∈ s, (map (X i) P) (t i)