mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : α
a : β
h1 : ρ.condKernel (a✝, a) = (ρ a✝).condKernel a
h2 : κ (a✝, a) = (ρ a✝).condKernel a
⊢ κ (a✝, a) = ρ.condKernel (a✝, a)

Tactic:
rw [h1, h2]

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)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (f n) ↑(Iic (a n))
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto : ∀ (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X ↑i
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (f n) (updateFinset x (Iic k) y)
n : ℕ
⊢ Nonempty (X n)

Tactic:
induction n using Nat.case_strong_induction_on with
    | hz => exact ⟨y ⟨0, mem_Iic.2 zero_le⟩⟩
    | hi m hm =>
      have : Nonempty (Π i : Iic m, X i) :=
        ⟨fun i ↦ @Classical.ofNonempty _ (hm i.1 (mem_Iic.1 i.2))⟩
      exact nonempty_of_isProbabilityMeasure (κ m Classical.ofNonempty)

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : AEMeasurable X μ
⊢ Var[X; μ | ⊥] = fun _ω ↦ Var[X; μ]

Tactic:
simp [condVar_bot', average_eq_integral, variance_eq_integral hX]

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

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst✝ : Nonempty 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
⊢ minimaxRisk ℓ 0 = 0

Tactic:
simp [minimaxRisk, iInf_subtype']

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

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst✝¹ : Nonempty 𝓧
inst✝ : IsEmpty 𝓨
this : IsEmpty (Subtype IsMarkovKernel)
⊢ minimaxRisk ℓ P = ∞

Tactic:
simp [minimaxRisk, iInf_subtype']

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

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst✝¹ : Nonempty 𝓨
inst✝ : IsEmpty Θ
⊢ minimaxRisk ℓ P = 0

Tactic:
simp [minimaxRisk, iInf_subtype']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n ↦ fs n a
a : α
b : β
⊢ f a b = ∑' (i : ℕ), fs i a b

Tactic:
ENNReal.tsum_eq_liminf_sum_nat

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n ↦ fs n a
a : α
b : β
⊢ f a b = Filter.liminf (fun n ↦ ∑ i ∈ Finset.range n, fs i a b) Filter.atTop
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n ↦ fs n a
a : α
b : β
h_finsetSum : ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) ↑n
⊢ ∀ᶠ (x : ℕ) in Filter.atTop, f a b = min (f a b) ↑x

Tactic:
Filter.eventually_atTop

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n ↦ fs n a
a : α
b : β
h_finsetSum : ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) ↑n
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → f a b = min (f a b) ↑b_1
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ ν : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
x : γ
h1 : (κ.singularPart ν).rnDeriv ν a x = (∂(κ.singularPart ν) a/∂ν a) x
h2 : (∂(κ.singularPart ν) a/∂ν a) x = 0 x
⊢ (κ.singularPart ν).rnDeriv ν a x = 0 x

Tactic:
rw [h1, h2]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ ∀ᵐ (a : α) ∂μ, κ a ≪ η a

Tactic:
suffices ∀ᵐ a ∂μ, κ.singularPart η a = 0 by
    filter_upwards [this] with a ha
    rwa [Kernel.singularPart_eq_zero_iff_absolutelyContinuous] at ha
  rw [← κ.rnDeriv_add_singularPart η, compProd_add_right, AbsolutelyContinuous.add_left_iff] at h
  have : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η :=
    MutuallySingular.compProd_of_right μ ν (.of_forall <| Kernel.mutuallySingular_singularPart _ _)
  refine compProd_eq_zero_iff.mp ?_
  exact eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2 this

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case a
ι : 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 : ι), MeasurableSet (if h : i ∈ s then t ⟨i, h⟩ else Set.univ)

Tactic:
rintro i
    split_ifs with hi
    · exact ht ⟨i, hi⟩
    · exact .univ

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

Goal state before:
pp: case refine_1
α : 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)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
have : f ⁻¹' s = (fun a => κ a s) ⁻¹' {1} := by
      simp only [preimage, mem_singleton_iff]
      simp_rw [hf, Measure.dirac_apply' _ hs]
      ext x
      exact (indicator_eq_one_iff_mem ENNReal).symm

Goal state after:
case refine_1
α : 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)
s : Set β
hs : MeasurableSet s
this : f ⁻¹' s = (fun a ↦ (κ a) s) ⁻¹' {1}
⊢ MeasurableSet (f ⁻¹' s)
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteKernel κ
inst✝¹ : StandardBorelSpace Ω
inst✝ : Nonempty Ω
⊢ Measure.map Prod.swap (μ ⊗ₘ κ) = ⇑(Kernel.swap Ω 𝓧) ∘ₘ μ ⊗ₘ κ

Tactic:
Measure.swap_comp

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteKernel κ
inst✝¹ : StandardBorelSpace Ω
inst✝ : Nonempty Ω
⊢ Measure.map Prod.swap (μ ⊗ₘ κ) = Measure.map Prod.swap (μ ⊗ₘ κ)
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
η : Kernel 𝓧 Ω
inst✝ : IsFiniteKernel η
h : (⇑κ ∘ₘ μ) ⊗ₘ η = ⇑(Kernel.swap Ω 𝓧) ∘ₘ μ ⊗ₘ κ
⊢ ⇑(Kernel.swap Ω 𝓧) ∘ₘ μ ⊗ₘ κ = Measure.map Prod.swap (μ ⊗ₘ κ)

Tactic:
Measure.swap_comp

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
η : Kernel 𝓧 Ω
inst✝ : IsFiniteKernel η
h : (⇑κ ∘ₘ μ) ⊗ₘ η = ⇑(Kernel.swap Ω 𝓧) ∘ₘ μ ⊗ₘ κ
⊢ Measure.map Prod.swap (μ ⊗ₘ κ) = Measure.map Prod.swap (μ ⊗ₘ κ)
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) b ≪ μ
this : (⇑κ ∘ₘ μ) ⊗ₘ κ†μ ≪ (⇑κ ∘ₘ μ).prod μ
⊢ ⇑(Kernel.swap 𝓧 Ω) ∘ₘ (⇑κ ∘ₘ μ) ⊗ₘ κ†μ ≪ Measure.map Prod.swap ((⇑κ ∘ₘ μ).prod μ)

Tactic:
Measure.swap_comp

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) b ≪ μ
this : (⇑κ ∘ₘ μ) ⊗ₘ κ†μ ≪ (⇑κ ∘ₘ μ).prod μ
⊢ Measure.map Prod.swap ((⇑κ ∘ₘ μ) ⊗ₘ κ†μ) ≪ Measure.map Prod.swap ((⇑κ ∘ₘ μ).prod μ)
Module: Mathlib.Probability.Decision.BayesEstimator

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝⁴ : StandardBorelSpace Θ
inst✝³ : Nonempty Θ
hl : Measurable (Function.uncurry ℓ)
P : Kernel Θ 𝓧
inst✝² : IsFiniteKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsSFiniteKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
⊢ avgRisk ℓ P κ π = ∫⁻ (x : 𝓧), ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂κ x ∂⇑P ∘ₘ π

Tactic:
avgRisk_eq_lintegral_posterior_prod hl,

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝⁴ : StandardBorelSpace Θ
inst✝³ : Nonempty Θ
hl : Measurable (Function.uncurry ℓ)
P : Kernel Θ 𝓧
inst✝² : IsFiniteKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsSFiniteKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
⊢ ∫⁻ (θy : Θ × 𝓨), ℓ θy.1 θy.2 ∂⇑(P†π ×ₖ κ) ∘ₘ ⇑P ∘ₘ π =
    ∫⁻ (x : 𝓧), ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂κ x ∂⇑P ∘ₘ π
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝³ : Subsingleton 𝓧
inst✝² : Nonempty 𝓨
inst✝¹ : IsMarkovKernel P
inst✝ : SFinite π
hl : Measurable (uncurry ℓ)
⊢ bayesRisk ℓ P π = ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂π

Tactic:
simp [bayesRisk_of_subsingleton' hl]

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

Goal state before:
pp: case refine_2
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ ∑' (x : α), s.indicator (⇑p) x = 1

Tactic:
suffices ∀ (x) (_ : x ∉ s), p x = 0 from
      _root_.trans (tsum_congr
        fun a => (Set.indicator_apply s p a).trans
          (ite_eq_left_iff.2 <| symm ∘ this a)) p.tsum_coe

Goal state after:
case refine_2
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ ∀ x ∉ s, p x = 0
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 ↦ ENNReal.ofReal (↑(n.choose k) * ↑(p n) ^ k * (1 - ↑(p n)) ^ (n - k))) atTop (𝓝 (Po(r) {k}))

Tactic:
simp_rw [poissonMeasure_singleton]

Goal state after:
k : ℕ
r : ℝ≥0
p : ℕ → ↑unitInterval
hr : Tendsto (fun n ↦ ↑n * ↑(p n)) atTop (𝓝 ↑r)
⊢ Tendsto (fun n ↦ ENNReal.ofReal (↑(n.choose k) * ↑(p n) ^ k * (1 - ↑(p n)) ^ (n - k))) atTop
    (𝓝 (ENNReal.ofReal (Real.exp (-↑r) * ↑r ^ k / ↑k.factorial)))
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
⊢ μ[X | m] - μ[X | m] ^ 2 =ᵐ[μ] μ[X | m] * μ[1 - X | m]

Tactic:
by
      rw [sq, ← one_sub_mul, mul_comm]
      refine .mul ae_eq_rfl ?_
      calc
        1 - μ[X | m]
        _ = μ[1 | m] - μ[X | m] := by simp [Pi.one_def, hm]
        _ =ᵐ[μ] μ[1 - X | m] := by
          refine (condExp_sub (integrable_const _)
            (.of_bound (C := 1) hXmeas.aestronglyMeasurable ?_) _).symm
          filter_upwards [hX]
          rintro ω (hω | hω) <;> simp [hω]

Goal state after:
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)
⊢ μ = fun i ↦ map (Function.eval i) (infinitePi μ)

Tactic:
funext i

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
⊢ iIndepFun X P

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

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

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hm : m ≤ mΩ
hf : AEStronglyMeasurable f μ
⊢ ∀ᵐ (ω : Ω) ∂⇑(condExpKernel μ m) ∘ₘ μ.trim hm, f ω = AEStronglyMeasurable.mk f hf ω

Tactic:
rw [condExpKernel_comp_trim hm]

Goal state after:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hm : m ≤ mΩ
hf : AEStronglyMeasurable f μ
⊢ ∀ᵐ (ω : Ω) ∂μ, f ω = AEStronglyMeasurable.mk f hf ω
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: Ω : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : StandardBorelSpace Ω
hm : m ≤ m0
hμ : IsFiniteMeasure μ
t : Set Ω
ht : MeasurableSet t
h_indep : CondIndepSet m hm t t μ
this : ∀ (a : Ω), IsFiniteMeasure ((condExpKernel μ m) a)
h : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
ω : Ω
hω_eq : ((condExpKernel μ m) ω).real t = μ[t.indicator fun ω ↦ 1 | m] ω
hω : ((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = 1
⊢ ((condExpKernel μ m) ω).real t = 0 ∨ ((condExpKernel μ m) ω).real t = 1

Tactic:
measureReal_eq_zero_iff,

Goal state after:
Ω : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : StandardBorelSpace Ω
hm : m ≤ m0
hμ : IsFiniteMeasure μ
t : Set Ω
ht : MeasurableSet t
h_indep : CondIndepSet m hm t t μ
this : ∀ (a : Ω), IsFiniteMeasure ((condExpKernel μ m) a)
h : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
ω : Ω
hω_eq : ((condExpKernel μ m) ω).real t = μ[t.indicator fun ω ↦ 1 | m] ω
hω : ((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = 1
⊢ ((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω).real t = 1
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m m0 : MeasurableSpace Ω
μ : Measure Ω
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
inst✝¹ : StandardBorelSpace Ω
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iCondIndep m hm 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
h : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
ht : MeasurableSet t
ω : Ω
hω_eq : ((condExpKernel μ m) ω).real t = μ[t.indicator fun ω ↦ 1 | m] ω
hω : ((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = 1
⊢ ((condExpKernel μ m) ω).real t = 0 ∨ ((condExpKernel μ m) ω).real t = 1

Tactic:
measureReal_eq_zero_iff,

Goal state after:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m m0 : MeasurableSpace Ω
μ : Measure Ω
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
inst✝¹ : StandardBorelSpace Ω
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iCondIndep m hm 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
h : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
ht : MeasurableSet t
ω : Ω
hω_eq : ((condExpKernel μ m) ω).real t = μ[t.indicator fun ω ↦ 1 | m] ω
hω : ((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = 1
⊢ ((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω).real t = 1
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X Y : Stoch
κ : X ⟶ Y
⊢ ε ≫ Δ = Δ ≫ (ε ⊗ₘ ε)

Tactic:
by
    ext : 1
    simp only [WideSubcategory.comp_def, MorphismProperty.counit_hom]
    cat_disch

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