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

Goal state before:
pp: case inl.refine_2
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ ((partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a (n + 1)).map (restrict₂ ⋯)) x₀ =
    Measure.pi fun i ↦ μ ↑i

Tactic:
partialTraj_succ_of_le (by lia),

Goal state after:
case inl.refine_2
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ (((Kernel.id ×ₖ (const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))).map ⇑(piSingleton n) ∘ₖ
                partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map
            (_root_.IicProdIoc n (n + 1))).map
        (restrict₂ ⋯))
      x₀ =
    Measure.pi fun i ↦ μ ↑i
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ✝ η : Kernel α γ
hα : Countable α
a a' : α
c : γ
ha'_mem_a : a' ∈ measurableAtom a
κ : Kernel α γ
⊢ κ a' = κ a

Tactic:
ext s hs
      exact mem_of_mem_measurableAtom ha'_mem_a
        (Kernel.measurable_coe κ hs (measurableSet_singleton (κ a s))) rfl

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

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

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 η)
⊢ ∫⁻ (b : γ) in s, ↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal * κ.rnDeriv η a b ∂(κ + η) a = (κ a) s

Tactic:
· exact measurable_rnDeriv _ _

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 η)
⊢ ∫⁻ (b : γ) in s, ↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal * κ.rnDeriv η a b ∂(κ + η) a = (κ a) s
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((η.withDensity (κ.rnDeriv η) + κ.singularPart η) a) s = (κ a) s

Tactic:
← inter_union_sdiff s (mutuallySingularSetSlice κ η a)

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((η.withDensity (κ.rnDeriv η) + κ.singularPart η) a)
      (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a) =
    (κ a) (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a)
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
x : γ
heq : κ.rnDeriv η a x = (∂κ a/∂η a) x
⊢ (∂κ a/∂η a) x ≠ ∞ → κ.rnDeriv η a x < ∞

Tactic:
htop

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
x : γ
heq : κ.rnDeriv η a x = (∂κ a/∂η a) x
htop : (∂κ a/∂η a) x ≠ ∞
⊢ κ.rnDeriv η a x < ∞
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 : α
h : κ a ≪ η a
x : γ
h0 : 0 < κ.rnDeriv η a x
⊢ κ.rnDeriv η a x ≠ ∞ → 0 < (κ.rnDeriv η a x).toReal

Tactic:
htop

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : κ a ≪ η a
x : γ
h0 : 0 < κ.rnDeriv η a x
htop : κ.rnDeriv η a x ≠ ∞
⊢ 0 < (κ.rnDeriv η a x).toReal
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)
I : Finset ι
s : Set ((i : ↥I) → X ↑i)
hs : MeasurableSet s
⊢ (map I.restrict (infinitePi μ)) s = ((fun I ↦ Measure.pi fun i ↦ μ ↑i) I) s

Tactic:
map_apply (measurable_restrict I) hs,

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I : Finset ι
s : Set ((i : ↥I) → X ↑i)
hs : MeasurableSet s
⊢ (infinitePi μ) (I.restrict ⁻¹' s) = ((fun I ↦ Measure.pi fun i ↦ μ ↑i) I) s
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.refine_1
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : DependsOn f ↑(Iic b)
mf : Measurable f
x y : (i : ℕ) → X i
hxy : ∀ i ∈ ↑(Iic a), x i = y i
hab : a ≤ b
i : ↥(Iic a)
⊢ frestrictLe a x i = frestrictLe a y i

Tactic:
exact hxy i.1 i.2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ IsDeterministic Kernel.id

Tactic:
by unfold Kernel.id; infer_instance

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

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteKernel κ
inst✝¹ : StandardBorelSpace Ω
inst✝ : Nonempty Ω
⊢ ⇑(κ ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω)) ∘ₘ μ = ⇑(κ ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ

Tactic:
Kernel.swap_copy,

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteKernel κ
inst✝¹ : StandardBorelSpace Ω
inst✝ : Nonempty Ω
⊢ ⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω) ∘ₘ μ = ⇑(κ ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
s' : Finset ↑s
| (map s.domRestrict (infinitePi μ)) ((↑s').pi fun i ↦ t ↑i)

Tactic:
map_apply
        (by fun_prop) (by apply MeasurableSet.pi (countable_toSet _) (by measurability)),

Goal state after:
ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
s' : Finset ↑s
| (infinitePi μ) (s.domRestrict ⁻¹' (↑s').pi fun i ↦ t ↑i)
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 Θ 𝓧
π : Measure Θ
inst✝¹ : Countable Θ
inst✝ : MeasurableSingletonClass Θ
⊢ bayesRisk ℓ P π = ⨅ κ, ⨅ (_ : IsMarkovKernel κ), ∑' (θ : Θ), (∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ P) θ) * π {θ}

Tactic:
by
  simp [bayesRisk, avgRisk_countable]

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

Goal state before:
pp: y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
⊢ ∀ ⦃a : ℝ⦄, a ∈ Iio z → ∀ ⦃b : ℝ⦄, b ∈ Icc z y → a ≠ b

Tactic:
mem_Iio,

Goal state after:
y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
⊢ ∀ ⦃a : ℝ⦄, a < z → ∀ ⦃b : ℝ⦄, b ∈ Icc z y → a ≠ b
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
inst✝ : CompleteSpace E
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_cf : Integrable ((traj κ a) x₀)[f | ↑piLE c] ((traj κ a) x₀)
mcf : StronglyMeasurable ((traj κ a) x₀)[f | ↑piLE c]
x : (n : ℕ) → X n
h1 : ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x = ((traj κ a) x₀)[f | ↑piLE b] x
h2 :
  ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x =
    ∫ (y : (n : ℕ) → X n), ((traj κ a) x₀)[f | ↑piLE c] y ∂(traj κ b) (frestrictLe b x)
⊢ ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x =
    ∫ (y : (i : ↥(Iic c)) → X ↑i),
      ((traj κ a) x₀)[f | ↑piLE c] (updateFinset x (Iic c) y) ∂(partialTraj κ b c) (frestrictLe b x)

Tactic:
h2,

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)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_cf : Integrable ((traj κ a) x₀)[f | ↑piLE c] ((traj κ a) x₀)
mcf : StronglyMeasurable ((traj κ a) x₀)[f | ↑piLE c]
x : (n : ℕ) → X n
h1 : ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x = ((traj κ a) x₀)[f | ↑piLE b] x
h2 :
  ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x =
    ∫ (y : (n : ℕ) → X n), ((traj κ a) x₀)[f | ↑piLE c] y ∂(traj κ b) (frestrictLe b x)
⊢ ∫ (y : (n : ℕ) → X n), ((traj κ a) x₀)[f | ↑piLE c] y ∂(traj κ b) (frestrictLe b x) =
    ∫ (y : (i : ↥(Iic c)) → X ↑i),
      ((traj κ a) x₀)[f | ↑piLE c] (updateFinset x (Iic c) y) ∂(partialTraj κ b c) (frestrictLe b x)
Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm

Goal state before:
pp: p : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
⊢ Tendsto p atTop (𝓝 0)

Tactic:
by
  have : (fun n => (n * p n) * (1 / n)) =ᶠ[atTop] p := by
    filter_upwards [eventually_ge_atTop 1] with n hn
    field
  simpa using (hr.mul tendsto_one_div_atTop_nhds_zero_nat).congr' this

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

Goal state before:
pp: case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ∞
this : IsProbabilityMeasure ℙ
⊢ ∫⁻ (x : ℝ), ‖x‖ₑ * s.indicator ((volume s)⁻¹ • 1) x ≠ ∞

Tactic:
set ind := (volume s)⁻¹ • (1 : ℝ → ℝ≥0∞)

Goal state after:
case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ∞
this : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1
⊢ ∫⁻ (x : ℝ), ‖x‖ₑ * s.indicator ind x ≠ ∞
Module: Mathlib.Probability.IdentDistribIndep

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝ : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun X μ
hY_ind : iIndepFun Y ν
this : IsProbabilityMeasure μ
⊢ Measure.map (fun ω x ↦ X x ω) μ = Measure.map (fun ω x ↦ Y x ω) ν

Tactic:
have : IsProbabilityMeasure ν := hY_ind.isProbabilityMeasure

Goal state after:
Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝ : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun X μ
hY_ind : iIndepFun Y ν
this✝ : IsProbabilityMeasure μ
this : IsProbabilityMeasure ν
⊢ Measure.map (fun ω x ↦ X x ω) μ = Measure.map (fun ω x ↦ Y x ω) ν
Module: Mathlib.Probability.Independence.ZeroOne

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

Tactic:
h_0_1_top

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
h : ∀ᵐ (a : α) ∂μα, IsFiniteMeasure (κ a)
t : Set Ω
h_indep : IndepSet t t κ μα
a : α
h_0_1_top : (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ∞
⊢ IsFiniteMeasure (κ a) → (κ a) t = 0 ∨ (κ a) t = 1
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X Y : Stoch
κ : X ⟶ Y
inst✝ : Deterministic κ
this : κ.hom ≫ Δ = Δ ≫ (κ.hom ⊗ₘ κ.hom)
⊢ κ.hom.hom ∥ₖ κ.hom.hom ∘ₖ copy X.obj.carrier = copy Y.obj.carrier ∘ₖ κ.hom.hom

Tactic:
SFinKer.Hom.ext_iff

Goal state after:
X Y : Stoch
κ : X ⟶ Y
inst✝ : Deterministic κ
this : (κ.hom ≫ Δ).hom = (Δ ≫ (κ.hom ⊗ₘ κ.hom)).hom
⊢ κ.hom.hom ∥ₖ κ.hom.hom ∘ₖ copy X.obj.carrier = copy Y.obj.carrier ∘ₖ κ.hom.hom
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∞) ⦃s : Set X⦄,
    MeasurableSet s →
      ∫⁻ (x : X), B.indicator 1 x * s.indicator (fun x ↦ c) x ∂π x₀ =
        B.indicator 1 x₀ * ∫⁻ (x : X), s.indicator (fun x ↦ c) x ∂π x₀

Tactic:
rintro c A hA
    simp_rw [← smul_indicator_one_apply, mul_smul_comm, smul_eq_mul]
    rw [lintegral_const_mul, lintegral_const_mul, hπ.lintegral_indicator_mul_indicator h𝓑𝓧 hA hB,
      mul_left_comm] <;> measurability

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

Goal state before:
pp: Y : Type u_2
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
μ : Measure Y
inst✝ : IsProbabilityMeasure μ
f : Unit → ↑I → Y
hf_meas : Measurable (uncurry f)
hf_map : map (f ()) volume = (Kernel.const Unit μ) ()
⊢ ∃ f, Measurable f ∧ map f volume = μ

Tactic:
exact ⟨f (), by fun_prop, by simpa⟩

Goal state after:
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
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
h1_symm : Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (⇑e.symm) (Measure.map (fun x ↦ ((k x, g x), f x)) μ)
h2 :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
⊢ ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ =
    Measure.map (⇑e.symm) (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ)

Tactic:
h2,

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
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
h1_symm : Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (⇑e.symm) (Measure.map (fun x ↦ ((k x, g x), f x)) μ)
h2 :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
⊢ ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ =
    Measure.map (⇑e.symm)
      (Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ))
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_int✝¹ : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
h_mgf✝ : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℚ), mgf X (κ a) ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
h_int✝ : ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
ω' : Ω'
h_mgf : ∀ (i : ℚ), mgf X (κ ω') ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
⊢ mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
refine Rat.denseRange_cast.induction_on t ?_ h_mgf

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int✝¹ : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
h_mgf✝ : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℚ), mgf X (κ a) ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
h_int✝ : ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
ω' : Ω'
h_mgf : ∀ (i : ℚ), mgf X (κ ω') ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
⊢ IsClosed {b | mgf X (κ ω') b ≤ rexp (↑c * b ^ 2 / 2)}
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
⊢ (∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)) →
    Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω') →
      mgf (fun p ↦ X p.1 + Y p.2) ((κ ⊗ₖ η) ω') ↑q ≤ rexp (↑(c + cY) * ↑q ^ 2 / 2)

Tactic:
hY_mgf

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
hY_mgf : ∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)
⊢ Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω') →
    mgf (fun p ↦ X p.1 + Y p.2) ((κ ⊗ₖ η) ω') ↑q ≤ rexp (↑(c + cY) * ↑q ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
hY_mgf : ∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)
h_int_mul : Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω')
ω : Ω
⊢ mgf Y (η (ω', ω)) ↑q ≤ rexp (↑cY * ↑q ^ 2 / 2) →
    rexp (↑q * X ω) * ∫ (y : Ω''), rexp (↑q * Y y) ∂η (ω', ω) ≤ rexp (↑q * X ω) * rexp (↑cY * ↑q ^ 2 / 2)

Tactic:
hY_mgf

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
hY_mgf✝ : ∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)
h_int_mul : Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω')
ω : Ω
hY_mgf : mgf Y (η (ω', ω)) ↑q ≤ rexp (↑cY * ↑q ^ 2 / 2)
⊢ rexp (↑q * X ω) * ∫ (y : Ω''), rexp (↑q * Y y) ∂η (ω', ω) ≤ rexp (↑q * X ω) * rexp (↑cY * ↑q ^ 2 / 2)
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
⊢ ↑V ≃+ RestrictScalars k k[G] V.ρ.asModule

Tactic:
exact V.ρ.asModuleEquiv.symm.toAddEquiv.trans (RestrictScalars.addEquiv _ _ _).symm

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap = 0

Tactic:
ext; simp [sub_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap = 0

Tactic:
ext; simp [sub_hom]

Goal state after: