mathlib-initiative/mathlib-tactics huggingface dataset:
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 π
⊢ ⇑(Kernel.id ∥ₖ κ) ∘ₘ π ⊗ₘ P = ⇑(Kernel.id ∥ₖ κ) ∘ₘ ⇑(P†π ×ₖ Kernel.id) ∘ₘ ⇑P ∘ₘ π

Tactic:
posterior_prod_id_comp

Goal state after:
Θ : 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 π
⊢ ⇑(Kernel.id ∥ₖ κ) ∘ₘ π ⊗ₘ P = ⇑(Kernel.id ∥ₖ κ) ∘ₘ π ⊗ₘ P
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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f :
  (∀ᵐ (y : (i : ↥(Iic b)) → X ↑i) ∂(partialTraj κ a b) x₀, Integrable f ((traj κ b) y)) ∧
    Integrable (fun y ↦ ∫ (z : (n : ℕ) → X n), ‖f z‖ ∂(traj κ b) y) ((partialTraj κ a b) x₀)
⊢ ∀ᵐ (x : (i : ℕ) → X i) ∂(traj κ a) x₀, Integrable f ((traj κ b) (frestrictLe b x))

Tactic:
apply ae_of_ae_map (p := fun x ↦ Integrable f (traj κ b x))

Goal state after:
case hf
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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f :
  (∀ᵐ (y : (i : ↥(Iic b)) → X ↑i) ∂(partialTraj κ a b) x₀, Integrable f ((traj κ b) y)) ∧
    Integrable (fun y ↦ ∫ (z : (n : ℕ) → X n), ‖f z‖ ∂(traj κ b) y) ((partialTraj κ a b) x₀)
⊢ AEMeasurable (frestrictLe b) ((traj κ a) x₀)

case h
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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f :
  (∀ᵐ (y : (i : ↥(Iic b)) → X ↑i) ∂(partialTraj κ a b) x₀, Integrable f ((traj κ b) y)) ∧
    Integrable (fun y ↦ ∫ (z : (n : ℕ) → X n), ‖f z‖ ∂(traj κ b) y) ((partialTraj κ a b) x₀)
⊢ ∀ᵐ (y : (i : ↥(Iic b)) → X ↑i) ∂Measure.map (frestrictLe b) ((traj κ a) x₀), Integrable f ((traj κ b) y)

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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f :
  (∀ᵐ (y : (i : ↥(Iic b)) → X ↑i) ∂(partialTraj κ a b) x₀, Integrable f ((traj κ b) y)) ∧
    Integrable (fun y ↦ ∫ (z : (n : ℕ) → X n), ‖f z‖ ∂(traj κ b) y) ((partialTraj κ a b) x₀)
⊢ MeasurableSpace ((i : ↥(Iic b)) → X ↑i)
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : PMF α
s : Set α
hs : MeasurableSet s
⊢ p.toMeasure s = 0 ↔ Disjoint p.support s

Tactic:
rw [p.toMeasure_apply_eq_toOuterMeasure_apply hs, toOuterMeasure_apply_eq_zero_iff]

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r : ℝ≥0
t : ℝ
⊢ cexp ↑(-↑r) * cexp (↑↑r * cexp (↑t * I)) = cexp (↑↑r * (cexp (↑t * I) - 1))

Tactic:
← Complex.exp_add

Goal state after:
r : ℝ≥0
t : ℝ
⊢ cexp (↑(-↑r) + ↑↑r * cexp (↑t * I)) = cexp (↑↑r * (cexp (↑t * I) - 1))
Module: Mathlib.Probability.Independence.InfinitePi

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

Tactic:
rw [← this, ← AEMeasurable.map_map_of_aemeasurable, h, infinitePi_map_restrict]

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

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

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

Goal state before:
pp: ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ map (fun ω ↦ (ω i, ω j)) (infinitePi P) = (P i).prod (P j)

Tactic:
IndepFun.map_prod_eq_prod_map_map

Goal state after:
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ (map (fun ω ↦ ω i) (infinitePi P)).prod (map (fun ω ↦ ω j) (infinitePi P)) = (P i).prod (P j)

case hf
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ AEMeasurable (fun ω ↦ ω i) (infinitePi P)

case hg
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ AEMeasurable (fun ω ↦ ω j) (infinitePi P)

case a
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ (fun ω ↦ ω i) ⟂ᵢ[infinitePi P] fun ω ↦ ω j
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case refine_2.refine_2
Ω : 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'] ω
h_inter_eq :
  ∀ (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']
s : Finset ι
f : ι → Set Ω
h : μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']
hf : ∀ i ∈ s, f i ∈ π i
⊢ StronglyMeasurable fun a ↦ ∏ i ∈ s, ((condExpKernel μ m') a) (f i)

Tactic:
refine Measurable.stronglyMeasurable ?_
      exact Finset.measurable_fun_prod s (fun i hi ↦ measurable_condExpKernel (hπ i _ (hf i hi)))

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

Goal state before:
pp: X Y : Stoch
κ✝ : X ⟶ Y
X✝ Y✝ : Stoch
κ : X✝ ⟶ Y✝
⊢ κ ≫ ε = ε

Tactic:
ext : 2

Goal state after:
X Y : Stoch
κ✝ : X ⟶ Y
X✝ Y✝ : Stoch
κ : X✝ ⟶ Y✝
⊢ (κ ≫ ε).hom.hom = ε.hom.hom
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

Goal state after:
X Y : Stoch
κ✝ : X ⟶ Y
X✝ Y✝ Z✝ : Stoch
κ : X✝ ⟶ Y✝
η : Y✝ ⟶ Z✝
x✝ : Deterministic (κ ≫ η)
⊢ (κ ≫ Δ ≫ (η ⊗ₘ 𝟙 Y✝)).hom.hom = (Δ ≫ (κ ≫ η ⊗ₘ κ)).hom.hom
Module: Mathlib.Probability.Kernel.Invariance

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
hα : Nonempty α
⊢ (κ ∘ₖ η).Invariant μ

Tactic:
Invariant,

Goal state after:
case inr
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
hα : Nonempty α
⊢ ⇑(κ ∘ₖ η) ∘ₘ μ = μ
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_1
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ Kernel.id.map f₁ ∘ₖ Kernel.id.map Prod.snd = Kernel.id

Tactic:
Kernel.id_map hf₁,

Goal state after:
case refine_1
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ Kernel.deterministic f₁ hf₁ ∘ₖ Kernel.id.map Prod.snd = Kernel.id
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_2
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ (Kernel.id.map f₁).map Prod.snd = Kernel.id

Tactic:
Kernel.id_map hf₁,

Goal state after:
case refine_2
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ (Kernel.deterministic f₁ hf₁).map Prod.snd = Kernel.id
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_1
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ Kernel.id.map f₁ ∘ₖ Kernel.id.map Prod.fst = Kernel.id

Tactic:
Kernel.id_map hf₁,

Goal state after:
case refine_1
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ Kernel.deterministic f₁ hf₁ ∘ₖ Kernel.id.map Prod.fst = Kernel.id
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_2
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ (Kernel.id.map f₁).map Prod.fst = Kernel.id

Tactic:
Kernel.id_map hf₁,

Goal state after:
case refine_2
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ (Kernel.deterministic f₁ hf₁).map Prod.fst = Kernel.id
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
a✝ : PUnit.{u + 1} × X✝.carrier
s✝ : Set Y✝.carrier
hs : MeasurableSet s✝
⊢ (((Kernel.id ∥ₖ κ.hom).map Prod.snd) a✝) s✝ = ((κ.hom.comap Prod.snd ⋯) a✝) s✝

Tactic:
have := κ.2

Goal state after:
X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
a✝ : PUnit.{u + 1} × X✝.carrier
s✝ : Set Y✝.carrier
hs : MeasurableSet s✝
this : IsSFiniteKernel κ.hom
⊢ (((Kernel.id ∥ₖ κ.hom).map Prod.snd) a✝) s✝ = ((κ.hom.comap Prod.snd ⋯) a✝) s✝
Module: Mathlib.Probability.Independence.Conditional

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

Tactic:
by
  rw [iCondIndep_iff_iCondIndepSets, iCondIndepSets_iff]
  · rfl
  · exact hm

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

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
a✝ : X✝.carrier × PUnit.{u + 1}
s✝ : Set Y✝.carrier
hs : MeasurableSet s✝
⊢ (((κ.hom ∥ₖ Kernel.id).map Prod.fst) a✝) s✝ = ((κ.hom.comap Prod.fst ⋯) a✝) s✝

Tactic:
have := κ.2

Goal state after:
X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
a✝ : X✝.carrier × PUnit.{u + 1}
s✝ : Set Y✝.carrier
hs : MeasurableSet s✝
this : IsSFiniteKernel κ.hom
⊢ (((κ.hom ∥ₖ Kernel.id).map Prod.fst) a✝) s✝ = ((κ.hom.comap Prod.fst ⋯) a✝) s✝
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case hs2
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s

Tactic:
exact hm₂

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

Goal state before:
pp: case mp
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
⊢ 0 < X ω → ∃ a, 0 < a ∧ ↑a ≤ X ω

pp: case mpr
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
⊢ (∃ a, 0 < a ∧ ↑a ≤ X ω) → 0 < X ω

Tactic:
· intro hp
      obtain ⟨q, h1, h2⟩ := exists_rat_btwn hp
      exact ⟨q, (q.cast_pos.1 h1), h2.le⟩

Goal state after:
case mpr
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
⊢ (∃ a, 0 < a ∧ ↑a ≤ X ω) → 0 < 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:
simp_rw [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: A : Type u_1
G : Type u_2
W : Type u_3
inst✝³ : Semiring A
inst✝² : Monoid G
inst✝¹ : AddCommMonoid W
inst✝ : Module A W
ρ : Representation A G W
⊢ Function.Injective toSubmodule

Tactic:
by
  rintro ⟨_, _⟩
  congr!

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

Goal state before:
pp: case h₁
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 := ⋯
q : ℝ≥0 := ⋯
ω' : Ω'
hmX : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑cX * t ^ 2 / 2)
hmY : ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑cY * t ^ 2 / 2)
hlX : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')
hlY : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')
t : ℝ
⊢ ∫ (x : Ω), rexp (t * ↑q * Y x) ∂κ ω' ≤ rexp (↑cY * (t * ↑q) ^ 2 / 2)

Tactic:
exact hmY (t * q)

Goal state after:
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: case hs
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < P {ω | σ n k ω < min (τ n ω) ↑(T n)}
⊢ ∀ᵐ (ω : Ω) ∂P, Antitone fun x ↦ ω ∈ {ω | σ n x ω < min (τ n ω) ↑(T n)}

pp: case hsm
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < P {ω | σ n k ω < min (τ n ω) ↑(T n)}
⊢ ∀ (i : ℕ), NullMeasurableSet {ω | σ n i ω < min (τ n ω) ↑(T n)} P

pp: case hfin
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < P {ω | σ n k ω < min (τ n ω) ↑(T n)}
⊢ ∃ i, P {ω | σ n i ω < min (τ n ω) ↑(T n)} ≠ ∞

Tactic:
· filter_upwards [(hσ n).mono] with ω hω
    intros i j hij
    specialize hω hij
    simp [Set.ofPred] at *
    grind

Goal state after:
case hsm
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < P {ω | σ n k ω < min (τ n ω) ↑(T n)}
⊢ ∀ (i : ℕ), NullMeasurableSet {ω | σ n i ω < min (τ n ω) ↑(T n)} P

case hfin
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < P {ω | σ n k ω < min (τ n ω) ↑(T n)}
⊢ ∃ i, P {ω | σ n i ω < min (τ n ω) ↑(T n)} ≠ ∞
Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic

Goal state before:
pp: case inr
A : Type u_1
V : Type u_2
k : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : Ring A
inst✝⁸ : Algebra k A
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module A V
inst✝⁴ : IsScalarTower k A V
inst✝³ : IsSimpleModule A V
inst✝² : FiniteDimensional k V
inst✝¹ : IsAlgClosed k
inst✝ : IsMulCommutative A
this : Nontrivial V
v : V
v_nz : v ≠ 0
U : Submodule A V :=
  let __src := k ∙ v;
  { toAddSubmonoid := __src.toAddSubmonoid, smul_mem' := ⋯ }
hU : U = ⊤
⊢ Module.finrank k V = 1

Tactic:
rw [finrank_eq_one_iff_of_nonzero v v_nz]
    rwa [← top_le_iff] at hU ⊢

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

Goal state before:
pp: k : Type u
inst✝² : Semiring k
G : Type v1
H : Type v2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : H →* G
M : Rep k G
x✝³ x✝² : Rep k G
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ (resFunctor f).map (x✝¹ + x✝) = (resFunctor f).map x✝¹ + (resFunctor f).map x✝

Tactic:
ext : 2

Goal state after:
k : Type u
inst✝² : Semiring k
G : Type v1
H : Type v2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : H →* G
M : Rep k G
x✝³ x✝² : Rep k G
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ (Hom.hom ((resFunctor f).map (x✝¹ + x✝))).toLinearMap =
    (Hom.hom ((resFunctor f).map x✝¹ + (resFunctor f).map x✝)).toLinearMap
Module: Mathlib.RepresentationTheory.Rep.Res

Goal state before:
pp: k✝ : Type u
inst✝³ : Semiring k✝
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
f : H →* G
M : Rep k✝ G
k : Type u
inst✝ : CommSemiring k
x✝³ x✝² : Rep k G
x✝¹ : x✝³ ⟶ x✝²
x✝ : k
⊢ (resFunctor f).map (x✝ • x✝¹) = x✝ • (resFunctor f).map x✝¹

Tactic:
ext : 2

Goal state after:
k✝ : Type u
inst✝³ : Semiring k✝
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
f : H →* G
M : Rep k✝ G
k : Type u
inst✝ : CommSemiring k
x✝³ x✝² : Rep k G
x✝¹ : x✝³ ⟶ x✝²
x✝ : k
⊢ (Hom.hom ((resFunctor f).map (x✝ • x✝¹))).toLinearMap = (Hom.hom (x✝ • (resFunctor f).map x✝¹)).toLinearMap
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ✝ φ ψ : SimpleFunc E E
hφ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hψ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
ω : Ω
hωφ : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hωψ : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
⊢ (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, (φ + ψ) (X i ω)) = fun x ↦
    (↑x)⁻¹ • ∑ i ∈ Finset.range x, φ (X i ω) + (↑x)⁻¹ • ∑ i ∈ Finset.range x, ψ (X i ω)

Tactic:
simp [sum_add_distrib]

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
⊢ { toFun := fun f ↦ (resFunctor φ).map (↑(leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single 1 1)) ≫ f,
      map_add' := ⋯, map_smul' := ⋯ } =
    1

Tactic:
by
    ext
    simp [homEquiv]

Goal state after: