mathlib-initiative/mathlib-tactics huggingface dataset:
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)
χ_dep : ∀ (n : ℕ), DependsOn (χ n) ↑(Iic (a✝ n))
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj κ p (a✝ n) (χ n) (updateFinset x (Iic p) x₀) =
      lmarginalPartialTraj κ p (a✝ n) (χ n) (updateFinset y (Iic p) x₀)
m n : ℕ
hmn : m ≤ n
y a : (n : ℕ) → X n
ha : a ∈ A n
⊢ 1 a ≤ χ m a

Tactic:
simp [χ, A_anti hmn ha]

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)
e : ℕ ≃ ι
s : Set ((i : ι) → X i)
hs : s ∈ measurableCylinders X
⊢ (map (⇑(piCongrLeft X e)) (infinitePiNat fun n ↦ μ (e n))) s = (piContent μ) s

Tactic:
by
  obtain ⟨I, S, hS, rfl⟩ := (mem_measurableCylinders s).1 hs
  rw [map_apply _ hS.cylinder, cylinder, ← Set.preimage_comp, coe_piCongrLeft,
    restrict_comp_piCongrLeft, Set.preimage_comp, ← map_apply,
    infinitePiNat_map_restrict (fun n ↦ μ (e n)), ← cylinder, piContent_cylinder μ hS,
    ← pi_map_piCongrLeft (e.restrictPreimageFinset I), map_apply _ hS, coe_piCongrLeft]
  · simp
  any_goals fun_prop
  exact hS.preimage (by fun_prop)

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

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
⊢ Measurable fun p ↦ κ.rnDeriv η p.1 p.2

Tactic:
by
  simp_rw [rnDeriv_def]
  exact (measurable_rnDerivAux κ _).ennreal_ofReal.div
    (measurable_const.sub (measurable_rnDerivAux κ _)).ennreal_ofReal

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

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 ≤ 1 - κ.rnDerivAux (κ + η) a x

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 < 1 - κ.rnDerivAux (κ + η) a x

Tactic:
· simp only [sub_nonneg, hx.le]

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 < 1 - κ.rnDerivAux (κ + η) a x
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case succ
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)
χ_dep : ∀ (n : ℕ), DependsOn (χ n) ↑(Iic (a n))
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀) =
      lmarginalPartialTraj κ p (a n) (χ n) (updateFinset y (Iic p) x₀)
χ_anti : Antitone χ
lma_inv : ∀ (k M n : ℕ), a n ≤ M → lmarginalPartialTraj κ k M (χ n) = lmarginalPartialTraj κ k (a n) (χ n)
anti_lma : ∀ (k : ℕ) (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x
l : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
hl : ∀ (k : ℕ) (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 (l k x))
l_const : ∀ (x y : (i : ℕ) → X i), l p (updateFinset x (Iic p) x₀) = l p (updateFinset y (Iic p) x₀)
ε : ℝ≥0∞
hε : ∀ (x : (i : ℕ) → X i), l p (updateFinset x (Iic p) x₀) = ε
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀)
χ_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), χ n x ≤ 1
ind : (k : ℕ) → ((i : ↥(Iic k)) → X ↑i) → X (k + 1)
hind :
  ∀ (k : ℕ) (y : (i : ↥(Iic k)) → X ↑i),
    (∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (χ n) (updateFinset x (Iic k) y)) →
      ∀ (x : (i : ℕ) → X i) (n : ℕ),
        ε ≤ lmarginalPartialTraj κ (k + 1) (a n) (χ n) (update (updateFinset x (Iic k) y) (k + 1) (ind k y))
z : (n : ℕ) → X n := iterateInduction x₀ ind
k✝ k : ℕ
hn : p ≤ k
h : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (χ n) (updateFinset x (Iic k) (frestrictLe k z))
⊢ ∀ (x : (i : ℕ) → X i) (n : ℕ),
    ε ≤ lmarginalPartialTraj κ (k + 1) (a n) (χ n) (updateFinset x (Iic (k + 1)) (frestrictLe (k + 1) z))

Tactic:
| succ k hn h =>

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₀ ↦ ((trajContent κ x₀).measure ⋯ ⋯ ⋯) t

Tactic:
AddContent.measure_eq _ _ generateFrom_measurableCylinders.symm _ ht,

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₀ ↦ (trajContent κ x₀) t
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X i.fst i.snd)
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
⊢ (map (⇑(piCurry X).symm) (infinitePi fun i ↦ infinitePi fun j ↦ μ i j)) ((↑s).pi t) = ∏ i ∈ s, (μ i.fst i.snd) (t i)

Tactic:
rw [map_apply (by fun_prop) (.pi (countable_toSet _) fun _ _ ↦ ht _),
    ← Finset.sigma_image_fst_preimage_mk s, coe_piCurry_symm, Finset.coe_sigma,
    Set.uncurry_preimage_sigma_pi, infinitePi_pi, Finset.prod_sigma]

Goal state after:
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X i.fst i.snd)
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
⊢ ∏ i ∈ image Sigma.fst s, (infinitePi fun j ↦ μ i j) ((↑(s.preimage (Sigma.mk i) ⋯)).pi fun j ↦ t ⟨i, j⟩) =
    ∏ a ∈ image Sigma.fst s, ∏ s ∈ s.preimage (Sigma.mk a) ⋯, (μ ⟨a, s⟩.fst ⟨a, s⟩.snd) (t ⟨a, s⟩)

case mt
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X i.fst i.snd)
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
⊢ ∀ i ∈ image Sigma.fst s, MeasurableSet ((↑(s.preimage (Sigma.mk i) ⋯)).pi fun j ↦ t ⟨i, j⟩)
Module: Mathlib.Probability.Distributions.Beta

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ Real.Gamma α * Real.Gamma β / Real.Gamma (α + β) = (↑(Real.Gamma α) * ↑(Real.Gamma β) / ↑(Real.Gamma (α + β))).re

Tactic:
norm_cast

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

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
x✝ : x ∈ Ioc 0 1
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ x ^ (α - 1) * (1 - x) ^ (β - 1) = RCLike.re (↑x ^ (↑α - 1) * (1 - ↑x) ^ (↑β - 1))

Tactic:
norm_cast

Goal state after:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
x✝ : x ∈ Ioc 0 1
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ x ^ (α - 1) * (1 - x) ^ (β - 1) = RCLike.re (↑x ^ ↑(α - 1) * ↑(1 - x) ^ ↑(β - 1))
Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm

Goal state before:
pp: k : ℕ
r : ℝ≥0
p : ℕ → ↑unitInterval
hr : Tendsto (fun n ↦ ↑n * ↑(p n)) atTop (𝓝 ↑r)
⊢ Tendsto (fun n ↦ ↑n * ↑(p n)) atTop (𝓝 ↑r)

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Probability.IdentDistribIndep

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst✝ : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
this : IsFiniteMeasure ν
⊢ Measure.map (fun ω ↦ (X ω, Y ω)) μ = Measure.map (fun ω' ↦ (Z ω', W ω')) ν

Tactic:
hXY.map_prod_eq_prod_map_map hXZ.aemeasurable_fst hYW.aemeasurable_fst,

Goal state after:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst✝ : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
this : IsFiniteMeasure ν
⊢ (Measure.map X μ).prod (Measure.map Y μ) = Measure.map (fun ω' ↦ (Z ω', W ω')) ν
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✝² : Fintype S
inst✝¹ : Fintype T
inst✝ : IsFiniteMeasure P
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 : Ω), ((∏ s, ⇑(f s) ∘ X s) * ∏ t, ⇑(g t) ∘ Y t) x ∂P =
      (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P
⊢ map (fun ω ↦ (fun a ↦ X a ω, fun a ↦ Y a ω)) P = (map (fun c a ↦ X a c) P).prod (map (fun c a ↦ Y a c) P)

Tactic:
refine eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction fun f g ↦ ?_

Goal state after:
Ω : 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✝² : Fintype S
inst✝¹ : Fintype T
inst✝ : IsFiniteMeasure P
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 : Ω), ((∏ s, ⇑(f s) ∘ X s) * ∏ t, ⇑(g t) ∘ Y t) x ∂P =
      (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
⊢ ∫ (p : ((i : S) → E i) × ((j : T) → F j)),
      (∏ i, (f i) (p.1 i)) * ∏ j, (g j) (p.2 j) ∂map (fun ω ↦ (fun a ↦ X a ω, fun a ↦ Y a ω)) P =
    (∫ (x : (i : S) → E i), ∏ i, (f i) (x i) ∂map (fun c a ↦ X a c) P) *
      ∫ (y : (j : T) → F j), ∏ j, (g j) (y j) ∂map (fun c a ↦ Y a c) P
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)]

Goal state after:
Ω : 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
⊢ map (fun ω ↦ (Z ω, fun a ↦ Y a ω)) P = (map Z P).prod (map (fun c a ↦ Y a c) P)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
⊢ ((fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ })
          ((fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) κ₁ X₂✝ ≫
            (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Y₁✝ X₂✝ Y₂✝ κ₂)
          X₃✝ ≫
        (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ })
          { carrier := Y₁✝.carrier × Y₂✝.carrier, str := Prod.instMeasurableSpace } X₃✝ Y₃✝ η) ≫
      { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
          inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom =
    { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
          inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      (fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) κ₁
          { carrier := X₂✝.carrier × X₃✝.carrier, str := Prod.instMeasurableSpace } ≫
        (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Y₁✝
          { carrier := X₂✝.carrier × X₃✝.carrier, str := Prod.instMeasurableSpace }
          { carrier := Y₂✝.carrier × Y₃✝.carrier, str := Prod.instMeasurableSpace }
          ((fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) κ₂ X₃✝ ≫
            (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Y₂✝ X₃✝ Y₃✝ η)

Tactic:
ext : 1; dsimp
    simp only [Kernel.id_parallelComp_comp_parallelComp_id]
    rw [Kernel.deterministic_comp_eq_map, Kernel.comp_deterministic_eq_comap]
    ext _ _ hs
    rw [Kernel.map_apply' _ (by fun_prop) _ hs, Kernel.comap_apply' _ (by fun_prop)]
    repeat rw [Kernel.parallelComp_apply]
    rw [Measure.prod_apply hs, Measure.prod_apply (by measurability), lintegral_prod]
    · congr with a
      rw [Measure.prod_apply (by measurability)]
      rfl
    · refine Measurable.aemeasurable ?_
      exact measurable_measure_prodMk_left (by measurability)

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Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
⊢ ∀ i ∈ s, sets i = f i ⁻¹' g i

Tactic:
intro i

Goal state after:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
i : ι
⊢ i ∈ s → sets i = f i ⁻¹' g i
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
⊢ ∫ (x : Ω), (⇑f ∘ A.indicator 1 * ∏ t, ⇑(g t) ∘ X t) x ∂P =
    (∫ (x : Ω), (⇑f ∘ A.indicator 1) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ X t) x ∂P

Tactic:
have h2 ω : f (A.indicator 1 ω) =
      A.indicator (fun _ ↦ f 1) ω + Aᶜ.indicator (fun _ ↦ f 0) ω := by
    classical
    rw [Set.indicator_apply]
    split_ifs <;> simp_all

Goal state after:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
h2 : ∀ (ω : Ω), f (A.indicator 1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω
⊢ ∫ (x : Ω), (⇑f ∘ A.indicator 1 * ∏ t, ⇑(g t) ∘ X t) x ∂P =
    (∫ (x : Ω), (⇑f ∘ A.indicator 1) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ X t) x ∂P
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 : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
hin : ¬i ≤ n
this : {x | τ x = ↑i} = ∅
⊢ μ[f n | hτ.measurableSpace] =ᶠ[⊥] f i

Tactic:
norm_cast

Goal state after:
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 ∈ Set.range τ, stoppedValue f τ =ᵐ[μ.restrict {x | τ x = i}] μ[f n | hτ.measurableSpace]

Tactic:
intro i

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 ι
⊢ i ∈ Set.range τ → stoppedValue f τ =ᵐ[μ.restrict {x | τ x = i}] μ[f n | hτ.measurableSpace]
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case refine_2
Ω : 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)
h_right :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        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)
h :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
            (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ) (s ×ˢ t ×ˢ u)
⊢ ∀ {s : Set Ω} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (Measure.map (fun ω ↦ (ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
            (⇑(Kernel.id ×ₖ
                    ((condExpKernel μ (MeasurableSpace.comap k inferInstance)).map f ×ₖ
                      (condExpKernel μ (MeasurableSpace.comap k inferInstance)).map g)) ∘ₘ
                μ.trim ⋯)
              (s ×ˢ t ×ˢ u)

Tactic:
· rintro - t u ⟨s, hs, rfl⟩ ht hu
    convert! h hs ht hu
    · exact (h_left hs ht hu).symm
    · exact (h_right hs ht hu).symm

Goal state after: