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

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f) x = ρ'.condKernel x
s : Set (α × ℝ)
hs : MeasurableSet s
⊢ (ρ.fst ⊗ₘ ρ.condKernel) (Prod.map id (embeddingReal Ω) ⁻¹' s) =
    ∫⁻ (a : α), ((ρ.condKernel.map f) a) (Prod.mk a ⁻¹' s) ∂ρ.fst

Tactic:
Measure.compProd_apply

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f) x = ρ'.condKernel x
s : Set (α × ℝ)
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (ρ.condKernel a) (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) ∂ρ.fst =
    ∫⁻ (a : α), ((ρ.condKernel.map f) a) (Prod.mk a ⁻¹' s) ∂ρ.fst

α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f) x = ρ'.condKernel x
s : Set (α × ℝ)
hs : MeasurableSet s
⊢ MeasurableSet (Prod.map id (embeddingReal Ω) ⁻¹' s)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
⊢ Measurable ⇑{ toFun := fun x i ↦ ⋯ ▸ x, invFun := fun x ↦ x ⟨a + 1, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

Tactic:
by
    simp_rw [eqRec_eq_cast]
    refine measurable_pi_lambda _ (fun i ↦ (MeasurableEquiv.cast _ ?_).measurable)
    cases Nat.mem_Ioc_succ' i; rfl

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
⊢ ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)

Tactic:
induction A, hA using induction_on_inter hgen hpi with

Goal state after:
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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X ↑i)
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
⊢ ∫⁻ (a : (i : ↥(Iic b)) → X ↑i), S.indicator 1 a ∂(partialTraj κ a b) (frestrictLe a x₀) =
    ∫⁻ (z : (i : ↥(Iic b)) → X ↑i),
      (cylinder (Iic b) S).indicator 1 (updateFinset x₀ (Iic b) z) ∂(partialTraj κ a b) (frestrictLe a x₀)

Tactic:
congr with x

Goal state after:
case e_f
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
b : ℕ
S : Set ((i : ↥(Iic b)) → X ↑i)
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
x : (i : ↥(Iic b)) → X ↑i
⊢ S.indicator 1 x = (cylinder (Iic b) S).indicator 1 (updateFinset x₀ (Iic b) x)
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : ¬Measurable (Function.uncurry f)
⊢ (κ.withDensity f) a ≪ κ a

Tactic:
rw [withDensity_of_not_measurable _ hf]

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : ¬Measurable (Function.uncurry f)
⊢ 0 a ≪ κ a
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : ¬Measurable (Function.uncurry f)
⊢ IsFiniteKernel (κ.withDensity f)

Tactic:
rw [withDensity_of_not_measurable _ hf]

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : ¬Measurable (Function.uncurry f)
⊢ IsFiniteKernel 0
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : ¬Measurable (Function.uncurry f)
⊢ IsSFiniteKernel (κ.withDensity f)

Tactic:
rw [withDensity_of_not_measurable _ hf]

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : ¬Measurable (Function.uncurry f)
⊢ IsSFiniteKernel 0
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case neg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
this : IsEmpty ↥(Ioc a b)
x : (i : ↥(Iic a)) → X ↑i
s : Set ((i : ↥(Ioc a b)) → X ↑i)
ms : MeasurableSet s
hs : ¬s.Nonempty
⊢ (((partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a b).map (restrict₂ ⋯)) x) s =
    ((const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)) x) s

Tactic:
· rw [Set.not_nonempty_iff_eq_empty.1 hs]
      simp

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

Goal state before:
pp: case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ 0 ≤ (κ.map fun a ↦ (a, ())).density η a x univ

Tactic:
exact density_nonneg ((fst_map_id_prod _ measurable_const).trans_le hκη) _ _ _

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 κ
⊢ κ.singularPart κ = 0

Tactic:
by
  ext : 1; rw [zero_apply, singularPart_eq_zero_iff_absolutelyContinuous]

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

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

Tactic:
unfold discard

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ IsDeterministic (deterministic (fun x ↦ PUnit.unit) ⋯)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case ha.hs
ι✝ : 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
this : s.pi t = ⋂ s', (Subtype.val '' ↑s').pi fun i ↦ if i ∈ s then t i else Set.univ
⊢ ∀ (i : Finset ↑s), NullMeasurableSet ((Subtype.val '' ↑i).pi fun i ↦ if i ∈ s then t i else Set.univ) (infinitePi μ)

pp: case ha.hm
ι✝ : 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
this : s.pi t = ⋂ s', (Subtype.val '' ↑s').pi fun i ↦ if i ∈ s then t i else Set.univ
⊢ Antitone fun s' ↦ (Subtype.val '' ↑s').pi fun i ↦ if i ∈ s then t i else Set.univ

pp: case ha.hf
ι✝ : 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
this : s.pi t = ⋂ s', (Subtype.val '' ↑s').pi fun i ↦ if i ∈ s then t i else Set.univ
⊢ ∃ i, (infinitePi μ) ((Subtype.val '' ↑i).pi fun i ↦ if i ∈ s then t i else Set.univ) ≠ ∞

Tactic:
· refine fun s' ↦ MeasurableSet.nullMeasurableSet (MeasurableSet.pi ?_ (by measurability))
      exact (Finset.countable_toSet _).image _

Goal state after:
case ha.hm
ι✝ : 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
this : s.pi t = ⋂ s', (Subtype.val '' ↑s').pi fun i ↦ if i ∈ s then t i else Set.univ
⊢ Antitone fun s' ↦ (Subtype.val '' ↑s').pi fun i ↦ if i ∈ s then t i else Set.univ

case ha.hf
ι✝ : 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
this : s.pi t = ⋂ s', (Subtype.val '' ↑s').pi fun i ↦ if i ∈ s then t i else Set.univ
⊢ ∃ i, (infinitePi μ) ((Subtype.val '' ↑i).pi fun i ↦ if i ∈ s then t i else Set.univ) ≠ ∞
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
integral_le_kernel : ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ (κ a) t
⊢ ∫⁻ (b : β), 1 - (η b) s ∂κ a = ∫⁻ (x : β), (η x) sᶜ ∂κ a

Tactic:
congr with x

Goal state after:
case e_f
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
integral_le_kernel : ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ (κ a) t
x : β
⊢ 1 - (η x) s = (η x) sᶜ
Module: Mathlib.Probability.Decision.BayesEstimator

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝⁴ : StandardBorelSpace Θ
inst✝³ : Nonempty Θ
hl : Measurable (Function.uncurry ℓ)
P : Kernel Θ 𝓧
inst✝² : IsFiniteKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsSFiniteKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
⊢ ∫⁻ (a : 𝓧), ∫⁻ (x : Θ × 𝓨), ℓ x.1 x.2 ∂(P†π ×ₖ κ) a ∂⇑P ∘ₘ π =
    ∫⁻ (x : 𝓧), ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂κ x ∂⇑P ∘ₘ π

Tactic:
congr with x

Goal state after:
case e_f
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝⁴ : StandardBorelSpace Θ
inst✝³ : Nonempty Θ
hl : Measurable (Function.uncurry ℓ)
P : Kernel Θ 𝓧
inst✝² : IsFiniteKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsSFiniteKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
x : 𝓧
⊢ ∫⁻ (x : Θ × 𝓨), ℓ x.1 x.2 ∂(P†π ×ₖ κ) x = ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂κ x
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
p : PMF α
x : MeasurableSpace α
hx : x ∈ Set.range fun i ↦ (p i • dirac i).caratheodory
y : α
hy : (fun i ↦ (p i • dirac i).caratheodory) y = x
⊢ ⊤ ≤ x

Tactic:
exact
    ((le_of_eq (dirac_caratheodory y).symm).trans (le_smul_caratheodory _ _)).trans (le_of_eq hy)

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

Goal state before:
pp: case neg
α : Type u_1
a : α
s : Set α
ha : a ∉ s
b : α
⊢ s.indicator (⇑(pure a)) b = 0

Tactic:
exact ite_eq_right_iff.2 fun hb =>
      ite_eq_right_iff.2 fun h => (ha <| h ▸ hb).elim

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
s t : Set Ω
inst✝ : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (fun ω ↦ ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω).real t) =ᵐ[μ.restrict s]
    μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}]
⊢ ∀ᵐ (ω : Ω) ∂μ.restrict s, ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]

Tactic:
filter_upwards [condExp_set_generateFrom_singleton hs ht, this] with ω hω₁ hω₂

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
s t : Set Ω
inst✝ : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (fun ω ↦ ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω).real t) =ᵐ[μ.restrict s]
    μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}]
ω : Ω
hω₁ : μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}] ω = μ[|s].real t
hω₂ :
  ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω).real t =
    μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}] ω
⊢ ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: case refine_2
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
h2 : ∀ (ω : Ω), f (A.indicator 1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω
c : ℝ
ω : Ω
⊢ ‖c‖ * ∏ b, ‖(g b) (X b ω)‖ ≤ ‖c‖ * ∏ s, ‖g s‖

Tactic:
gcongr with s

Goal state after:
case h1
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
h2 : ∀ (ω : Ω), f (A.indicator 1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω
c : ℝ
ω : Ω
s : S
a✝ : s ∈ Finset.univ
⊢ ‖(g s) (X s ω)‖ ≤ ‖g s‖
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : Ω → E
⊢ (∫ (ω : Ω), g ω ∂μ.tilted fun x ↦ t * X x) = ∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ

Tactic:
integral_tilted,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : Ω → E
⊢ ∫ (x : Ω), (rexp (t * X x) / ∫ (x : Ω), rexp (t * X x) ∂μ) • g x ∂μ = ∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ
Module: Mathlib.Probability.ProbabilityMassFunction.Integrals

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
⊢ ∑' (a : ↑p.support), (p.toMeasure {↑a}).toReal • f ↑a = ∑' (a : ↑p.support), (p ↑a).toReal • f ↑a

Tactic:
congr with x

Goal state after:
case e_f
α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
x : ↑p.support
⊢ (p.toMeasure {↑x}).toReal • f ↑x = (p ↑x).toReal • f ↑x
Module: Mathlib.Probability.ProbabilityMassFunction.Integrals

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSingletonClass α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Fintype α
p : PMF α
f : α → E
⊢ ∑ x, p.toMeasure.real {x} • f x = ∑ a, (p a).toReal • f a

Tactic:
congr with x

Goal state after:
case e_f
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSingletonClass α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Fintype α
p : PMF α
f : α → E
x : α
⊢ p.toMeasure.real {x} • f x = (p x).toReal • f x
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
x✝ : Locally p 𝓕 X P ∧ Locally q 𝓕 X P
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
n : ℕ
this :
  ∀ (p q : (ι → Ω → E) → Prop),
    IsStable 𝓕 p →
      IsStable 𝓕 q →
        ∀ (hpX : Locally p 𝓕 X P) (hqX : Locally q 𝓕 X P),
          p
            (stoppedProcess (fun i ↦ {ω | ⊥ < (hpX.localSeq ⊓ hqX.localSeq) n ω}.indicator (X i))
              ((hpX.localSeq ⊓ hqX.localSeq) n))
⊢ q
    (stoppedProcess (fun i ↦ {ω | ⊥ < (hpX.localSeq ⊓ hqX.localSeq) n ω}.indicator (X i))
      ((hpX.localSeq ⊓ hqX.localSeq) n))

Tactic:
inf_comm hpX.localSeq

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
x✝ : Locally p 𝓕 X P ∧ Locally q 𝓕 X P
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
n : ℕ
this :
  ∀ (p q : (ι → Ω → E) → Prop),
    IsStable 𝓕 p →
      IsStable 𝓕 q →
        ∀ (hpX : Locally p 𝓕 X P) (hqX : Locally q 𝓕 X P),
          p
            (stoppedProcess (fun i ↦ {ω | ⊥ < (hpX.localSeq ⊓ hqX.localSeq) n ω}.indicator (X i))
              ((hpX.localSeq ⊓ hqX.localSeq) n))
⊢ q
    (stoppedProcess (fun i ↦ {ω | ⊥ < (hqX.localSeq ⊓ hpX.localSeq) n ω}.indicator (X i))
      ((hqX.localSeq ⊓ hpX.localSeq) n))
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 • m ∈ σ.toSubmodule.carrier

Tactic:
zero_smul

Goal state after:
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
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 ρ
k : ℕ
x✝ : k < N
⊢ IntervalIntegrable (fun x ↦ x + 1) ρ ↑k ↑(k + 1)

Tactic:
exact (continuous_id.add continuous_const).intervalIntegrable _ _

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

Goal state before:
pp: case hbc
Ω : 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))) ((κ ⊗ₖ η) ω')
⊢ ∫ (a : Ω), rexp (↑q * X a) ∂κ ω' ≤ rexp (↑c * ↑q ^ 2 / 2)

Tactic:
exact hX_mgf q

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R : Type u
G : Type v
inst✝¹ : CommRing R
inst✝ : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
⊢ W.ρ g = (isoToLinearEquiv i).conj (V.ρ g)

Tactic:
FDRep.isoToLinearEquiv,

Goal state after:
R : Type u
G : Type v
inst✝¹ : CommRing R
inst✝ : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
⊢ W.ρ g = (FGModuleCat.isoToLinearEquiv ((Action.forget (FGModuleCat R) G).mapIso i)).conj (V.ρ g)
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: case add
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : k[G]
x : V
g h : k[G]
gw : f ((((lift k (V →ₗ[k] V) G) ρ) g) x) = (((lift k (W →ₗ[k] W) G) σ) g) (f x)
hw : f ((((lift k (V →ₗ[k] V) G) ρ) h) x) = (((lift k (W →ₗ[k] W) G) σ) h) (f x)
⊢ f ((((lift k (V →ₗ[k] V) G) ρ) (g + h)) x) = (((lift k (W →ₗ[k] W) G) σ) (g + h)) (f x)

Tactic:
simp only [map_add, LinearMap.add_apply, hw, gw]

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
g : G
⊢ (ρ g) ((ρ.asAlgebraHom (average k G)) v) = (ρ.asAlgebraHom (average k G)) v

Tactic:
← asAlgebraHom_single_one,

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
g : G
⊢ (ρ.asAlgebraHom (single g 1)) ((ρ.asAlgebraHom (average k G)) v) = (ρ.asAlgebraHom (average k G)) v