mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (if 0 ≤ x then 1 - rexp (-(r * x)) else 0)

Tactic:
split_ifs with h

Goal state after:
case pos
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))

case neg
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal 0
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
⊢ 1 < ∑' (a : α), p a

Tactic:
have : 0 < ∑' b, ite (b = a) 0 (p b) := by
    rw [pos_iff_ne_zero, ENNReal.summable.tsum_ne_zero_iff]
    exact ⟨a', ite_ne_left_iff.2 ⟨ha, Ne.symm <| (p.mem_support_iff a').2 ha'⟩⟩

Goal state after:
α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : 0 < ∑' (b : α), if b = a then 0 else p b
⊢ 1 < ∑' (a : α), p a
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
p : PMF α
a b : α
⊢ (if b = a then p a else 0) ≤ p b

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
p : PMF α
a b : α
h : b = a
⊢ p a ≤ p b

case neg
α : Type u_1
p : PMF α
a b : α
h : ¬b = a
⊢ 0 ≤ p b
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ↑unitInterval
⊢ IsProbabilityMeasure
    (if p ≠ 0 then Measure.sum fun n ↦ ENNReal.ofReal ((1 - ↑p) ^ n * ↑p) • Measure.dirac n else Measure.dirac 0)

Tactic:
split_ifs with h

Goal state after:
case pos
p : ↑unitInterval
h : p ≠ 0
⊢ IsProbabilityMeasure (Measure.sum fun n ↦ ENNReal.ofReal ((1 - ↑p) ^ n * ↑p) • Measure.dirac n)

case neg
p : ↑unitInterval
h : ¬p ≠ 0
⊢ IsProbabilityMeasure (Measure.dirac 0)
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
⊢ 0 ≤ if t ≤ x then r * t ^ r * x ^ (-(r + 1)) else 0

Tactic:
split_ifs with h

Goal state after:
case pos
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ x
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))

case neg
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : ¬t ≤ x
⊢ 0 ≤ 0
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
⊢ 0 ≤ if 0 ≤ x then 1 - rexp (-(r * x)) else 0

Tactic:
split_ifs with h

Goal state after:
case pos
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ 1 - rexp (-(r * x))

case neg
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ 0 ≤ 0
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ ((∫⁻ (x : ℝ) in Ici t, paretoPDF t r x) + 0).toReal = 1

Tactic:
rightSide,

Goal state after:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ ((∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))) + 0).toReal = 1
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
a : α
⊢ (p a * ∑' (i : β), if h : p a = 0 then 0 else (f a h) i) = p a

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
a : α
h : p a = 0
⊢ p a * ∑' (i : β), 0 = p a

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
a : α
h : ¬p a = 0
⊢ p a * ∑' (i : β), (f a h) i = p a
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : Nonempty α
s : Set α
inst✝ : Fintype ↑s
⊢ (uniformOfFintype α).toOuterMeasure s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)

Tactic:
rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply, Fintype.card_subtype,
    Finset.card_univ]

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

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun ω ↦ ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

Tactic:
nontriviality Ω
  simp_rw [condExpKernel_apply_eq_condDistrib]
  exact AEStronglyMeasurable.integral_condDistrib
    (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
    hf.comp_snd_map_prod_id

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

Goal state before:
pp: case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h✝ : Nonempty Ω
h :
  (fun a ↦ ((condDistrib id id μ) (id a)).real s) =ᵐ[μ]
    μ[(id ⁻¹' s).indicator fun ω ↦ 1 | MeasurableSpace.comap id (m ⊓ mΩ)]
⊢ (fun ω ↦ ((condExpKernel μ m) ω).real s) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m ⊓ mΩ]

Tactic:
simp only [id_eq, MeasurableSpace.comap_id, preimage_id_eq] at h

Goal state after:
case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h✝ : Nonempty Ω
h : (fun a ↦ ((condDistrib id id μ) a).real s) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m ⊓ mΩ]
⊢ (fun ω ↦ ((condExpKernel μ m) ω).real s) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m ⊓ mΩ]
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f μ
⊢ μ[f | m ⊓ mΩ] =ᵐ[μ] fun ω ↦ ∫ (y : Ω), f y ∂(condExpKernel μ m) ω

Tactic:
by
  rcases isEmpty_or_nonempty Ω with h | h
  · have : μ = 0 := Measure.eq_zero_of_isEmpty μ
    simpa [this] using! trivial
  have hX : @Measurable Ω Ω mΩ (m ⊓ mΩ) id := measurable_id.mono le_rfl (inf_le_right : m ⊓ mΩ ≤ mΩ)
  simp_rw [condExpKernel_apply_eq_condDistrib]
  have h := condExp_ae_eq_integral_condDistrib_id hX hf_int
  simpa only [MeasurableSpace.comap_id, id_eq] using! h

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

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
⊢ μ[f | m] =ᵐ[μ.trim hm] fun ω ↦ ∫ (y : Ω), f y ∂(condExpKernel μ m) ω

Tactic:
refine (condExp_congr_ae_trim hm hf_int.1.ae_eq_mk).trans ?_

Goal state after:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
⊢ μ[AEStronglyMeasurable.mk f ⋯ | m] =ᵐ[μ.trim hm] fun ω ↦ ∫ (y : Ω), f y ∂(condExpKernel μ m) ω
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s μ
t : Set Ω
ht_tail : MeasurableSet t
⊢ μ t = 0 ∨ μ t = 1

Tactic:
by
  simpa only [ae_dirac_eq, Filter.eventually_pure]
    using! Kernel.measure_zero_or_one_of_measurableSet_limsup_atBot h_le h_indep ht_tail

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

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

Tactic:
rcases isEmpty_or_nonempty α with _ | hα

Goal state after:
case inl
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
h✝ : IsEmpty α
⊢ (κ ∘ₖ η).Invariant μ

case inr
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
hα : Nonempty α
⊢ (κ ∘ₖ η).Invariant μ
Module: Mathlib.Probability.Kernel.Irreducible

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
c : ℝ≥0∞
φ : Measure α
κ : Kernel α α
hκ : IsIrreducible φ κ
s : Set α
hs : MeasurableSet s
hsp : (c • φ) s > 0
⊢ ∀ (a : α), ∃ n, ((κ ^ n) a) s > 0

Tactic:
simpa using hκ.irreducible hs <| by simp_all

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
f : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hA : MeasurableSet A
hB : MeasurableSet B
x₀ : X
⊢ ∫⁻ (x : X) in A ∩ B, f x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X) in A, f x ∂π x₀

Tactic:
rw [← lintegral_indicator hA, ← hπ.setLIntegral_eq_indicator_mul_lintegral h𝓑𝓧 _ hB,
    setLIntegral_indicator] <;> measurability

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

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
ω : Ω
⊢ ‖if ω ∈ X ⁻¹' s then 1 ω else 0‖ ≤ 1

Tactic:
split_ifs with h

Goal state after:
case pos
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
ω : Ω
h : ω ∈ X ⁻¹' s
⊢ ‖1 ω‖ ≤ 1

case neg
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
ω : Ω
h : ω ∉ X ⁻¹' s
⊢ ‖0‖ ≤ 1
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ CondIndepFun m' hm' f g μ ↔
    Measure.map (fun ω ↦ (ω, f ω, g ω)) μ =
      ⇑(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) ∘ₘ μ.trim hm'

Tactic:
rw [condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hf hg]
  congr!
  · rw [Measure.compProd_map (by fun_prop), compProd_trim_condExpKernel]
    exact Measure.map_map (by fun_prop) ((measurable_id.mono le_rfl hm').prodMk measurable_id)
  · rw [Measure.compProd_eq_comp_prod]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
⊢ (μ.tilted fun x ↦ t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)

Tactic:
rw [tilted_apply_eq_ofReal_integral' _ hs, mgf]

Goal state after:
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 μ)) ∘ₘ Measure.map k μ ⊗ₘ condDistrib g k μ

Tactic:
rw [Measure.compProd_eq_comp_prod, Measure.comp_assoc]

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
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 μ
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: 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 ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ))

Tactic:
rw [Kernel.deterministic_comp_eq_map, Kernel.prodAssoc_symm_prod]

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

Goal state before:
pp: case hg
Ω : 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) ω
hg : ∀ {c : ℝ}, Integrable (fun ω ↦ c * ∏ s, (g s) (X s ω)) P
⊢ Integrable (fun a ↦ f 0 * ∏ x, (g x) (X x a)) P

Tactic:
exact hg

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
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᵐ[⇑κ ∘ₘ ν] Y
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * Y ω)) (⇑κ ∘ₘ ν)

Tactic:
by
    refine (integrable_congr ?_).mpr (h.integrable_exp_mul t)
    filter_upwards [h'] with ω hω using by rw [hω]

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: case zero
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
σ : Subrepresentation ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
⊢ 0 • v ∈ σ.toSubmodule.carrier

Tactic:
simp [zero_smul]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
f : α → ℝ
A : ℝ
x : α
⊢ |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |A|

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : f x ∈ Set.Ioc (-A) A
⊢ |f x| ≤ |A|

case neg
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : f x ∉ Set.Ioc (-A) A
⊢ |0| ≤ |A|
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
x : ℝ
hx : x ∈ Set.Ioc ↑k ↑(k + 1)
⊢ 1 * (2 * x) = 2 * x

Tactic:
by rw [one_mul]

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
U : Type u_5
inst✝⁷ : Semiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f : ρ.IntertwiningMap σ
n : ℕ
⊢ ⇑(n • f) = n • ⇑f

Tactic:
rw [coe_nsmul]

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
U : Type u_5
inst✝⁷ : Semiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
φ✝ φ : ρ.Equiv σ
g : G
⊢ ↑φ.toLinearEquiv.symm ∘ₗ σ g = ρ g ∘ₗ ↑φ.toLinearEquiv.symm

Tactic:
rw [← cancel_left φ.toLinearEquiv.injective, ← comp_assoc, ← comp_assoc, φ.1.2 g, φ.comp_symm,
      comp_assoc, φ.comp_symm, id_comp, comp_id]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n
n : ℕ
hn : X n ω ∉ Set.Ioi ↑n
npos : n ∈ Set.Ioi 0
⊢ 0 = (if -↑n < X n ω ∧ X n ω ≤ ↑n then X n ω else 0) - X n ω

Tactic:
split_ifs with h

Goal state after:
case pos
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n
n : ℕ
hn : X n ω ∉ Set.Ioi ↑n
npos : n ∈ Set.Ioi 0
h : -↑n < X n ω ∧ X n ω ≤ ↑n
⊢ 0 = X n ω - X n ω

case neg
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n
n : ℕ
hn : X n ω ∉ Set.Ioi ↑n
npos : n ∈ Set.Ioi 0
h : ¬(-↑n < X n ω ∧ X n ω ≤ ↑n)
⊢ 0 = 0 - X n ω
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
f : res φ (leftRegular k H) ⟶ A
g : G
h : H
⊢ (Hom.hom f) (MonoidAlgebra.single (φ g * h) 1) = (A.ρ g) ((Hom.hom f) (MonoidAlgebra.single h 1))

Tactic:
have := by simpa using (hom_comm_apply f g (.single h 1)).symm

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
f : res φ (leftRegular k H) ⟶ A
g : G
h : H
this : (A.ρ g) ((Hom.hom f) (MonoidAlgebra.single h 1)) = (Hom.hom f) (MonoidAlgebra.single (φ g * h) 1)
⊢ (Hom.hom f) (MonoidAlgebra.single (φ g * h) 1) = (A.ρ g) ((Hom.hom f) (MonoidAlgebra.single h 1))
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↑(A.toCoinvariantsKer S)
⊢ (Hom.hom
          (ofHom { toLinearMap := (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype, isIntertwining' := ⋯ } ≫
            A.toCoinvariantsMkQ S)).toLinearMap
      x =
    (Hom.hom 0).toLinearMap x

Tactic:
exact (Submodule.Quotient.mk_eq_zero _).2 x.2

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k✝ : Type u_1
inst✝¹³ : Field k✝
G✝ : Type u_2
inst✝¹² : Finite G✝
inst✝¹¹ : NeZero ↑(Nat.card G✝)
inst✝¹⁰ : Group G✝
V✝ : Type u_3
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝[G✝] V✝
W : Type u_4
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝[G✝] W
G : Type u_5
k : Type u_6
V : Type u_7
inst✝⁵ : Group G
inst✝⁴ : Field k
inst✝³ : Finite G
inst✝² : NeZero ↑(Nat.card G)
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ ρ.IsSemisimpleRepresentation

Tactic:
rw [isSemisimpleRepresentation_iff_isSemisimpleModule_asModule]

Goal state after:
k✝ : Type u_1
inst✝¹³ : Field k✝
G✝ : Type u_2
inst✝¹² : Finite G✝
inst✝¹¹ : NeZero ↑(Nat.card G✝)
inst✝¹⁰ : Group G✝
V✝ : Type u_3
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝[G✝] V✝
W : Type u_4
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝[G✝] W
G : Type u_5
k : Type u_6
V : Type u_7
inst✝⁵ : Group G
inst✝⁴ : Field k
inst✝³ : Finite G
inst✝² : NeZero ↑(Nat.card G)
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ IsSemisimpleModule k[G] ρ.asModule
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝⁷ : Semiring k
inst✝⁶ : Monoid G
X✝ Y✝ : Type w
inst✝⁵ : AddCommGroup X✝
inst✝⁴ : AddCommGroup Y✝
inst✝³ : Module k X✝
inst✝² : Module k Y✝
ρ : Representation k G X✝
σ : Representation k G Y✝
A B C : Rep k G
Z : Type w
inst✝¹ : AddCommGroup Z
inst✝ : Module k Z
τ : Representation k G Z
X Y : Rep k G
f : X ⟶ Y
x✝ : IsIso ((forget (Rep k G)).map f)
i : (forget (Rep k G)).obj X ≅ (forget (Rep k G)).obj Y := asIso ((forget (Rep k G)).map f)
⊢ IsIso f

Tactic:
let e : X.ρ.Equiv Y.ρ := { f.hom, i.toEquiv with }

Goal state after:
k : Type u
G : Type v
inst✝⁷ : Semiring k
inst✝⁶ : Monoid G
X✝ Y✝ : Type w
inst✝⁵ : AddCommGroup X✝
inst✝⁴ : AddCommGroup Y✝
inst✝³ : Module k X✝
inst✝² : Module k Y✝
ρ : Representation k G X✝
σ : Representation k G Y✝
A B C : Rep k G
Z : Type w
inst✝¹ : AddCommGroup Z
inst✝ : Module k Z
τ : Representation k G Z
X Y : Rep k G
f : X ⟶ Y
x✝ : IsIso ((forget (Rep k G)).map f)
i : (forget (Rep k G)).obj X ≅ (forget (Rep k G)).obj Y := asIso ((forget (Rep k G)).map f)
e : X.ρ.Equiv Y.ρ :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toIntertwiningMap := __src, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯ }
⊢ IsIso f