mathlib-initiative/mathlib-tactics huggingface dataset:
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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
⊢ (partialTraj κ a b) u ⊗ₘ traj κ b = Measure.map (fun x ↦ (frestrictLe b x, x)) ((traj κ a) u)

Tactic:
by
  ext s ms
  rw [Measure.map_apply, Measure.compProd_apply, ← traj_comp_partialTraj hab, comp_apply']
  · congr 1 with x
    rw [← traj_map_updateFinset, Measure.map_apply, Measure.map_apply]
    · congr 1 with y
      simp only [Set.mem_preimage]
      congrm (fun i ↦ ?_, fun i ↦ ?_) ∈ s <;> simp [updateFinset]
    any_goals fun_prop
    all_goals exact ms.preimage (by fun_prop)
  any_goals exact ms.preimage (by fun_prop)
  fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ↑unitInterval
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → E
hp : p ≠ 0
⊢ Integrable f (geometricMeasure p) ↔ Summable fun n ↦ (1 - ↑p) ^ n * ↑p * ‖f n‖

Tactic:
rw [geometricMeasure_eq hp, integrable_sum_dirac_iff (by simp)]

Goal state after:
p : ↑unitInterval
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → E
hp : p ≠ 0
⊢ (Summable fun i ↦ (ENNReal.ofReal ((1 - ↑p) ^ i * ↑p)).toReal * ‖f i‖) ↔ Summable fun n ↦ (1 - ↑p) ^ n * ↑p * ‖f n‖
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

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

Tactic:
· refine (tsum_congr fun b => ?_).trans tsum_zero
    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.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
⊢ (pure a).bindOnSupport f = f a ⋯

Tactic:
refine PMF.ext fun b => ?_

Goal state after:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
⊢ ((pure a).bindOnSupport f) b = (f a ⋯) b
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r : ℝ≥0
t : ℝ
⊢ ∫ (x : ℝ), cexp (↑(inner ℝ x t) * I) ∂Po(ℝ, r) = cexp (↑↑r * (cexp (↑t * I) - 1))

Tactic:
integral_map .of_discrete (by fun_prop),

Goal state after:
r : ℝ≥0
t : ℝ
⊢ ∫ (x : ℕ), cexp (↑(inner ℝ (↑x) t) * I) ∂Po(r) = cexp (↑↑r * (cexp (↑t * I) - 1))
Module: Mathlib.Probability.HasLawExists

Goal state before:
pp: ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ ∃ Ω x P X, (∀ (i : ι), Measurable (X i)) ∧ (∀ (i : ι), HasLaw (X i) (μ i) P) ∧ iIndepFun X P ∧ IsProbabilityMeasure P

Tactic:
use Π i, (𝓧 i), .pi, infinitePi μ, fun i ↦ Function.eval i

Goal state after:
case h
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ (∀ (i : ι), Measurable ((fun i ↦ Function.eval i) i)) ∧
    (∀ (i : ι), HasLaw ((fun i ↦ Function.eval i) i) (μ i) (infinitePi μ)) ∧
      iIndepFun (fun i ↦ Function.eval i) (infinitePi μ) ∧ IsProbabilityMeasure (infinitePi μ)
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
hμs : μ s = 0 ∨ μ s = ∞
⊢ pdf X ℙ μ =ᵐ[μ] 0

Tactic:
rcases hμs with H | H

Goal state after:
case inl
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
H : μ s = 0
⊢ pdf X ℙ μ =ᵐ[μ] 0

case inr
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
H : μ s = ∞
⊢ pdf X ℙ μ =ᵐ[μ] 0
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: case neg
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
⊢ (μ.restrict s)[f | MeasurableSpace.generateFrom {s}] =ᵐ[μ.restrict s] fun x ↦ ∫ (x : Ω), f x ∂μ[|s]

Tactic:
refine (ae_eq_condExp_of_forall_setIntegral_eq (generateFrom_singleton_le hs) hf.restrict ?_ ?_
      stronglyMeasurable_const.aestronglyMeasurable).symm

Goal state after:
case neg.refine_1
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
⊢ ∀ (s_1 : Set Ω),
    MeasurableSet s_1 → (μ.restrict s) s_1 < ∞ → IntegrableOn (fun x ↦ ∫ (x : Ω), f x ∂μ[|s]) s_1 (μ.restrict s)

case neg.refine_2
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
⊢ ∀ (s_1 : Set Ω),
    MeasurableSet s_1 →
      (μ.restrict s) s_1 < ∞ →
        ∫ (x : Ω) in s_1, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s = ∫ (x : Ω) in s_1, f x ∂μ.restrict s
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: case neg.refine_2.inr.inr.inr
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = univ
⊢ ∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s = ∫ (x : Ω) in t, f x ∂μ.restrict s

Tactic:
simp only [h, Measure.restrict_univ, cond, integral_smul_measure, ENNReal.toReal_inv, ←
        measureReal_def, integral_const, MeasurableSet.univ, measureReal_restrict_apply, univ_inter]

Goal state after:
case neg.refine_2.inr.inr.inr
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = univ
⊢ μ.real s • (μ.real s)⁻¹ • ∫ (x : Ω) in s, f x ∂μ = ∫ (x : Ω) in s, f x ∂μ
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = univ
⊢ μ s ≠ ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
inst✝¹⁰ : (s : S) → TopologicalSpace (E s)
inst✝⁹ : (s : S) → MeasurableSpace (E s)
inst✝⁸ : ∀ (s : S), BorelSpace (E s)
inst✝⁷ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁶ : (t : T) → TopologicalSpace (F t)
inst✝⁵ : (t : T) → MeasurableSpace (F t)
inst✝⁴ : ∀ (t : T), BorelSpace (F t)
inst✝³ : ∀ (t : T), HasOuterApproxClosed (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst✝² : IsFiniteMeasure P
inst✝¹ : Finite S
inst✝ : Finite T
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : ((t : T) → F t) →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ (f fun x ↦ X x ω) * g fun x ↦ Y x ω) x ∂P =
      (∫ (x : Ω), (fun ω ↦ f fun x ↦ X x ω) x ∂P) * ∫ (x : Ω), (fun ω ↦ g fun x ↦ Y x ω) x ∂P
this✝ : Fintype S
this : Fintype T
f : (s : S) → E s →ᵇ ℝ
g : (t : T) → F t →ᵇ ℝ
⊢ ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ∏ t, ⇑(g t) ∘ Y t) x ∂P =
    (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P

Tactic:
convert!
    h (∏ s, (f s).compContinuous ⟨Function.eval s, by fun_prop⟩)
      (∏ t, (g t).compContinuous ⟨Function.eval t, by fun_prop⟩) <;> simp

Goal state after:
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1

Tactic:
apply measure_eq_zero_or_one_of_indepSet_self' ?_
    ((indep_limsup_atTop_self h_le h_indep).indepSet_of_measurableSet ht_tail ht_tail)
  filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance

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

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (x : X), B.indicator 1 x * A.indicator 1 x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), A.indicator 1 x ∂π x₀

Tactic:
simp_rw [← inter_indicator_mul]
  rw [lintegral_indicator ((h𝓑𝓧 _ hB).inter hA), lintegral_indicator hA]
  simp only [MeasureTheory.lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter,
    Pi.one_apply, one_mul]
  rw [← hπ.inter_eq_indicator_mul h𝓑𝓧 hA hB, inter_comm]

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

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
⊢ Kernel.deterministic Prod.snd ⋯ ∘ₖ (Kernel.id ∥ₖ κ.hom) = κ.hom ∘ₖ Kernel.id.map Prod.snd

Tactic:
Kernel.id_map (by fun_prop)

Goal state after:
X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
⊢ Kernel.deterministic Prod.snd ⋯ ∘ₖ (Kernel.id ∥ₖ κ.hom) = κ.hom ∘ₖ Kernel.deterministic Prod.snd ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
⊢ Kernel.deterministic Prod.fst ⋯ ∘ₖ (κ.hom ∥ₖ Kernel.id) = κ.hom ∘ₖ Kernel.id.map Prod.fst

Tactic:
Kernel.id_map (by fun_prop)

Goal state after:
X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
⊢ Kernel.deterministic Prod.fst ⋯ ∘ₖ (κ.hom ∥ₖ Kernel.id) = κ.hom ∘ₖ Kernel.deterministic Prod.fst ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: a✝¹ : PUnit.{u + 1}
s✝ : Set (PUnit.{u + 1} × PUnit.{u + 1})
a✝ : MeasurableSet s✝
⊢ ((Kernel.copy PUnit.{u + 1}) a✝¹) s✝ = ((Kernel.id.map fun x ↦ (PUnit.unit, x)) a✝¹) s✝

Tactic:
Kernel.id_map (by fun_prop)

Goal state after:
a✝¹ : PUnit.{u + 1}
s✝ : Set (PUnit.{u + 1} × PUnit.{u + 1})
a✝ : MeasurableSet s✝
⊢ ((Kernel.copy PUnit.{u + 1}) a✝¹) s✝ = ((Kernel.deterministic (fun x ↦ (PUnit.unit, x)) ⋯) a✝¹) s✝
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : 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)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
a : Ω
⊢ ((condDistrib f k μ) (k a)) t = (((condExpKernel μ (MeasurableSpace.comap k mγ)).map f) a) t →
    ((condDistrib g k μ) (k a)) u = (((condExpKernel μ (MeasurableSpace.comap k mγ)).map g) a) u →
      ((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) (k a)) (s ×ˢ t ×ˢ u) =
        ((Kernel.id ×ₖ
              ((condExpKernel μ (MeasurableSpace.comap k mγ)).map f ×ₖ
                (condExpKernel μ (MeasurableSpace.comap k mγ)).map g))
            a)
          ((k ⁻¹' s) ×ˢ t ×ˢ u)

Tactic:
haX

Goal state after:
Ω : 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)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
a : Ω
haX : ((condDistrib f k μ) (k a)) t = (((condExpKernel μ (MeasurableSpace.comap k mγ)).map f) a) t
⊢ ((condDistrib g k μ) (k a)) u = (((condExpKernel μ (MeasurableSpace.comap k mγ)).map g) a) u →
    ((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) (k a)) (s ×ˢ t ×ˢ u) =
      ((Kernel.id ×ₖ
            ((condExpKernel μ (MeasurableSpace.comap k mγ)).map f ×ₖ
              (condExpKernel μ (MeasurableSpace.comap k mγ)).map g))
          a)
        ((k ⁻¹' s) ×ˢ t ×ˢ u)
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: case refine_2
Ω : 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 ⋯)
⊢ ∀ᵐ (x : Ω) ∂μ.restrict {x | σ x ≤ τ x}ᶜ,
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x

Tactic:
suffices μ[stoppedValue f τ | (hσ.min hτ).measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}]
        μ[stoppedValue f τ | hσ.measurableSpace] by
      rw [ae_restrict_iff' (hσ.measurableSpace_le _ (hσ.measurableSet_le_stopping_time hτ).compl)]
      rw [Filter.EventuallyEq, ae_restrict_iff'] at this
      swap; · exact hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ)
      filter_upwards [this] with x hx hx_mem
      simp only [Set.mem_compl_iff, Set.mem_ofPred_eq, not_le] at hx_mem
      exact hx hx_mem.le

Goal state after:
case refine_2
Ω : 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 τ | ⋯.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[stoppedValue f τ | hσ.measurableSpace]
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst✝ : SFinite μ
s : Set Ω
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (μ.tilted fun x ↦ t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)

Tactic:
simp_rw [tilted_mul_apply_eq_ofReal_integral_mgf s, exp_sub]
    rwa [exp_cgf]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ = ∑ j ∈ range K, ∑ i ∈ Ico j N, ∫ (x : ℝ) in ↑i..↑(i + 1), 1 ∂ρ

Tactic:
by
        apply sum_congr rfl fun j hj => ?_
        rw [intervalIntegral.sum_integral_adjacent_intervals_Ico ((mem_range.1 hj).le.trans hKN)]
        intro k _
        exact continuous_const.intervalIntegrable _ _

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

Goal state before:
pp: case pos.mgf_le
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
h2 : ∀ᵐ (ω' : Ω) ∂⇑κ ∘ₘ ν, ∀ (t : ℝ), mgf Y (η ω') t ≤ rexp (↑cY * t ^ 2 / 2)
⊢ ∀ᵐ (ω' : Ω' × Ω) ∂ν ⊗ₘ κ, ∀ (t : ℝ), mgf Y ((prodMkLeft Ω' η) ω') t ≤ rexp (↑cY * t ^ 2 / 2)

Tactic:
rw [← Measure.snd_compProd, Measure.snd] at h2

Goal state after:
case pos.mgf_le
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
h2 : ∀ᵐ (ω' : Ω) ∂Measure.map Prod.snd (ν ⊗ₘ κ), ∀ (t : ℝ), mgf Y (η ω') t ≤ rexp (↑cY * t ^ 2 / 2)
⊢ ∀ᵐ (ω' : Ω' × Ω) ∂ν ⊗ₘ κ, ∀ (t : ℝ), mgf Y ((prodMkLeft Ω' η) ω') t ≤ rexp (↑cY * t ^ 2 / 2)
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
⊢ ((linearizeMap (α_ X Y Z).hom).comp (μ (X ⊗ Y) Z)).comp (rTensor (linearize k G Z) (μ X Y)) =
    ((μ X (Y ⊗ Z)).comp (lTensor (linearize k G X) (μ Y Z))).comp
      ↑(assoc (linearize k G X) (linearize k G Y) (linearize k G Z))

Tactic:
ext x y z : 9

Goal state after:
G : Type v
inst✝¹ : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x : X.V
y : Y.V
z : Z.V
⊢ (((TensorProduct.AlgebraTensorModule.curry
                  (TensorProduct.AlgebraTensorModule.curry
                    (((linearizeMap (α_ X Y Z).hom).comp (μ (X ⊗ Y) Z)).comp
                        (rTensor (linearize k G Z) (μ X Y))).toLinearMap) ∘ₗ
                MonoidAlgebra.lsingle x)
              1 ∘ₗ
            MonoidAlgebra.lsingle y)
          1 ∘ₗ
        MonoidAlgebra.lsingle z)
      1 =
    (((TensorProduct.AlgebraTensorModule.curry
                  (TensorProduct.AlgebraTensorModule.curry
                    (((μ X (Y ⊗ Z)).comp (lTensor (linearize k G X) (μ Y Z))).comp
                        ↑(assoc (linearize k G X) (linearize k G Y) (linearize k G Z))).toLinearMap) ∘ₗ
                MonoidAlgebra.lsingle x)
              1 ∘ₗ
            MonoidAlgebra.lsingle y)
          1 ∘ₗ
        MonoidAlgebra.lsingle z)
      1
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
Y : Ω → ℝ
h' : X =ᵐ[μ] Y
⊢ HasSubgaussianMGF Y c μ

Tactic:
by
  rw [HasSubgaussianMGF_iff_kernel] at h ⊢
  apply h.congr
  simpa

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
inst✝⁵ : CommSemiring 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
g : G
φ : ρ.Equiv σ
w : W
⊢ (φ.toLinearEquiv.conj (ρ g)) w = (σ g) w

Tactic:
have := (congr($(φ.symm.toIntertwiningMap.2 g) w)).symm

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring 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
g : G
φ : ρ.Equiv σ
w : W
this : (ρ g ∘ₗ (↑φ.symm).toLinearMap) w = ((↑φ.symm).toLinearMap ∘ₗ σ g) w
⊢ (φ.toLinearEquiv.conj (ρ g)) w = (σ g) w
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case convert_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (fun ω ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * t ^ 2 / 2
⊢ AEMeasurable X (μ.tilted fun x ↦ u * X x)

Tactic:
exact hm.mono_ac (tilted_absolutelyContinuous μ (u * X ·))

Goal state after:
Module: Mathlib.Probability.StrongLaw

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

Tactic:
exact memLp_finsetSum' _ fun j _ => (hident j).aestronglyMeasurable_fst.memLp_truncation

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

Goal state before:
pp: G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
k : Type u
inst✝ : CommRing k
φ : H →* G
S : ShortComplex (Rep k G)
exact✝ : S.Exact
mono_f : Mono S.f
epi_g : Epi S.g
⊢ Mono (S.map (resFunctor φ)).f

Tactic:
by simpa [mono_iff_injective] using! mono_f

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: case refine_2
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
f : V →ₗ[k] W
hf : ρ.IsIntertwiningMap σ f
γ : G
v : V
⊢ (σ γ ∘ₗ f ∘ₗ ρ γ⁻¹) v = f v

Tactic:
simp [hf.isIntertwining]

Goal state after:
Module: Mathlib.RepresentationTheory.Irreducible

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : Monoid G
inst✝⁶ : Field k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AddCommGroup W
inst✝² : Module k W
ρ : Representation k G V
σ : Representation k G W
f : ρ.IntertwiningMap σ
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
⊢ Bijective ⇑f ∨ f = 0

Tactic:
by
  rw [← LinearEquiv.map_eq_zero_iff (equivLinearMapAsModule ρ σ)]
  exact LinearMap.bijective_or_eq_zero (equivLinearMapAsModule ρ σ f)

Goal state after: