mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ Tendsto (fun n ↦ (piContent μ) (A n)) atTop (𝓝 0)

Tactic:
let t n : Finset u := (s n).preimage Subtype.val Subtype.val_injective.injOn

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 ⋯
⊢ 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
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
this : (η a) s = 0
⊢ ((κ + η) a) s = (κ a) s

Tactic:
simp [this]

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)
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 : ℕ
hk : p ≤ k
⊢ ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (χ n) (updateFinset x (Iic k) (frestrictLe k z))

Tactic:
induction k, hk using Nat.le_induction with
    | base => exact fun x n ↦ by simpa [z, frestrictLe_iterateInduction] using hpos x n
    | succ k hn h =>
      intro x n
      convert! hind k (fun i ↦ z i.1) h x n
      ext i
      simp only [updateFinset, mem_Iic, frestrictLe_apply, dite_eq_ite, update, z]
      split_ifs with h1 h2 h3 h4 h5
      any_goals lia
      cases h2
      rw [iterateInduction, dif_neg (by lia)]

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)
⊢ IsProbabilityMeasure (infinitePi μ)

Tactic:
by
  constructor
  rw [← cylinder_univ ∅, cylinder, ← map_apply (measurable_restrict _) .univ,
    infinitePi_map_restrict, measure_univ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝³ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ_eq : ∀ᵐ (a : α) ∂μ, κ a = (η.withDensity (κ.rnDeriv η)) a
s : Set (α × β)
hs : MeasurableSet s
x✝ : (μ ⊗ₘ η) s < ∞
⊢ ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = (μ ⊗ₘ κ) s

Tactic:
rw [Measure.compProd_congr hκ_eq, Measure.compProd_withDensity, withDensity_apply _ hs]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝³ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ_eq : ∀ᵐ (a : α) ∂μ, κ a = (η.withDensity (κ.rnDeriv η)) a
s : Set (α × β)
hs : MeasurableSet s
x✝ : (μ ⊗ₘ η) s < ∞
⊢ Measurable (Function.uncurry (κ.rnDeriv η))
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 𝓨
hX : Nonempty 𝓧
x : 𝓧
κ : { κ // IsMarkovKernel κ }
⊢ (fun μ ↦ ⟨Kernel.const 𝓧 ↑μ, ⋯⟩) ((fun κ ↦ ⟨↑κ x, ⋯⟩) κ) = κ

Tactic:
ext y; simp only [Kernel.const_apply, Subsingleton.elim x y]

Goal state after:
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 : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
⊢ ∀ᵐ (x : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) x = μ.withDensity fun ω ↦ κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x

Tactic:
filter_upwards [rnDeriv_posterior_symm h_ac, absolutelyContinuous_posterior h_ac] with x h h_ac'

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 : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
x : 𝓧
h : ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x
h_ac' : (κ†μ) x ≪ μ
⊢ (κ†μ) x = μ.withDensity fun ω ↦ κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x
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 κ π = ∫⁻ (θy : Θ × 𝓨), ℓ θy.1 θy.2 ∂⇑(P†π ×ₖ κ) ∘ₘ ⇑P ∘ₘ π

Tactic:
by
  rw [avgRisk, ← Measure.lintegral_compProd (f := fun θy ↦ ℓ θy.1 θy.2) (by fun_prop)]
  congr
  calc π ⊗ₘ (κ ∘ₖ P) = (Kernel.id ∥ₖ κ) ∘ₘ (π ⊗ₘ P) := Measure.parallelComp_comp_compProd.symm
  _ = (Kernel.id ∥ₖ κ) ∘ₘ ((P†π) ×ₖ Kernel.id) ∘ₘ P ∘ₘ π := by rw [posterior_prod_id_comp]
  _ = ((P†π) ×ₖ κ) ∘ₘ P ∘ₘ π := by
      rw [Measure.comp_assoc, Kernel.parallelComp_comp_prod, Kernel.id_comp, Kernel.comp_id]

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

Goal state before:
pp: α β x : ℝ
hx1 : 0 < x
hx2 : x < 1
hα : 0 < α
hβ : 0 < β
⊢ 0 < 1 - x

Tactic:
linarith

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

Goal state before:
pp: X : Type u_1
inst✝² : MeasurableSpace X
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSingletonClass X
x y : X
p : ↑I
f : X → E
⊢ Integrable f Ber(x, y, p)

Tactic:
by
  simp [bernoulliMeasure_def, integrable_add_measure, integrable_dirac,
    Integrable.smul_measure_nnreal]

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

Goal state before:
pp: case hx
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
x✝ : x ∈ Ioc 0 1
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ 0 ≤ 1 - x

Tactic:
linarith

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

Goal state before:
pp: case hx
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
x✝ : x ∈ Ioc 0 1
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ 0 ≤ x

Tactic:
linarith

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

Goal state before:
pp: y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
a✝² : ℝ
a✝¹ : a✝² < z
b✝ : ℝ
a✝ : z ≤ b✝ ∧ b✝ ≤ y
⊢ a✝² ≠ b✝

Tactic:
linarith

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

Goal state before:
pp: n k : ℕ
p : ↑I
⊢ ↑((Iio n).ncard.choose k) * ↑p ^ k * (1 - ↑p) ^ ((Iio n).ncard - k) = ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)

Tactic:
ncard_Iio_nat

Goal state after:
n k : ℕ
p : ↑I
⊢ ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k) = ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: x a✝¹ r : ℝ
hx : x ≤ 0
a : ℝ
a✝ : a < x
⊢ ¬0 ≤ a

Tactic:
linarith

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

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
a : ℝ
x✝ : a ≤ x
⊢ ¬0 ≤ a

Tactic:
linarith

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : PMF α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : s ∩ p.support = t ∩ p.support
⊢ p.toMeasure s = p.toMeasure t

Tactic:
simpa only [p.toMeasure_apply_eq_toOuterMeasure_apply, hs, ht] using
    p.toOuterMeasure_apply_eq_of_inter_support_eq h

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

Goal state before:
pp: p : ↑unitInterval
hp : p ≠ 0
n : ℕ
⊢ (geometricMeasure p).real {n} = (1 - ↑p) ^ n * ↑p

Tactic:
by
  rw [measureReal_def, geometricMeasure_singleton hp,
    ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]

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

Goal state before:
pp: t r x : ℝ
hx : x ≤ t
a : ℝ
a✝ : a < x
⊢ ¬t ≤ a

Tactic:
linarith

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

Goal state before:
pp: t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
⊢ 0 < x

Tactic:
linarith

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

Goal state before:
pp: case refine_2
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
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
i_f' : Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) (Measure.map (frestrictLe b) ((traj κ a) x₀))
⊢ AEStronglyMeasurable ((fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) ∘ frestrictLe b) ((traj κ a) x₀)

Tactic:
exact (i_f'.1.comp_ae_measurable' (measurable_frestrictLe b).aemeasurable)

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

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ -(r + 1) < -1

Tactic:
linarith

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm

Goal state before:
pp: k : ℕ
r : ℝ≥0
p : ℕ → ↑unitInterval
hr : Tendsto (fun n ↦ ↑n * ↑(p n)) atTop (𝓝 ↑r)
t1 : Tendsto (fun n ↦ ENNReal.ofReal (↑(n.choose k) * ↑(p n) ^ k * (1 - ↑(p n)) ^ (n - k))) atTop (𝓝 (Po(r) {k}))
⊢ (fun n ↦ ENNReal.ofReal (↑(n.choose k) * ↑(p n) ^ k * (1 - ↑(p n)) ^ (n - k))) =ᶠ[atTop] fun n ↦ Bin(n, p n) {k}

Tactic:
simpa only [EventuallyEq, eventually_atTop, ge_iff_le] using
    ⟨k, fun b hb ↦ (binomial_singleton b k (p b)).symm⟩

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

Goal state before:

Tactic:
(∑' b, ite (b ∈ s) (∑' a, p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0) =
        ∑' (b) (a), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
      tsum_congr fun b => by split_ifs with hbs <;> simp only [tsum_zero]
    _ = ∑' (a) (b), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
      ENNReal.tsum_comm
    _ = ∑' a, p a * ∑' b, ite (b ∈ s) (dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
      (tsum_congr fun a => by simp only [← ENNReal.tsum_mul_left, mul_ite, mul_zero])
    _ = ∑' a, p a * dite (p a = 0) (fun h => 0) fun h => ∑' b, ite (b ∈ s) (f a h b) 0 :=
      tsum_congr fun a => by split_ifs with ha <;> simp only [ite_self, tsum_zero]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
mX : MeasurableSpace 𝓧
A : Set Ω
X : Ω → 𝓧
h : A.indicator 1 ⟂ᵢ[P] X
⊢ IndepSets {A} {s | MeasurableSet s} P

Tactic:
rw [IndepSets_iff]
  rintro s - hs ⟨t, ht, rfl⟩
  rw [Set.mem_singleton_iff.1 hs]
  have hA' : A = A.indicator (1 : Ω → ℝ) ⁻¹' {1} := by ext; simp [Set.indicator]
  rw [hA']
  exact h.measure_inter_preimage_eq_mul _ _ (by simp) ht

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_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.Independence.ZeroOne

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

Tactic:
specialize h_indep t t (measurableSet_generateFrom (Set.mem_singleton t))
    (measurableSet_generateFrom (Set.mem_singleton t))
  filter_upwards [h_indep] with a ha
  by_cases h0 : κ a t = 0
  · exact Or.inl h0
  by_cases h_top : κ a t = ∞
  · exact Or.inr (Or.inr h_top)
  rw [← one_mul (κ a (t ∩ t)), Set.inter_self, ENNReal.mul_left_inj h0 h_top] at ha
  exact Or.inr (Or.inl ha.symm)

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
φ₁ φ₂ : Measure α
hφ : φ₁ ≤ φ₂
κ : Kernel α α
hκ : IsIrreducible φ₂ κ
s : Set α
hs : MeasurableSet s
hsp : φ₁ s > 0
⊢ ∀ (a : α), ∃ n, ((κ ^ n) a) s > 0

Tactic:
by
    simpa using hκ.irreducible hs <| Std.lt_of_lt_of_le hsp (hφ s)

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Ω
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndepSets m' hm' π μ ↔
    ∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, f i ∈ π i) → μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']

Tactic:
simp only [iCondIndepSets, Kernel.iIndepSets]
  have h_eq' : ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i, i ∈ s → f i ∈ π i) i (_hi : i ∈ s),
      (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω (f i))) =ᵐ[μ] μ⟦f i | m'⟧ :=
    fun s f H i hi ↦ condExpKernel_ae_eq_condExp hm' (hπ i (f i) (H i hi))
  have h_eq : ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i, i ∈ s → f i ∈ π i), ∀ᵐ ω ∂μ,
      ∀ i ∈ s, ENNReal.toReal (condExpKernel μ m' ω (f i)) = (μ⟦f i | m'⟧) ω := by
    intro s f H
    simp_rw [← Finset.mem_coe]
    rw [ae_ball_iff (Finset.countable_toSet s)]
    exact h_eq' s f H
  have h_inter_eq : ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i, i ∈ s → f i ∈ π i),
      (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω (⋂ i ∈ s, f i)))
        =ᵐ[μ] μ⟦⋂ i ∈ s, f i | m'⟧ := by
    refine fun s f H ↦ condExpKernel_ae_eq_condExp hm' ?_
    exact MeasurableSet.biInter (Finset.countable_toSet _) (fun i hi ↦ hπ i _ (H i hi))
  refine ⟨fun h s f hf ↦ ?_, fun h s f hf ↦ ?_⟩ <;> specialize h s hf
  · have h' := ae_eq_of_ae_eq_trim h
    filter_upwards [h_eq s f hf, h_inter_eq s f hf, h'] with ω h_eq h_inter_eq h'
    rw [← h_inter_eq, h', ENNReal.toReal_prod, Finset.prod_apply]
    exact Finset.prod_congr rfl h_eq
  · refine ((stronglyMeasurable_condExpKernel ?_).ae_eq_trim_iff hm' ?_).mpr ?_
    · exact .biInter (Finset.countable_toSet _) (fun i hi ↦ hπ i _ (hf i hi))
    · refine Measurable.stronglyMeasurable ?_
      exact Finset.measurable_fun_prod s (fun i hi ↦ measurable_condExpKernel (hπ i _ (hf i hi)))
    filter_upwards [h_eq s f hf, h_inter_eq s f hf, h] with ω h_eq h_inter_eq h
    have h_ne_top : condExpKernel μ m' ω (⋂ i ∈ s, f i) ≠ ∞ :=
      (measure_ne_top (condExpKernel μ m' ω) _)
    have : (∏ i ∈ s, condExpKernel μ m' ω (f i)) ≠ ∞ :=
      ENNReal.prod_ne_top fun _ _ ↦ measure_ne_top (condExpKernel μ m' ω) _
    rw [← ENNReal.ofReal_toReal h_ne_top, h_inter_eq, h, Finset.prod_apply,
      ← ENNReal.ofReal_toReal this, ENNReal.toReal_prod]
    congr 1
    exact Finset.prod_congr rfl (fun i hi ↦ (h_eq i hi).symm)

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

Goal state before:
pp: case mpr
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := ⋯
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
e : X × ↑I
⊢ (∃ i, ↑a < ↑i ∧ ∃ (x : 0 ≤ i ∧ ↑i ≤ 1), (κ e.1).real (Icc 0 ⟨↑i, ⋯⟩) < ↑e.2) →
    ∃ a_2, ∃ (h : 0 ≤ a_2 ∧ a_2 ≤ 1), (κ e.1).real (Icc 0 ⟨a_2, ⋯⟩) < ↑e.2 ∧ a < ⟨a_2, ⋯⟩

Tactic:
· intro he
        obtain ⟨q, hqa, hqI, h⟩ := he
        refine ⟨q, ⟨by simp [hqI.1], hqI.2⟩, h, ?_⟩
        change a.1 < q
        simp [hqa]

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 : ι
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] =ᵐ[μ.restrict {x | τ x = ↑i}] f i

Tactic:
simp [this]

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 : ι
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
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst✝ : SFinite μ
s : Set Ω
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (μ.tilted fun x ↦ t * X x) s = ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ

Tactic:
tilted_mul_apply_mgf s,

Goal state after:
case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst✝ : SFinite μ
s : Set Ω
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

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

pp: case e'_3
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ 1 = (p + (1 - p)) ^ n

Tactic:
· rw [Finset.sum_fin_eq_sum_range]
      apply Finset.sum_congr rfl
      intro i hi
      rw [Finset.mem_range] at hi
      rw [dif_pos hi]

Goal state after:
case e'_3
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ 1 = (p + (1 - p)) ^ n
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case hxy
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
h0 : ¬κ ω' = 0
⊢ mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
exact h t

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
⊢ ∫ (a : α) in p.support, f a ∂p.toMeasure = ∑' (a : ↑p.support), (p.toMeasure {↑a}).toReal • f ↑a

Tactic:
apply setIntegral_countable f p.support_countable

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
⊢ IntegrableOn f p.support p.toMeasure