mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ↑unitInterval
⊢ IsProbabilityMeasure (geometricMeasure p)

Tactic:
by
  rw [geometricMeasure]
  split_ifs with h
  · exact (hasSum_one_geometricMeasure h).isProbabilityMeasure_sum_dirac
      (geometricMeasure_nonneg p)
  · infer_instance

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

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0..x, r * rexp (-(r * a))
⊢ ContinuousOn (fun a ↦ -1 * rexp (-(r * a))) (Icc 0 x)

Tactic:
have : Continuous (fun a ↦ rexp (-(r * a))) := by
          simp only [← neg_mul]; exact (continuous_const_mul (-r)).rexp

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this✝ : ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0..x, r * rexp (-(r * a))
this : Continuous fun a ↦ rexp (-(r * a))
⊢ ContinuousOn (fun a ↦ -1 * rexp (-(r * a))) (Icc 0 x)
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ Po(r).real {n} = rexp (-↑r) * ↑r ^ n / ↑n !

Tactic:
by
  rw [measureReal_def, poissonMeasure_singleton, ENNReal.toReal_ofReal (by positivity)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : PMF α
g : β → γ
⊢ map g (map f p) = map (g ∘ f) p

Tactic:
by simp [map, Function.comp_def]

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
⊢ iIndepFun (s.restrict X) P

Tactic:
rw [iIndepFun_iff_map_fun_eq_pi_map]

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
⊢ map (fun ω i ↦ s.restrict X i ω) P = Measure.pi fun i ↦ map (s.restrict X i) P

ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
⊢ ∀ (i : ↥s), AEMeasurable (s.restrict X i) P
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: case inl
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : IsEmpty Ω
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map Function.diag μ

Tactic:
simp [Measure.eq_zero_of_isEmpty μ]

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

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B, (π a) A ∂μ = (⇑π ∘ₘ μ) (A ∩ B)

Tactic:
rw [Measure.bind_apply (by measurability) (π.measurable.mono h𝓑𝓧 le_rfl).aemeasurable]

Goal state after:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B, (π a) A ∂μ = ∫⁻ (a : X), (π a) (A ∩ B) ∂μ
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case hπ
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
m : ι → MeasurableSpace Ω
hm : ∀ (i : ι), m i ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ (i : ι), ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s

Tactic:
exact hm

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic (⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic (⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ =
    Kernel.deterministic ((Prod.map id Prod.swap ∘ ⇑MeasurableEquiv.prodAssoc) ∘ Prod.map Prod.swap id) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ =
    Kernel.deterministic ((Prod.map id Prod.swap ∘ ⇑MeasurableEquiv.prodAssoc) ∘ Prod.map Prod.swap id) ⋯

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ =
    Kernel.deterministic ((Prod.map id Prod.swap ∘ ⇑MeasurableEquiv.prodAssoc) ∘ Prod.map Prod.swap id) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic (⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.swap) ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic (⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.swap) ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ =
    Kernel.deterministic ((Prod.map Prod.swap id ∘ ⇑MeasurableEquiv.prodAssoc.symm) ∘ Prod.map id Prod.swap) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ =
    Kernel.deterministic ((Prod.map Prod.swap id ∘ ⇑MeasurableEquiv.prodAssoc.symm) ∘ Prod.map id Prod.swap) ⋯

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ =
    Kernel.deterministic ((Prod.map Prod.swap id ∘ ⇑MeasurableEquiv.prodAssoc.symm) ∘ Prod.map id Prod.swap) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ IsSFiniteKernel (Kernel.discard X.carrier)

Tactic:
by rw [Kernel.discard]; infer_instance

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id Function.diag) ⋯ ∘ₖ Kernel.deterministic (Prod.map Function.diag id) ⋯)

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic (⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id Function.diag) ⋯ ∘ₖ Kernel.deterministic (Prod.map Function.diag id) ⋯)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic (⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id Function.diag) ⋯ ∘ₖ Kernel.deterministic (Prod.map Function.diag id) ⋯)

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic
            ((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.map id ⇑MeasurableEquiv.prodAssoc) ∘
              Prod.map id (Prod.map Prod.swap id))
            ⋯ ∘ₖ
          Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id Function.diag) ⋯ ∘ₖ Kernel.deterministic (Prod.map Function.diag id) ⋯)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic
            ((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.map id ⇑MeasurableEquiv.prodAssoc) ∘
              Prod.map id (Prod.map Prod.swap id))
            ⋯ ∘ₖ
          Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id Function.diag) ⋯ ∘ₖ Kernel.deterministic (Prod.map Function.diag id) ⋯)

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic
          (((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.map id ⇑MeasurableEquiv.prodAssoc) ∘
              Prod.map id (Prod.map Prod.swap id)) ∘
            Prod.map id ⇑MeasurableEquiv.prodAssoc.symm)
          ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id Function.diag) ⋯ ∘ₖ Kernel.deterministic (Prod.map Function.diag id) ⋯)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic
          (((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.map id ⇑MeasurableEquiv.prodAssoc) ∘
              Prod.map id (Prod.map Prod.swap id)) ∘
            Prod.map id ⇑MeasurableEquiv.prodAssoc.symm)
          ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id Function.diag) ⋯ ∘ₖ Kernel.deterministic (Prod.map Function.diag id) ⋯)

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic
        ((((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.map id ⇑MeasurableEquiv.prodAssoc) ∘
              Prod.map id (Prod.map Prod.swap id)) ∘
            Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ∘
          ⇑MeasurableEquiv.prodAssoc)
        ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id Function.diag) ⋯ ∘ₖ Kernel.deterministic (Prod.map Function.diag id) ⋯)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic
        ((((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.map id ⇑MeasurableEquiv.prodAssoc) ∘
              Prod.map id (Prod.map Prod.swap id)) ∘
            Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ∘
          ⇑MeasurableEquiv.prodAssoc)
        ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id Function.diag) ⋯ ∘ₖ Kernel.deterministic (Prod.map Function.diag id) ⋯)

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic
        ((((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.map id ⇑MeasurableEquiv.prodAssoc) ∘
              Prod.map id (Prod.map Prod.swap id)) ∘
            Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ∘
          ⇑MeasurableEquiv.prodAssoc)
        ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Function.diag ∘ Prod.map Function.diag id) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic
        ((((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.map id ⇑MeasurableEquiv.prodAssoc) ∘
              Prod.map id (Prod.map Prod.swap id)) ∘
            Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ∘
          ⇑MeasurableEquiv.prodAssoc)
        ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Function.diag ∘ Prod.map Function.diag id) ⋯

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic
      (((((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.map id ⇑MeasurableEquiv.prodAssoc) ∘
              Prod.map id (Prod.map Prod.swap id)) ∘
            Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ∘
          ⇑MeasurableEquiv.prodAssoc) ∘
        Prod.map id Function.diag ∘ Prod.map Function.diag id)
      ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic
      (((((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.map id ⇑MeasurableEquiv.prodAssoc) ∘
              Prod.map id (Prod.map Prod.swap id)) ∘
            Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ∘
          ⇑MeasurableEquiv.prodAssoc) ∘
        Prod.map id Function.diag ∘ Prod.map Function.diag id)
      ⋯

Tactic:
Kernel.deterministic_comp_deterministic

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic
      (((((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.map id ⇑MeasurableEquiv.prodAssoc) ∘
              Prod.map id (Prod.map Prod.swap id)) ∘
            Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ∘
          ⇑MeasurableEquiv.prodAssoc) ∘
        Prod.map id Function.diag ∘ Prod.map Function.diag id)
      ⋯
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: case refine_2
Ω : 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) τ)) μ
⊢ Measurable (stoppedValue (fun n ↦ f n) τ)

Tactic:
exact measurable_stoppedValue h.stronglyAdapted.isStronglyProgressive_of_discrete hτ

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
⊢ (μ.tilted fun x ↦ t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)

Tactic:
tilted_apply_eq_ofReal_integral' _ hs,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
⊢ ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / ∫ (x : Ω), rexp (t * X x) ∂μ ∂μ) =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ ∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • X ω ∂μ = (∫ (x : Ω), X x * rexp (t * X x) ∂μ) / mgf X μ t

Tactic:
← integral_div,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ ∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • X ω ∂μ = ∫ (a : Ω), X a * rexp (t * X a) / mgf X μ t ∂μ
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
⊢ binomial p h 1 = map (fun x ↦ bif x then 1 else 0) (bernoulli p h)

Tactic:
by
  ext i; fin_cases i <;> simp [binomial_apply, bernoulli_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: case zero
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)
m : M
hm : m ∈ σ.toSubmodule.carrier
⊢ 0 ∈ σ.toSubmodule.carrier

Tactic:
exact σ.toSubmodule.zero_mem'

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: case single
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)
m : M
hm : m ∈ σ.toSubmodule.carrier
g : G
a : A
⊢ MonoidAlgebra.single g a • m ∈ σ.toSubmodule.carrier

Tactic:
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.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
X : Type w
g : G
⊢ (linearize k G (Action.trivial G X)) g = LinearMap.id

Tactic:
by
  ext (x : X) : 2
  rw [LinearMap.comp_apply, LinearMap.id_comp, MonoidAlgebra.lsingle_apply, linearize_single]
  simp only [Action.trivial_ρ]
  rfl

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

Goal state before:
pp: Ω : 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
⊢ mgf X μ t = mgf (-X) μ (-t)

Tactic:
by simp [mgf]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Res

Goal state before:
pp: case mp
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
k : Type u
inst✝ : CommRing k
φ : H →* G
S : ShortComplex (Rep k G)
h : (S.map (resFunctor φ)).ShortExact
h₁ : S.Exact
h₂ : Mono (S.map (resFunctor φ)).f
h₃ : Epi (S.map (resFunctor φ)).g
⊢ S.ShortExact

Tactic:
simp only [ShortComplex.map_f, mono_iff_injective, ShortComplex.map_g,
      epi_iff_surjective] at h₂ h₃

Goal state after:
case mp
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
k : Type u
inst✝ : CommRing k
φ : H →* G
S : ShortComplex (Rep k G)
h : (S.map (resFunctor φ)).ShortExact
h₁ : S.Exact
h₂ : Function.Injective ⇑(Hom.hom (resMap φ S.f))
h₃ : Function.Surjective ⇑(Hom.hom (resMap φ S.g))
⊢ S.ShortExact