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∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
⊢ ∫⁻ (θ : Θ), ↑C * ∫⁻ (x : 𝓧), κ.bound ∂P θ ∂π ≤ ∫⁻ (θ : Θ), ↑C * κ.bound * P.bound ∂π

Tactic:
by
    conv_lhs => simp only [lintegral_const, ← mul_assoc]
    gcongr with θ
    exact Kernel.measure_le_bound P θ Set.univ

Goal state after:
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)
⊢ map (⇑(MeasurableEquiv.curry ι κ X)) (infinitePi fun p ↦ μ p.1 p.2) = infinitePi fun i ↦ infinitePi fun j ↦ μ i j

Tactic:
rw [MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq, infinitePi_map_curry_symm]

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)
E : Type u_2
inst✝ : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f : Integrable f ((traj κ b ∘ₖ partialTraj κ a b) x₀)
⊢ ∀ᵐ (x : (i : ℕ) → X i) ∂(traj κ a) x₀, Integrable f ((traj κ b) (frestrictLe b x))

Tactic:
integrable_comp_iff

Goal state after:
X : ℕ → Type u_1
inst✝² : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝¹ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝ : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f :
  (∀ᵐ (y : (i : ↥(Iic b)) → X ↑i) ∂(partialTraj κ a b) x₀, Integrable f ((traj κ b) y)) ∧
    Integrable (fun y ↦ ∫ (z : (n : ℕ) → X n), ‖f z‖ ∂(traj κ b) y) ((partialTraj κ a b) x₀)
⊢ ∀ᵐ (x : (i : ℕ) → X i) ∂(traj κ a) x₀, Integrable f ((traj κ b) (frestrictLe b x))

case hf
X : ℕ → Type u_1
inst✝² : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝¹ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝ : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f : Integrable f ((traj κ b ∘ₖ partialTraj κ a b) x₀)
⊢ AEStronglyMeasurable f ((traj κ b ∘ₖ partialTraj κ a b) x₀)
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: case refine_1
α : Type u_1
p : PMF α
a b : α
hb : b ≠ a
⊢ {a}.indicator (⇑p) b = 0

Tactic:
classical exact ite_eq_right_iff.2 fun hb' => False.elim <| hb hb'

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

Goal state before:
pp: α : Type u_1
p : PMF α
s : Set α
⊢ p.toOuterMeasure (s ∩ p.support) = p.toOuterMeasure s

Tactic:
by
  simp only [toOuterMeasure_apply, PMF.support, Set.indicator_inter_support]

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

Goal state before:
pp: p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ HasSum (fun n ↦ (1 - p) ^ n * p) 1

Tactic:
have := hasSum_geometric_of_lt_one (sub_nonneg.mpr hp_le_one) (sub_lt_self 1 hp_pos)

Goal state after:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (fun n ↦ (1 - p) ^ n) (1 - (1 - p))⁻¹
⊢ HasSum (fun n ↦ (1 - p) ^ n * p) 1
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
p : PMF α
x : α
⊢ p x * (pure x) x = p x

Tactic:
pure_apply_self,

Goal state after:
α : Type u_1
p : PMF α
x : α
⊢ p x * 1 = p x
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
⊢ tsum (s.indicator ⇑p) ≠ 0

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r₁ r₂ : ℝ≥0
⊢ Po(ℝ, r₁) ∗ Po(ℝ, r₂) = Po(ℝ, r₁ + r₂)

Tactic:
apply Measure.ext_of_charFun
  ext t
  simp only [charFun_conv, charFun_map_cast_poissonMeasure, ← Complex.exp_add]
  congr; push_cast; ring

Goal state after:
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
hns : μ s ≠ 0
hnt : μ s ≠ ∞
hu : IsUniform X s ℙ μ
⊢ AEMeasurable X ℙ

Tactic:
dsimp [IsUniform, ProbabilityTheory.cond] at hu
  by_contra h
  rw [map_of_not_aemeasurable h] at hu
  apply zero_ne_one' ℝ≥0∞
  calc
    0 = (0 : Measure E) Set.univ := rfl
    _ = _ := by rw [hu, Measure.smul_apply, restrict_apply MeasurableSet.univ,
      Set.univ_inter, smul_eq_mul, ENNReal.inv_mul_cancel hns hnt]

Goal state after:
Module: Mathlib.Probability.HasCondDistrib

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
P : Measure Ω
X : Ω → 𝓧
Y : Ω → 𝓨
κ : Kernel 𝓧 𝓨
inst✝¹ : SFinite P
inst✝ : IsSFiniteKernel κ
h : HasCondDistrib Y X κ P
f : 𝓧 ≃ᵐ 𝓩
⊢ HasCondDistrib Y (⇑f ∘ X) (κ.comap ⇑f.symm ⋯) P

Tactic:
apply HasCondDistrib.comp_right (hf := f.measurable)

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
P : Measure Ω
X : Ω → 𝓧
Y : Ω → 𝓨
κ : Kernel 𝓧 𝓨
inst✝¹ : SFinite P
inst✝ : IsSFiniteKernel κ
h : HasCondDistrib Y X κ P
f : 𝓧 ≃ᵐ 𝓩
⊢ HasCondDistrib Y X ((κ.comap ⇑f.symm ⋯).comap ⇑f ⋯) P
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 ν
this✝ : IsProbabilityMeasure μ
this : IsProbabilityMeasure ν
⊢ Measure.map (fun ω x ↦ X x ω) μ = Measure.map (fun ω x ↦ Y x ω) ν

Tactic:
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]

Goal state after:
Ω : 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 ν
this✝ : IsProbabilityMeasure μ
this : IsProbabilityMeasure ν
⊢ (Measure.infinitePi fun i ↦ Measure.map (X i) μ) = Measure.infinitePi fun i ↦ Measure.map (Y i) ν
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
t : Set α
x : α
⊢ (if x ∈ t then (uniformOfFinset s hs) x else 0) = if x ∈ s ∧ x ∈ t then (↑(#s))⁻¹ else 0

Tactic:
simp_rw [uniformOfFinset_apply, ← ite_and, and_comm]

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : Nonempty Ω
ω : Ω
⊢ (condExpKernel μ m) ω = (condDistrib id id μ) (id ω)

Tactic:
simp [condExpKernel_eq, Kernel.comap_apply]

Goal state after:
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
⊢ φ s > 0

Tactic:
by simp_all

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

Goal state before:
pp: case refine_1
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ { hom := Kernel.id.map Prod.snd, property := ⋯ } ≫ { hom := Kernel.id.map f₁, property := ⋯ } =
    𝟙
      { carrier := { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier × X.carrier,
        str := Prod.instMeasurableSpace }

pp: case refine_2
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ { hom := Kernel.id.map f₁, property := ⋯ } ≫ { hom := Kernel.id.map Prod.snd, property := ⋯ } = 𝟙 X

Tactic:
· ext : 1; dsimp
      rw [Kernel.id_map hf₁, Kernel.deterministic_comp_eq_map hf₁, Kernel.id_map hf₂,
        Kernel.deterministic_map hf₂ hf₁]
      ext : 1
      simp [Kernel.deterministic_apply, Kernel.id_apply, f₁]

Goal state after:
case refine_2
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ { hom := Kernel.id.map f₁, property := ⋯ } ≫ { hom := Kernel.id.map Prod.snd, property := ⋯ } = 𝟙 X
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst✝⁹ : (t : T) → TopologicalSpace (F t)
inst✝⁸ : (t : T) → MeasurableSpace (F t)
inst✝⁷ : ∀ (t : T), BorelSpace (F t)
inst✝⁶ : ∀ (t : T), HasOuterApproxClosed (F t)
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst✝¹ : IsFiniteMeasure P
inst✝ : Finite T
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : ((t : T) → F t) →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ f (Z ω) * g fun x ↦ Y x ω) x ∂P =
      (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (fun ω ↦ g fun x ↦ Y x ω) x ∂P
⊢ Z ⟂ᵢ[P] fun ω t ↦ Y t ω

Tactic:
have := Fintype.ofFinite T
  refine indepFun_pi_of_prod_bcf mZ mY fun f g ↦ ?_
  convert! h f (∏ t, (g t).compContinuous ⟨Function.eval t, by fun_prop⟩) <;> simp

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

Goal state before:
pp: case refine_1
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ { hom := Kernel.id.map Prod.fst, property := ⋯ } ≫ { hom := Kernel.id.map f₁, property := ⋯ } =
    𝟙
      { carrier := X.carrier × { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier,
        str := Prod.instMeasurableSpace }

pp: case refine_2
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ { hom := Kernel.id.map f₁, property := ⋯ } ≫ { hom := Kernel.id.map Prod.fst, property := ⋯ } = 𝟙 X

Tactic:
· ext : 1; dsimp
      rw [Kernel.id_map hf₁, Kernel.deterministic_comp_eq_map hf₁, Kernel.id_map hf₂,
        Kernel.deterministic_map hf₂ hf₁]
      ext : 1
      simp [Kernel.deterministic_apply, Kernel.id_apply, f₁]

Goal state after:
case refine_2
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ { hom := Kernel.id.map f₁, property := ⋯ } ≫ { hom := Kernel.id.map Prod.fst, property := ⋯ } = 𝟙 X
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 ∩ A).indicator (fun j ↦ 1 j * 1 j) x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), A.indicator 1 x ∂π x₀

Tactic:
rw [lintegral_indicator ((h𝓑𝓧 _ hB).inter hA), lintegral_indicator hA]

Goal state after:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B ∩ A, 1 a * 1 a ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (a : X) in A, 1 a ∂π x₀
Module: Mathlib.Probability.Kernel.Category.SFinKer

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

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

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

Goal state before:
pp: case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
⊢ ∀ ⦃f_1 : ℕ → X → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (x : X), f_1 n x * f x ∂π x₀ = f_1 n x₀ * ∫⁻ (x : X), f x ∂π x₀) →
          ∫⁻ (x : X), (fun x ↦ ⨆ n, f_1 n x) x * f x ∂π x₀ = (fun x ↦ ⨆ n, f_1 n x) x₀ * ∫⁻ (x : X), f x ∂π x₀

Tactic:
· rintro g' hg'_meas hg'_mono hg'
    simp_rw [ENNReal.iSup_mul]
    rw [lintegral_iSup (fun n ↦ ((hg'_meas _).mono h𝓑𝓧 le_rfl).fun_mul hf)
      (hg'_mono.mul_const zero_le)]
    simp_rw [hg']

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

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

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

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

Goal state before:
pp: case e'_3
Ω : 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
⊢ μ.trim hm' ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g) =
    ⇑(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) ∘ₘ μ.trim hm'

Tactic:
· rw [Measure.compProd_eq_comp_prod]

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
⊢ Measure.map (fun ω ↦ (ω, f ω, g ω)) μ =
      ⇑(Kernel.id ×ₖ
            ((condExpKernel μ (MeasurableSpace.comap k inferInstance)).map f ×ₖ
              (condExpKernel μ (MeasurableSpace.comap k inferInstance)).map g)) ∘ₘ
        μ.trim ⋯ ↔
    Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ =
      ⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ

Tactic:
Measure.ext_prod₃_iff

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
⊢ (∀ {s : Set Ω} {t : Set β} {u : Set β'},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            (Measure.map (fun ω ↦ (ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
              (⇑(Kernel.id ×ₖ
                      ((condExpKernel μ (MeasurableSpace.comap k inferInstance)).map f ×ₖ
                        (condExpKernel μ (MeasurableSpace.comap k inferInstance)).map g)) ∘ₘ
                  μ.trim ⋯)
                (s ×ˢ t ×ˢ u)) ↔
    ∀ {s : Set γ} {t : Set β} {u : Set β'},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
              (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ) (s ×ˢ t ×ˢ u)
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
h'' : ∀ᵐ (ω' : Ω') ∂ν, ∀ᵐ (ω : Ω) ∂κ ω', X ω = Y ω
ω' : Ω'
h_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h' : ∀ᵐ (ω : Ω) ∂κ ω', X ω = Y ω
t : ℝ
⊢ mgf Y (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
mgf_congr (Filter.EventuallyEq.symm h')

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h'✝ : X =ᵐ[⇑κ ∘ₘ ν] Y
h'' : ∀ᵐ (ω' : Ω') ∂ν, ∀ᵐ (ω : Ω) ∂κ ω', X ω = Y ω
ω' : Ω'
h_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h' : ∀ᵐ (ω : Ω) ∂κ ω', X ω = Y ω
t : ℝ
⊢ mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
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), ∀ x₁ ∈ ρ₁.toSubmodule, ∀ x₂ ∈ ρ₂.toSubmodule, (ρ g) x₁ + (ρ g) x₂ ∈ ρ₁.toSubmodule ⊔ ρ₂.toSubmodule

Tactic:
intro g x₁ hx₁ x₂ hx₂

Goal state after:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
g : G
x₁ : W
hx₁ : x₁ ∈ ρ₁.toSubmodule
x₂ : W
hx₂ : x₂ ∈ ρ₂.toSubmodule
⊢ (ρ g) x₁ + (ρ g) x₂ ∈ ρ₁.toSubmodule ⊔ ρ₂.toSubmodule
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ), mgf (fun ω ↦ X ω + Y ω) (κ ω') t ≤ rexp (↑((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) * t ^ 2 / 2)

Tactic:
by
      let p := (cX.sqrt + cY.sqrt) / cX.sqrt
      let q := (cX.sqrt + cY.sqrt) / cY.sqrt
      filter_upwards [hX.mgf_le, hY.mgf_le, hX.ae_forall_memLp_exp_mul p,
        hY.ae_forall_memLp_exp_mul q] with ω' hmX hmY hlX hlY t
      calc (κ ω')[fun ω ↦ exp (t * (X ω + Y ω))]
      _ ≤ (κ ω')[fun ω ↦ exp (t * X ω) ^ (p : ℝ)] ^ (1 / (p : ℝ)) *
          (κ ω')[fun ω ↦ exp (t * Y ω) ^ (q : ℝ)] ^ (1 / (q : ℝ)) := by
        simp_rw [mul_add, exp_add]
        apply integral_mul_le_Lp_mul_Lq_of_nonneg
        · exact ⟨by simp [field, p, q], by positivity, by positivity⟩
        · exact ae_of_all _ fun _ ↦ exp_nonneg _
        · exact ae_of_all _ fun _ ↦ exp_nonneg _
        · simpa using (hlX t)
        · simpa using (hlY t)
      _ ≤ exp (cX * (t * p) ^ 2 / 2) ^ (1 / (p : ℝ)) *
          exp (cY * (t * q) ^ 2 / 2) ^ (1 / (q : ℝ)) := by
        simp_rw [← exp_mul _ p, ← exp_mul _ q, mul_right_comm t _ p, mul_right_comm t _ q]
        gcongr
        · exact hmX (t * p)
        · exact hmY (t * q)
      _ = exp ((cX.sqrt + cY.sqrt) ^ 2 * t ^ 2 / 2) := by
        simp_rw [← exp_mul, ← exp_add]
        simp only [NNReal.coe_div, NNReal.coe_add, coe_sqrt, one_div, inv_div, exp_eq_exp, p, q]
        field_simp
        linear_combination t ^ 2 * (-√↑cY * Real.sq_sqrt cX.coe_nonneg
            -√↑cX * Real.sq_sqrt cY.coe_nonneg)

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

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF id c (Measure.map X μ)
⊢ HasSubgaussianMGF X c μ

Tactic:
rw [← Function.id_comp X]

Goal state after:
case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF id c (Measure.map X μ)
⊢ HasSubgaussianMGF (id ∘ X) c μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case h_subG
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
⊢ ∀ i ∈ Finset.univ, HasSubgaussianMGF (X ↑i) (c ↑i) μ

Tactic:
exact fun i _ ↦ h_subG i i.2

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case mk'.mk'
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 σ
toIntertwiningMap✝¹ : ρ.IntertwiningMap σ
invFun✝¹ : W → V
left_inv✝¹ : Function.LeftInverse invFun✝¹ toIntertwiningMap✝¹.toFun
right_inv✝¹ : Function.RightInverse invFun✝¹ toIntertwiningMap✝¹.toFun
toIntertwiningMap✝ : ρ.IntertwiningMap σ
invFun✝ : W → V
left_inv✝ : Function.LeftInverse invFun✝ toIntertwiningMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toIntertwiningMap✝.toFun
h1 :
  ⇑{ toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹,
          right_inv := right_inv✝¹ }.toLinearEquiv =
    ⇑{ toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝,
          right_inv := right_inv✝ }.toLinearEquiv
h2 :
  { toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹,
        right_inv := right_inv✝¹ }.invFun =
    { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝,
        right_inv := right_inv✝ }.invFun
⊢ { toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
simp_all [IntertwiningMap.ext_iff]

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

Goal state before:
pp: case hb
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
ht : t < 0
⊢ ∀ᵐ (ω : Ω) ∂μ, (-X) ω ∈ Set.Icc (-b) (-a)

Tactic:
filter_upwards [hb] with ω ⟨hl, hr⟩ using ⟨neg_le_neg_iff.2 hr, neg_le_neg_iff.2 hl⟩

Goal state after:
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 : (forget₂ (FDRep R G) (Rep R G)).obj X ⟶ (forget₂ (FDRep R G) (Rep R G)).obj Y
g : G
⊢ X.ρ g ≫ InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap) =
    InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap) ≫ Y.ρ g

Tactic:
by
    ext1
    simp only [FGModuleCat.obj_carrier]
    exact f.hom.2 g

Goal state after: