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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
⊢ Integrable (fun x ↦ ∫ (y : Ω), ‖f (x, y)‖ ∂(Measure.map (fun a ↦ (X a, Y a)) μ).condKernel x)
    (Measure.map (fun a ↦ (X a, Y a)) μ).fst

Tactic:
exact hf_int.integral_norm_condKernel

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun m ↦ ∫ (x : γ), κ.density ν a x (seq m) ∂ν a) atTop (𝓝 ((κ a).real univ))

Tactic:
by
  have : IsFiniteKernel κ := isFiniteKernel_of_isFiniteKernel_fst (h := isFiniteKernel_of_le hκν)
  simp_rw [integral_density hκν a (hseq_meas _)]
  have h_cont := ENNReal.continuousOn_toReal.continuousAt (x := κ a univ) ?_
  swap
  · rw [mem_nhds_iff]
    refine ⟨Iio (κ a univ + 1), fun x hx ↦ ne_top_of_lt (?_ : x < κ a univ + 1), isOpen_Iio, ?_⟩
    · simpa using hx
    · simp only [mem_Iio]
      exact ENNReal.lt_add_right (measure_ne_top _ _) one_ne_zero
  refine h_cont.tendsto.comp ?_
  convert! tendsto_measure_iUnion_atTop (monotone_const.set_prod hseq)
  rw [← prod_iUnion, hseq_iUnion, univ_prod_univ]

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

Goal state before:
pp: case pos
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ μ s = 0

Tactic:
exact hμs

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

Goal state before:
pp: β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x ↦ f x.2) (Measure.map (fun ω ↦ (X ω, ω)) μ)

Tactic:
by
  refine ⟨fun x => hf.mk f x.2, hf.stronglyMeasurable_mk.comp_measurable measurable_snd, ?_⟩
  suffices h : Measure.QuasiMeasurePreserving Prod.snd (μ.map fun ω ↦ (X ω, ω)) μ from
    Measure.QuasiMeasurePreserving.ae_eq h hf.ae_eq_mk
  refine ⟨measurable_snd, Measure.AbsolutelyContinuous.mk fun s hs hμs => ?_⟩
  rw [Measure.map_apply measurable_snd hs]
  by_cases hX : AEMeasurable X μ
  · rw [Measure.map_apply_of_aemeasurable]
    · rw [← univ_prod, mk_preimage_prod, preimage_univ, univ_inter, preimage_id']
      exact hμs
    · exact hX.prodMk aemeasurable_id
    · exact measurable_snd hs
  · rw [Measure.map_of_not_aemeasurable]
    · simp
    · contrapose hX; exact measurable_fst.comp_aemeasurable hX

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

Goal state before:
pp: case inl
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 : ℕ
hba : b ≤ a
⊢ partialTraj κ a b = (Kernel.id ×ₖ (partialTraj κ a b).map (restrict₂ ⋯)).map (_root_.IicProdIoc a b)

Tactic:
partialTraj_le hba,

Goal state after:
case inl
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 : ℕ
hba : b ≤ a
⊢ deterministic (frestrictLe₂ hba) ⋯ =
    (Kernel.id ×ₖ (deterministic (frestrictLe₂ hba) ⋯).map (restrict₂ ⋯)).map (_root_.IicProdIoc a b)
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
a : α
⊢ ((Kernel.sum κ).withDensity f) a = (Kernel.sum fun i ↦ (κ i).withDensity f) a

Tactic:
sum_apply,

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
a : α
⊢ ((Kernel.sum κ).withDensity f) a = Measure.sum fun n ↦ ((κ n).withDensity f) a
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
a : α
⊢ ((Kernel.sum κ) a).withDensity (f a) = Measure.sum fun n ↦ ((κ n) a).withDensity (f a)

Tactic:
sum_apply,

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
a : α
⊢ (Measure.sum fun n ↦ (κ n) a).withDensity (f a) = Measure.sum fun n ↦ ((κ n) a).withDensity (f a)
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᵐ[κ a] f a
⊢ (κ.withDensity fun a x ↦ f a x - g a x) + κ.withDensity g = κ.withDensity f

Tactic:
rw [← withDensity_add_right _ hg]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᵐ[κ a] f a
⊢ κ.withDensity ((fun a x ↦ f a x - g a x) + g) = κ.withDensity f

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᵐ[κ a] f a
⊢ Measurable (Function.uncurry fun a x ↦ f a x - g a x)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case inl
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
k : ℕ
x : (n : ℕ) → X n
h : Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop atBot
⊢ ∃ l, Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 l)

Tactic:
rw [OrderBot.atBot_eq] at h
      exact ⟨0, h.mono_right <| pure_le_nhds 0⟩

Goal state after:
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))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ ∫⁻ (z : (i : ↥(Iic b)) → X ↑i), f (updateFinset x₀ (Iic b) z) ∂(partialTraj κ a b) (frestrictLe a x₀) = f x₀

Tactic:
partialTraj_le hba,

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ ∫⁻ (z : (i : ↥(Iic b)) → X ↑i),
      f (updateFinset x₀ (Iic b) z) ∂(deterministic (frestrictLe₂ hba) ⋯) (frestrictLe a x₀) =
    f x₀
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: 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))

Tactic:
refine @IsMarkovKernel.isProbabilityMeasure _ _ _ _ _ ?_ _

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
⊢ IsMarkovKernel ((partialTraj κ b c).map (restrict₂ ⋯))
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 n : ℕ
η : Kernel ((i : ↥(Iic a)) → X ↑i) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe b) = partialTraj κ a b
x : (i : ↥(Iic a)) → X ↑i
⊢ IsProjectiveLimit (η x) (inducedFamily fun n ↦ (partialTraj κ a n) x)

Tactic:
rw [isProjectiveLimit_nat_iff' _ _ n]

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 n : ℕ
η : Kernel ((i : ↥(Iic a)) → X ↑i) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe b) = partialTraj κ a b
x : (i : ↥(Iic a)) → X ↑i
⊢ ∀ ⦃n_1 : ℕ⦄, n ≤ n_1 → Measure.map (frestrictLe n_1) (η x) = inducedFamily (fun n ↦ (partialTraj κ a n) x) (Iic n_1)

X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a n : ℕ
η : Kernel ((i : ↥(Iic a)) → X ↑i) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe b) = partialTraj κ a b
x : (i : ↥(Iic a)) → X ↑i
⊢ IsProjectiveMeasureFamily (inducedFamily fun n ↦ (partialTraj κ a n) x)
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 𝓨
π : Measure Θ
⊢ avgRisk ℓ P (Kernel.const 𝓧 ν) π = ∫⁻ (θ : Θ), (P θ) Set.univ * ∫⁻ (y : 𝓨), ℓ θ y ∂ν ∂π

Tactic:
by
  simp [avgRisk, Kernel.const_comp]

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∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst✝¹ : SFinite μ
π : Measure Θ
inst✝ : SFinite π
hl_pos : μ Set.univ = ∞ → ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂π = 0 → ∃ y, ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
hμ : μ Set.univ = 0
⊢ μ = 0

Tactic:
simpa using hμ

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

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_3
𝓨 : Type u_5
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝¹ : Fintype 𝓨
inst✝ : MeasurableSingletonClass 𝓨
hℓ : Measurable ℓ
μ : Measure 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
⊢ avgRisk ℓ (Kernel.const Θ μ) κ π = ∑ y, ∫⁻ (θ : Θ), ℓ θ y * (⇑κ ∘ₘ μ) {y} ∂π

Tactic:
simp [avgRisk_fintype' hℓ]

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

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ ∫ (a : ℝ) in Ioo 0 1, 1 / beta α β * a ^ (α - 1) * (1 - a) ^ (β - 1) = 1

Tactic:
simp_rw [mul_assoc, integral_const_mul]

Goal state after:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ 1 / beta α β * ∫ (a : ℝ) in Ioo 0 1, a ^ (α - 1) * (1 - a) ^ (β - 1) = 1
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
R : Type u_2
inst✝⁵ : NatCast R
inst✝⁴ : MeasurableSpace R
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : Countable R
inst✝ : MeasurableSingletonClass R
r : ℝ≥0
f : R → E
hf : Integrable f Po(R, r)
⊢ ∫ (x : R), f x ∂Po(R, r) = ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f ↑n

Tactic:
rw [integral_map .of_discrete .of_discrete]
  rw [integrable_map_cast_poissonMeasure_iff] at hf
  exact integral_poissonMeasure' hf

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
s : Finset α
h : ∑ a ∈ s, f a = 1
h' : ∀ a ∉ s, f a = 0
a : α
⊢ a ∈ (ofFinset f s h h').support ↔ a ∈ ↑s ∩ Function.support f

Tactic:
simpa [mem_support_iff] using mt (h' a)

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
H : ¬(f a' h) b = 0
⊢ (f a' h) b = 0

Tactic:
simpa [h] using h_1 a'

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

Goal state before:
pp: ι : Type u_1
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), Measurable (X i)
⊢ iIndepFun (fun i ω ↦ X i (ω i)) (infinitePi P)

Tactic:
by
  rw [iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop), infinitePi_map_pi _ mX]
  congrm infinitePi fun i ↦ ?_
  rw [← infinitePi_map_eval P i, map_map (mX i) (by fun_prop), Function.comp_def]

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
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
h : AEStronglyMeasurable (fun a ↦ ∫ (y : Ω), f (id a, y).2 ∂(condDistrib id id μ) (id a)) μ
⊢ AEStronglyMeasurable (fun ω ↦ ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ

Tactic:
rw [MeasurableSpace.comap_id] at h

Goal state after:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
h : AEStronglyMeasurable (fun a ↦ ∫ (y : Ω), f (id a, y).2 ∂(condDistrib id id μ) (id a)) μ
⊢ AEStronglyMeasurable (fun ω ↦ ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
⊢ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ } ≫
      (let f₁ := fun x ↦ (x, PUnit.unit);
        have hf₁ := ⋯;
        have hf₂ := ⋯;
        { hom := { hom := Kernel.id.map Prod.fst, property := ⋯ }, inv := { hom := Kernel.id.map f₁, property := ⋯ },
          hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom =
    (let f₁ := fun x ↦ (x, PUnit.unit);
        have hf₁ := ⋯;
        have hf₂ := ⋯;
        { hom := { hom := Kernel.id.map Prod.fst, property := ⋯ }, inv := { hom := Kernel.id.map f₁, property := ⋯ },
          hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom ≫
      κ

Tactic:
ext : 1; dsimp
    rw [Kernel.id_map (by fun_prop), Kernel.id_map (by fun_prop)]
    simp only [Kernel.deterministic_comp_eq_map, Kernel.comp_deterministic_eq_comap]
    ext _ _ hs
    have := κ.2
    rw [Kernel.map_apply' _ (by fun_prop) _ hs, Kernel.comap_apply' _ (by fun_prop),
      Kernel.parallelComp_apply' <| measurable_fst hs]
    simp only [Kernel.id_apply, MeasurableSpace.measurableSet_top, Measure.dirac_apply']
    rw [← lintegral_indicator_one hs]
    rfl

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

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ CondIndepFun m' hm' f g μ ↔
    Measure.map (fun ω ↦ (ω, f ω, g ω)) μ =
      ⇑(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) ∘ₘ μ.trim hm'

Tactic:
by
  rw [condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hf hg]
  congr!
  · rw [Measure.compProd_map (by fun_prop), compProd_trim_condExpKernel]
    exact Measure.map_map (by fun_prop) ((measurable_id.mono le_rfl hm').prodMk measurable_id)
  · rw [Measure.compProd_eq_comp_prod]

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

Goal state before:
pp: case neg
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hξ : f a ξ ≤ x
hx : ¬x = 1
g : ↑I → ℝ := fun y ↦ (κ a).real (Icc 0 y)
nebot : (𝓝[>] x).NeBot := nhdsGT_neBot_of_exists_gt (Exists.intro 1 (lt_of_le_of_ne x.property.right hx))
⊢ ↑ξ ≤ (κ a).real (Icc 0 x)

Tactic:
refine le_of_tendsto_of_tendsto (b := 𝓝[>] x) (g := g) continuousWithinAt_const ?_ ?_

Goal state after:
case neg.refine_1
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hξ : f a ξ ≤ x
hx : ¬x = 1
g : ↑I → ℝ := fun y ↦ (κ a).real (Icc 0 y)
nebot : (𝓝[>] x).NeBot := nhdsGT_neBot_of_exists_gt (Exists.intro 1 (lt_of_le_of_ne x.property.right hx))
⊢ Tendsto g (𝓝[>] x) (𝓝 ((κ a).real (Icc 0 x)))

case neg.refine_2
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hξ : f a ξ ≤ x
hx : ¬x = 1
g : ↑I → ℝ := fun y ↦ (κ a).real (Icc 0 y)
nebot : (𝓝[>] x).NeBot := nhdsGT_neBot_of_exists_gt (Exists.intro 1 (lt_of_le_of_ne x.property.right hx))
⊢ (fun x ↦ ↑ξ) ≤ᶠ[𝓝[>] x] g
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: case neg.refine_1
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hξ : f a ξ ≤ x
hx : ¬x = 1
g : ↑I → ℝ := fun y ↦ (κ a).real (Icc 0 y)
nebot : (𝓝[>] x).NeBot := nhdsGT_neBot_of_exists_gt (Exists.intro 1 (lt_of_le_of_ne x.property.right hx))
h : StieltjesFunction ℝ := cdf (Measure.map Subtype.val (κ a))
h_continuousWithinAt : ContinuousWithinAt (↑h) (Ioi ↑x) ↑x
⊢ Tendsto g (𝓝[>] x) (𝓝 ((κ a).real (Icc 0 x)))

Tactic:
g,

Goal state after:
case neg.refine_1
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hξ : f a ξ ≤ x
hx : ¬x = 1
g : ↑I → ℝ := fun y ↦ (κ a).real (Icc 0 y)
nebot : (𝓝[>] x).NeBot := nhdsGT_neBot_of_exists_gt (Exists.intro 1 (lt_of_le_of_ne x.property.right hx))
h : StieltjesFunction ℝ := cdf (Measure.map Subtype.val (κ a))
h_continuousWithinAt : ContinuousWithinAt (↑h) (Ioi ↑x) ↑x
⊢ Tendsto (fun y ↦ (κ a).real (Icc 0 y)) (𝓝[>] x) (𝓝 ((κ a).real (Icc 0 x)))
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: case refine_1
Ω : 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✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
h_int : Integrable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ)) μ
⊢ ∀ (t : Set Ω), MeasurableSet ({ω | τ ω ≤ σ ω} ∩ t) → MeasurableSet ({ω | τ ω ≤ σ ω} ∩ t)

Tactic:
intro t ht
      rw [Set.inter_comm _ t] at ht ⊢
      rw [hτ.measurableSet_inter_le_iff hσ, IsStoppingTime.measurableSet_min_iff hτ hσ] at ht
      exact ht.2

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

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ eLpNorm X (↑p) (μ.tilted fun x ↦ t * X x) < ∞

Tactic:
rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top]

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ (∫⁻ (a : Ω), ‖X a‖ₑ ^ (↑p).toReal ∂μ.tilted fun x ↦ t * X x) < ∞

case neg.hp_ne_zero
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ ↑p ≠ 0

case neg.hp_ne_top
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ ↑p ≠ ∞
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
σ : Subrepresentation (Representation.ofModule M)
c : A[G]
m : M
hm : m ∈ σ.toSubmodule.carrier
⊢ c • m ∈ σ.toSubmodule.carrier

Tactic:
induction c using MonoidAlgebra.induction_linear with
    | zero => rw [zero_smul]; exact σ.toSubmodule.zero_mem'
    | add x y hx hy => rw [add_smul]; exact σ.toSubmodule.add_mem' hx hy
    | single g a =>
      rw [← mul_one a, ← smul_eq_mul, ← MonoidAlgebra.smul_single, Algebra.smul_def, mul_smul]
      exact σ.toSubmodule.smul_mem' ((algebraMap A A) a) <| by
        simpa [Representation.ofModule, RestrictScalars.lsmul] using! σ.apply_mem_toSubmodule g hm

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
x : α
⊢ truncation f A x ≤ f x

Tactic:
calc
      truncation f A x ≤ |truncation f A x| := le_abs_self _
      _ ≤ |f x| := abs_truncation_le_abs_self _ _ _
      _ = f x := abs_of_nonneg (h'f x)

Goal state after: