mathlib-initiative/mathlib-tactics huggingface dataset:
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 η
⊢ ((κ + η).withDensity fun a x ↦ ↑(κ.rnDerivAux (κ + η) a x).toNNReal) = κ

Tactic:
ext a s hs
  rw [Kernel.withDensity_apply']
  swap; · fun_prop
  simp_rw [ofNNReal_toNNReal]
  exact setLIntegral_rnDerivAux κ η a hs

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)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
⊢ Tendsto (fun n ↦ (piContent μ) (A n)) atTop (𝓝 0)

Tactic:
have r_comp_f n : (s n).restrict ∘ f = (g n) ∘ (fun (x : Π i : u, X i) i ↦ x i) := by
    ext x i
    simp only [Function.comp_apply, Finset.restrict,
      Equiv.piCongrLeft_apply, Equiv.coe_fn_symm_mk, f, aux, g, t]
    rw [dif_pos (Set.mem_iUnion.2 ⟨n, i.2⟩)]

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
⊢ Tendsto (fun n ↦ (piContent μ) (A n)) atTop (𝓝 0)
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
⊢ ((κ.singularPart η) a) s = (κ a) s

Tactic:
have hs' : ∀ x ∈ s, 1 ≤ rnDerivAux κ (κ + η) a x := fun _ hx ↦ hs hx
  rw [singularPart, Kernel.withDensity_apply']
  swap; · exact measurable_singularPart_fun κ η
  calc
    ∫⁻ x in s, ↑(Real.toNNReal (rnDerivAux κ (κ + η) a x)) -
      ↑(Real.toNNReal (1 - rnDerivAux κ (κ + η) a x)) * rnDeriv κ η a x
      ∂(κ + η) a
    = ∫⁻ _ in s, 1 ∂(κ + η) a := by
        refine setLIntegral_congr_fun_ae hsm ?_
        have h_le : κ ≤ κ + η := le_add_of_nonneg_right bot_le
        filter_upwards [rnDerivAux_le_one h_le] with x hx hxs
        have h_eq_one : rnDerivAux κ (κ + η) a x = 1 := le_antisymm hx (hs' x hxs)
        simp [h_eq_one]
  _ = (κ + η) a s := by simp
  _ = κ a s := by
        suffices η a s = 0 by simp [this]
        exact measure_mono_null hs (measure_mutuallySingularSetSlice κ η a)

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✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ (κ.singularPart η) a = 0 ↔ (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ≪ η a

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (κ.singularPart η) a = 0
⊢ (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ≪ η a

case refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ≪ η a
⊢ (κ.singularPart η) a = 0
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 : α
⊢ (η.withDensity (κ.rnDeriv η)) a = 0 ↔ (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ⟂ₘ η a

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a = 0
⊢ (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ⟂ₘ η a

case refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ⟂ₘ η a
⊢ (η.withDensity (κ.rnDeriv η)) a = 0
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 η
⊢ MeasurableSet {a | (κ a) (κ.mutuallySingularSetSlice η a) = 0}

Tactic:
exact measurable_kernel_prodMk_left (measurableSet_mutuallySingularSet κ η)
    (measurableSet_singleton 0)

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)
I : Set ι
⊢ ∀ (s : Finset ↑I) (t : (i : ↑I) → Set (X ↑i)),
    (∀ (i : ↑I), MeasurableSet (t i)) → (map I.domRestrict (infinitePi μ)) ((↑s).pi t) = ∏ i ∈ s, (μ ↑i) (t i)

Tactic:
intro s t ht

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I : Set ι
s : Finset ↑I
t : (i : ↑I) → Set (X ↑i)
ht : ∀ (i : ↑I), MeasurableSet (t i)
⊢ (map I.domRestrict (infinitePi μ)) ((↑s).pi t) = ∏ i ∈ s, (μ ↑i) (t i)
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)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
⊢ (infinitePi μ) (s.pi t) = ∏' (i : ↑s), (μ ↑i) (t ↑i)

Tactic:
wlog s_ne : Nonempty s

Goal state after:
case inr
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
this :
  ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i))
    [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] {s : Set ι},
    Countable ↑s →
      ∀ {t : (i : ι) → Set (X i)},
        (∀ i ∈ s, MeasurableSet (t i)) → Nonempty ↑s → (infinitePi μ) (s.pi t) = ∏' (i : ↑s), (μ ↑i) (t ↑i)
s_ne : ¬Nonempty ↑s
⊢ (infinitePi μ) (s.pi t) = ∏' (i : ↑s), (μ ↑i) (t ↑i)

ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
⊢ (infinitePi μ) (s.pi t) = ∏' (i : ↑s), (μ ↑i) (t ↑i)
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.copy 𝓧 ∘ₖ Kernel.deterministic f hf) ∘ₘ μ = Measure.map f μ ⊗ₘ Kernel.id

Tactic:
by
    rw [Measure.compProd_id_eq_copy_comp, ← Measure.comp_assoc,
      Measure.deterministic_comp_eq_map]

Goal state after:
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)),
    (∀ (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:
intro s t ht

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)
⊢ (map (⇑(piCurry X).symm) (infinitePi fun i ↦ infinitePi fun j ↦ μ i j)) ((↑s).pi t) = ∏ i ∈ s, (μ i.fst i.snd) (t i)
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 ×ₖ (partialTraj κ a b).map (restrict₂ ⋯)).map (_root_.IicProdIoc a b) = partialTraj κ a b

pp: case hf
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
⊢ Measurable (frestrictLe b)

pp: case hg
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
⊢ Measurable (restrict₂ ⋯)

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
⊢ MeasurableSpace ((i : ↥(Ioc a b)) → X ↑i)

Tactic:
map_id,

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
⊢ (Kernel.id ×ₖ (partialTraj κ a b).map (restrict₂ ⋯)).map (_root_.IicProdIoc a b) = partialTraj κ a b

case hf
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
⊢ Measurable (frestrictLe b)

case hg
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
⊢ Measurable (restrict₂ ⋯)

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
⊢ MeasurableSpace ((i : ↥(Ioc a b)) → X ↑i)
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 Θ 𝓧
inst✝² : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsMarkovKernel κ
π : Measure Θ
inst✝ : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
⊢ avgRisk ℓ P κ π ≤ ↑C

Tactic:
by
  refine (avgRisk_le_mul' P κ π hℓC).trans ?_
  rcases isEmpty_or_nonempty Θ
  · simp
  · rcases isEmpty_or_nonempty 𝓧 <;> simp

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

Goal state before:
pp: case pos
x₀ : ℝ
γ : ℝ≥0
h : γ = 0
⊢ Integrable (cauchyPDFReal x₀ γ) volume

Tactic:
simp only [h, cauchyPDFReal_scale_zero]

Goal state after:
case pos
x₀ : ℝ
γ : ℝ≥0
h : γ = 0
⊢ Integrable 0 volume
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, ENNReal.ofReal (if 0 ≤ y then r * rexp (-(r * y)) else 0) = ENNReal.ofReal 0

Tactic:
setLIntegral_congr_fun measurableSet_Iic,

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ ∫⁻ (x : ℝ) in Iic x, ?m.54 x = ENNReal.ofReal 0

r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ EqOn (fun y ↦ ENNReal.ofReal (if 0 ≤ y then r * rexp (-(r * y)) else 0)) ?m.54 (Iic x)

r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ ℝ → ℝ≥0∞
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
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
hf : Integrable f ((traj κ a) x₀)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ ∫ (x : (i : ↥(Iic b)) → X ↑i) in A, ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x ∂(partialTraj κ a b) x₀ =
    ∫ (y : (n : ℕ) → X n) in frestrictLe b ⁻¹' A, f y ∂(traj κ a) x₀

Tactic:
by
  refine setIntegral_traj_partialTraj' hab ?_ hA
  rw [← traj_comp_partialTraj hab, comp_apply, ← Measure.snd_compProd] at hf
  exact hf.comp_measurable measurable_snd

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
⊢ Function.Injective toMeasure

Tactic:
intro p

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p : PMF α
⊢ ∀ ⦃a₂ : PMF α⦄, p.toMeasure = a₂.toMeasure → p = a₂
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0..x, r * rexp (-(r * a))
⊢ ∀ x_1 ∈ Ioo 0 x, HasDerivWithinAt (fun a ↦ -1 * rexp (-(r * a))) (r * rexp (-(r * x_1))) (Ioi x_1) x_1

Tactic:
simp only [neg_mul, one_mul]
        exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp

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

Goal state before:
pp: p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (fun i ↦ (1 - p) ^ i * p) 1
⊢ HasSum (fun n ↦ (1 - p) ^ n * p) 1

Tactic:
exact this

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 Z ν)
⊢ IsFiniteMeasure ν

Tactic:
exact Measure.isFiniteMeasure_of_map hXZ.aemeasurable_snd

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

Goal state before:
pp: Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
⊢ μ[f | MeasurableSpace.generateFrom {s}] =ᵐ[μ.restrict s] fun x ↦ ∫ (x : Ω), f x ∂μ[|s]

Tactic:
by
  by_cases hμs : μ s = 0
  · rw [Measure.restrict_eq_zero.2 hμs]
    rfl
  refine ae_eq_trans (condExp_restrict_ae_eq_restrict
    (generateFrom_singleton_le hs)
    (measurableSet_generateFrom rfl) hf).symm ?_
  · refine (ae_eq_condExp_of_forall_setIntegral_eq (generateFrom_singleton_le hs) hf.restrict ?_ ?_
      stronglyMeasurable_const.aestronglyMeasurable).symm
    · rintro t - -
      rw [integrableOn_const_iff]
      exact Or.inr <| measure_lt_top (μ.restrict s) t
    · rintro t ht -
      obtain (h | h | h | h) := measurableSet_generateFrom_singleton_iff.1 ht
      · simp [h]
      · simp only [h, cond, integral_smul_measure, ENNReal.toReal_inv, integral_const,
        MeasurableSet.univ, measureReal_restrict_apply, univ_inter, measureReal_restrict_apply_self,
        ← measureReal_def]
        rw [smul_inv_smul₀, Measure.restrict_restrict hs, inter_self]
        exact ENNReal.toReal_ne_zero.2 ⟨hμs, measure_ne_top _ _⟩
      · simp only [h, integral_const, MeasurableSet.univ, measureReal_restrict_apply, univ_inter,
          measureReal_restrict_apply hs.compl, compl_inter_self, measureReal_empty, zero_smul,
          ((Measure.restrict_apply_eq_zero hs.compl).2 <| compl_inter_self s ▸ measure_empty),
          setIntegral_measure_zero]
      · simp only [h, Measure.restrict_univ, cond, integral_smul_measure, ENNReal.toReal_inv, ←
        measureReal_def, integral_const, MeasurableSet.univ, measureReal_restrict_apply, univ_inter]
        rw [smul_inv_smul₀]
        exact (measureReal_ne_zero_iff (by finiteness)).2 hμs

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

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

Tactic:
hω₁

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
s t : Set Ω
inst✝ : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (fun ω ↦ ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω).real t) =ᵐ[μ.restrict s]
    μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}]
ω : Ω
hω₁ : μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}] ω = μ[|s].real t
⊢ ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω).real t =
      μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}] ω →
    ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]
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
⊢ ∀ᵐ (ω : Ω) ∂μ, μ[t.indicator fun ω ↦ 1 | m] ω = 0 ∨ μ[t.indicator fun ω ↦ 1 | m] ω = 1

Tactic:
have h := ae_of_ae_trim hm
    (Kernel.measure_zero_or_one_of_measurableSet_limsup h_le h_indep hf hns hnsp hns_univ ht_tail)
  have ht : MeasurableSet t := limsup_le_iSup.trans (iSup_le h_le) t ht_tail
  filter_upwards [condExpKernel_ae_eq_condExp hm ht, h] with ω hω_eq hω
  rwa [← hω_eq, measureReal_eq_zero_iff, measureReal_def, ENNReal.toReal_eq_one_iff]

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

Goal state before:
pp: case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ ∫⁻ (x : X), c * (B.indicator 1 x * A.indicator 1 x) ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), c * A.indicator 1 x ∂π x₀

Tactic:
lintegral_const_mul,

Goal state after:
case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ c * ∫⁻ (a : X), B.indicator 1 a * A.indicator 1 a ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), c * A.indicator 1 x ∂π x₀

case refine_1.hf
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ Measurable fun x ↦ B.indicator 1 x * A.indicator 1 x
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ c * ∫⁻ (a : X), B.indicator 1 a * A.indicator 1 a ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), c * A.indicator 1 x ∂π x₀

pp: case refine_1.hf
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ Measurable fun x ↦ B.indicator 1 x * A.indicator 1 x

Tactic:
lintegral_const_mul,

Goal state after:
case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ c * ∫⁻ (a : X), B.indicator 1 a * A.indicator 1 a ∂π x₀ = B.indicator 1 x₀ * (c * ∫⁻ (a : X), A.indicator 1 a ∂π x₀)

case refine_1.hf
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ Measurable (A.indicator 1)

case refine_1.hf
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ Measurable fun x ↦ B.indicator 1 x * A.indicator 1 x
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (s_1 : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s_1, f i ∈ {s i}) →
        μ[(⋂ i ∈ s_1, f i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s_1, μ[(f i).indicator fun ω ↦ 1 | m']) ↔
    ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω ↦ 1 | m']

Tactic:
simp_all only [Set.mem_singleton_iff]

Goal state after:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (s_1 : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s_1, f i = s i) →
        μ[(⋂ i ∈ s_1, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ x ∈ s_1, μ[(s x).indicator fun ω ↦ 1 | m']) ↔
    ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω ↦ 1 | m']