mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
y : 𝓨
⊢ ⨅ (_ : IsMarkovKernel (Kernel.const 𝓧 (Measure.dirac y))), avgRisk ℓ P (Kernel.const 𝓧 (Measure.dirac y)) π ≤
    ∫⁻ (θ : Θ), ℓ θ y * (P θ) Set.univ ∂π

Tactic:
simp only [iInf_pos, avgRisk_const_right', mul_comm]

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
y : 𝓨
⊢ ∫⁻ (θ : Θ), (∫⁻ (y : 𝓨), ℓ θ y ∂Measure.dirac y) * (P θ) Set.univ ∂π ≤ ∫⁻ (θ : Θ), ℓ θ y * (P θ) Set.univ ∂π
Module: Mathlib.Probability.Distributions.Beta

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ (betaMeasure α β) univ = 1

Tactic:
simp [betaMeasure, lintegral_betaPDF_eq_one hα hβ]

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)
a b : ℕ
hab : a ≤ b
x₀ : (n : ↥(Iic a)) → X ↑n
⊢ (partialTraj κ a b) x₀ ⊗ₘ κ b = Measure.map (fun x ↦ (frestrictLe b x, x (b + 1))) ((traj κ a) x₀)

Tactic:
have hf : (fun x : Π n, X n ↦ (frestrictLe b x, x (b + 1))) =
      (Prod.map id (fun x ↦ x (b + 1))) ∘ (fun x ↦ (frestrictLe b x, x)) := rfl
  rw [hf, ← Measure.map_map (by fun_prop) (by fun_prop), ← partialTraj_compProd_traj hab,
    ← Measure.compProd_map (by fun_prop), map_traj_succ_self]

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

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ (paretoMeasure t r).real (Iic x) = ∫ (x : ℝ) in Iic x, paretoPDFReal t r x

Tactic:
paretoMeasure,

Goal state after:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ (volume.withDensity (paretoPDF t r)).real (Iic x) = ∫ (x : ℝ) in Iic x, paretoPDFReal t r x
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ (paretoMeasure t r).real (Iic x) = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal

Tactic:
paretoMeasure,

Goal state after:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ (volume.withDensity (paretoPDF t r)).real (Iic x) = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal
Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm

Goal state before:
pp: p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
n : ℕ
hn : k ≤ n
⊢ p n < 1 / 2 → (1 - p n) ^ (n - k) = (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹

Tactic:
hne

Goal state after:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
n : ℕ
hn : k ≤ n
hne : p n < 1 / 2
⊢ (1 - p n) ^ (n - k) = (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
⊢ (∑' (a : α → β), q a * ∑' (a_1 : α), if b = a a_1 then p a_1 else 0) =
    ∑' (f : α → β) (a : α), if b = f a then q f * p a else 0

Tactic:
refine tsum_congr fun f => ENNReal.tsum_mul_left.symm.trans (tsum_congr fun a => ?_)

Goal state after:
α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
f : α → β
a : α
⊢ (q f * if b = f a then p a else 0) = if b = f a then q f * p a else 0
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
mX : MeasurableSpace 𝓧
A : Set Ω
X : Ω → 𝓧
h : A.indicator 1 ⟂ᵢ[P] X
s : Set Ω
hs : s ∈ {A}
t : Set 𝓧
ht : MeasurableSet t
⊢ P (s ∩ X ⁻¹' t) = P s * P (X ⁻¹' t)

Tactic:
rw [Set.mem_singleton_iff.1 hs]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
mX : MeasurableSpace 𝓧
A : Set Ω
X : Ω → 𝓧
h : A.indicator 1 ⟂ᵢ[P] X
s : Set Ω
hs : s ∈ {A}
t : Set 𝓧
ht : MeasurableSet t
⊢ P (A ∩ X ⁻¹' t) = P A * P (X ⁻¹' t)
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]
        rw [smul_inv_smul₀]
        exact (measureReal_ne_zero_iff (by finiteness)).2 hμs

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

Goal state before:
pp: case refine_1
X Y Z : SFinKer
⊢ Kernel.deterministic ⇑prodAssoc.symm ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ = Kernel.id

Tactic:
Kernel.deterministic_comp_deterministic,

Goal state after:
case refine_1
X Y Z : SFinKer
⊢ Kernel.deterministic (⇑prodAssoc.symm ∘ ⇑prodAssoc) ⋯ = Kernel.id
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_2
X Y Z : SFinKer
⊢ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc.symm ⋯ = Kernel.id

Tactic:
Kernel.deterministic_comp_deterministic,

Goal state after:
case refine_2
X Y Z : SFinKer
⊢ Kernel.deterministic (⇑prodAssoc ∘ ⇑prodAssoc.symm) ⋯ = Kernel.id
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ Kernel.deterministic (Prod.map (fun x ↦ PUnit.unit) id) ⋯ ∘ₖ Kernel.deterministic Function.diag ⋯ =
    (Kernel.deterministic id ⋯).map fun x ↦ (PUnit.unit, x)

Tactic:
Kernel.deterministic_comp_deterministic,

Goal state after:
X : SFinKer
⊢ Kernel.deterministic (Prod.map (fun x ↦ PUnit.unit) id ∘ Function.diag) ⋯ =
    (Kernel.deterministic id ⋯).map fun x ↦ (PUnit.unit, x)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ Kernel.deterministic (Prod.map id fun x ↦ PUnit.unit) ⋯ ∘ₖ Kernel.deterministic Function.diag ⋯ =
    (Kernel.deterministic id ⋯).map fun x ↦ (x, PUnit.unit)

Tactic:
Kernel.deterministic_comp_deterministic,

Goal state after:
X : SFinKer
⊢ Kernel.deterministic ((Prod.map id fun x ↦ PUnit.unit) ∘ Function.diag) ⋯ =
    (Kernel.deterministic id ⋯).map fun x ↦ (x, PUnit.unit)
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
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
⊢ ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ) ∘ₖ (Kernel.id ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ

Tactic:
congr 2

Goal state after:
case e_f
Ω : 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
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
⊢ Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ =
    Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ) ∘ₖ (Kernel.id ×ₖ condDistrib g k μ)
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
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
h1_symm : Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (⇑e.symm) (Measure.map (fun x ↦ ((k x, g x), f x)) μ)
⊢ ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.deterministic ⇑e ⋯ ∘ₖ (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ))) ∘ₘ Measure.map k μ

Tactic:
congr 2

Goal state after:
case e_f
Ω : 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
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
h1_symm : Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (⇑e.symm) (Measure.map (fun x ↦ ((k x, g x), f x)) μ)
⊢ Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ =
    Kernel.deterministic ⇑e ⋯ ∘ₖ (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ))
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:
congr 2

Goal state after:
case e_f.e_a
α : 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} = p ↑x
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
inst✝ : Fintype α
p : PMF α
f : α → E
x : α
⊢ (p.toMeasure {x}).toReal • f x = (p x).toReal • f x

Tactic:
congr 2

Goal state after:
case e_f.e_a
α : 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 {x} = p x
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
⊢ ↑M * edist s t ^ q = 0

Tactic:
simp [h, hX.q_pos]

Goal state after:
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:
exact σ.toSubmodule.add_mem' hx hy

Goal state after:
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 (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • m ∈ σ.toSubmodule.carrier
hy : y • m ∈ σ.toSubmodule.carrier
⊢ x • m + y • m ∈ σ.toSubmodule.carrier

Tactic:
exact σ.toSubmodule.add_mem' hx hy

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : ConditionallyCompleteLinearOrderBot ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁴ : Zero E
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable 𝓕 p
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))
n : ℕ
⊢ p fun i ↦ {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator (stoppedProcess X (fun ω ↦ ⨅ j, ⨅ (_ : j ≥ n), τ j ω) i)

Tactic:
← stoppedProcess_stoppedProcess_of_le_right
    (τ := fun ω ↦ τ n ω) (fun _ ↦ (iInf_le _ n).trans <| iInf_le _ le_rfl),

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : ConditionallyCompleteLinearOrderBot ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁴ : Zero E
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable 𝓕 p
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))
n : ℕ
⊢ p fun i ↦
    {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator
      (stoppedProcess (stoppedProcess X fun ω ↦ τ n ω) (fun x ↦ ⨅ j, ⨅ (_ : j ≥ n), τ j x) i)
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : 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)}
⊢ False

Tactic:
suffices (1 / 2) ^ n ≤ P (⋂ k : ℕ, {ω | σ n k ω < min (τ n ω) (T n)}) by
    refine (by simp : ¬ (1 / 2 : ℝ≥0∞) ^ n ≤ 0) <| this.trans <| nonpos_iff_eq_zero.2 ?_
    rw [measure_eq_zero_iff_ae_notMem]
    filter_upwards [(hσ n).tendsto_top] with ω hTop hmem
    simp_rw [WithTop.tendsto_nhds_top_iff, eventually_atTop] at hTop
    simp only [Set.mem_iInter, Set.mem_ofPred_eq] at hmem
    obtain ⟨N, hN⟩ := hTop (T n)
    specialize hN N le_rfl
    specialize hmem N
    grind

Goal state after:
ι : 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)}
⊢ (1 / 2) ^ n ≤ P (⋂ k, {ω | σ n k ω < min (τ n ω) ↑(T n)})
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
f : X ⟶ Y
x✝ : (X ⊗ Z).V
⊢ (((rTensor (linearize k G Z) (linearizeMap f)).comp (δ X Z)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1 =
    (((δ Y Z).comp (linearizeMap (f ▷ Z))).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1

Tactic:
simp [δ_apply_single _]

Goal state after:
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
f : X ⟶ Y
x✝ : (Z ⊗ X).V
⊢ (((lTensor (linearize k G Z) (linearizeMap f)).comp (δ Z X)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1 =
    (((δ Z Y).comp (linearizeMap (Z ◁ f))).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1

Tactic:
simp [δ_apply_single _]

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
k : Type u
inst✝ : CommSemiring k
X : Action (Type u) G
x✝ : X.V
⊢ ((↑(rid k (linearize k G X)).symm).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1 =
    ((((lTensor (linearize k G X) (η k G)).comp (δ X (𝟙_ (Action (Type u) G)))).comp
            (linearizeMap (ρ_ X).inv)).toLinearMap ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1

Tactic:
simp [δ_apply_single _]

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x✝ a✝ : (X ⊗ Y).V
⊢ ((((μ X Y).comp (δ X Y)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝ =
    (((IntertwiningMap.id (linearize k G (X ⊗ Y))).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝

Tactic:
simp [δ_apply_single _]

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x✝¹ : X.V
x✝ : Y.V
⊢ ((TensorProduct.AlgebraTensorModule.curry ((δ X Y).comp (μ X Y)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝¹) 1 ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((TensorProduct.AlgebraTensorModule.curry
              (IntertwiningMap.id ((linearize k G X).tprod (linearize k G Y))).toLinearMap ∘ₗ
            MonoidAlgebra.lsingle x✝¹)
          1 ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1

Tactic:
simp [δ_apply_single _]

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
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
⊢ HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν

Tactic:
by
  by_cases hκ : IsSFiniteKernel κ
  swap; · simp [hκ]
  refine .of_rat (integrable_exp_add_compProd hX hY) fun q ↦ ?_
  filter_upwards [hX.mgf_le, hX.ae_integrable_exp_mul q, Measure.ae_ae_of_ae_compProd hY.mgf_le,
    Measure.ae_integrable_of_integrable_comp <| integrable_exp_add_compProd hX hY q]
    with ω' hX_mgf hX_int hY_mgf h_int_mul
  calc mgf (fun p ↦ X p.1 + Y p.2) ((κ ⊗ₖ η) ω') q
  _ = ∫ x, exp (q * X x) * ∫ y, exp (q * Y y) ∂(η (ω', x)) ∂(κ ω') := by
    simp_rw [mgf, mul_add, exp_add] at h_int_mul ⊢
    simp_rw [integral_compProd h_int_mul, integral_const_mul]
  _ ≤ ∫ x, exp (q * X x) * exp (cY * q ^ 2 / 2) ∂(κ ω') := by
    refine integral_mono_of_nonneg ?_ (hX_int.mul_const _) ?_
    · exact ae_of_all _ fun ω ↦ mul_nonneg (by positivity)
        (integral_nonneg (fun _ ↦ by positivity))
    · filter_upwards [all_ae_of hY_mgf q] with ω hY_mgf
      gcongr
      exact hY_mgf
  _ ≤ exp (↑(c + cY) * q ^ 2 / 2) := by
    rw [integral_mul_const, NNReal.coe_add, add_mul, add_div, exp_add]
    gcongr
    exact hX_mgf q

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
h_eq :
  (⇑(condExpKernel μ m) ∘ₘ μ.trim hm)[fun ω ↦ rexp (t * X ω) | m] =ᵐ[(⇑(condExpKernel μ m) ∘ₘ μ.trim hm).trim hm]
    fun ω ↦ ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel (⇑(condExpKernel μ m) ∘ₘ μ.trim hm) m) ω
⊢ ∀ᵐ (ω' : Ω) ∂μ.trim hm, μ[fun ω ↦ rexp (t * X ω) | m] ω' ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
condExpKernel_comp_trim

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
h_eq : μ[fun ω ↦ rexp (t * X ω) | m] =ᵐ[μ.trim hm] fun ω ↦ ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω
⊢ ∀ᵐ (ω' : Ω) ∂μ.trim hm, μ[fun ω ↦ rexp (t * X ω) | m] ω' ≤ rexp (↑c * t ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
⊢ HasSubgaussianMGF (fun ω ↦ X ω - Y ω) (cX + cY) μ

Tactic:
sub_eq_add_neg

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
⊢ HasSubgaussianMGF (fun ω ↦ X ω + -Y ω) (cX + cY) μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case refine_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) cX μ
hY : HasSubgaussianMGF (fun ω ↦ Y ω - ∫ (x : Ω), Y x ∂μ) cY μ
hindep : X ⟂ᵢ[μ] Y
h_le : ∫ (x : Ω), Y x ∂μ ≤ ∫ (x : Ω), X x ∂μ
⊢ rexp (-(∫ (x : Ω), X x ∂μ - ∫ (x : Ω), Y x ∂μ) ^ 2 / (2 * ↑(cX + cY))) =
    rexp (-(∫ (x : Ω), Y x ∂μ - ∫ (x : Ω), X x ∂μ) ^ 2 / (2 * (↑cX + ↑cY)))

Tactic:
congr 2

Goal state after:
case refine_3.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) cX μ
hY : HasSubgaussianMGF (fun ω ↦ Y ω - ∫ (x : Ω), Y x ∂μ) cY μ
hindep : X ⟂ᵢ[μ] Y
h_le : ∫ (x : Ω), Y x ∂μ ≤ ∫ (x : Ω), X x ∂μ
⊢ -(∫ (x : Ω), X x ∂μ - ∫ (x : Ω), Y x ∂μ) ^ 2 = -(∫ (x : Ω), Y x ∂μ - ∫ (x : Ω), X x ∂μ) ^ 2
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring A
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module A V
ρ : Representation A G V
g : G
hg : g ∈ Submonoid.center G
g' : G
v : V
⊢ (ρ g) ((ρ g') v) = (ρ g') ((ρ g) v)

Tactic:
rw [Submonoid.mem_center_iff] at hg

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring A
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module A V
ρ : Representation A G V
g : G
hg : ∀ (g_1 : G), g_1 * g = g * g_1
g' : G
v : V
⊢ (ρ g) ((ρ g') v) = (ρ g') ((ρ g) v)