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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
⊢ (κ.withDensity fun a x ↦ ↑(f a x) * g a x) = (κ.withDensity fun a x ↦ ↑(f a x)).withDensity g

Tactic:
by
  ext a : 1
  rw [Kernel.withDensity_apply]
  swap; · fun_prop
  change (Measure.withDensity (κ a) ((fun x ↦ (f a x : ℝ≥0∞)) * (fun x ↦ (g a x : ℝ≥0∞)))) =
      (withDensity (withDensity κ fun a x ↦ f a x) g) a
  rw [withDensity_mul]
  · rw [Kernel.withDensity_apply _ hg, Kernel.withDensity_apply]
    exact measurable_coe_nnreal_ennreal.comp hf
  · fun_prop
  · fun_prop

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 η
a : α
h_eq_add : ∀ (a : α) (s : Set γ), MeasurableSet s → ((η.withDensity (κ.rnDeriv η) + κ.singularPart η) a) s = (κ a) s
⊢ (η.withDensity (κ.rnDeriv η)) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 0

Tactic:
specialize h_eq_add a (mutuallySingularSetSlice κ η a)ᶜ
    (measurableSet_mutuallySingularSetSlice κ η a).compl

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h_eq_add :
  ((η.withDensity (κ.rnDeriv η) + κ.singularPart η) a) (κ.mutuallySingularSetSlice η a)ᶜ =
    (κ a) (κ.mutuallySingularSetSlice η a)ᶜ
⊢ (η.withDensity (κ.rnDeriv η)) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
this : ∀ᵐ (a : α) ∂μ, (κ.singularPart η) a = 0
a : α
ha : (κ.singularPart η) a = 0
⊢ κ a ≪ η a

Tactic:
Kernel.singularPart_eq_zero_iff_absolutelyContinuous

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
this : ∀ᵐ (a : α) ∂μ, (κ.singularPart η) a = 0
a : α
ha : κ a ≪ η a
⊢ κ a ≪ η a
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: 𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
Ω : Type u_5
inst✝⁵ : Countable Ω
inst✝⁴ : MeasurableSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace Ω
κ : Kernel Ω 𝓧
inst✝¹ : IsFiniteKernel κ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_rnDeriv : ∀ (ω : Ω), ∀ᵐ (x : 𝓧) ∂⇑κ ∘ₘ μ, κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x = (∂κ ω/∂⇑κ ∘ₘ μ) x
⊢ ∀ᵐ (x : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) x = μ.withDensity fun ω ↦ (∂κ ω/∂⇑κ ∘ₘ μ) x

Tactic:
rw [← ae_all_iff] at h_rnDeriv

Goal state after:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
Ω : Type u_5
inst✝⁵ : Countable Ω
inst✝⁴ : MeasurableSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace Ω
κ : Kernel Ω 𝓧
inst✝¹ : IsFiniteKernel κ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_rnDeriv : ∀ᵐ (a : 𝓧) ∂⇑κ ∘ₘ μ, ∀ (i : Ω), κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) i a = (∂κ i/∂⇑κ ∘ₘ μ) a
⊢ ∀ᵐ (x : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) x = μ.withDensity fun ω ↦ (∂κ ω/∂⇑κ ∘ₘ μ) x
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, ENNReal.ofReal (if 0 ≤ y then r * rexp (-(r * y)) else 0) = ENNReal.ofReal 0

Tactic:
rw [setLIntegral_congr_fun measurableSet_Iic, lintegral_zero, ENNReal.ofReal_zero]

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ EqOn (fun y ↦ ENNReal.ofReal (if 0 ≤ y then r * rexp (-(r * y)) else 0)) (fun x ↦ 0) (Iic x)
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ (ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)).toReal = rexp (-↑r) * ↑r ^ n / ↑n !

Tactic:
ENNReal.toReal_ofReal (by positivity)

Goal state after:
r : ℝ≥0
n : ℕ
⊢ rexp (-↑r) * ↑r ^ n / ↑n ! = rexp (-↑r) * ↑r ^ n / ↑n !
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ≥0
f : ℕ → E
n : ℕ
⊢ (ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)).toReal = rexp (-↑r) * ↑r ^ n / ↑n !

Tactic:
ENNReal.toReal_ofReal (by positivity)

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ≥0
f : ℕ → E
n : ℕ
⊢ rexp (-↑r) * ↑r ^ n / ↑n ! = rexp (-↑r) * ↑r ^ n / ↑n !
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
x✝ : ℕ
⊢ (rexp (-↑r) * ↑r ^ x✝ / ↑x✝!) • f x✝ = (ENNReal.ofReal (rexp (-↑r) * ↑r ^ x✝ / ↑x✝!)).toReal • f x✝

Tactic:
ENNReal.toReal_ofReal (by positivity)

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
x✝ : ℕ
⊢ (rexp (-↑r) * ↑r ^ x✝ / ↑x✝!) • f x✝ = (rexp (-↑r) * ↑r ^ x✝ / ↑x✝!) • f x✝
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
this : (fun n ↦ (rexp (-↑r) * ↑r ^ n / ↑n !) • f n) = fun n ↦ (ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)).toReal • f n
x✝ : ℕ
⊢ (ENNReal.ofReal (rexp (-↑r) * ↑r ^ x✝ / ↑x✝!)).toReal = rexp (-↑r) * ↑r ^ x✝ / ↑x✝!

Tactic:
ENNReal.toReal_ofReal (by positivity)

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
this : (fun n ↦ (rexp (-↑r) * ↑r ^ n / ↑n !) • f n) = fun n ↦ (ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)).toReal • f n
x✝ : ℕ
⊢ rexp (-↑r) * ↑r ^ x✝ / ↑x✝! = rexp (-↑r) * ↑r ^ x✝ / ↑x✝!
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: case e_f
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ≥0
f : ℕ → E
n : ℕ
⊢ (ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)).toReal • f n = (rexp (-↑r) * ↑r ^ n / ↑n !) • f n

Tactic:
ENNReal.toReal_ofReal (by positivity)

Goal state after:
case e_f
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ≥0
f : ℕ → E
n : ℕ
⊢ (rexp (-↑r) * ↑r ^ n / ↑n !) • f n = (rexp (-↑r) * ↑r ^ n / ↑n !) • f n
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

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

Tactic:
normalize_apply

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω},
    m ≤ m₀ →
      ∀ {μ : Measure Ω} [IsFiniteMeasure μ],
        AEMeasurable X μ →
          (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
Y : Ω → ℝ
hYmeas : Measurable Y
hXY : X =ᵐ[μ] Y
⊢ ∀ᵐ (ω : Ω) ∂μ, Y ω = 0 ∨ Y ω = 1

Tactic:
filter_upwards [hX, hXY] with ω hXω hXYω

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω},
    m ≤ m₀ →
      ∀ {μ : Measure Ω} [IsFiniteMeasure μ],
        AEMeasurable X μ →
          (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
Y : Ω → ℝ
hYmeas : Measurable Y
hXY : X =ᵐ[μ] Y
ω : Ω
hXω : X ω = 0 ∨ X ω = 1
hXYω : X ω = Y ω
⊢ Y ω = 0 ∨ Y ω = 1
Module: Mathlib.Probability.IdentDistribIndep

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst✝ : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
⊢ Measure.map (fun ω ↦ (X ω, Y ω)) μ = Measure.map (fun ω' ↦ (Z ω', W ω')) ν

Tactic:
have : IsFiniteMeasure ν := by
      have : IsFiniteMeasure (ν.map Z) := by rw [← hXZ.map_eq]; infer_instance
      exact Measure.isFiniteMeasure_of_map hXZ.aemeasurable_snd

Goal state after:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst✝ : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
this : IsFiniteMeasure ν
⊢ Measure.map (fun ω ↦ (X ω, Y ω)) μ = Measure.map (fun ω' ↦ (Z ω', W ω')) ν
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ map ((fun f ↦ f i) ∘ fun ω i j ↦ X i j (ω i j)) (infinitePi fun i ↦ infinitePi (μ i)) =
    infinitePi fun i_1 ↦ map (fun ω ↦ X i i_1 (ω i i_1)) (infinitePi fun i ↦ infinitePi (μ i))

Tactic:
← map_map (by fun_prop) (by fun_prop),

Goal state after:
case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ map (fun f ↦ f i) (map (fun ω i j ↦ X i j (ω i j)) (infinitePi fun i ↦ infinitePi (μ i))) =
    infinitePi fun i_1 ↦ map (fun ω ↦ X i i_1 (ω i i_1)) (infinitePi fun i ↦ infinitePi (μ i))
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
⊢ map (X i j) (μ i j) =
    map (((fun f ↦ f j) ∘ fun f ↦ f i) ∘ fun ω i j ↦ X i j (ω i j)) (infinitePi fun i ↦ infinitePi (μ i))

Tactic:
← map_map (by fun_prop) (by fun_prop),

Goal state after:
case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
⊢ map (X i j) (μ i j) =
    map ((fun f ↦ f j) ∘ fun f ↦ f i) (map (fun ω i j ↦ X i j (ω i j)) (infinitePi fun i ↦ infinitePi (μ i)))
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
⊢ map (X i j) (μ i j) =
    map ((fun f ↦ f j) ∘ fun f ↦ f i) (infinitePi fun i ↦ map (fun f j ↦ X i j (f j)) (infinitePi (μ i)))

pp: case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
⊢ ∀ (i : ι), Measurable fun f j ↦ X i j (f j)

Tactic:
← map_map (by fun_prop) (by fun_prop),

Goal state after:
case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
⊢ map (X i j) (μ i j) =
    map (fun f ↦ f j) (map (fun f ↦ f i) (infinitePi fun i ↦ map (fun f j ↦ X i j (f j)) (infinitePi (μ i))))

case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
⊢ ∀ (i : ι), Measurable fun f j ↦ X i j (f j)
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case refine_2
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω ↦ 1 | m']
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
i : ι
hi : i ∈ s
⊢ MeasurableSet (g i)

pp: case refine_2
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
⊢ μ[(⋂ i ∈ s, sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(sets i).indicator fun ω ↦ 1 | m']

Tactic:
· simp only [g, dif_pos hi]
      exact (h_sets i hi).choose_spec.1

Goal state after:
case refine_2
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
⊢ μ[(⋂ i ∈ s, sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(sets i).indicator fun ω ↦ 1 | m']
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ (∫⁻ (a : Ω), ‖X a‖ₑ ^ (↑p).toReal ∂μ.tilted fun x ↦ t * X x) < ∞

Tactic:
ENNReal.coe_toReal,

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ (∫⁻ (a : Ω), ‖X a‖ₑ ^ ↑p ∂μ.tilted fun x ↦ t * X x) < ∞
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
⊢ ∀ᵐ (ω' : Ω') ∂ν, (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-ε ^ 2 / (2 * ↑c))

Tactic:
by
  by_cases hc0 : c = 0
  · filter_upwards [h.measure_univ_le_one] with ω' h
    simp only [hc0, NNReal.coe_zero, mul_zero, div_zero, exp_zero]
    refine ENNReal.toReal_le_of_le_ofReal zero_le_one ?_
    simp only [ENNReal.ofReal_one]
    exact (measure_mono (Set.subset_univ _)).trans h
  filter_upwards [measure_ge_le_exp_add h ε] with ω' h
  calc (κ ω').real {ω | ε ≤ X ω}
  -- choose the minimizer of the r.h.s. of `h` for `t ≥ 0`. That is, `t = ε / c`.
  _ ≤ exp (-(ε / c) * ε + c * (ε / c) ^ 2 / 2) := h (ε / c) (by positivity)
  _ = exp (- ε ^ 2 / (2 * c)) := by congr; field

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 ∂ρ
⊢ ∑ k ∈ range K, (∑ j ∈ Ioo k K, (↑j ^ 2)⁻¹) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ ≤
    ∑ k ∈ range K, 2 / (↑k + 1) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ

Tactic:
gcongr with k

Goal state after:
case ha
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := ⋯
ρ : Measure ℝ := ⋯
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
⊢ 0 ≤ ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ

case hbc
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := ⋯
ρ : Measure ℝ := ⋯
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
⊢ ∑ j ∈ Ioo k K, (↑j ^ 2)⁻¹ ≤ 2 / (↑k + 1)
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 ∂ρ
⊢ ∑ k ∈ range K, 2 / (↑k + 1) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ ≤ ∑ k ∈ range K, ∫ (x : ℝ) in ↑k..↑(k + 1), 2 * x ∂ρ

Tactic:
gcongr with k

Goal state after:
case h
Ω : 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 ∂ρ
k : ℕ
a✝ : k ∈ range K
⊢ 2 / (↑k + 1) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ ≤ ∫ (x : ℝ) in ↑k..↑(k + 1), 2 * x ∂ρ
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))) ((κ ⊗ₖ η) ω')
⊢ ∫ (x : Ω), rexp (↑q * X x) * rexp (↑cY * ↑q ^ 2 / 2) ∂κ ω' ≤ rexp (↑(c + cY) * ↑q ^ 2 / 2)

Tactic:
rw [integral_mul_const, NNReal.coe_add, add_mul, add_div, exp_add]
    gcongr
    exact hX_mgf q

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

Goal state before:
pp: case h₂
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ mgf Y μ t ≤ rexp (↑cY * t ^ 2 / 2)

Tactic:
· exact hY.mgf_le t

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case mk'.mk'
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
toIntertwiningMap✝¹ : σ.IntertwiningMap ρ
invFun✝¹ : V → W
left_inv✝¹ : Function.LeftInverse invFun✝¹ toIntertwiningMap✝¹.toFun
right_inv✝¹ : Function.RightInverse invFun✝¹ toIntertwiningMap✝¹.toFun
toIntertwiningMap✝ : σ.IntertwiningMap ρ
invFun✝ : V → W
left_inv✝ : Function.LeftInverse invFun✝ toIntertwiningMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toIntertwiningMap✝.toFun
h :
  { toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹,
        right_inv := right_inv✝¹ }.toLinearEquiv =
    { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝,
        right_inv := right_inv✝ }.toLinearEquiv
⊢ { toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
simpa [IntertwiningMap.ext_iff] using h

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
a : A
g : τ.IntertwiningMap π
x✝¹ : V
x✝ : U
⊢ ((TensorProduct.AlgebraTensorModule.curry (f.tensor (a • g)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (a • f.tensor g).toLinearMap) x✝¹) x✝

Tactic:
simp [TensorProduct.tmul_smul]

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V✝ : Type u_3
W : Type u_4
inst✝⁸ : CommRing k
inst✝⁷ : Group G
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module k V✝
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
ρ✝ : Representation k G V✝
σ : Representation k G W
V : Type u_5
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
S : Subgroup G
inst✝ : S.Normal
g : ↥S
x✝ : ↥(invariants (MonoidHom.comp ρ S.subtype))
x : V
hx : x ∈ invariants (MonoidHom.comp ρ S.subtype)
⊢ ↑(((MonoidHom.comp (ρ.toInvariants S) S.subtype) g) ⟨x, hx⟩) = ↑(LinearMap.id ⟨x, hx⟩)

Tactic:
by simpa using (hx g)

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: case mp
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f
⊢ (Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹) ∘ₗ X.ρ g = Y.ρ g ∘ₗ f

Tactic:
LinearMap.comp_assoc,

Goal state after:
case mp
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f
⊢ Y.ρ g ∘ₗ (f ∘ₗ X.ρ g⁻¹) ∘ₗ X.ρ g = Y.ρ g ∘ₗ f