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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
this : ⇑(condDistrib (AEMeasurable.mk Y hY) (AEMeasurable.mk X hX) μ) =ᵐ[Measure.map (AEMeasurable.mk X hX) μ] ⇑κ
⊢ ⇑(condDistrib Y X μ) =ᵐ[Measure.map X μ] ⇑κ

Tactic:
rwa [Measure.map_congr hX.ae_eq_mk, condDistrib_congr hY.ae_eq_mk hX.ae_eq_mk]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
ν : Measure γ
inst✝ : IsFiniteMeasure ν
f : γ → α
hX : AEMeasurable X (Measure.map f ν)
hY : AEMeasurable Y (Measure.map f ν)
hf : AEMeasurable f ν
⊢ ⇑(condDistrib Y X (Measure.map f ν)) =ᵐ[Measure.map (X ∘ f) ν] ⇑(condDistrib (Y ∘ f) (X ∘ f) ν)

Tactic:
← AEMeasurable.map_map_of_aemeasurable hX hf

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
ν : Measure γ
inst✝ : IsFiniteMeasure ν
f : γ → α
hX : AEMeasurable X (Measure.map f ν)
hY : AEMeasurable Y (Measure.map f ν)
hf : AEMeasurable f ν
⊢ ⇑(condDistrib Y X (Measure.map f ν)) =ᵐ[Measure.map X (Measure.map f ν)] ⇑(condDistrib (Y ∘ f) (X ∘ f) ν)
Module: Mathlib.Probability.Kernel.Integral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : β → E
a : α
inst✝ : CompleteSpace E
g : α → β
hg : Measurable g
hf : StronglyMeasurable f
⊢ ∫ (x : β), f x ∂(deterministic g hg) a = f (g a)

Tactic:
by
  rw [deterministic_apply, integral_dirac' _ _ hf]

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

Goal state before:
pp: case succ
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
k : ℕ
hak : a ≤ k
hk :
  Nat.leRec Kernel.id (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1)))
      ⋯ =
    (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ partialTraj κ a k).map (_root_.IicProdIoc k (k + 1))
⊢ Nat.leRec Kernel.id (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1)))
      ⋯ =
    (Kernel.id ×ₖ (κ (k + 1)).map ⇑(piSingleton (k + 1)) ∘ₖ partialTraj κ a (k + 1)).map
      (_root_.IicProdIoc (k + 1) (k + 1 + 1))

Tactic:
Nat.leRec_succ,

Goal state after:
case succ
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
k : ℕ
hak : a ≤ k
hk :
  Nat.leRec Kernel.id (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1)))
      ⋯ =
    (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ partialTraj κ a k).map (_root_.IicProdIoc k (k + 1))
⊢ (Kernel.id ×ₖ (κ (k + 1)).map ⇑(piSingleton (k + 1)) ∘ₖ
          Nat.leRec Kernel.id
            (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1)))
            ?succ.h1).map
      (_root_.IicProdIoc (k + 1) (k + 1 + 1)) =
    (Kernel.id ×ₖ (κ (k + 1)).map ⇑(piSingleton (k + 1)) ∘ₖ partialTraj κ a (k + 1)).map
      (_root_.IicProdIoc (k + 1) (k + 1 + 1))

case succ.h1
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
k : ℕ
hak : a ≤ k
hk :
  Nat.leRec Kernel.id (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1)))
      ⋯ =
    (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ partialTraj κ a k).map (_root_.IicProdIoc k (k + 1))
⊢ a ≤ k + 1
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : (κ.fst a) (countablePartitionSet n x) = 0
⊢ ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ.fst a) (countablePartitionSet n x)).toReal = 0

Tactic:
simp only [h]

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : (κ.fst a) (countablePartitionSet n x) = 0
⊢ ((κ a) (countablePartitionSet n x ×ˢ univ) / 0).toReal = 0
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel (X × Y) Z
inst✝ : IsSFiniteKernel η
x : X
s : Set (X × Z)
ms : MeasurableSet s
⊢ ∫⁻ (b : Y), (η (x, b)) (Prod.mk x ⁻¹' s) ∂κ x = ((η ∘ₖ (Kernel.id ×ₖ κ)) x) (Prod.mk x ⁻¹' s)

Tactic:
comp_apply' _ _ _ (measurable_prodMk_left ms),

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel (X × Y) Z
inst✝ : IsSFiniteKernel η
x : X
s : Set (X × Z)
ms : MeasurableSet s
⊢ ∫⁻ (b : Y), (η (x, b)) (Prod.mk x ⁻¹' s) ∂κ x = ∫⁻ (b : X × Y), (η b) (Prod.mk x ⁻¹' s) ∂(Kernel.id ×ₖ κ) x
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: case neg
ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
i : ι
hi : i ∉ u
⊢ setBer(u, p) ({a | i ∈ a} ∩ {a | i ∉ u}) = 0

Tactic:
calc
    setBer(u, p) ({s | i ∈ s} ∩ {s | i ∉ u})
    _ = setBer(u, p) {s | i ∈ s} := by simp [hi]
    _ = infinitePi (fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False)
          (cylinder {i} {fun _ ↦ True}) := by
      rw [setBernoulli_apply']; congr!; ext; simp [funext_iff]
    _ = 0 := by simp [infinitePi_cylinder, hi]

Goal state after:
Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs

Goal state before:
pp: V : Type u_1
p : ↑I
inst✝ : Countable V
S : Set (Sym2 V)
⊢ S ⊆ Sym2.diagSetᶜ → S ∈ Set.range edgeSet

Tactic:
hS

Goal state after:
V : Type u_1
p : ↑I
inst✝ : Countable V
S : Set (Sym2 V)
hS : S ⊆ Sym2.diagSetᶜ
⊢ S ∈ Set.range edgeSet
Module: Mathlib.Probability.Decision.Risk.Defs

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst✝ : Nonempty 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
⊢ minimaxRisk ℓ 0 = 0

Tactic:
by simp [minimaxRisk, iInf_subtype']

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
⊢ (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a b).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)

Tactic:
have : IsEmpty (Ioc a b) := by simpa [hba] using Subtype.isEmpty_false

Goal state after:
case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
this : IsEmpty ↥(Ioc a b)
⊢ (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a b).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑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 κ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
⊢ (κ.withDensity f).rnDeriv κ a =ᵐ[κ a] f a

Tactic:
have h_ae := (κ.withDensity f).rnDeriv_eq_rnDeriv_measure (η := κ) (a := a)
  have hf' : ∀ a, Measurable (f a) := fun _ ↦ hf.of_uncurry_left
  filter_upwards [h_ae, (κ a).rnDeriv_withDensity (hf' a)] with x hx1 hx2
  rw [hx1, κ.withDensity_apply hf, hx2]

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
⊢ ∀ᵐ (a : α) ∂μ, κ a = (η.withDensity (κ.rnDeriv η)) a

Tactic:
filter_upwards [h_ac] with a ha using (Kernel.withDensity_rnDeriv_eq ha).symm

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∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
inst✝¹ : Fintype Θ
inst✝ : MeasurableSingletonClass Θ
⊢ avgRisk ℓ P κ π = ∑ θ, (∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ P) θ) * π {θ}

Tactic:
simp [avgRisk, lintegral_fintype]

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

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ ∫ (t : ℝ) in Ioc 0 1, t ^ (α - 1) * (1 - t) ^ (β - 1) =
    RCLike.re (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (↑α - 1) * (1 - ↑x) ^ (↑β - 1) ∂volume)

Tactic:
← integral_re

Goal state after:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ ∫ (t : ℝ) in Ioc 0 1, t ^ (α - 1) * (1 - t) ^ (β - 1) =
    ∫ (x : ℝ) in Ioc 0 1, RCLike.re (↑x ^ (↑α - 1) * (1 - ↑x) ^ (↑β - 1)) ∂volume

α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ Integrable (fun x ↦ ↑x ^ (↑α - 1) * (1 - ↑x) ^ (↑β - 1)) (volume.restrict (Ioc 0 1))
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝³ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝² : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) x₀ ⊗ₘ traj κ b)
hf' : Integrable (uncurry f) (Measure.map (fun x ↦ (frestrictLe b x, x)) ((traj κ a) x₀))
⊢ ∫ (x : (i : ↥(Iic b)) → X ↑i), ∫ (y : (n : ℕ) → X n), f x y ∂(traj κ b) x ∂(partialTraj κ a b) x₀ =
    ∫ (x : (n : ℕ) → X n), f (frestrictLe b x) x ∂(traj κ a) x₀

Tactic:
simp_rw [← uncurry_apply_pair f, ← Measure.integral_compProd hf,
    partialTraj_compProd_traj hab, integral_map (by fun_prop) hf'.1]

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

Goal state before:
pp: α : Type u_1
p : PMF α
a : α
⊢ p a = 0 ↔ a ∉ p.support

Tactic:
mem_support_iff,

Goal state after:
α : Type u_1
p : PMF α
a : α
⊢ p a = 0 ↔ ¬p a ≠ 0
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: case hf
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ 0 ≤ᵐ[volume.restrict (Ici 0)] fun x ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
EventuallyLE,

Goal state after:
case hf
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Ici 0), 0 x ≤ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: case hf
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)))
⊢ 0 ≤ᵐ[volume.restrict (Ici t)] fun x ↦ r * t ^ r * x ^ (-(r + 1))

Tactic:
EventuallyLE,

Goal state after:
case hf
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)))
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Ici t), 0 x ≤ r * t ^ r * x ^ (-(r + 1))
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: case false
p : ℝ≥0
h : p ≤ 1
⊢ false ∈ (bernoulli p h).support ↔ false ∈ {b | bif b then p ≠ 0 else p ≠ 1}

Tactic:
mem_support_iff,

Goal state after:
case false
p : ℝ≥0
h : p ≤ 1
⊢ (bernoulli p h) false ≠ 0 ↔ false ∈ {b | bif b then p ≠ 0 else p ≠ 1}
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
⊢ Measure.map X ℙ = μ[|toMeasurable μ s] ↔ Measure.map X ℙ = μ[|s]

Tactic:
ProbabilityTheory.cond_toMeasurable_eq

Goal state after:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
⊢ Measure.map X ℙ = μ[|s] ↔ Measure.map X ℙ = μ[|s]
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: case neg.refine_1
Ω : 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 μ
hμs : ¬μ s = 0
t : Set Ω
⊢ IntegrableOn (fun x ↦ ∫ (x : Ω), f x ∂μ[|s]) t (μ.restrict s)

Tactic:
integrableOn_const_iff

Goal state after:
case neg.refine_1
Ω : 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 μ
hμs : ¬μ s = 0
t : Set Ω
⊢ ‖∫ (x : Ω), f x ∂μ[|s]‖ₑ = 0 ∨ (μ.restrict s) t < ∞
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
⊢ Indep (⨆ a, ⨆ n ∈ ns a, s n) (limsup s f) κ μα

Tactic:
by
  rcases eq_or_ne μα 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μα] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_indep.ae_isProbabilityMeasure hμ
  replace h_indep := h_indep.congr η_eq
  apply Indep.congr (Filter.EventuallyEq.symm η_eq)
  apply indep_iSup_of_directed_le
  · exact fun a => indep_biSup_limsup h_le h_indep hf (hnsp a)
  · exact fun a => iSup₂_le fun n _ => h_le n
  · exact limsup_le_iSup.trans (iSup_le h_le)
  · intro a b
    obtain ⟨c, hc⟩ := hns a b
    refine ⟨c, ?_, ?_⟩ <;> refine iSup_mono fun n => iSup_mono' fun hn => ⟨?_, le_rfl⟩
    · exact hc.1 hn
    · exact hc.2 hn

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

Goal state before:
pp: case refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (t : Set ι), BddBelow t → tᶜ ∈ atBot

Tactic:
simp only [mem_atBot_sets, Set.mem_compl_iff, BddBelow, lowerBounds, Set.Nonempty]
    rintro t ⟨a, ha⟩
    obtain ⟨b, hb⟩ : ∃ b, b < a := exists_lt a
    refine ⟨b, fun c hc hct => ?_⟩
    suffices ∀ i ∈ t, c < i from lt_irrefl c (this c hct)
    exact fun i hi => hc.trans_lt (hb.trans_le (ha hi))

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

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

Tactic:
mul_smul_comm,

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

Goal state before:
pp: case e_6.mpr
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ξ : ↑ξ ≤ (κ a).real (Icc 0 x)
c : ↑I
hc : c ∈ {x | (κ a).real (Icc 0 x) < ↑ξ}
h : x < c
h_lt : ¬(κ a).real (Icc 0 x) ≤ (κ a).real (Icc 0 c)
⊢ False

Tactic:
refine h_lt ?_

Goal state after:
case e_6.mpr
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ξ : ↑ξ ≤ (κ a).real (Icc 0 x)
c : ↑I
hc : c ∈ {x | (κ a).real (Icc 0 x) < ↑ξ}
h : x < c
h_lt : ¬(κ a).real (Icc 0 x) ≤ (κ a).real (Icc 0 c)
⊢ (κ a).real (Icc 0 x) ≤ (κ a).real (Icc 0 c)
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 κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, AEStronglyMeasurable X (κ ω')

Tactic:
by
  have h_int := h.ae_integrable_exp_mul 1
  filter_upwards [h_int] with ω h_int
  simpa using (aemeasurable_of_aemeasurable_exp h_int.1.aemeasurable).aestronglyMeasurable

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

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ ∑ a, ↑(p ^ ↑a * (1 - p) ^ (↑(Fin.last n) - ↑a) * ↑(n.choose ↑a)) = 1

Tactic:
norm_cast
    convert! (add_pow p (1 - p) n).symm
    · 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]
    · rw [add_tsub_cancel_of_le (mod_cast h), one_pow]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case inl
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x

Tactic:
simp only [truncation, indicator, hx, Set.mem_Ioc, id, Function.comp_apply]
    by_cases h'x : f x ≤ A
    · have : -A < f x := by linarith [h x]
      simp only [this, true_and]
    · simp only [h'x, and_false]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case inl
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x

pp: case inr
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 = f x
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x

Tactic:
· simp only [truncation, indicator, hx, Set.mem_Ioc, id, Function.comp_apply]
    by_cases h'x : f x ≤ A
    · have : -A < f x := by linarith [h x]
      simp only [this, true_and]
    · simp only [h'x, and_false]

Goal state after:
case inr
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 = f x
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case h₁
Ω : 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 : ℝ
⊢ ∫ (x : Ω), rexp (t * ↑p * X x) ∂κ ω' ≤ rexp (↑cX * (t * ↑p) ^ 2 / 2)

pp: case h₁
Ω : 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 : ℝ
⊢ ∫ (x : Ω), rexp (t * ↑q * Y x) ∂κ ω' ≤ rexp (↑cY * (t * ↑q) ^ 2 / 2)

Tactic:
· exact hmX (t * p)

Goal state after:
case h₁
Ω : 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 : ℝ
⊢ ∫ (x : Ω), rexp (t * ↑q * Y x) ∂κ ω' ≤ rexp (↑cY * (t * ↑q) ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case refine_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ mgf id (Measure.map X μ) t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
rw [mgf_id_map hX]
    exact h.mgf_le t

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R : Type u
G : Type v
inst✝¹ : CommRing R
inst✝ : Monoid G
V : FDRep R G
⊢ ((forget₂ (FDRep R G) (Rep R G)).obj V).ρ = V.ρ

Tactic:
ext g v; rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
hcard : IsUnit ↑(Nat.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ (↑(Nat.card G))⁻¹ʳ • Finset.univ.card • v = v

Tactic:
Finset.card_univ,

Goal state after:
k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
hcard : IsUnit ↑(Nat.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ (↑(Nat.card G))⁻¹ʳ • Fintype.card G • v = v