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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
x : α
hxuniv : (κ x) univ = (ρ.condKernel x) univ
t : Set ℝ
ht : MeasurableSet t
heq : (κ x) t = (ρ.condKernel x) t
⊢ (κ x) tᶜ = (ρ.condKernel x) tᶜ

Tactic:
measure_compl ht <| measure_ne_top _ _,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
x : α
hxuniv : (κ x) univ = (ρ.condKernel x) univ
t : Set ℝ
ht : MeasurableSet t
heq : (κ x) t = (ρ.condKernel x) t
⊢ (κ x) univ - (κ x) t = (ρ.condKernel x) tᶜ
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω ↦ f (a, ω)) (ρ.condKernel a)

Tactic:
have hf_ae : AEStronglyMeasurable f ρ := hf_int.1

Goal state after:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
hf_ae : AEStronglyMeasurable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω ↦ f (a, ω)) (ρ.condKernel a)
Module: Mathlib.Probability.Kernel.Disintegration.Integral

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

Tactic:
have hf_ae : AEStronglyMeasurable f ρ := hf_int.1

Goal state after:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
hf_ae : AEStronglyMeasurable f ρ
⊢ Integrable (fun x ↦ ∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst
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 μ
a : α
haX : X a = AEMeasurable.mk X hX a
haY : Y a = AEMeasurable.mk Y hY a
⊢ (AEMeasurable.mk X hX a, AEMeasurable.mk Y hY a) = (X a, Y a)

Tactic:
rw [haX, haY]

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

Goal state before:
pp: V : Type u_1
inst✝ : Countable V
⊢ G(V, 0) = dirac ⊥

Tactic:
by simp [binomialRandom_eq_map]

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

Goal state before:
pp: V : Type u_1
inst✝ : Countable V
⊢ G(V, 1) = dirac ⊤

Tactic:
by simp [binomialRandom_eq_map]

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:
pp: case neg
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
hμm : ¬IsFiniteMeasure μ
⊢ Var[fun x ↦ c; μ | m] = 0

Tactic:
simp [condVar, condExp_of_not_integrable, integrable_const_iff_isFiniteMeasure hc,
      integrable_const_iff_isFiniteMeasure <| pow_ne_zero _ hc, hμm, Pi.pow_def]

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
ω : Ω
hω : μ[c • X | m] ω = (c • μ[X | m]) ω
⊢ ((c • X - μ[c • X | m]) ^ 2) ω = (c ^ 2 • (X - μ[X | m]) ^ 2) ω

Tactic:
simp [hω, ← mul_sub, mul_pow]

Goal state after:
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 η
h_le : κ ≤ κ + η
this :
  (((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) +
      (κ + η).withDensity fun a x ↦ ↑(κ.rnDerivAux (κ + η) a x).toNNReal) =
    κ + η
a : α
s : Set γ
a✝ : MeasurableSet s
h :
  (((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) a) s +
      (((κ + η).withDensity fun a x ↦ ↑(κ.rnDerivAux (κ + η) a x).toNNReal) a) s =
    (κ a) s + (η a) s
⊢ (((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) a) s = (η a) s

Tactic:
withDensity_rnDerivAux,

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
this :
  (((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) +
      (κ + η).withDensity fun a x ↦ ↑(κ.rnDerivAux (κ + η) a x).toNNReal) =
    κ + η
a : α
s : Set γ
a✝ : MeasurableSet s
h : (((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) a) s + (κ a) s = (κ a) s + (η a) s
⊢ (((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) a) s = (η 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 α γ
a : α
x : γ
⊢ x ∉ κ.mutuallySingularSetSlice η a ↔ κ.rnDerivAux (κ + η) a x < 1

Tactic:
simp [mutuallySingularSetSlice]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case a
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ ∀ (i : ι), MeasurableSet (if h : i ∈ s then t ⟨i, h⟩ else Set.univ)

pp: case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ MeasurableSet (Set.univ.pi t)

Tactic:
· rintro i
    split_ifs with hi
    · exact ht ⟨i, hi⟩
    · exact .univ

Goal state after:
case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ MeasurableSet (Set.univ.pi t)
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ deterministic f hf ∥ₖ deterministic f hf ∘ₖ copy α = copy β ∘ₖ deterministic f hf

Tactic:
simp_rw [parallelComp_comp_copy, deterministic_prod_deterministic, copy,
      deterministic_comp_deterministic, Function.comp_def, Function.diag_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ IsDeterministic (copy α)

Tactic:
by unfold copy; 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.swap Ω 𝓧) ∘ₘ μ ⊗ₘ κ

Tactic:
rw [compProd_posterior_eq_map_swap, Measure.swap_comp]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X i.fst i.snd)
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
⊢ (infinitePi fun i ↦ infinitePi fun j ↦ μ i j)
      (Sigma.uncurry ⁻¹' (↑((image Sigma.fst s).sigma fun a ↦ s.preimage (Sigma.mk a) ⋯)).pi fun x ↦ t x) =
    ∏ i ∈ (image Sigma.fst s).sigma fun a ↦ s.preimage (Sigma.mk a) ⋯, (μ i.fst i.snd) (t i)

Tactic:
Finset.coe_sigma,

Goal state after:
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X i.fst i.snd)
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
⊢ (infinitePi fun i ↦ infinitePi fun j ↦ μ i j)
      (Sigma.uncurry ⁻¹' ((↑(image Sigma.fst s)).sigma fun i ↦ ↑(s.preimage (Sigma.mk i) ⋯)).pi fun x ↦ t x) =
    ∏ i ∈ (image Sigma.fst s).sigma fun a ↦ s.preimage (Sigma.mk a) ⋯, (μ i.fst i.snd) (t i)
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: n k : ℕ
p : ↑I
⊢ Bin(n, p) {k} = ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k))

Tactic:
rw [← ENNReal.ofReal_toReal (a := Bin(n, p) _) (by simp), ← measureReal_def,
    binomial_real_singleton]

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

Goal state before:
pp: α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
ha : a ∉ s
⊢ s.indicator (⇑p) a * (∑' (a' : α), s.indicator (⇑p) a')⁻¹ = 0

Tactic:
Set.indicator_apply_eq_zero.mpr fun ha' => absurd ha' ha,

Goal state after:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
ha : a ∉ s
⊢ 0 * (∑' (a' : α), s.indicator (⇑p) a')⁻¹ = 0
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω ↦ (((condExpKernel μ m') ω) (f i)).toReal) =ᵐ[μ] μ[(f i).indicator fun ω ↦ 1 | m']
h_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = μ[(f i).indicator fun ω ↦ 1 | m'] ω
⊢ ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      (fun ω ↦ (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal) =ᵐ[μ] μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m']

Tactic:
refine fun s f H ↦ condExpKernel_ae_eq_condExp hm' ?_

Goal state after:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω ↦ (((condExpKernel μ m') ω) (f i)).toReal) =ᵐ[μ] μ[(f i).indicator fun ω ↦ 1 | m']
h_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = μ[(f i).indicator fun ω ↦ 1 | m'] ω
s : Finset ι
f : ι → Set Ω
H : ∀ i ∈ s, f i ∈ π i
⊢ MeasurableSet (⋂ i ∈ s, f i)
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✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (t : Set ι), BddAbove t → tᶜ ∈ atTop

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:
· simp only [mem_atTop_sets, Set.mem_compl_iff, BddAbove, upperBounds, Set.Nonempty]
    rintro t ⟨a, ha⟩
    obtain ⟨b, hb⟩ : ∃ b, a < b := exists_gt a
    refine ⟨b, fun c hc hct => ?_⟩
    suffices ∀ i ∈ t, i < c from lt_irrefl c (this c hct)
    exact fun i hi => (ha hi).trans_lt (hb.trans_le hc)

Goal state after:
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

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.Stoch

Goal state before:
pp: X Y : Stoch
κ✝ : X ⟶ Y
X✝ Y✝ Z✝ : Stoch
κ : X✝ ⟶ Y✝
η : Y✝ ⟶ Z✝
x✝ : Deterministic (κ ≫ η)
⊢ κ ≫ Δ ≫ (η ⊗ₘ 𝟙 Y✝) = Δ ≫ (κ ≫ η ⊗ₘ κ)

Tactic:
ext : 2
    dsimp
    simp only [id_parallelComp_id, id_comp, id_parallelComp_comp_parallelComp_id]
    have : IsDeterministic (κ ≫ η).hom.hom := inferInstance
    exact (comp_parallelComp_comp_copy).symm

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

Goal state before:
pp: X : SFinKer
⊢ { hom := Kernel.copy X.carrier, property := ⋯ } ≫ { hom := Kernel.discard X.carrier, property := ⋯ } ▷ X = (λ_ X).inv

Tactic:
ext : 1; dsimp
    simp only [Kernel.discard, Kernel.copy, Kernel.id]
    rw [Kernel.deterministic_parallelComp_deterministic,
      Kernel.deterministic_comp_deterministic, Kernel.deterministic_map measurable_id (by fun_prop)]
    rfl

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

Goal state before:
pp: X : SFinKer
⊢ { hom := Kernel.copy X.carrier, property := ⋯ } ≫ X ◁ { hom := Kernel.discard X.carrier, property := ⋯ } = (ρ_ X).inv

Tactic:
ext : 1; dsimp
    simp only [Kernel.discard, Kernel.copy, Kernel.id]
    rw [Kernel.deterministic_parallelComp_deterministic,
      Kernel.deterministic_comp_deterministic, Kernel.deterministic_map measurable_id (by fun_prop)]
    rfl

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 ρ
⊢ ∑ x ∈ (range K).sigma fun a ↦ Ico a N, ∫ (x : ℝ) in ↑x.snd..↑(x.snd + 1), 1 ∂ρ =
    ∑ x ∈ (range N).sigma fun a ↦ range (min (a + 1) K), ∫ (x : ℝ) in ↑x.fst..↑(x.fst + 1), 1 ∂ρ

Tactic:
refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_

Goal state after:
case refine_1
Ω : 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 ρ
⊢ ∀ a ∈ (range K).sigma fun a ↦ Ico a N, ⟨a.snd, a.fst⟩ ∈ (range N).sigma fun a ↦ range (min (a + 1) K)

case refine_2
Ω : 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 ρ
⊢ ∀ a ∈ (range N).sigma fun a ↦ range (min (a + 1) K), ⟨a.snd, a.fst⟩ ∈ (range K).sigma fun a ↦ Ico a N

case refine_3
Ω : 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 ρ
⊢ ∀ a ∈ (range K).sigma fun a ↦ Ico a N, ⟨⟨a.snd, a.fst⟩.snd, ⟨a.snd, a.fst⟩.fst⟩ = a

case refine_4
Ω : 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 ρ
⊢ ∀ a ∈ (range N).sigma fun a ↦ range (min (a + 1) K), ⟨⟨a.snd, a.fst⟩.snd, ⟨a.snd, a.fst⟩.fst⟩ = a

case refine_5
Ω : 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 ρ
⊢ ∀ a ∈ (range K).sigma fun a ↦ Ico a N,
    ∫ (x : ℝ) in ↑a.snd..↑(a.snd + 1), 1 ∂ρ = ∫ (x : ℝ) in ↑⟨a.snd, a.fst⟩.fst..↑(⟨a.snd, a.fst⟩.fst + 1), 1 ∂ρ
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
X Y : Action (Type w) G
f : X ⟶ Y
x : X.V
r : k
⊢ (linearizeMap f) (MonoidAlgebra.single x r) = MonoidAlgebra.single ((ConcreteCategory.hom f.hom) x) r

Tactic:
simp [linearizeMap]

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 : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∑ x ∈ (range K).sigma range, (↑x.fst ^ 2)⁻¹ * ∫ (x : ℝ) in ↑x.snd..↑(x.snd + 1), x ^ 2 ∂ρ =
    ∑ x ∈ (range K).sigma fun a ↦ Ioo a K, (↑x.snd ^ 2)⁻¹ * ∫ (x : ℝ) in ↑x.fst..↑(x.fst + 1), x ^ 2 ∂ρ

Tactic:
refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_

Goal state after:
case refine_1
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∀ a ∈ (range K).sigma range, ⟨a.snd, a.fst⟩ ∈ (range K).sigma fun a ↦ Ioo a K

case refine_2
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∀ a ∈ (range K).sigma fun a ↦ Ioo a K, ⟨a.snd, a.fst⟩ ∈ (range K).sigma range

case refine_3
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∀ a ∈ (range K).sigma range, ⟨⟨a.snd, a.fst⟩.snd, ⟨a.snd, a.fst⟩.fst⟩ = a

case refine_4
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∀ a ∈ (range K).sigma fun a ↦ Ioo a K, ⟨⟨a.snd, a.fst⟩.snd, ⟨a.snd, a.fst⟩.fst⟩ = a

case refine_5
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∀ a ∈ (range K).sigma range,
    (↑a.fst ^ 2)⁻¹ * ∫ (x : ℝ) in ↑a.snd..↑(a.snd + 1), x ^ 2 ∂ρ =
      (↑⟨a.snd, a.fst⟩.snd ^ 2)⁻¹ * ∫ (x : ℝ) in ↑⟨a.snd, a.fst⟩.fst..↑(⟨a.snd, a.fst⟩.fst + 1), x ^ 2 ∂ρ
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: k : Type u
inst✝⁸ : Semiring k
G : Type v
inst✝⁷ : Monoid G
V : Type v'
inst✝⁶ : AddCommMonoid V
inst✝⁵ : Module k V
W : Type w'
inst✝⁴ : AddCommMonoid W
inst✝³ : Module k W
H : Type w
inst✝² : Subsingleton H
inst✝¹ : MulOneClass H
inst✝ : MulAction G H
g : G
⊢ ↑(MonoidAlgebra.uniqueLinearEquiv k H) ∘ₗ (ofMulAction k G H) g =
    (trivial k G k) g ∘ₗ ↑(MonoidAlgebra.uniqueLinearEquiv k H)

Tactic:
by ext a; simp [Subsingleton.elim (g • a) a]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
⊢ HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ

Tactic:
have : HasSubgaussianMGF (fun ω ↦ ∑ (i : s), X i ω) (∑ (i : s), c i) μ := by
    apply sum_of_iIndepFun_of_forall_aemeasurable
    · exact h_indep.precomp Subtype.val_injective
    · exact fun i ↦ (h_subG i i.2).aemeasurable
    · exact fun i _ ↦ h_subG i i.2

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
this : HasSubgaussianMGF (fun ω ↦ ∑ i, X (↑i) ω) (∑ i, c ↑i) μ
⊢ HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := ⋯
S : ℕ → Ω → ℝ := ⋯
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := ⋯
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := ⋯
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N i : ℕ
a✝ : i ∈ range N
⊢ ↑1 ≤ c ^ i

Tactic:
rw [Nat.cast_one]

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N i : ℕ
a✝ : i ∈ range N
⊢ 1 ≤ c ^ i