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

Goal state before:
pp: X Y Z : SFinKer
⊢ ((α_ X Y Z).inv ≫
        { hom := { hom := Kernel.swap (X ⊗ Y).carrier Z.carrier, property := ⋯ },
              inv := { hom := Kernel.swap Z.carrier (X ⊗ Y).carrier, property := ⋯ }, hom_inv_id := ⋯,
              inv_hom_id := ⋯ }.hom ≫
          (α_ Z X Y).inv).hom =
    (X ◁
          { hom := { hom := Kernel.swap Y.carrier Z.carrier, property := ⋯ },
              inv := { hom := Kernel.swap Z.carrier Y.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        (α_ X Z Y).inv ≫
          { hom := { hom := Kernel.swap X.carrier Z.carrier, property := ⋯ },
                inv := { hom := Kernel.swap Z.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯,
                inv_hom_id := ⋯ }.hom ▷
            Y).hom

Tactic:
;

Goal state after:
X Y Z : SFinKer
⊢ ((α_ X Y Z).inv ≫
        { hom := { hom := Kernel.swap (X ⊗ Y).carrier Z.carrier, property := ⋯ },
              inv := { hom := Kernel.swap Z.carrier (X ⊗ Y).carrier, property := ⋯ }, hom_inv_id := ⋯,
              inv_hom_id := ⋯ }.hom ≫
          (α_ Z X Y).inv).hom =
    (X ◁
          { hom := { hom := Kernel.swap Y.carrier Z.carrier, property := ⋯ },
              inv := { hom := Kernel.swap Z.carrier Y.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        (α_ X Z Y).inv ≫
          { hom := { hom := Kernel.swap X.carrier Z.carrier, property := ⋯ },
                inv := { hom := Kernel.swap Z.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯,
                inv_hom_id := ⋯ }.hom ▷
            Y).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ (α_ X Y Z).inv ≫
      { hom := { hom := Kernel.swap (X ⊗ Y).carrier Z.carrier, property := ⋯ },
            inv := { hom := Kernel.swap Z.carrier (X ⊗ Y).carrier, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        (α_ Z X Y).inv =
    X ◁
        { hom := { hom := Kernel.swap Y.carrier Z.carrier, property := ⋯ },
            inv := { hom := Kernel.swap Z.carrier Y.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      (α_ X Z Y).inv ≫
        { hom := { hom := Kernel.swap X.carrier Z.carrier, property := ⋯ },
              inv := { hom := Kernel.swap Z.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ▷
          Y

Tactic:
ext : 1; dsimp
    simp only [Kernel.id, Kernel.swap]
    repeat rw [Kernel.deterministic_parallelComp_deterministic]
    repeat rw [Kernel.deterministic_comp_deterministic]
    rfl

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

Goal state before:
pp: X Y : SFinKer
⊢ ({ hom := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ },
            inv := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        { hom := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ },
            inv := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom).hom =
    (𝟙 (X ⊗ Y)).hom

Tactic:
;

Goal state after:
X Y : SFinKer
⊢ ({ hom := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ },
            inv := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        { hom := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ },
            inv := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom).hom =
    (𝟙 (X ⊗ Y)).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ IsSFiniteKernel (Kernel.deterministic (fun x ↦ PUnit.unit) ⋯)

Tactic:
;

Goal state after:
X : SFinKer
⊢ IsSFiniteKernel (Kernel.deterministic (fun x ↦ PUnit.unit) ⋯)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ IsSFiniteKernel (Kernel.deterministic Function.diag ⋯)

Tactic:
;

Goal state after:
X : SFinKer
⊢ IsSFiniteKernel (Kernel.deterministic Function.diag ⋯)
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).hom =
    (λ_ X).inv.hom

Tactic:
;

Goal state after:
X : SFinKer
⊢ ({ hom := Kernel.copy X.carrier, property := ⋯ } ≫ { hom := Kernel.discard X.carrier, property := ⋯ } ▷ X).hom =
    (λ_ X).inv.hom
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 := ⋯ }).hom =
    (ρ_ X).inv.hom

Tactic:
;

Goal state after:
X : SFinKer
⊢ ({ hom := Kernel.copy X.carrier, property := ⋯ } ≫ X ◁ { hom := Kernel.discard X.carrier, property := ⋯ }).hom =
    (ρ_ X).inv.hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

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

Tactic:
;

Goal state after:
X : SFinKer
⊢ ({ hom := Kernel.copy X.carrier, property := ⋯ } ≫ X ◁ { hom := Kernel.copy X.carrier, property := ⋯ }).hom =
    ({ hom := Kernel.copy X.carrier, property := ⋯ } ≫
        { hom := Kernel.copy X.carrier, property := ⋯ } ▷ X ≫ (α_ X X X).hom).hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ (Δ ≫ (β_ X X).hom).hom = Δ.hom

Tactic:
;

Goal state after:
X : SFinKer
⊢ (Δ ≫ (β_ X X).hom).hom = Δ.hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ Kernel.swap X.carrier X.carrier ∘ₖ Kernel.copy X.carrier = Kernel.copy X.carrier

Tactic:
;

Goal state after:
X : SFinKer
⊢ Kernel.swap X.carrier X.carrier ∘ₖ Kernel.copy X.carrier = Kernel.copy X.carrier
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Δ.hom = ((Δ ⊗ₘ Δ) ≫ MonoidalCategory.tensorμ X X Y Y).hom

Tactic:
;

Goal state after:
X Y : SFinKer
⊢ Δ.hom = ((Δ ⊗ₘ Δ) ≫ MonoidalCategory.tensorμ X X Y Y).hom
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : 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 : ℝ
⊢ Integrable (fun ω ↦ c * ∏ s, (g s) (X s ω)) P

Tactic:
refine Integrable.of_bound ?_ (‖c‖ * ∏ s, ‖g s‖) (ae_of_all _ fun ω ↦ ?_)

Goal state after:
case refine_1
Ω : 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 : ℝ
⊢ AEStronglyMeasurable (fun ω ↦ c * ∏ s, (g s) (X s ω)) P

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 * ∏ s, (g s) (X s ω)‖ ≤ ‖c‖ * ∏ s, ‖g s‖
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ ε.hom = ((ε ⊗ₘ ε) ≫ (λ_ (𝟙_ SFinKer)).hom).hom

Tactic:
;

Goal state after:
X Y : SFinKer
⊢ ε.hom = ((ε ⊗ₘ ε) ≫ (λ_ (𝟙_ SFinKer)).hom).hom
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x x✝ : ↑I
⊢ x✝ ∈ Iic x ↔ x✝ ∈ Icc 0 x

Tactic:
;

Goal state after:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x x✝ : ↑I
⊢ x✝ ∈ Iic x ↔ x✝ ∈ Icc 0 x
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: ⊢ Δ.hom = (λ_ (𝟙_ SFinKer)).inv.hom

Tactic:
;

Goal state after:
⊢ Δ.hom = (λ_ (𝟙_ SFinKer)).inv.hom
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
κ : Kernel X.carrier Y.carrier
inst✝¹ : IsDeterministic κ
inst✝ : IsMarkovKernel κ
⊢ ({ hom := κ, property := ⋯ } ≫ Δ).hom = (Δ ≫ ({ hom := κ, property := ⋯ } ⊗ₘ { hom := κ, property := ⋯ })).hom

Tactic:
;

Goal state after:
X Y : SFinKer
κ : Kernel X.carrier Y.carrier
inst✝¹ : IsDeterministic κ
inst✝ : IsMarkovKernel κ
⊢ ({ hom := κ, property := ⋯ } ≫ Δ).hom = (Δ ≫ ({ hom := κ, property := ⋯ } ⊗ₘ { hom := κ, property := ⋯ })).hom
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
hin : ¬i ≤ n
this : {x | τ x = ↑i} = ∅
⊢ μ[f n | hτ.measurableSpace] =ᶠ[⊥] f i

Tactic:
;

Goal state after:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
hin : ¬i ≤ n
this : {x | τ x = ↑i} = ∅
⊢ μ[f n | hτ.measurableSpace] =ᶠ[⊥] f i
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case e'_3
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ}, MeasurableSet s → MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
            (Measure.map (fun ω ↦ (ω, f ω, g ω)) μ) ((k ⁻¹' s) ×ˢ t ×ˢ u)
h_right :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ) (s ×ˢ t ×ˢ u) =
            (⇑(Kernel.id ×ₖ
                    ((condExpKernel μ (MeasurableSpace.comap k mγ)).map f ×ₖ
                      (condExpKernel μ (MeasurableSpace.comap k mγ)).map g)) ∘ₘ
                μ.trim ⋯)
              ((k ⁻¹' s) ×ˢ t ×ˢ u)
h :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
            (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ) (s ×ˢ t ×ˢ u)
t : Set β
u : Set β'
s : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ (⇑(Kernel.id ×ₖ
            ((condExpKernel μ (MeasurableSpace.comap k inferInstance)).map f ×ₖ
              (condExpKernel μ (MeasurableSpace.comap k inferInstance)).map g)) ∘ₘ
        μ.trim ⋯)
      ((k ⁻¹' s) ×ˢ t ×ˢ u) =
    (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ) (s ×ˢ t ×ˢ u)

Tactic:
· exact (h_right hs ht hu).symm

Goal state after:
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
⊢ μ[stoppedValue f τ | hσ.measurableSpace ⊓ hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}]
    μ[stoppedValue f τ | hτ.measurableSpace ⊓ hσ.measurableSpace]

Tactic:
inf_comm

Goal state after:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
⊢ μ[stoppedValue f τ | hτ.measurableSpace ⊓ hσ.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}]
    μ[stoppedValue f τ | hτ.measurableSpace ⊓ hσ.measurableSpace]
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ AEMeasurable X (μ.tilted fun x ↦ t * X x)

pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ.tilted fun x ↦ t * X x) ^ 2 ∂μ.tilted fun x ↦ t * X x) =
    iteratedDeriv 2 (cgf X μ) t

Tactic:
;

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ AEMeasurable X (μ.tilted fun x ↦ t * X x)

Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ.tilted fun x ↦ t * X x) ^ 2 ∂μ.tilted fun x ↦ t * X x) =
    iteratedDeriv 2 (cgf X μ) t
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
i : Fin (1 + 1)
⊢ (binomial p h 1) i = (map (fun x ↦ bif x then 1 else 0) (bernoulli p h)) i

Tactic:
;

Goal state after:
p : ℝ≥0
h : p ≤ 1
i : Fin (1 + 1)
⊢ (binomial p h 1) i = (map (fun x ↦ bif x then 1 else 0) (bernoulli p h)) i
Module: Mathlib.Probability.ProbabilityMassFunction.Integrals

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

Tactic:
;

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.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 κ ν
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * (-X) ω)) (⇑κ ∘ₘ ν)

Tactic:
simpa using h.integrable_exp_mul (-t)

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝² : LinearOrder ι
𝓕 : Filtration ι mΩ
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
ω : Ω
hτω : Tendsto (fun x ↦ τ x ω) atTop (𝓝 ⊤)
⊢ Tendsto (fun x ↦ σ x ω) atTop (𝓝 ⊤) → Tendsto (fun x ↦ (τ ⊓ σ) x ω) atTop (𝓝 ⊤)

Tactic:
hσω

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝² : LinearOrder ι
𝓕 : Filtration ι mΩ
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
ω : Ω
hτω : Tendsto (fun x ↦ τ x ω) atTop (𝓝 ⊤)
hσω : Tendsto (fun x ↦ σ x ω) atTop (𝓝 ⊤)
⊢ Tendsto (fun x ↦ (τ ⊓ σ) x ω) atTop (𝓝 ⊤)
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝² : LinearOrder ι
𝓕 : Filtration ι mΩ
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
ω : Ω
hτω : Monotone fun x ↦ τ x ω
⊢ (Monotone fun x ↦ σ x ω) → Monotone fun x ↦ (τ ⊓ σ) x ω

Tactic:
hσω

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝² : LinearOrder ι
𝓕 : Filtration ι mΩ
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
ω : Ω
hτω : Monotone fun x ↦ τ x ω
hσω : Monotone fun x ↦ σ x ω
⊢ Monotone fun x ↦ (τ ⊓ σ) x ω
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
h : HasSubgaussianMGF X c κ ν
ε : ℝ
ω' : Ω'
h1 : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h2 : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
a✝ : IsFiniteMeasure (κ ω')
t : ℝ
ht : 0 ≤ t
⊢ mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
exact h1 t

Goal state after:
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 ≤ ε
hc0 : ¬c = 0
ω' : Ω'
h : ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-t * ε + ↑c * t ^ 2 / 2)
⊢ -(ε / ↑c) * ε + ↑c * (ε / ↑c) ^ 2 / 2 = -ε ^ 2 / (2 * ↑c)

Tactic:
;

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : ¬c = 0
ω' : Ω'
h : ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-t * ε + ↑c * t ^ 2 / 2)
⊢ -(ε / ↑c) * ε + ↑c * (ε / ↑c) ^ 2 / 2 = -ε ^ 2 / (2 * ↑c)
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Ω
p : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp : IsStable 𝓕 p
X : ι → Ω → E
hX : (fun Y ↦ Locally p 𝓕 Y P) X
τ : Ω → WithTop ι
hτ : IsStoppingTime 𝓕 τ
n : ℕ
⊢ p
    (stoppedProcess (fun i ↦ {ω | ⊥ < τ ω}.indicator ({ω | ⊥ < Locally.localSeq hX n ω}.indicator (X i)))
      (Locally.localSeq hX n ⊓ τ))

Tactic:
inf_comm,

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
p : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp : IsStable 𝓕 p
X : ι → Ω → E
hX : (fun Y ↦ Locally p 𝓕 Y P) X
τ : Ω → WithTop ι
hτ : IsStoppingTime 𝓕 τ
n : ℕ
⊢ p
    (stoppedProcess (fun i ↦ {ω | ⊥ < τ ω}.indicator ({ω | ⊥ < Locally.localSeq hX n ω}.indicator (X i)))
      (τ ⊓ Locally.localSeq hX n))
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ' : Subrepresentation ρ
x✝ : ↥ρ'.toSubmodule
⊢ ↑(((ρ 1).restrict ⋯) x✝) = ↑(1 x✝)

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ' : Subrepresentation ρ
x✝ : ↥ρ'.toSubmodule
⊢ ↑(((ρ 1).restrict ⋯) x✝) = ↑(1 x✝)
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ' : Subrepresentation ρ
x y : G
x✝ : ↥ρ'.toSubmodule
⊢ ↑(((ρ (x * y)).restrict ⋯) x✝) = ↑(((ρ x).restrict ⋯ * (ρ y).restrict ⋯) x✝)

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ' : Subrepresentation ρ
x y : G
x✝ : ↥ρ'.toSubmodule
⊢ ↑(((ρ (x * y)).restrict ⋯) x✝) = ↑(((ρ x).restrict ⋯ * (ρ y).restrict ⋯) x✝)
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: case add
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 ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • v ∈ σ.toSubmodule.carrier
hy : y • v ∈ σ.toSubmodule.carrier
⊢ x • v + y • v ∈ σ.toSubmodule.carrier

Tactic:
;

Goal state after:
case add
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 ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • v ∈ σ.toSubmodule.carrier
hy : y • v ∈ σ.toSubmodule.carrier
⊢ x • v + y • v ∈ σ.toSubmodule.carrier