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

Goal state before:
pp: ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
⊢ (infinitePi fun p ↦ μ p.fst p.snd) = map (⇑(piCurry X).symm) (infinitePi fun i ↦ infinitePi fun j ↦ μ i j)

Tactic:
infinitePi_map_piCurry_symm

Goal state after:
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
⊢ (infinitePi fun p ↦ μ p.fst p.snd) = infinitePi fun p ↦ μ p.fst p.snd
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
this :
  ⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm) ∘ ⇑(MeasurableEquiv.curry ι κ X).symm =
    ⇑(piCurry fun x x_1 ↦ X).symm
⊢ map (⇑(piCurry fun x x_1 ↦ X).symm) (infinitePi fun i ↦ infinitePi fun j ↦ μ i j) =
    map (⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm)) (infinitePi fun p ↦ μ p.1 p.2)

Tactic:
infinitePi_map_piCurry_symm

Goal state after:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
this :
  ⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm) ∘ ⇑(MeasurableEquiv.curry ι κ X).symm =
    ⇑(piCurry fun x x_1 ↦ X).symm
⊢ (infinitePi fun p ↦ μ p.fst p.snd) =
    map (⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm)) (infinitePi fun p ↦ μ p.1 p.2)
Module: Mathlib.Probability.Distributions.Cauchy

Goal state before:
pp: x₀ x✝ : ℝ
⊢ cauchyPDF x₀ 0 x✝ = 0 x✝

Tactic:
simp [cauchyPDF]

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p q : PMF α
h : p.toMeasure = q.toMeasure
⊢ p = q

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p q : PMF α
h : p.toMeasure = q.toMeasure
x : α
⊢ p x = q x
Module: Mathlib.Probability.Distributions.Exponential

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

Tactic:
case pos =>
    rw [lintegral_Iic_eq_lintegral_Iio_add_Icc _ h, lintegral_exponentialPDF_of_nonpos (le_refl 0),
      zero_add]
    simp only [exponentialPDF_eq]
    rw [setLIntegral_congr_fun measurableSet_Icc (g := fun x ↦ ENNReal.ofReal (r * rexp (-(r * x))))
      (by intro a ha; simp [ha.1])]
    rw [← ENNReal.toReal_eq_toReal_iff' _ ENNReal.ofReal_ne_top,
        ← integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall fun _ ↦ le_of_lt
        (mul_pos hr (exp_pos _)))]
    · have : ∫ a in uIoc 0 x, r * rexp (-(r * a)) = ∫ a in 0..x, r * rexp (-(r * a)) := by
        rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_eq_mul, if_pos h, one_mul]
      rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this]
      rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _]
      · rw [ENNReal.toReal_ofReal_eq_iff.2
          (sub_nonneg.2 (Real.exp_le_one_iff.2 <| by nlinarith))]
        norm_num; ring
      · simp only [intervalIntegrable_iff, uIoc_of_le h]
        exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
      · have : Continuous (fun a ↦ rexp (-(r * a))) := by
          simp only [← neg_mul]; exact (continuous_const_mul (-r)).rexp
        exact Continuous.continuousOn (Continuous.comp' (continuous_const_mul (-1)) this)
      · simp only [neg_mul, one_mul]
        exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp
    · refine Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)
      rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc]
      exact exp_neg_integrableOn_Ioc hr
    · refine ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)
      rw [integrableOn_Icc_iff_integrableOn_Ioc]
      exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: case false.mp
p : ℝ≥0
h : p ≤ 1
h' : 1 - ↑p = 0
⊢ p = 1

Tactic:
simp only [tsub_eq_zero_iff_le, one_le_coe_iff] at h'

Goal state after:
case false.mp
p : ℝ≥0
h : p ≤ 1
h' : 1 ≤ p
⊢ p = 1
Module: Mathlib.Probability.Distributions.TwoValued

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω},
    m ≤ m₀ →
      ∀ {μ : Measure Ω} [IsFiniteMeasure μ],
        AEMeasurable X μ →
          (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
Y : Ω → ℝ
hYmeas : Measurable Y
hXY : X =ᵐ[μ] Y
⊢ Var[Y; μ | m] =ᵐ[μ] μ[Y | m] * μ[1 - Y | m]

Tactic:
refine this hm hYmeas.aemeasurable ?_ hYmeas

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω},
    m ≤ m₀ →
      ∀ {μ : Measure Ω} [IsFiniteMeasure μ],
        AEMeasurable X μ →
          (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
Y : Ω → ℝ
hYmeas : Measurable Y
hXY : X =ᵐ[μ] Y
⊢ ∀ᵐ (ω : Ω) ∂μ, Y ω = 0 ∨ Y ω = 1
Module: Mathlib.Probability.IdentDistribIndep

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝ : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun X μ
hY_ind : iIndepFun Y ν
⊢ Measure.map (fun ω x ↦ X x ω) μ = Measure.map (fun ω x ↦ Y x ω) ν

Tactic:
have : IsProbabilityMeasure μ := hX_ind.isProbabilityMeasure
    have : IsProbabilityMeasure ν := hY_ind.isProbabilityMeasure
    rw [(iIndepFun_iff_map_fun_eq_infinitePi_map₀' (fun i ↦ (h i).aemeasurable_fst)).mp hX_ind,
      (iIndepFun_iff_map_fun_eq_infinitePi_map₀' (fun i ↦ (h i).aemeasurable_snd)).mp hY_ind]
    congr with i
    rw [(h i).map_eq]

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:
rw [Kernel.deterministic_comp_deterministic, Kernel.id]

Goal state after:
case refine_1
X Y Z : SFinKer
⊢ Kernel.deterministic (⇑prodAssoc.symm ∘ ⇑prodAssoc) ⋯ = Kernel.deterministic 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:
rw [Kernel.deterministic_comp_deterministic, Kernel.id]

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

Goal state before:
pp: case neg.refine_1
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 : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hξ : f a ξ ≤ x
hx : ¬x = 1
g : ↑I → ℝ := fun y ↦ (κ a).real (Icc 0 y)
nebot : (𝓝[>] x).NeBot := nhdsGT_neBot_of_exists_gt (Exists.intro 1 (lt_of_le_of_ne x.property.right hx))
h : StieltjesFunction ℝ := cdf (Measure.map Subtype.val (κ a))
h_continuousWithinAt : ContinuousWithinAt (↑h) (Ioi ↑x) ↑x
⊢ Tendsto (fun y ↦ (κ a).real (Icc 0 y)) (𝓝[>] x) (𝓝 ((κ a).real (Icc 0 x)))

Tactic:
← unitInterval.cdf_eq_real (κ a)

Goal state after:
case neg.refine_1
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 : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hξ : f a ξ ≤ x
hx : ¬x = 1
g : ↑I → ℝ := fun y ↦ (κ a).real (Icc 0 y)
nebot : (𝓝[>] x).NeBot := nhdsGT_neBot_of_exists_gt (Exists.intro 1 (lt_of_le_of_ne x.property.right hx))
h : StieltjesFunction ℝ := cdf (Measure.map Subtype.val (κ a))
h_continuousWithinAt : ContinuousWithinAt (↑h) (Ioi ↑x) ↑x
⊢ Tendsto (fun y ↦ ↑(cdf (Measure.map Subtype.val (κ a))) ↑y) (𝓝[>] x) (𝓝 (↑(cdf (Measure.map Subtype.val (κ a))) ↑x))
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: case e_6.mpr
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 : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hξ : ↑ξ ≤ (κ a).real (Icc 0 x)
⊢ ∀ b ∈ {x | (κ a).real (Icc 0 x) < ↑ξ}, b ≤ x

Tactic:
intro c hc

Goal state after:
case e_6.mpr
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 : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hξ : ↑ξ ≤ (κ a).real (Icc 0 x)
c : ↑I
hc : c ∈ {x | (κ a).real (Icc 0 x) < ↑ξ}
⊢ c ≤ x
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)) μ
⊢ Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)

Tactic:
rw [Measure.map_map (by fun_prop) (by fun_prop)]

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
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)) μ
⊢ Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e ∘ fun a ↦ (k a, g a, f a)) μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case pos
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
hp : p = 0
⊢ eLpNorm (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω') < ∞

Tactic:
simp [hp]

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

Goal state before:
pp: case neg.hp_ne_zero
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ ↑p ≠ 0

Tactic:
simp [hp]

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
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)) μ)
h2 :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
h2_symm :
  ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ =
    Measure.map (⇑e.symm) (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ)
h :
  Measure.map (fun ω ↦ (k ω, g ω, f ω)) μ = ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ
⊢ Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ) =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)

Tactic:
by rw [h]

Goal state after:
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 ρ
⊢ ∀ (g : G) ⦃v : W⦄, v ∈ ρ₁.toSubmodule ⊓ ρ₂.toSubmodule → (ρ g) v ∈ ρ₁.toSubmodule ⊓ ρ₂.toSubmodule

Tactic:
by
      simp only [Submodule.mem_inf, and_imp]
      rintro g x hx₁ hx₂
      exact ⟨ρ₁.apply_mem_toSubmodule g hx₁, ρ₂.apply_mem_toSubmodule g hx₂⟩

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
⊢ truncation f A = (Set.Ioc 0 A).indicator id ∘ f

Tactic:
ext x

Goal state after:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x
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 ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
B : ∀ (a b : ℝ), ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
⊢ ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)

Tactic:
calc
    ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc (j : ℝ) N} =
        ∑ j ∈ range K, ENNReal.ofReal (∫ _ in Set.Ioc (j : ℝ) N, (1 : ℝ) ∂ρ) := by simp_rw [B]
    _ = ENNReal.ofReal (∑ j ∈ range K, ∫ _ in Set.Ioc (j : ℝ) N, (1 : ℝ) ∂ρ) := by
      simp [ENNReal.ofReal_sum_of_nonneg]
    _ = ENNReal.ofReal (∑ j ∈ range K, ∫ _ in (j : ℝ)..N, (1 : ℝ) ∂ρ) := by
      congr 1
      refine sum_congr rfl fun j hj => ?_
      rw [intervalIntegral.integral_of_le (Nat.cast_le.2 ((mem_range.1 hj).le.trans hKN))]
    _ ≤ ENNReal.ofReal (𝔼[X] + 1) := ENNReal.ofReal_le_ofReal A

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
⊢ ↑(rid k (linearize k G X)) =
    ((linearizeMap (ρ_ X).hom).comp (μ X (𝟙_ (Action (Type w) G)))).comp (lTensor (linearize k G X) (ε k G))

Tactic:
ext x

Goal state after:
G : Type v
inst✝¹ : Monoid G
X : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x a✝ : X.V
⊢ (((TensorProduct.AlgebraTensorModule.curry (↑(rid k (linearize k G X))).toLinearMap ∘ₗ MonoidAlgebra.lsingle x) 1)
          1).coeff
      a✝ =
    (((TensorProduct.AlgebraTensorModule.curry
                (((linearizeMap (ρ_ X).hom).comp (μ X (𝟙_ (Action (Type w) G)))).comp
                    (lTensor (linearize k G X) (ε k G))).toLinearMap ∘ₗ
              MonoidAlgebra.lsingle x)
            1)
          1).coeff
      a✝
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
X : Type w
g : G
x : X
⊢ MonoidAlgebra.single ((ConcreteCategory.hom ((Action.trivial G X).ρ g)) x) 1 = MonoidAlgebra.single x 1

Tactic:
simp only [Action.trivial_ρ]

Goal state after:
k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
X : Type w
g : G
x : X
⊢ MonoidAlgebra.single ((ConcreteCategory.hom (1 g)) x) 1 = MonoidAlgebra.single x 1
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * X ω)) (μ.trim hm)

Tactic:
refine (hX.integrable_exp_mul t).trim hm ?_
    exact Measurable.stronglyMeasurable <| by fun_prop

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : HasSubgaussianMGF X c μ
⊢ integrableExpSet X μ = Set.univ

Tactic:
by
  ext t
  simpa using! hX.integrable_exp_mul t

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✝⁵ : Semiring 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
f g : ρ.IntertwiningMap σ
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
ext x

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring 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
f g : ρ.IntertwiningMap σ
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
x : V
⊢ f.toLinearMap x = g.toLinearMap x
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
X Y : FDRep R G
f : X ⟶ Y
g : G
⊢ ModuleCat.Hom.hom ((forget₂ (FGModuleCat R) (ModuleCat R)).map f.hom) ∘ₗ
      ((((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).V.endRingEquiv.toMonoidHom.comp
          (((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).ρ)
        g =
    ((((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj Y).V.endRingEquiv.toMonoidHom.comp
          (((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj Y).ρ)
        g ∘ₗ
      ModuleCat.Hom.hom ((forget₂ (FGModuleCat R) (ModuleCat R)).map f.hom)

Tactic:
ext x

Goal state after:
R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
X Y : FDRep R G
f : X ⟶ Y
g : G
x : ↑(((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).V
⊢ (ModuleCat.Hom.hom ((forget₂ (FGModuleCat R) (ModuleCat R)).map f.hom) ∘ₗ
        ((((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).V.endRingEquiv.toMonoidHom.comp
            (((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).ρ)
          g)
      x =
    (((((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj Y).V.endRingEquiv.toMonoidHom.comp
            (((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj Y).ρ)
          g ∘ₗ
        ModuleCat.Hom.hom ((forget₂ (FGModuleCat R) (ModuleCat R)).map f.hom))
      x
Module: Mathlib.RepresentationTheory.Invariants

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 : Rep k G
g : G
⊢ X.ρ.invariants.subtype ∘ₗ (Representation.trivial k G ↑((invariantsFunctor k G).obj X)) g =
    X.ρ g ∘ₗ X.ρ.invariants.subtype

Tactic:
ext x

Goal state after:
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
X : Rep k G
g : G
x : ↑((invariantsFunctor k G).obj X)
⊢ (X.ρ.invariants.subtype ∘ₗ (Representation.trivial k G ↑((invariantsFunctor k G).obj X)) g) x =
    (X.ρ g ∘ₗ X.ρ.invariants.subtype) x
Module: Mathlib.RepresentationTheory.Irreducible

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
inst✝⁶ : Monoid G
inst✝⁵ : Field k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
ρ : Representation k G V
inst✝² : ρ.IsIrreducible
inst✝¹ : FiniteDimensional k V
inst✝ : IsAlgClosed k
⊢ Module.finrank k (ρ.IntertwiningMap ρ) = 1

Tactic:
by
  rw [LinearEquiv.finrank_eq (LinearEquiv.ofBijective (Algebra.linearMap k (IntertwiningMap ρ ρ))
      algebraMap_intertwiningMap_bijective_of_isAlgClosed).symm]
  exact CommSemiring.finrank_self k

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W : Type u_4
X : Type u_5
inst✝¹² : CommRing k✝
inst✝¹¹ : Monoid G✝
inst✝¹⁰ : AddCommGroup V✝
inst✝⁹ : Module k✝ V✝
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module k✝ W
inst✝⁶ : AddCommGroup X
inst✝⁵ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ : Representation k✝ G✝ W
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
inst✝⁴ : CommRing k
inst✝³ : Group G
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
S : Subgroup G
inst✝ : S.Normal
g : ↥S
⊢ (MonoidHom.comp (ρ.toCoinvariants S) S.subtype) g = LinearMap.id

Tactic:
ext x

Goal state after:
k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W : Type u_4
X : Type u_5
inst✝¹² : CommRing k✝
inst✝¹¹ : Monoid G✝
inst✝¹⁰ : AddCommGroup V✝
inst✝⁹ : Module k✝ V✝
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module k✝ W
inst✝⁶ : AddCommGroup X
inst✝⁵ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ : Representation k✝ G✝ W
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
inst✝⁴ : CommRing k
inst✝³ : Group G
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
S : Subgroup G
inst✝ : S.Normal
g : ↥S
x : V
⊢ ((MonoidHom.comp (ρ.toCoinvariants S) S.subtype) g ∘ₗ mk (MonoidHom.comp ρ S.subtype)) x =
    (LinearMap.id ∘ₗ mk (MonoidHom.comp ρ S.subtype)) x
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.{?u.16, u, v} k G
B : Rep.{max w t, u, w} k H
A : Rep.{max w t, u, v} k G
f : B ⟶ coind.{u, v, w, max t w} φ A
g : G
⊢ (LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ (MonoidHom.comp B.ρ φ) g =
    A.ρ g ∘ₗ LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap

Tactic:
ext x

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.{?u.16, u, v} k G
B : Rep.{max w t, u, w} k H
A : Rep.{max w t, u, v} k G
f : B ⟶ coind.{u, v, w, max t w} φ A
g : G
x : ↑B
⊢ ((LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ (MonoidHom.comp B.ρ φ) g)
      x =
    (A.ρ g ∘ₗ LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap) x
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
⊢ ofHom { toLinearMap := (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype, isIntertwining' := ⋯ } ≫
      A.toCoinvariantsMkQ S =
    0

Tactic:
ext x

Goal state after:
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