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

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f) x = ρ'.condKernel x
this : Measure.map (Prod.map id f) ρ = ρ'.fst ⊗ₘ ρ.condKernel.map f
heq :
  ∀ᵐ (x : α) ∂(Measure.map (Prod.map id f) ρ).fst, (ρ.condKernel.map f) x = (Measure.map (Prod.map id f) ρ).condKernel x
⊢ ∀ᵐ (x : α) ∂ρ.fst, ∀ (s : Set ℝ), MeasurableSet s → (ρ'.condKernel x) s = (ρ.condKernel x) (f ⁻¹' s)

Tactic:
hρ'

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f) x = ρ'.condKernel x
this : Measure.map (Prod.map id f) ρ = ρ'.fst ⊗ₘ ρ.condKernel.map f
heq : ∀ᵐ (x : α) ∂ρ.fst, (ρ.condKernel.map f) x = (Measure.map (Prod.map id f) ρ).condKernel x
⊢ ∀ᵐ (x : α) ∂ρ.fst, ∀ (s : Set ℝ), MeasurableSet s → (ρ'.condKernel x) s = (ρ.condKernel x) (f ⁻¹' s)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
⊢ frestrictLe₂ hab ∘ IicProdIoc a b = Prod.fst

Tactic:
ext x i

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a b)) → X ↑i)
i : ↥(Iic a)
⊢ (frestrictLe₂ hab ∘ IicProdIoc a b) x i = x.1 i
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
⊢ restrict₂ ⋯ ∘ IicProdIoc a b = Prod.snd

Tactic:
ext x i

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a b)) → X ↑i)
i : ↥(Ioc a b)
⊢ (restrict₂ ⋯ ∘ IicProdIoc a b) x i = x.2 i
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a : ι
⊢ IicProdIoc a a = Prod.fst

Tactic:
ext x i

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a : ι
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a a)) → X ↑i)
i : ↥(Iic a)
⊢ IicProdIoc a a x i = x.1 i
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hba : b ≤ a
⊢ IicProdIoc a b = frestrictLe₂ hba ∘ Prod.fst

Tactic:
ext x i

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hba : b ≤ a
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a b)) → X ↑i)
i : ↥(Iic b)
⊢ IicProdIoc a b x i = (frestrictLe₂ hba ∘ Prod.fst) x i
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 : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
⊢ _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc

Tactic:
ext x i

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
x : (((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a k)) → X ↑i)) × ((i : ↥(Ioc k (k + 1))) → X ↑i)
i : ↥(Iic (k + 1))
⊢ (_root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id) x i =
    ((⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc) x i
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
p : ↑I
s : Set ℕ
⊢ (map Set.ncard setBer(u, p)) s = setBer(u, p) {t | t ⊆ u ∧ t.ncard ∈ s}

Tactic:
by
  rw [map_apply (by fun_prop) .of_discrete, setBernoulli_apply_eq_apply_subsets]
  simp [And.comm]

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
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
this : (f a b).toReal ≤ ↑n
⊢ f a b ≤ ↑n

Tactic:
← ENNReal.le_ofReal_iff_toReal_le (hf_ne_top a b) _

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
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
this : f a b ≤ ENNReal.ofReal ↑n
⊢ f a b ≤ ↑n

α : 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
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
this : (f a b).toReal ≤ ↑n
⊢ 0 ≤ ↑n
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)
n : ℕ
⊢ (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i

Tactic:
ext x i

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)
n : ℕ
x : (i : ↑u) → X ↑i
i : ↥(s n)
⊢ ((s n).restrict ∘ f) x i = (⇑(g n) ∘ fun x i ↦ x ↑i) x i
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 : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn f ↑(Iic a)
hab : a ≤ b
x : (n : ℕ) → X n
⊢ ∫⁻ (x_1 : (i : ↥(Ioc b c)) → X ↑i),
      f (Function.updateFinset x (Ioc b c) x_1) ∂((partialTraj κ b c).map (restrict₂ ⋯)) (frestrictLe b x) =
    f x

Tactic:
refine @lintegral_eq_const _ _ _ ?_ _ _ (ae_of_all _ fun y ↦ hf fun i hi ↦ ?_)

Goal state after:
case refine_1
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn f ↑(Iic a)
hab : a ≤ b
x : (n : ℕ) → X n
⊢ IsProbabilityMeasure (((partialTraj κ b c).map (restrict₂ ⋯)) (frestrictLe b x))

case refine_2
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn f ↑(Iic a)
hab : a ≤ b
x : (n : ℕ) → X n
y : (i : ↥(Ioc b c)) → X ↑i
i : ℕ
hi : i ∈ ↑(Iic a)
⊢ Function.updateFinset x (Ioc b c) y i = x 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 : ℕ
⊢ (traj κ a).map (frestrictLe b) = partialTraj κ a b

Tactic:
ext x
  rw [map_apply, traj_apply, frestrictLe, isProjectiveLimit_trajFun, inducedFamily_Iic]
  fun_prop

Goal state after:
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 Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
⊢ ∫⁻ (θ : Θ), ↑C * ∫⁻ (x : 𝓧), (κ x) Set.univ ∂P θ ∂π ≤ ∫⁻ (θ : Θ), ↑C * ∫⁻ (x : 𝓧), κ.bound ∂P θ ∂π

Tactic:
gcongr with θ x

Goal state after:
case hfg
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
θ : Θ
x : 𝓧
⊢ (κ x) Set.univ ≤ κ.bound
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)
⊢ map (⇑(piCurry X).symm) (infinitePi fun i ↦ infinitePi fun j ↦ μ i j) = infinitePi fun p ↦ μ p.fst p.snd

Tactic:
by
  apply eq_infinitePi
  intro s t ht
  classical
  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]
  · exact Finset.prod_congr rfl (fun _ _ ↦ infinitePi_pi _ fun _ _ ↦ ht _)
  · simp only [mem_image, Sigma.exists, exists_and_right, exists_eq_right, forall_exists_index]
    exact fun i j hij ↦ MeasurableSet.pi (countable_toSet _) fun k hk ↦ by simp_all

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

Goal state before:
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 b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ MeasurableSet ((fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

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 : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ MeasurableSet s

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 : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ Measurable fun x ↦ (frestrictLe b x, 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 b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ MeasurableSet s

Tactic:
any_goals exact ms.preimage (by fun_prop)

Goal state after:
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 : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ Measurable fun x ↦ (frestrictLe b x, x)
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))
⊢ ∫ (a : ℝ) in 0..x, r * rexp (-(r * a)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal

Tactic:
intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _

Goal state after:
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))
⊢ -1 * rexp (-(r * x)) - -1 * rexp (-(r * 0)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal

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))
⊢ IntervalIntegrable (fun a ↦ r * rexp (-(r * a))) volume 0 x

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))
⊢ ContinuousOn (fun a ↦ -1 * rexp (-(r * a))) (Icc 0 x)

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
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
⊢ (p.bind f).toOuterMeasure s = ∑' (a : α), p a * (f a).toOuterMeasure s

Tactic:
classical
  calc
    (p.bind f).toOuterMeasure s = ∑' b, if b ∈ s then ∑' a, p a * f a b else 0 := by
      simp [toOuterMeasure_apply, Set.indicator_apply]
    _ = ∑' (b) (a), p a * if b ∈ s then f a b else 0 := tsum_congr fun b => by split_ifs <;> simp
    _ = ∑' (a) (b), p a * if b ∈ s then f a b else 0 := ENNReal.tsum_comm
    _ = ∑' a, p a * ∑' b, if b ∈ s then f a b else 0 := tsum_congr fun _ => ENNReal.tsum_mul_left
    _ = ∑' a, p a * ∑' b, if b ∈ s then f a b else 0 :=
      (tsum_congr fun a => (congr_arg fun x => p a * x) <| tsum_congr fun b => by split_ifs <;> rfl)
    _ = ∑' a, p a * (f a).toOuterMeasure s :=
      tsum_congr fun a => by simp only [toOuterMeasure_apply, Set.indicator_apply]

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

Goal state before:
pp: case false.mpr
p : ℝ≥0
h : p ≤ 1
⊢ p = 1 → 1 - ↑p = 0

Tactic:
· intro h'
      simp only [h', ENNReal.coe_one, tsub_self]

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

Goal state before:
pp: case pos
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : volume s = 0 ∨ volume s = ∞
⊢ Integrable (fun x ↦ x * (pdf X ℙ volume x).toReal) volume

Tactic:
have I : Integrable (fun x ↦ x * ENNReal.toReal (0)) := by simp
    apply I.congr
    filter_upwards [pdf_eq_zero_of_measure_eq_zero_or_top huX hnt] with x hx
    simp [hx]

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

Goal state before:
pp: case refine_1
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ (∑ a ∈ s, if a ∈ s then (↑(#s))⁻¹ else 0) = 1

Tactic:
simp only [Finset.sum_ite_mem, Finset.inter_self, Finset.sum_const, nsmul_eq_mul]

Goal state after:
case refine_1
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ ↑(#s) * (↑(#s))⁻¹ = 1
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : StandardBorelSpace β
inst✝ : Nonempty β
X : Ω → β
Y : Ω → γ
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
⊢ (fun a ↦ ((condDistrib X Y μ) (Y a)) s) =ᵐ[μ] fun a ↦ ((condExpKernel μ (MeasurableSpace.comap Y mγ)) a) (X ⁻¹' s)

Tactic:
filter_upwards [condDistrib_ae_eq_condExp hY hX (μ := μ) hs,
    condExpKernel_ae_eq_condExp hY.comap_le (μ := μ) (hX hs)] with a ha₁ ha₂

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : StandardBorelSpace β
inst✝ : Nonempty β
X : Ω → β
Y : Ω → γ
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
a : Ω
ha₁ : ((condDistrib X Y μ) (Y a)).real s = μ[(X ⁻¹' s).indicator fun ω ↦ 1 | MeasurableSpace.comap Y mγ] a
ha₂ :
  ((condExpKernel μ (MeasurableSpace.comap Y mγ)) a).real (X ⁻¹' s) =
    μ[(X ⁻¹' s).indicator fun ω ↦ 1 | MeasurableSpace.comap Y mγ] a
⊢ ((condDistrib X Y μ) (Y a)) s = ((condExpKernel μ (MeasurableSpace.comap Y mγ)) a) (X ⁻¹' s)
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
h : ∀ᵐ (a : α) ∂μα, IsFiniteMeasure (κ a)
t : Set Ω
h_indep : IndepSet t t κ μα
⊢ ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1

Tactic:
filter_upwards [measure_eq_zero_or_one_or_top_of_indepSet_self h_indep, h] with a h_0_1_top h'
  simpa only [measure_ne_top (κ a), or_false] using h_0_1_top

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

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
s t : Set Ω
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (s ∩ t) = ((condExpKernel μ m') a) s * ((condExpKernel μ m') a) t
hs : s ∈ s1
ht : t ∈ s2
h'✝ : (fun x ↦ ((condExpKernel μ m') x) (s ∩ t)) =ᵐ[μ] fun x ↦ ((condExpKernel μ m') x) s * ((condExpKernel μ m') x) t
ω : Ω
hs_eq : (((condExpKernel μ m') ω) s).toReal = μ[s.indicator fun ω ↦ 1 | m'] ω
ht_eq : (((condExpKernel μ m') ω) t).toReal = μ[t.indicator fun ω ↦ 1 | m'] ω
hst_eq : (((condExpKernel μ m') ω) (s ∩ t)).toReal = μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω
h' : ((condExpKernel μ m') ω) (s ∩ t) = ((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t
⊢ (((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t).toReal =
    (((condExpKernel μ m') ω) s).toReal * (((condExpKernel μ m') ω) t).toReal

Tactic:
ENNReal.toReal_mul

Goal state after:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
s t : Set Ω
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (s ∩ t) = ((condExpKernel μ m') a) s * ((condExpKernel μ m') a) t
hs : s ∈ s1
ht : t ∈ s2
h'✝ : (fun x ↦ ((condExpKernel μ m') x) (s ∩ t)) =ᵐ[μ] fun x ↦ ((condExpKernel μ m') x) s * ((condExpKernel μ m') x) t
ω : Ω
hs_eq : (((condExpKernel μ m') ω) s).toReal = μ[s.indicator fun ω ↦ 1 | m'] ω
ht_eq : (((condExpKernel μ m') ω) t).toReal = μ[t.indicator fun ω ↦ 1 | m'] ω
hst_eq : (((condExpKernel μ m') ω) (s ∩ t)).toReal = μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω
h' : ((condExpKernel μ m') ω) (s ∩ t) = ((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t
⊢ (((condExpKernel μ m') ω) s).toReal * (((condExpKernel μ m') ω) t).toReal =
    (((condExpKernel μ m') ω) s).toReal * (((condExpKernel μ m') ω) t).toReal
Module: Mathlib.Probability.Kernel.Proper

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

Tactic:
by
  rw [← lintegral_indicator hA, ← hπ.setLIntegral_eq_indicator_mul_lintegral h𝓑𝓧 _ hB,
    setLIntegral_indicator] <;> measurability

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

Goal state before:
pp: case e'_2
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ (∑ i ∈ Finset.range (n + 1),
      if h : i < n + 1 then p ^ ↑⟨i, h⟩ * (1 - p) ^ (n - ↑⟨i, h⟩) * ↑(n.choose ↑⟨i, h⟩) else 0) =
    ∑ m ∈ Finset.range (n + 1), p ^ m * (1 - p) ^ (n - m) * ↑(n.choose m)

Tactic:
apply Finset.sum_congr rfl

Goal state after:
case e'_2
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ ∀ x ∈ Finset.range (n + 1),
    (if h : x < n + 1 then p ^ ↑⟨x, h⟩ * (1 - p) ^ (n - ↑⟨x, h⟩) * ↑(n.choose ↑⟨x, h⟩) else 0) =
      p ^ x * (1 - p) ^ (n - x) * ↑(n.choose x)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : {ω | 0 < X ω} = ⋃ ε, {ω | ↑↑ε ≤ X ω}
hb : ∀ (ε : ℚ), ∀ᵐ (ω' : Ω') ∂ν, 0 < ε → (κ ω') {ω | ↑ε ≤ X ω} = 0
ω' : Ω'
hn : ∀ (i : ℚ), 0 < i → (κ ω') {ω | ↑i ≤ X ω} = 0
⊢ ∀ (a : ℚ), 0 < a → (κ ω') {ω | ↑a ≤ X ω} = 0

Tactic:
exact fun _ ↦ hn _

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case hg
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 := ⋯
q : ℝ≥0 := ⋯
ω' : Ω'
hmX : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑cX * t ^ 2 / 2)
hmY : ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑cY * t ^ 2 / 2)
hlX : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')
hlY : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')
t : ℝ
⊢ MemLp (fun a ↦ rexp (t * Y a)) (ENNReal.ofReal ↑q) (κ ω')

Tactic:
simpa using (hlY t)

Goal state after: