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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ ∫ (x : α) in s, (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd ↑r).real s

Tactic:
rw [integral_toReal]
  · rw [setLIntegral_preCDF_fst _ _ hs, measureReal_def]
  · exact measurable_preCDF.aemeasurable
  · refine ae_restrict_of_ae ?_
    filter_upwards [preCDF_le_one ρ] with a ha
    exact (ha r).trans_lt ENNReal.one_lt_top

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
this :
  (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) - (1 + -((↑(√↑n)⁻¹ * ↑t) ^ 2 / 2))) =o[atTop] fun n ↦
    ((√↑n)⁻¹ * t) ^ 2
aux : (fun n ↦ ‖1 / ↑n‖) = fun n ↦ ‖1 / ↑n‖
⊢ (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) - (1 + -↑t ^ 2 / 2 / ↑n)) =o[atTop] fun x ↦ t ^ 2 * (1 / ↑x)

Tactic:
convert! this using 4 with n <;> norm_cast

Goal state after:
case e'_7
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
this :
  (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) - (1 + -((↑(√↑n)⁻¹ * ↑t) ^ 2 / 2))) =o[atTop] fun n ↦
    ((√↑n)⁻¹ * t) ^ 2
aux : (fun n ↦ ‖1 / ↑n‖) = fun n ↦ ‖1 / ↑n‖
n : ℕ
⊢ -t ^ 2 / 2 / ↑n = -(((√↑n)⁻¹ * t) ^ 2 / 2)

case e'_8
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
this :
  (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) - (1 + -((↑(√↑n)⁻¹ * ↑t) ^ 2 / 2))) =o[atTop] fun n ↦
    ((√↑n)⁻¹ * t) ^ 2
aux : (fun n ↦ ‖1 / ↑n‖) = fun n ↦ ‖1 / ↑n‖
x✝ : ℕ
⊢ t ^ 2 * (1 / ↑x✝) = ((√↑x✝)⁻¹ * t) ^ 2
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
B : ℝ≥0 → Ω → ℝ
hB : IsBrownianReal B P
x✝¹ : Ω
x✝ : Continuous fun x ↦ B x x✝¹
⊢ Continuous fun x ↦ (-B) x x✝¹

Tactic:
by simpa [← Pi.neg_def, continuous_neg_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq : ∀ (i : ℕ), ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' f' i) ∂ν a = (κ a) (f' i)
h_eq : ∀ (a : β), Prod.mk a ⁻¹' ⋃ i, f' i = ⋃ i, Prod.mk a ⁻¹' f' i
h_disj : ∀ (a : β), Pairwise (Disjoint on fun i ↦ Prod.mk a ⁻¹' f' i)
⊢ ∑' (i : ℕ), ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' f' i) ∂ν a = ∑' (i : ℕ), (κ a) (f' i)

Tactic:
hf_eq

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (X i)
a b c : ι
⊢ Measurable (IocProdIoc a b c)

Tactic:
by
  refine measurable_pi_lambda _ (fun i ↦ ?_)
  by_cases h : i ≤ b
  · simpa [IocProdIoc, h] using measurable_fst.eval
  · simpa [IocProdIoc, h] using measurable_snd.eval

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

Goal state before:
pp: case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u
⊢ (countablePartition γ n).Countable

Tactic:
exact (finite_countablePartition _ _).countable

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

Goal state before:
pp: case e_f
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
b : ℕ
S : Set ((i : ↥(Iic b)) → X ↑i)
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
x : (i : ↥(Iic b)) → X ↑i
⊢ x ∈ S ↔ (Iic b).restrict (updateFinset x₀ (Iic b) x) ∈ S

Tactic:
congrm (fun i ↦ ?_) ∈ S

Goal state after:
case e_f
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
b : ℕ
S : Set ((i : ↥(Iic b)) → X ↑i)
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
x : (i : ↥(Iic b)) → X ↑i
i : ↥(Iic b)
⊢ x i = (Iic b).restrict (updateFinset x₀ (Iic b) x) i
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)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)
⊢ ((((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)) a) s = (κ a) s

Tactic:
← withDensity_mul,

Goal state after:
α : 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)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)
⊢ (((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x) a) s = (κ a) s

case hf
α : 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)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)
⊢ Measurable (Function.uncurry fun a x ↦ (1 - κ.rnDerivAux (κ + η) a x).toNNReal)

case hg
α : 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)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)
⊢ Measurable (Function.uncurry (κ.rnDeriv η))
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab✝ : a ≤ b
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
hbc : b ≤ b
⊢ lmarginalPartialTraj κ a b (lmarginalPartialTraj κ b b f) x₀ = lmarginalPartialTraj κ a b f x₀

Tactic:
lmarginalPartialTraj_le κ le_rfl hf

Goal state after:
case inr.inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab✝ : a ≤ b
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
hbc : b ≤ b
⊢ lmarginalPartialTraj κ a b f x₀ = lmarginalPartialTraj κ a b f x₀
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 : ℕ
hab : a ≤ b
⊢ traj κ b ∘ₖ partialTraj κ a b = traj κ a

Tactic:
by
  refine eq_traj _ _ fun n ↦ ?_
  rw [map_comp, traj_map_frestrictLe, partialTraj_comp_partialTraj' _ hab]

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)
s : Finset ι
f : ((i : ↥s) → X ↑i) → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (y : (i : ι) → X i), f (s.restrict y) ∂infinitePi μ = ∫⁻ (y : (i : ↥s) → X ↑i), f y ∂Measure.pi fun i ↦ μ ↑i

Tactic:
← lintegral_map hf (measurable_restrict _),

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Finset ι
f : ((i : ↥s) → X ↑i) → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : (i : ↥s) → X ↑i), f a ∂Measure.map s.restrict (infinitePi μ) =
    ∫⁻ (y : (i : ↥s) → X ↑i), f y ∂Measure.pi fun i ↦ μ ↑i
Module: Mathlib.Probability.Distributions.Bernoulli

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
hx : x ∈ s
hy : y ∈ s
⊢ Ber(x, y, p) s = 1

Tactic:
simp_all [bernoulliMeasure_apply]

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
hx : x ∈ s
hy : y ∉ s
⊢ Ber(x, y, p) s = ↑(toNNReal p)

Tactic:
simp_all [bernoulliMeasure_apply]

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
hx : x ∉ s
hy : y ∈ s
⊢ Ber(x, y, p) s = ↑(toNNReal (σ p))

Tactic:
simp_all [bernoulliMeasure_apply]

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
hx : x ∉ s
hy : y ∉ s
⊢ Ber(x, y, p) s = 0

Tactic:
simp_all [bernoulliMeasure_apply]

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

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
x✝ : x ∈ Ioc 0 1
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ x ^ (α - 1) * (1 - x) ^ (β - 1) = RCLike.re (↑(x ^ (α - 1)) * ↑((1 - x) ^ (β - 1)))

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

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

Tactic:
RCLike.re_to_complex,

Goal state after:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
x✝ : x ∈ Ioc 0 1
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ x ^ (α - 1) * (1 - x) ^ (β - 1) = (↑(x ^ (α - 1)) * ↑((1 - x) ^ (β - 1))).re

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

case hx
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
x✝ : x ∈ Ioc 0 1
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ 0 ≤ x
Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm

Goal state before:
pp: p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
⊢ Tendsto (fun n ↦ ↑(n.choose k) * p n ^ k) atTop (𝓝 (r ^ k / ↑k.factorial))

Tactic:
by
  have : (fun n => n.choose k * (p n) ^ k) ~[atTop] (fun n ↦ ((n * p n) ^ k) / k.factorial) :=
    calc
    _ ~[atTop] (fun n => (n ^ k / k.factorial) * (p n) ^ k) :=
      (isEquivalent_choose k).mul IsEquivalent.refl
    _ ~[atTop] (fun n ↦ ((n * p n) ^ k) / k.factorial) :=
      EventuallyEq.isEquivalent (.of_eq (by ext; field))
  refine (IsEquivalent.tendsto_nhds_iff this).mpr ?_
  simpa [div_eq_mul_inv] using (hr.pow k).mul_const ((k.factorial : ℝ)⁻¹)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
f : α → β
a : α
⊢ (q f * if b = f a then p a else 0) = if b = f a then q f * p a else 0

Tactic:
simpa only [mul_zero] using mul_ite (b = f a) (q f) (p a) 0

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
⊢ ∀ᵐ (ω : Ω) ∂μ, 1 - X ω = 0 ∨ 1 - X ω = 1

Tactic:
by simpa [sub_eq_zero, or_comm, eq_comm (a := (1 : ℝ))] using hX

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

Goal state before:
pp: case neg
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : 1 = (κ a) t
h0 : ¬(κ a) t = 0
h_top : ¬(κ a) t = ∞
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ∞

Tactic:
exact Or.inr (Or.inl ha.symm)

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

Goal state before:
pp: case refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) ns

pp: case refine_3
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (n : ι), ∃ a, n ∈ ns a

Tactic:
· exact Monotone.directed_le fun i j hij k hki => le_trans hki hij

Goal state after:
case refine_3
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (n : ι), ∃ a, n ∈ ns a
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case e_f
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
a : Y₁✝.carrier
⊢ ∫⁻ (y : Y₂✝.carrier), (η.hom a✝.2) (Prod.mk (a, y) ⁻¹' ⇑prodAssoc ⁻¹' s✝) ∂κ₂.hom a✝.1.2 =
    ((κ₂.hom (prodAssoc a✝).2.1).prod (η.hom (prodAssoc a✝).2.2)) (Prod.mk a ⁻¹' s✝)

Tactic:
Measure.prod_apply (by measurability)

Goal state after:
case e_f
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
a : Y₁✝.carrier
⊢ ∫⁻ (y : Y₂✝.carrier), (η.hom a✝.2) (Prod.mk (a, y) ⁻¹' ⇑prodAssoc ⁻¹' s✝) ∂κ₂.hom a✝.1.2 =
    ∫⁻ (x : Y₂✝.carrier), (η.hom (prodAssoc a✝).2.2) (Prod.mk x ⁻¹' Prod.mk a ⁻¹' s✝) ∂κ₂.hom (prodAssoc a✝).2.1
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ}, MeasurableSet s → MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
            (Measure.map (fun ω ↦ (ω, f ω, g ω)) μ) ((k ⁻¹' s) ×ˢ t ×ˢ u)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ) (s ×ˢ t ×ˢ u) =
    ∫⁻ (a : Ω),
      ((Kernel.id ×ₖ
            ((condExpKernel μ (MeasurableSpace.comap k mγ)).map f ×ₖ
              (condExpKernel μ (MeasurableSpace.comap k mγ)).map g))
          a)
        ((k ⁻¹' s) ×ˢ t ×ˢ u) ∂μ.trim ⋯

Tactic:
Measure.bind_apply (hs.prod (ht.prod hu)) (by fun_prop),

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ}, MeasurableSet s → MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
            (Measure.map (fun ω ↦ (ω, f ω, g ω)) μ) ((k ⁻¹' s) ×ˢ t ×ˢ u)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ ∫⁻ (a : γ), ((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) a) (s ×ˢ t ×ˢ u) ∂Measure.map k μ =
    ∫⁻ (a : Ω),
      ((Kernel.id ×ₖ
            ((condExpKernel μ (MeasurableSpace.comap k mγ)).map f ×ₖ
              (condExpKernel μ (MeasurableSpace.comap k mγ)).map g))
          a)
        ((k ⁻¹' s) ×ˢ t ×ˢ u) ∂μ.trim ⋯
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : 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 : ℝ
⊢ log (mgf X (κ ω') t) ≤ log (rexp (↑c * t ^ 2 / 2))

Tactic:
by
    by_cases h0 : κ ω' = 0
    · simpa [h0] using by positivity
    gcongr
    · exact mgf_pos' h0 (h_int t)
    · exact h t

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∑ i ∈ range N, ∑ j ∈ range (min (i + 1) K), ∫ (x : ℝ) in ↑i..↑(i + 1), 1 ∂ρ ≤
    ∑ i ∈ range N, (↑i + 1) * ∫ (x : ℝ) in ↑i..↑(i + 1), 1 ∂ρ

Tactic:
gcongr with i
        simp only [Nat.cast_add, Nat.cast_one, sum_const, card_range, nsmul_eq_mul, Nat.cast_min]
        refine mul_le_mul_of_nonneg_right (min_le_left _ _) ?_
        apply intervalIntegral.integral_nonneg
        · simp only [le_add_iff_nonneg_right, zero_le_one]
        · simp only [zero_le_one, imp_true_iff]

Goal state after:
Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic

Goal state before:
pp: A : Type u_1
V : Type u_2
k : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : Ring A
inst✝⁸ : Algebra k A
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module A V
inst✝⁴ : IsScalarTower k A V
inst✝³ : IsSimpleModule A V
inst✝² : FiniteDimensional k V
inst✝¹ : IsAlgClosed k
inst✝ : IsMulCommutative A
⊢ Module.finrank k V = 1

Tactic:
have : Nontrivial V := IsSimpleModule.nontrivial A V
  obtain ⟨v, v_nz⟩ := exists_ne (0 : V)
  set U : Submodule A V := { Submodule.span k {v} with
    smul_mem' a w hw := by
      have ⟨t, ht⟩ := (IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed k).2
        (Module.toModuleEnd A V a)
      simpa only [← show _ = a • w from congr($ht w)] using! (k ∙ v).smul_mem t hw }
  obtain hU | hU := eq_bot_or_eq_top U
  · exact (v_nz <| hU.le <| Submodule.mem_span_singleton_self v).elim
  · rw [finrank_eq_one_iff_of_nonzero v v_nz]
    rwa [← top_le_iff] at hU ⊢

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (fun ω ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * t ^ 2 / 2
⊢ Var[X; μ.tilted fun x ↦ u * X x] ≤ ((b - a) / 2) ^ 2

Tactic:
convert! variance_le_sq_of_bounded ((tilted_absolutelyContinuous μ (u * X ·)) hb) _
    · exact isProbabilityMeasure_tilted (hi u)
    · exact hm.mono_ac (tilted_absolutelyContinuous μ (u * X ·))

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

Goal state before:
pp: case hb
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
ht : t < 0
⊢ ∀ᵐ (ω : Ω) ∂μ, (-X) ω ∈ Set.Icc (-b) (-a)

pp: case hc
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
ht : t < 0
⊢ ∫ (x : Ω), (-X) x ∂μ = 0

pp: case ht
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
ht : t < 0
⊢ 0 < -t

Tactic:
· filter_upwards [hb] with ω ⟨hl, hr⟩ using ⟨neg_le_neg_iff.2 hr, neg_le_neg_iff.2 hl⟩

Goal state after:
case hc
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
ht : t < 0
⊢ ∫ (x : Ω), (-X) x ∂μ = 0

case ht
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
ht : t < 0
⊢ 0 < -t